Email Gateway (Aug 19 2022 at 16:12): Email Gateway (Aug 19 2022 at 16:12):From: M A <tesleft@hotmail.com>
Hi
failed to parse lemma when prove the following
would like to see any further usage when continuing adding letters into it
lemma mfold5 [simp]:"mfold5 f [a,b,c,d,e] x = f e (f d (f c (f b (f a x))))"
lemma mfold [simp]:"mfold f [a,b,c] x = f c (f b (f a x))"apply(simp_all)apply(auto)donelemma mfoldr [simp]:"mfoldr f [a,b,c] x = f a (f b (f c x))"apply(induct_tac x)apply(auto)donelemma mfoldl [simp]:"mfoldl f x [a,b,c] = f (f (f x a) b) c"apply(induct_tac x)apply(auto)done
Regards,
Martin
Last updated: Nov 21 2024 at 12:39 UTC