[STATEMENT]
lemma eval_liftFm_helper :
  assumes "length init = i"
  assumes "length I = amount"
  shows "eval F (init @xs) = eval (liftFm i amount F) (init@I@xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
length init = i

goal (1 subgoal):
 1. eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs)
[PROOF STEP]
proof(induction F arbitrary: i init)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>x i init. length init = i \<Longrightarrow> eval (fm.Atom x) (init @ xs) = eval (liftFm i amount (fm.Atom x)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 5. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 6. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 7. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExQ F) (init @ xs) = eval (liftFm i amount (ExQ F)) (init @ I @ xs)
 8. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllQ F) (init @ xs) = eval (liftFm i amount (AllQ F)) (init @ I @ xs)
 9. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
 10. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
case (Atom x)
[PROOF STATE]
proof (state)
this:
length init = i

goal (10 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>x i init. length init = i \<Longrightarrow> eval (fm.Atom x) (init @ xs) = eval (liftFm i amount (fm.Atom x)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 5. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 6. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 7. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExQ F) (init @ xs) = eval (liftFm i amount (ExQ F)) (init @ I @ xs)
 8. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllQ F) (init @ xs) = eval (liftFm i amount (AllQ F)) (init @ I @ xs)
 9. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
 10. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length init = i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length init = i

goal (1 subgoal):
 1. eval (fm.Atom x) (init @ xs) = eval (liftFm i amount (fm.Atom x)) (init @ I @ xs)
[PROOF STEP]
apply(cases x)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>length init = i; x = Less x1\<rbrakk> \<Longrightarrow> eval (fm.Atom x) (init @ xs) = eval (liftFm i amount (fm.Atom x)) (init @ I @ xs)
 2. \<And>x2. \<lbrakk>length init = i; x = Eq x2\<rbrakk> \<Longrightarrow> eval (fm.Atom x) (init @ xs) = eval (liftFm i amount (fm.Atom x)) (init @ I @ xs)
 3. \<And>x3. \<lbrakk>length init = i; x = Leq x3\<rbrakk> \<Longrightarrow> eval (fm.Atom x) (init @ xs) = eval (liftFm i amount (fm.Atom x)) (init @ I @ xs)
 4. \<And>x4. \<lbrakk>length init = i; x = Neq x4\<rbrakk> \<Longrightarrow> eval (fm.Atom x) (init @ xs) = eval (liftFm i amount (fm.Atom x)) (init @ I @ xs)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>length init = i; x = Less x1\<rbrakk> \<Longrightarrow> (insertion (nth_default 0 (init @ xs)) x1 < 0) = (insertion (nth_default 0 (init @ I @ xs)) (liftPoly i amount x1) < 0)
 2. \<And>x2. \<lbrakk>length init = i; x = Eq x2\<rbrakk> \<Longrightarrow> (insertion (nth_default 0 (init @ xs)) x2 = 0) = (insertion (nth_default 0 (init @ I @ xs)) (liftPoly i amount x2) = 0)
 3. \<And>x3. \<lbrakk>length init = i; x = Leq x3\<rbrakk> \<Longrightarrow> (insertion (nth_default 0 (init @ xs)) x3 \<le> 0) = (insertion (nth_default 0 (init @ I @ xs)) (liftPoly i amount x3) \<le> 0)
 4. \<And>x4. \<lbrakk>length init = i; x = Neq x4\<rbrakk> \<Longrightarrow> (insertion (nth_default 0 (init @ xs)) x4 = 0) = (insertion (nth_default 0 (init @ I @ xs)) (liftPoly i amount x4) = 0)
[PROOF STEP]
using lift_insertion assms Atom.prems
[PROOF STATE]
proof (prove)
using this:
\<forall>init. length init = ?i \<longrightarrow> (\<forall>I xs. insertion (nth_default 0 (init @ xs)) ?p = insertion (nth_default 0 (init @ I @ xs)) (liftPoly ?i (length I) ?p))
length init = i
length I = amount
length init = i

goal (4 subgoals):
 1. \<And>x1. \<lbrakk>length init = i; x = Less x1\<rbrakk> \<Longrightarrow> (insertion (nth_default 0 (init @ xs)) x1 < 0) = (insertion (nth_default 0 (init @ I @ xs)) (liftPoly i amount x1) < 0)
 2. \<And>x2. \<lbrakk>length init = i; x = Eq x2\<rbrakk> \<Longrightarrow> (insertion (nth_default 0 (init @ xs)) x2 = 0) = (insertion (nth_default 0 (init @ I @ xs)) (liftPoly i amount x2) = 0)
 3. \<And>x3. \<lbrakk>length init = i; x = Leq x3\<rbrakk> \<Longrightarrow> (insertion (nth_default 0 (init @ xs)) x3 \<le> 0) = (insertion (nth_default 0 (init @ I @ xs)) (liftPoly i amount x3) \<le> 0)
 4. \<And>x4. \<lbrakk>length init = i; x = Neq x4\<rbrakk> \<Longrightarrow> (insertion (nth_default 0 (init @ xs)) x4 = 0) = (insertion (nth_default 0 (init @ I @ xs)) (liftPoly i amount x4) = 0)
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
eval (fm.Atom x) (init @ xs) = eval (liftFm i amount (fm.Atom x)) (init @ I @ xs)

goal (9 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExQ F) (init @ xs) = eval (liftFm i amount (ExQ F)) (init @ I @ xs)
 7. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllQ F) (init @ xs) = eval (liftFm i amount (AllQ F)) (init @ I @ xs)
 8. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
 9. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExQ F) (init @ xs) = eval (liftFm i amount (ExQ F)) (init @ I @ xs)
 7. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllQ F) (init @ xs) = eval (liftFm i amount (AllQ F)) (init @ I @ xs)
 8. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
 9. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
case (ExQ F)
[PROOF STATE]
proof (state)
this:
length ?init = ?i \<Longrightarrow> eval F (?init @ xs) = eval (liftFm ?i amount F) (?init @ I @ xs)
length init = i

goal (9 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExQ F) (init @ xs) = eval (liftFm i amount (ExQ F)) (init @ I @ xs)
 7. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllQ F) (init @ xs) = eval (liftFm i amount (AllQ F)) (init @ I @ xs)
 8. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
 9. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
have map: "\<And>y. (map_fm_binders (\<lambda>a x. liftAtom (i + x) (amount) a) F (y + Suc 0)) = (map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F y
[PROOF STEP]
apply(induction F)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) TrueF (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) TrueF y
 2. \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) FalseF (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) FalseF y
 3. \<And>x y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (fm.Atom x) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (fm.Atom x) y
 4. \<And>F1 F2 y. \<lbrakk>\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F1 (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F1 y; \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F2 (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F2 y\<rbrakk> \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (And F1 F2) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (And F1 F2) y
 5. \<And>F1 F2 y. \<lbrakk>\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F1 (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F1 y; \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F2 (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F2 y\<rbrakk> \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (Or F1 F2) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (Or F1 F2) y
 6. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (Neg F) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (Neg F) y
 7. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (ExQ F) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (ExQ F) y
 8. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (AllQ F) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (AllQ F) y
 9. \<And>x1 F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (ExN x1 F) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (ExN x1 F) y
 10. \<And>x1 F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (AllN x1 F) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (AllN x1 F) y
[PROOF STEP]
by(simp_all)
[PROOF STATE]
proof (state)
this:
map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (?y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F ?y

goal (9 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExQ F) (init @ xs) = eval (liftFm i amount (ExQ F)) (init @ I @ xs)
 7. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllQ F) (init @ xs) = eval (liftFm i amount (AllQ F)) (init @ I @ xs)
 8. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
 9. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (ExQ F) (init @ xs) = eval (liftFm i amount (ExQ F)) (init @ I @ xs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. eval F (x # init @ xs)) = (\<exists>x. eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (Suc 0)) (x # init @ I @ xs))
[PROOF STEP]
apply(rule ex_cong1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. eval F (x # init @ xs) = eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (Suc 0)) (x # init @ I @ xs)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval F (x # init @ xs) = eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (Suc 0)) (x # init @ I @ xs)
[PROOF STEP]
using map[of 0]
[PROOF STATE]
proof (prove)
using this:
map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (0 + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F 0

goal (1 subgoal):
 1. eval F (x # init @ xs) = eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (Suc 0)) (x # init @ I @ xs)
[PROOF STEP]
using ExQ(1)[of "x#init" "i+1"] ExQ(2)
[PROOF STATE]
proof (prove)
using this:
map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (0 + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F 0
length (x # init) = i + 1 \<Longrightarrow> eval F ((x # init) @ xs) = eval (liftFm (i + 1) amount F) ((x # init) @ I @ xs)
length init = i

goal (1 subgoal):
 1. eval F (x # init @ xs) = eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (Suc 0)) (x # init @ I @ xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
eval (ExQ F) (init @ xs) = eval (liftFm i amount (ExQ F)) (init @ I @ xs)

goal (8 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllQ F) (init @ xs) = eval (liftFm i amount (AllQ F)) (init @ I @ xs)
 7. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
 8. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllQ F) (init @ xs) = eval (liftFm i amount (AllQ F)) (init @ I @ xs)
 7. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
 8. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
case (AllQ F)
[PROOF STATE]
proof (state)
this:
length ?init = ?i \<Longrightarrow> eval F (?init @ xs) = eval (liftFm ?i amount F) (?init @ I @ xs)
length init = i

goal (8 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllQ F) (init @ xs) = eval (liftFm i amount (AllQ F)) (init @ I @ xs)
 7. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
 8. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
have map: "\<And>y. (map_fm_binders (\<lambda>a x. liftAtom (i + x) (amount) a) F (y + Suc 0)) = (map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F y
[PROOF STEP]
apply(induction F)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) TrueF (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) TrueF y
 2. \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) FalseF (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) FalseF y
 3. \<And>x y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (fm.Atom x) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (fm.Atom x) y
 4. \<And>F1 F2 y. \<lbrakk>\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F1 (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F1 y; \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F2 (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F2 y\<rbrakk> \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (And F1 F2) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (And F1 F2) y
 5. \<And>F1 F2 y. \<lbrakk>\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F1 (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F1 y; \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F2 (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F2 y\<rbrakk> \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (Or F1 F2) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (Or F1 F2) y
 6. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (Neg F) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (Neg F) y
 7. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (ExQ F) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (ExQ F) y
 8. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (AllQ F) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (AllQ F) y
 9. \<And>x1 F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (ExN x1 F) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (ExN x1 F) y
 10. \<And>x1 F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (AllN x1 F) (y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) (AllN x1 F) y
[PROOF STEP]
by(simp_all)
[PROOF STATE]
proof (state)
this:
map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (?y + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F ?y

goal (8 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllQ F) (init @ xs) = eval (liftFm i amount (AllQ F)) (init @ I @ xs)
 7. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
 8. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (AllQ F) (init @ xs) = eval (liftFm i amount (AllQ F)) (init @ I @ xs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. eval F (x # init @ xs)) = (\<forall>x. eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (Suc 0)) (x # init @ I @ xs))
[PROOF STEP]
apply(rule all_cong1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. eval F (x # init @ xs) = eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (Suc 0)) (x # init @ I @ xs)
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval F (x # init @ xs) = eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (Suc 0)) (x # init @ I @ xs)
[PROOF STEP]
using map[of 0]
[PROOF STATE]
proof (prove)
using this:
map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (0 + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F 0

goal (1 subgoal):
 1. eval F (x # init @ xs) = eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (Suc 0)) (x # init @ I @ xs)
[PROOF STEP]
using AllQ(1)[of "x#init" "i+1"] AllQ(2)
[PROOF STATE]
proof (prove)
using this:
map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (0 + Suc 0) = map_fm_binders (\<lambda>a x. liftAtom (i + 1 + x) amount a) F 0
length (x # init) = i + 1 \<Longrightarrow> eval F ((x # init) @ xs) = eval (liftFm (i + 1) amount F) ((x # init) @ I @ xs)
length init = i

goal (1 subgoal):
 1. eval F (x # init @ xs) = eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (Suc 0)) (x # init @ I @ xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
eval (AllQ F) (init @ xs) = eval (liftFm i amount (AllQ F)) (init @ I @ xs)

goal (7 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
 7. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
 7. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
case (ExN x1 F)
[PROOF STATE]
proof (state)
this:
length ?init = ?i \<Longrightarrow> eval F (?init @ xs) = eval (liftFm ?i amount F) (?init @ I @ xs)
length init = i

goal (7 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
 7. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
have map: "\<And>y. (map_fm_binders (\<lambda>a x. liftAtom (i + x) (amount) a) F (y + x1)) = (map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F y
[PROOF STEP]
apply(induction F)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) TrueF (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) TrueF y
 2. \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) FalseF (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) FalseF y
 3. \<And>x y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (fm.Atom x) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (fm.Atom x) y
 4. \<And>F1 F2 y. \<lbrakk>\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F1 (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F1 y; \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F2 (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F2 y\<rbrakk> \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (And F1 F2) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (And F1 F2) y
 5. \<And>F1 F2 y. \<lbrakk>\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F1 (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F1 y; \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F2 (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F2 y\<rbrakk> \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (Or F1 F2) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (Or F1 F2) y
 6. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (Neg F) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (Neg F) y
 7. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (ExQ F) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (ExQ F) y
 8. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (AllQ F) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (AllQ F) y
 9. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (ExN x1a F) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (ExN x1a F) y
 10. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (AllN x1a F) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (AllN x1a F) y
[PROOF STEP]
apply(simp_all add: add.commute add.left_commute)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (Suc (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (Suc y)
 2. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (Suc (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (Suc y)
 3. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (x1a + (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (x1a + y)
 4. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (x1a + (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (x1a + y)
[PROOF STEP]
apply (metis add_Suc)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (Suc (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (Suc y)
 2. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (x1a + (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (x1a + y)
 3. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (x1a + (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (x1a + y)
[PROOF STEP]
apply (metis add_Suc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (x1a + (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (x1a + y)
 2. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (x1a + (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (x1a + y)
[PROOF STEP]
apply (metis add.assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (x1a + (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (x1a + y)
[PROOF STEP]
by (metis add.assoc)
[PROOF STATE]
proof (state)
this:
map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (?y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F ?y

goal (7 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
 7. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>l. length l = x1 \<and> eval F (l @ init @ xs)) = (\<exists>l. length l = x1 \<and> eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F x1) (l @ init @ I @ xs))
[PROOF STEP]
apply(rule ex_cong1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. (length l = x1 \<and> eval F (l @ init @ xs)) = (length l = x1 \<and> eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F x1) (l @ init @ I @ xs))
[PROOF STEP]
subgoal for l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (length l = x1 \<and> eval F (l @ init @ xs)) = (length l = x1 \<and> eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F x1) (l @ init @ I @ xs))
[PROOF STEP]
using map[of 0] ExN(1)[of "l@init" "i+x1"] ExN(2)
[PROOF STATE]
proof (prove)
using this:
map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (0 + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F 0
length (l @ init) = i + x1 \<Longrightarrow> eval F ((l @ init) @ xs) = eval (liftFm (i + x1) amount F) ((l @ init) @ I @ xs)
length init = i

goal (1 subgoal):
 1. (length l = x1 \<and> eval F (l @ init @ xs)) = (length l = x1 \<and> eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F x1) (l @ init @ I @ xs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
eval (ExN x1 F) (init @ xs) = eval (liftFm i amount (ExN x1 F)) (init @ I @ xs)

goal (6 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
case (AllN x1 F)
[PROOF STATE]
proof (state)
this:
length ?init = ?i \<Longrightarrow> eval F (?init @ xs) = eval (liftFm ?i amount F) (?init @ I @ xs)
length init = i

goal (6 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
have map: "\<And>y. (map_fm_binders (\<lambda>a x. liftAtom (i + x) (amount) a) F (y + x1)) = (map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F y
[PROOF STEP]
apply(induction F)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) TrueF (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) TrueF y
 2. \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) FalseF (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) FalseF y
 3. \<And>x y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (fm.Atom x) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (fm.Atom x) y
 4. \<And>F1 F2 y. \<lbrakk>\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F1 (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F1 y; \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F2 (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F2 y\<rbrakk> \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (And F1 F2) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (And F1 F2) y
 5. \<And>F1 F2 y. \<lbrakk>\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F1 (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F1 y; \<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F2 (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F2 y\<rbrakk> \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (Or F1 F2) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (Or F1 F2) y
 6. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (Neg F) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (Neg F) y
 7. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (ExQ F) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (ExQ F) y
 8. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (AllQ F) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (AllQ F) y
 9. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (ExN x1a F) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (ExN x1a F) y
 10. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) (AllN x1a F) (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) (AllN x1a F) y
[PROOF STEP]
apply(simp_all add: add.commute add.left_commute)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (Suc (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (Suc y)
 2. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (Suc (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (Suc y)
 3. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (x1a + (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (x1a + y)
 4. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (x1a + (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (x1a + y)
[PROOF STEP]
apply (metis add_Suc)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (Suc (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (Suc y)
 2. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (x1a + (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (x1a + y)
 3. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (x1a + (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (x1a + y)
[PROOF STEP]
apply (metis add_Suc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (x1a + (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (x1a + y)
 2. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (x1a + (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (x1a + y)
[PROOF STEP]
apply (metis add.assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1a F y. (\<And>y. map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (y + x1) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F y) \<Longrightarrow> map_fm_binders (\<lambda>a x. liftAtom (x + i) amount a) F (x1a + (y + x1)) = map_fm_binders (\<lambda>a x. liftAtom (x + (i + x1)) amount a) F (x1a + y)
[PROOF STEP]
by (metis add.assoc)
[PROOF STATE]
proof (state)
this:
map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (?y + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F ?y

goal (6 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
 6. \<And>x1 F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>l. length l = x1 \<longrightarrow> eval F (l @ init @ xs)) = (\<forall>l. length l = x1 \<longrightarrow> eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F x1) (l @ init @ I @ xs))
[PROOF STEP]
apply(rule all_cong1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. (length l = x1 \<longrightarrow> eval F (l @ init @ xs)) = (length l = x1 \<longrightarrow> eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F x1) (l @ init @ I @ xs))
[PROOF STEP]
subgoal for l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (length l = x1 \<longrightarrow> eval F (l @ init @ xs)) = (length l = x1 \<longrightarrow> eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F x1) (l @ init @ I @ xs))
[PROOF STEP]
using map[of 0] AllN(1)[of "l@init" "i+x1"] AllN(2)
[PROOF STATE]
proof (prove)
using this:
map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F (0 + x1) = map_fm_binders (\<lambda>a x. liftAtom (i + x1 + x) amount a) F 0
length (l @ init) = i + x1 \<Longrightarrow> eval F ((l @ init) @ xs) = eval (liftFm (i + x1) amount F) ((l @ init) @ I @ xs)
length init = i

goal (1 subgoal):
 1. (length l = x1 \<longrightarrow> eval F (l @ init @ xs)) = (length l = x1 \<longrightarrow> eval (map_fm_binders (\<lambda>a x. liftAtom (i + x) amount a) F x1) (l @ init @ I @ xs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
eval (AllN x1 F) (init @ xs) = eval (liftFm i amount (AllN x1 F)) (init @ I @ xs)

goal (5 subgoals):
 1. \<And>i init. length init = i \<Longrightarrow> eval TrueF (init @ xs) = eval (liftFm i amount TrueF) (init @ I @ xs)
 2. \<And>i init. length init = i \<Longrightarrow> eval FalseF (init @ xs) = eval (liftFm i amount FalseF) (init @ I @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (And F1 F2) (init @ xs) = eval (liftFm i amount (And F1 F2)) (init @ I @ xs)
 4. \<And>F1 F2 i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F1 (init @ xs) = eval (liftFm i amount F1) (init @ I @ xs); \<And>i init. length init = i \<Longrightarrow> eval F2 (init @ xs) = eval (liftFm i amount F2) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Or F1 F2) (init @ xs) = eval (liftFm i amount (Or F1 F2)) (init @ I @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. length init = i \<Longrightarrow> eval F (init @ xs) = eval (liftFm i amount F) (init @ I @ xs); length init = i\<rbrakk> \<Longrightarrow> eval (Neg F) (init @ xs) = eval (liftFm i amount (Neg F)) (init @ I @ xs)
[PROOF STEP]
qed auto


[STATEMENT]
lemma eval_liftFm :
  assumes "length I = amount"
  assumes "length L \<ge> d"
  shows "eval F L = eval (liftFm d amount F) (insert_into L d I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval F L = eval (liftFm d amount F) (insert_into L d I)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval F L = eval (liftFm d amount F) (insert_into L d I)
[PROOF STEP]
define init where "init = take d L"
[PROOF STATE]
proof (state)
this:
init = take d L

goal (1 subgoal):
 1. eval F L = eval (liftFm d amount F) (insert_into L d I)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
init = take d L
[PROOF STEP]
have "length init = d"
[PROOF STATE]
proof (prove)
using this:
init = take d L

goal (1 subgoal):
 1. length init = d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
init = take d L
length I = amount
d \<le> length L

goal (1 subgoal):
 1. length init = d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length init = d

goal (1 subgoal):
 1. eval F L = eval (liftFm d amount F) (insert_into L d I)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length init = d
[PROOF STEP]
have "(eval F (init @ (drop d L)) = eval (liftFm d amount F) (init @ I @ (drop d L)))"
[PROOF STATE]
proof (prove)
using this:
length init = d

goal (1 subgoal):
 1. eval F (init @ drop d L) = eval (liftFm d amount F) (init @ I @ drop d L)
[PROOF STEP]
using eval_liftFm_helper[of init d I amount  F "(drop d L)"] assms
[PROOF STATE]
proof (prove)
using this:
length init = d
\<lbrakk>length init = d; length I = amount\<rbrakk> \<Longrightarrow> eval F (init @ drop d L) = eval (liftFm d amount F) (init @ I @ drop d L)
length I = amount
d \<le> length L

goal (1 subgoal):
 1. eval F (init @ drop d L) = eval (liftFm d amount F) (init @ I @ drop d L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval F (init @ drop d L) = eval (liftFm d amount F) (init @ I @ drop d L)

goal (1 subgoal):
 1. eval F L = eval (liftFm d amount F) (insert_into L d I)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval F (init @ drop d L) = eval (liftFm d amount F) (init @ I @ drop d L)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval F (init @ drop d L) = eval (liftFm d amount F) (init @ I @ drop d L)

goal (1 subgoal):
 1. eval F L = eval (liftFm d amount F) (insert_into L d I)
[PROOF STEP]
unfolding insert_into.simps assms init_def
[PROOF STATE]
proof (prove)
using this:
eval F (take d L @ drop d L) = eval (liftFm d amount F) (take d L @ I @ drop d L)

goal (1 subgoal):
 1. eval F L = eval (liftFm d amount F) (take d L @ I @ drop d L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval F L = eval (liftFm d amount F) (insert_into L d I)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_in_lift : "var\<notin>vars(p::real mpoly) \<Longrightarrow> var+z\<notin>vars(liftPoly 0 z p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var \<notin> vars p \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p)
[PROOF STEP]
proof(induction p rule: mpoly_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m a. var \<notin> vars (MPoly_Type.monom m a) \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z (MPoly_Type.monom m a))
 2. \<And>p1 p2 m a. \<lbrakk>var \<notin> vars p1 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p1); var \<notin> vars p2 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p2); p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0; var \<notin> vars (p1 + p2)\<rbrakk> \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z (p1 + p2))
[PROOF STEP]
case (monom m a)
[PROOF STATE]
proof (state)
this:
var \<notin> vars (MPoly_Type.monom m a)

goal (2 subgoals):
 1. \<And>m a. var \<notin> vars (MPoly_Type.monom m a) \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z (MPoly_Type.monom m a))
 2. \<And>p1 p2 m a. \<lbrakk>var \<notin> vars p1 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p1); var \<notin> vars p2 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p2); p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0; var \<notin> vars (p1 + p2)\<rbrakk> \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z (p1 + p2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
var \<notin> vars (MPoly_Type.monom m a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
var \<notin> vars (MPoly_Type.monom m a)

goal (1 subgoal):
 1. var + z \<notin> vars (liftPoly 0 z (MPoly_Type.monom m a))
[PROOF STEP]
using lift_vars_monom[of 0 z m a]
[PROOF STATE]
proof (prove)
using this:
var \<notin> vars (MPoly_Type.monom m a)
vars (liftPoly 0 z (MPoly_Type.monom m a)) = (\<lambda>x. if 0 \<le> x then x + z else x) ` vars (MPoly_Type.monom m a)

goal (1 subgoal):
 1. var + z \<notin> vars (liftPoly 0 z (MPoly_Type.monom m a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
var + z \<notin> vars (liftPoly 0 z (MPoly_Type.monom m a))

goal (1 subgoal):
 1. \<And>p1 p2 m a. \<lbrakk>var \<notin> vars p1 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p1); var \<notin> vars p2 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p2); p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0; var \<notin> vars (p1 + p2)\<rbrakk> \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z (p1 + p2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p1 p2 m a. \<lbrakk>var \<notin> vars p1 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p1); var \<notin> vars p2 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p2); p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0; var \<notin> vars (p1 + p2)\<rbrakk> \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z (p1 + p2))
[PROOF STEP]
case (sum p1 p2 m a)
[PROOF STATE]
proof (state)
this:
var \<notin> vars p1 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p1)
var \<notin> vars p2 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p2)
p2 = MPoly_Type.monom m a
m \<notin> monomials p1
a \<noteq> 0
var \<notin> vars (p1 + p2)

goal (1 subgoal):
 1. \<And>p1 p2 m a. \<lbrakk>var \<notin> vars p1 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p1); var \<notin> vars p2 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p2); p2 = MPoly_Type.monom m a; m \<notin> monomials p1; a \<noteq> 0; var \<notin> vars (p1 + p2)\<rbrakk> \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z (p1 + p2))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. var + z \<notin> vars (liftPoly 0 z (p1 + p2))
[PROOF STEP]
using sum
[PROOF STATE]
proof (prove)
using this:
var \<notin> vars p1 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p1)
var \<notin> vars p2 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p2)
p2 = MPoly_Type.monom m a
m \<notin> monomials p1
a \<noteq> 0
var \<notin> vars (p1 + p2)

goal (1 subgoal):
 1. var + z \<notin> vars (liftPoly 0 z (p1 + p2))
[PROOF STEP]
using vars_lift_add[of 0 z p1 p2]
      vars_add[of p1 p2]
[PROOF STATE]
proof (prove)
using this:
var \<notin> vars p1 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p1)
var \<notin> vars p2 \<Longrightarrow> var + z \<notin> vars (liftPoly 0 z p2)
p2 = MPoly_Type.monom m a
m \<notin> monomials p1
a \<noteq> 0
var \<notin> vars (p1 + p2)
vars (liftPoly 0 z (p1 + p2)) \<subseteq> vars (liftPoly 0 z p1) \<union> vars (liftPoly 0 z p2)
vars (p1 + p2) \<subseteq> vars p1 \<union> vars p2

goal (1 subgoal):
 1. var + z \<notin> vars (liftPoly 0 z (p1 + p2))
[PROOF STEP]
by (metis (no_types, lifting) Set.basic_monos(7) Un_iff monomials.rep_eq vars_add_monom)
[PROOF STATE]
proof (state)
this:
var + z \<notin> vars (liftPoly 0 z (p1 + p2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_const : "insertion f (liftPoly 0 z (Const (C::real))) = insertion f (Const C :: real mpoly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (liftPoly 0 z (Const C)) = insertion f (Const C)
[PROOF STEP]
apply(cases "C=0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. C = 0 \<Longrightarrow> insertion f (liftPoly 0 z (Const C)) = insertion f (Const C)
 2. C \<noteq> 0 \<Longrightarrow> insertion f (liftPoly 0 z (Const C)) = insertion f (Const C)
[PROOF STEP]
unfolding insertion_code monomials_Const coeff_Const monomials_liftPoly
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. C = 0 \<Longrightarrow> (\<Sum>m\<in>lowerPowers 0 z ` (if C = 0 then {} else {0}). MPoly_Type.coeff (liftPoly 0 z (Const C)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>(if C = 0 then {} else {0}). (C when m = 0) * (\<Prod>k\<in>keys m. f k ^ lookup m k))
 2. C \<noteq> 0 \<Longrightarrow> (\<Sum>m\<in>lowerPowers 0 z ` (if C = 0 then {} else {0}). MPoly_Type.coeff (liftPoly 0 z (Const C)) m * (\<Prod>k\<in>keys m. f k ^ lookup m k)) = (\<Sum>m\<in>(if C = 0 then {} else {0}). (C when m = 0) * (\<Prod>k\<in>keys m. f k ^ lookup m k))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<noteq> 0 \<Longrightarrow> MPoly_Type.coeff (liftPoly 0 z (Const C)) (lowerPowers 0 z 0) * (\<Prod>k\<in>keys (lowerPowers 0 z 0). f k ^ lookup (lowerPowers 0 z 0) k) = C
[PROOF STEP]
unfolding lower_power_zero[of 0 z] lookup_zero power.power_0 comm_monoid_mult_class.prod.neutral_const coeff_liftPoly coeff_Const
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<noteq> 0 \<Longrightarrow> (if \<exists>j\<in>{0..<0 + z}. 0 < 0 then 0 else C when higherPowers 0 z 0 = 0) * 1 = C
[PROOF STEP]
unfolding higherPowers_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<noteq> 0 \<Longrightarrow> (if \<exists>j\<in>{0..<0 + z}. 0 < 0 then 0 else C when map_fun id (map_fun id (map_fun lookup Abs_poly_mapping)) (\<lambda>b i p x. p (inc_above b i x)) 0 z 0 = 0) * 1 = C
[PROOF STEP]
by auto


[STATEMENT]
lemma liftPoly_sub: "liftPoly 0 z (a - b) = (liftPoly 0 z a) - (liftPoly 0 z b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftPoly 0 z (a - b) = liftPoly 0 z a - liftPoly 0 z b
[PROOF STEP]
unfolding liftPoly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun id (map_fun id (map_fun mapping_of MPoly)) higherPoly\<^sub>0 0 z (a - b) = map_fun id (map_fun id (map_fun mapping_of MPoly)) higherPoly\<^sub>0 0 z a - map_fun id (map_fun id (map_fun mapping_of MPoly)) higherPoly\<^sub>0 0 z b
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 0 z (mapping_of (a - b))) = MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 0 z (mapping_of (a - b))) = MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))
[PROOF STEP]
have h1: "mapping_of (a - b) = mapping_of a - mapping_of b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mapping_of (a - b) = mapping_of a - mapping_of b
[PROOF STEP]
by (simp add: minus_mpoly.rep_eq)
[PROOF STATE]
proof (state)
this:
mapping_of (a - b) = mapping_of a - mapping_of b

goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 0 z (mapping_of (a - b))) = MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))
[PROOF STEP]
have h2: "MPoly (higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b)) =
    MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b)) = MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b)) = MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))
[PROOF STEP]
have h0a: "higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b) = (higherPoly\<^sub>0 0 z (mapping_of a)) - (higherPoly\<^sub>0 0 z (mapping_of b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b) = higherPoly\<^sub>0 0 z (mapping_of a) - higherPoly\<^sub>0 0 z (mapping_of b)
[PROOF STEP]
using poly_mapping_eq_iff[where a = "higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b)", where b = "(higherPoly\<^sub>0 0 z (mapping_of a)) - (higherPoly\<^sub>0 0 z (mapping_of b))"]
        minus_poly_mapping.rep_eq[where x = "higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b)", where xa = "(higherPoly\<^sub>0 0 z (mapping_of a)) - (higherPoly\<^sub>0 0 z (mapping_of b))"]
[PROOF STATE]
proof (prove)
using this:
(higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b) = higherPoly\<^sub>0 0 z (mapping_of a) - higherPoly\<^sub>0 0 z (mapping_of b)) = (lookup (higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b)) = lookup (higherPoly\<^sub>0 0 z (mapping_of a) - higherPoly\<^sub>0 0 z (mapping_of b)))
lookup (higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b) - (higherPoly\<^sub>0 0 z (mapping_of a) - higherPoly\<^sub>0 0 z (mapping_of b))) = (\<lambda>k. lookup (higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b)) k - lookup (higherPoly\<^sub>0 0 z (mapping_of a) - higherPoly\<^sub>0 0 z (mapping_of b)) k)

goal (1 subgoal):
 1. higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b) = higherPoly\<^sub>0 0 z (mapping_of a) - higherPoly\<^sub>0 0 z (mapping_of b)
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup (higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b) - (higherPoly\<^sub>0 0 z (mapping_of a) - higherPoly\<^sub>0 0 z (mapping_of b))) = (\<lambda>k. lookup (higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b)) k - lookup (higherPoly\<^sub>0 0 z (mapping_of a) - higherPoly\<^sub>0 0 z (mapping_of b)) k); higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b) \<noteq> higherPoly\<^sub>0 0 z (mapping_of a) - higherPoly\<^sub>0 0 z (mapping_of b); lookup (higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b)) \<noteq> lookup (higherPoly\<^sub>0 0 z (mapping_of a) - higherPoly\<^sub>0 0 z (mapping_of b))\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (simp add: higherPoly\<^sub>0.rep_eq poly_mapping_eqI minus_poly_mapping.rep_eq)
[PROOF STATE]
proof (state)
this:
higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b) = higherPoly\<^sub>0 0 z (mapping_of a) - higherPoly\<^sub>0 0 z (mapping_of b)

goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b)) = MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b) = higherPoly\<^sub>0 0 z (mapping_of a) - higherPoly\<^sub>0 0 z (mapping_of b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b) = higherPoly\<^sub>0 0 z (mapping_of a) - higherPoly\<^sub>0 0 z (mapping_of b)

goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b)) = MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))
[PROOF STEP]
by (simp add: minus_mpoly.abs_eq)
[PROOF STATE]
proof (state)
this:
MPoly (higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b)) = MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
MPoly (higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b)) = MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))

goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 0 z (mapping_of (a - b))) = MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))
[PROOF STEP]
show "MPoly (higherPoly\<^sub>0 0 z (mapping_of (a - b))) =
    MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) -
    MPoly (higherPoly\<^sub>0 0 z (mapping_of b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 0 z (mapping_of (a - b))) = MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))
[PROOF STEP]
using h1 h2
[PROOF STATE]
proof (prove)
using this:
mapping_of (a - b) = mapping_of a - mapping_of b
MPoly (higherPoly\<^sub>0 0 z (mapping_of a - mapping_of b)) = MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))

goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 0 z (mapping_of (a - b))) = MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
MPoly (higherPoly\<^sub>0 0 z (mapping_of (a - b))) = MPoly (higherPoly\<^sub>0 0 z (mapping_of a)) - MPoly (higherPoly\<^sub>0 0 z (mapping_of b))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift_sub : "insertion (f::nat\<Rightarrow>real) (liftPoly 0 z (a - b)) = insertion f (liftPoly 0 z a - liftPoly 0 z b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (liftPoly 0 z (a - b)) = insertion f (liftPoly 0 z a - liftPoly 0 z b)
[PROOF STEP]
using liftPoly_sub[of "z" "a" "b"]
[PROOF STATE]
proof (prove)
using this:
liftPoly 0 z (a - b) = liftPoly 0 z a - liftPoly 0 z b

goal (1 subgoal):
 1. insertion f (liftPoly 0 z (a - b)) = insertion f (liftPoly 0 z a - liftPoly 0 z b)
[PROOF STEP]
by auto


[STATEMENT]
lemma lift_minus :
  assumes "insertion (f::nat \<Rightarrow> real) (liftPoly 0 z (c - Const (C::real))) = 0"
  shows "insertion f (liftPoly 0 z c) = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (liftPoly 0 z c) = C
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insertion f (liftPoly 0 z c) = C
[PROOF STEP]
have "insertion f (liftPoly 0 z (c - Const C)) = insertion f ((liftPoly 0 z c) - (liftPoly 0 z (Const C)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (liftPoly 0 z (c - Const C)) = insertion f (liftPoly 0 z c - liftPoly 0 z (Const C))
[PROOF STEP]
by (simp add: lift_sub)
[PROOF STATE]
proof (state)
this:
insertion f (liftPoly 0 z (c - Const C)) = insertion f (liftPoly 0 z c - liftPoly 0 z (Const C))

goal (1 subgoal):
 1. insertion f (liftPoly 0 z c) = C
[PROOF STEP]
have "... = insertion f (liftPoly 0 z c) - (insertion f (liftPoly 0 z (Const C)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (liftPoly 0 z c - liftPoly 0 z (Const C)) = insertion f (liftPoly 0 z c) - insertion f (liftPoly 0 z (Const C))
[PROOF STEP]
using insertion_sub
[PROOF STATE]
proof (prove)
using this:
insertion ?f (?A - ?B) = insertion ?f ?A - insertion ?f ?B

goal (1 subgoal):
 1. insertion f (liftPoly 0 z c - liftPoly 0 z (Const C)) = insertion f (liftPoly 0 z c) - insertion f (liftPoly 0 z (Const C))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insertion f (liftPoly 0 z c - liftPoly 0 z (Const C)) = insertion f (liftPoly 0 z c) - insertion f (liftPoly 0 z (Const C))

goal (1 subgoal):
 1. insertion f (liftPoly 0 z c) = C
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion f (liftPoly 0 z c - liftPoly 0 z (Const C)) = insertion f (liftPoly 0 z c) - insertion f (liftPoly 0 z (Const C))

goal (1 subgoal):
 1. insertion f (liftPoly 0 z c) = C
[PROOF STEP]
have "... = insertion f (liftPoly 0 z c) - C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (liftPoly 0 z c) - insertion f (liftPoly 0 z (Const C)) = insertion f (liftPoly 0 z c) - C
[PROOF STEP]
using lift_const[of f z C] insertion_const
[PROOF STATE]
proof (prove)
using this:
insertion f (liftPoly 0 z (Const C)) = insertion f (Const C)
insertion ?f (Const ?c) = ?c

goal (1 subgoal):
 1. insertion f (liftPoly 0 z c) - insertion f (liftPoly 0 z (Const C)) = insertion f (liftPoly 0 z c) - C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insertion f (liftPoly 0 z c) - insertion f (liftPoly 0 z (Const C)) = insertion f (liftPoly 0 z c) - C

goal (1 subgoal):
 1. insertion f (liftPoly 0 z c) = C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insertion f (liftPoly 0 z c) - insertion f (liftPoly 0 z (Const C)) = insertion f (liftPoly 0 z c) - C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insertion f (liftPoly 0 z c) - insertion f (liftPoly 0 z (Const C)) = insertion f (liftPoly 0 z c) - C

goal (1 subgoal):
 1. insertion f (liftPoly 0 z c) = C
[PROOF STEP]
using \<open>insertion f (liftPoly 0 z (c - Const C)) = insertion f (liftPoly 0 z c - liftPoly 0 z (Const C))\<close> assms calculation
[PROOF STATE]
proof (prove)
using this:
insertion f (liftPoly 0 z c) - insertion f (liftPoly 0 z (Const C)) = insertion f (liftPoly 0 z c) - C
insertion f (liftPoly 0 z (c - Const C)) = insertion f (liftPoly 0 z c - liftPoly 0 z (Const C))
insertion f (liftPoly 0 z (c - Const C)) = 0
insertion f (liftPoly 0 z c - liftPoly 0 z (Const C)) = insertion f (liftPoly 0 z c) - insertion f (liftPoly 0 z (Const C))

goal (1 subgoal):
 1. insertion f (liftPoly 0 z c) = C
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insertion f (liftPoly 0 z c) = C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lift00 : "liftPoly 0 0 (a::real mpoly) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftPoly 0 0 a = a
[PROOF STEP]
unfolding liftPoly_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun id (map_fun id (map_fun mapping_of MPoly)) higherPoly\<^sub>0 0 0 a = a
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 0 0 (mapping_of a)) = a
[PROOF STEP]
unfolding higherPoly\<^sub>0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly (map_fun id (map_fun id (map_fun lookup Abs_poly_mapping)) (\<lambda>b i mp mon. if \<exists>j\<in>{b..<b + i}. 0 < lookup mon j then 0 else mp (higherPowers b i mon)) 0 0 (mapping_of a)) = a
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly (Abs_poly_mapping (\<lambda>mon. lookup (mapping_of a) (higherPowers 0 0 mon))) = a
[PROOF STEP]
unfolding higherPowers_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly (Abs_poly_mapping (\<lambda>mon. lookup (mapping_of a) (map_fun id (map_fun id (map_fun lookup Abs_poly_mapping)) (\<lambda>b i p x. p (inc_above b i x)) 0 0 mon))) = a
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly (mapping_of a) = a
[PROOF STEP]
by (simp add: mapping_of_inverse)