[STATEMENT]
lemma eval_lowerFm_helper :
  assumes "freeIn i F"
  assumes "length init = i"
  shows "eval (lowerFm i 1 F) (init @xs) = eval F (init@[x]@xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
freeIn i F
length init = i

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

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

goal (1 subgoal):
 1. eval (lowerFm i 1 TrueF) (init @ xs) = eval TrueF (init @ [x] @ xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (lowerFm i 1 TrueF) (init @ xs) = eval TrueF (init @ [x] @ xs)

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

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

goal (1 subgoal):
 1. eval (lowerFm i 1 FalseF) (init @ xs) = eval FalseF (init @ [x] @ xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (lowerFm i 1 FalseF) (init @ xs) = eval FalseF (init @ [x] @ xs)

goal (8 subgoals):
 1. \<And>xa i init. \<lbrakk>freeIn i (fm.Atom xa); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (fm.Atom xa)) (init @ xs) = eval (fm.Atom xa) (init @ [x] @ xs)
 2. \<And>F1 F2 i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F1; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F1) (init @ xs) = eval F1 (init @ [x] @ xs); \<And>i init. \<lbrakk>freeIn i F2; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F2) (init @ xs) = eval F2 (init @ [x] @ xs); freeIn i (And F1 F2); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (And F1 F2)) (init @ xs) = eval (And F1 F2) (init @ [x] @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F1; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F1) (init @ xs) = eval F1 (init @ [x] @ xs); \<And>i init. \<lbrakk>freeIn i F2; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F2) (init @ xs) = eval F2 (init @ [x] @ xs); freeIn i (Or F1 F2); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (Or F1 F2)) (init @ xs) = eval (Or F1 F2) (init @ [x] @ xs)
 4. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (Neg F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (Neg F)) (init @ xs) = eval (Neg F) (init @ [x] @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExQ F)) (init @ xs) = eval (ExQ F) (init @ [x] @ xs)
 6. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllQ F)) (init @ xs) = eval (AllQ F) (init @ [x] @ xs)
 7. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
 8. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>xa i init. \<lbrakk>freeIn i (fm.Atom xa); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (fm.Atom xa)) (init @ xs) = eval (fm.Atom xa) (init @ [x] @ xs)
 2. \<And>F1 F2 i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F1; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F1) (init @ xs) = eval F1 (init @ [x] @ xs); \<And>i init. \<lbrakk>freeIn i F2; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F2) (init @ xs) = eval F2 (init @ [x] @ xs); freeIn i (And F1 F2); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (And F1 F2)) (init @ xs) = eval (And F1 F2) (init @ [x] @ xs)
 3. \<And>F1 F2 i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F1; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F1) (init @ xs) = eval F1 (init @ [x] @ xs); \<And>i init. \<lbrakk>freeIn i F2; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F2) (init @ xs) = eval F2 (init @ [x] @ xs); freeIn i (Or F1 F2); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (Or F1 F2)) (init @ xs) = eval (Or F1 F2) (init @ [x] @ xs)
 4. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (Neg F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (Neg F)) (init @ xs) = eval (Neg F) (init @ [x] @ xs)
 5. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExQ F)) (init @ xs) = eval (ExQ F) (init @ [x] @ xs)
 6. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllQ F)) (init @ xs) = eval (AllQ F) (init @ [x] @ xs)
 7. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
 8. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
case (Atom A)
[PROOF STATE]
proof (state)
this:
freeIn i (fm.Atom A)
length init = i

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

goal (1 subgoal):
 1. eval (lowerFm i 1 (fm.Atom A)) (init @ xs) = eval (fm.Atom A) (init @ [x] @ xs)
[PROOF STEP]
apply(cases A)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>freeIn i (fm.Atom A); length init = i; A = Less x1\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (fm.Atom A)) (init @ xs) = eval (fm.Atom A) (init @ [x] @ xs)
 2. \<And>x2. \<lbrakk>freeIn i (fm.Atom A); length init = i; A = Eq x2\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (fm.Atom A)) (init @ xs) = eval (fm.Atom A) (init @ [x] @ xs)
 3. \<And>x3. \<lbrakk>freeIn i (fm.Atom A); length init = i; A = Leq x3\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (fm.Atom A)) (init @ xs) = eval (fm.Atom A) (init @ [x] @ xs)
 4. \<And>x4. \<lbrakk>freeIn i (fm.Atom A); length init = i; A = Neq x4\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (fm.Atom A)) (init @ xs) = eval (fm.Atom A) (init @ [x] @ xs)
[PROOF STEP]
by (simp_all add: insertion_lowerPoly1)
[PROOF STATE]
proof (state)
this:
eval (lowerFm i 1 (fm.Atom A)) (init @ xs) = eval (fm.Atom A) (init @ [x] @ xs)

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

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

goal (1 subgoal):
 1. eval (lowerFm i 1 (And F1 F2)) (init @ xs) = eval (And F1 F2) (init @ [x] @ xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (lowerFm i 1 (And F1 F2)) (init @ xs) = eval (And F1 F2) (init @ [x] @ xs)

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

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

goal (1 subgoal):
 1. eval (lowerFm i 1 (Or F1 F2)) (init @ xs) = eval (Or F1 F2) (init @ [x] @ xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (lowerFm i 1 (Or F1 F2)) (init @ xs) = eval (Or F1 F2) (init @ [x] @ xs)

goal (5 subgoals):
 1. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (Neg F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (Neg F)) (init @ xs) = eval (Neg F) (init @ [x] @ xs)
 2. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExQ F)) (init @ xs) = eval (ExQ F) (init @ [x] @ xs)
 3. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllQ F)) (init @ xs) = eval (AllQ F) (init @ [x] @ xs)
 4. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
 5. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (Neg F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (Neg F)) (init @ xs) = eval (Neg F) (init @ [x] @ xs)
 2. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExQ F)) (init @ xs) = eval (ExQ F) (init @ [x] @ xs)
 3. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllQ F)) (init @ xs) = eval (AllQ F) (init @ [x] @ xs)
 4. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
 5. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
case (Neg F)
[PROOF STATE]
proof (state)
this:
\<lbrakk>freeIn ?i F; length ?init = ?i\<rbrakk> \<Longrightarrow> eval (lowerFm ?i 1 F) (?init @ xs) = eval F (?init @ [x] @ xs)
freeIn i (Neg F)
length init = i

goal (5 subgoals):
 1. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (Neg F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (Neg F)) (init @ xs) = eval (Neg F) (init @ [x] @ xs)
 2. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExQ F)) (init @ xs) = eval (ExQ F) (init @ [x] @ xs)
 3. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllQ F)) (init @ xs) = eval (AllQ F) (init @ [x] @ xs)
 4. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
 5. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>freeIn ?i F; length ?init = ?i\<rbrakk> \<Longrightarrow> eval (lowerFm ?i 1 F) (?init @ xs) = eval F (?init @ [x] @ xs)
freeIn i (Neg F)
length init = i
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>freeIn ?i F; length ?init = ?i\<rbrakk> \<Longrightarrow> eval (lowerFm ?i 1 F) (?init @ xs) = eval F (?init @ [x] @ xs)
freeIn i (Neg F)
length init = i

goal (1 subgoal):
 1. eval (lowerFm i 1 (Neg F)) (init @ xs) = eval (Neg F) (init @ [x] @ xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (lowerFm i 1 (Neg F)) (init @ xs) = eval (Neg F) (init @ [x] @ xs)

goal (4 subgoals):
 1. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExQ F)) (init @ xs) = eval (ExQ F) (init @ [x] @ xs)
 2. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllQ F)) (init @ xs) = eval (AllQ F) (init @ [x] @ xs)
 3. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
 4. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExQ F)) (init @ xs) = eval (ExQ F) (init @ [x] @ xs)
 2. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllQ F)) (init @ xs) = eval (AllQ F) (init @ [x] @ xs)
 3. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
 4. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
case (ExQ F)
[PROOF STATE]
proof (state)
this:
\<lbrakk>freeIn ?i F; length ?init = ?i\<rbrakk> \<Longrightarrow> eval (lowerFm ?i 1 F) (?init @ xs) = eval F (?init @ [x] @ xs)
freeIn i (ExQ F)
length init = i

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

goal (4 subgoals):
 1. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExQ F)) (init @ xs) = eval (ExQ F) (init @ [x] @ xs)
 2. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllQ F)) (init @ xs) = eval (AllQ F) (init @ [x] @ xs)
 3. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
 4. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (lowerFm i 1 (ExQ F)) (init @ xs) = eval (ExQ F) (init @ [x] @ xs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. eval (map_fm_binders (\<lambda>a x. lowerAtom (i + x) (Suc 0) a) F (Suc 0)) (x # init @ xs)) = (\<exists>xa. eval F (xa # init @ x # xs))
[PROOF STEP]
apply(rule ex_cong1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. eval (map_fm_binders (\<lambda>a x. lowerAtom (i + x) (Suc 0) a) F (Suc 0)) (xa # init @ xs) = eval F (xa # init @ x # xs)
[PROOF STEP]
subgoal for xa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (map_fm_binders (\<lambda>a x. lowerAtom (i + x) (Suc 0) a) F (Suc 0)) (xa # init @ xs) = eval F (xa # init @ x # xs)
[PROOF STEP]
using map[of 0] ExQ(1)[of "Suc i" "xa#init"] ExQ(2) ExQ(3)
[PROOF STATE]
proof (prove)
using this:
map_fm_binders (\<lambda>a x. lowerAtom (i + x) 1 a) F (0 + 1) = map_fm_binders (\<lambda>a x. lowerAtom (i + 1 + x) 1 a) F 0
\<lbrakk>freeIn (Suc i) F; length (xa # init) = Suc i\<rbrakk> \<Longrightarrow> eval (lowerFm (Suc i) 1 F) ((xa # init) @ xs) = eval F ((xa # init) @ [x] @ xs)
freeIn i (ExQ F)
length init = i

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

goal (3 subgoals):
 1. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllQ F)) (init @ xs) = eval (AllQ F) (init @ [x] @ xs)
 2. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
 3. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllQ F)) (init @ xs) = eval (AllQ F) (init @ [x] @ xs)
 2. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
 3. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
case (AllQ F)
[PROOF STATE]
proof (state)
this:
\<lbrakk>freeIn ?i F; length ?init = ?i\<rbrakk> \<Longrightarrow> eval (lowerFm ?i 1 F) (?init @ xs) = eval F (?init @ [x] @ xs)
freeIn i (AllQ F)
length init = i

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

goal (3 subgoals):
 1. \<And>F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllQ F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllQ F)) (init @ xs) = eval (AllQ F) (init @ [x] @ xs)
 2. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
 3. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (lowerFm i 1 (AllQ F)) (init @ xs) = eval (AllQ F) (init @ [x] @ xs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. eval (map_fm_binders (\<lambda>a x. lowerAtom (i + x) (Suc 0) a) F (Suc 0)) (x # init @ xs)) = (\<forall>xa. eval F (xa # init @ x # xs))
[PROOF STEP]
apply(rule all_cong1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. eval (map_fm_binders (\<lambda>a x. lowerAtom (i + x) (Suc 0) a) F (Suc 0)) (xa # init @ xs) = eval F (xa # init @ x # xs)
[PROOF STEP]
subgoal for xa
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (map_fm_binders (\<lambda>a x. lowerAtom (i + x) (Suc 0) a) F (Suc 0)) (xa # init @ xs) = eval F (xa # init @ x # xs)
[PROOF STEP]
using map[of 0] AllQ(1)[of "Suc i" "xa#init"] AllQ(2) AllQ(3)
[PROOF STATE]
proof (prove)
using this:
map_fm_binders (\<lambda>a x. lowerAtom (i + x) 1 a) F (0 + 1) = map_fm_binders (\<lambda>a x. lowerAtom (i + 1 + x) 1 a) F 0
\<lbrakk>freeIn (Suc i) F; length (xa # init) = Suc i\<rbrakk> \<Longrightarrow> eval (lowerFm (Suc i) 1 F) ((xa # init) @ xs) = eval F ((xa # init) @ [x] @ xs)
freeIn i (AllQ F)
length init = i

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

goal (2 subgoals):
 1. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
 2. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
 2. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
case (ExN x1 F)
[PROOF STATE]
proof (state)
this:
\<lbrakk>freeIn ?i F; length ?init = ?i\<rbrakk> \<Longrightarrow> eval (lowerFm ?i 1 F) (?init @ xs) = eval F (?init @ [x] @ xs)
freeIn i (ExN x1 F)
length init = i

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

goal (2 subgoals):
 1. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (ExN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
 2. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (lowerFm i 1 (ExN x1 F)) (init @ xs) = eval (ExN x1 F) (init @ [x] @ xs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>l. length l = x1 \<and> eval (map_fm_binders (\<lambda>a x. lowerAtom (i + x) (Suc 0) a) F x1) (l @ init @ xs)) = (\<exists>l. length l = x1 \<and> eval F (l @ init @ x # xs))
[PROOF STEP]
apply(rule ex_cong1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. (length l = x1 \<and> eval (map_fm_binders (\<lambda>a x. lowerAtom (i + x) (Suc 0) a) F x1) (l @ init @ xs)) = (length l = x1 \<and> eval F (l @ init @ x # xs))
[PROOF STEP]
subgoal for l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (length l = x1 \<and> eval (map_fm_binders (\<lambda>a x. lowerAtom (i + x) (Suc 0) a) F x1) (l @ init @ xs)) = (length l = x1 \<and> eval F (l @ init @ x # xs))
[PROOF STEP]
using map[of 0] ExN(1)[of "i+x1" "l@init"] ExN(2) ExN(3)
[PROOF STATE]
proof (prove)
using this:
map_fm_binders (\<lambda>a x. lowerAtom (i + x) 1 a) F (0 + x1) = map_fm_binders (\<lambda>a x. lowerAtom (i + x1 + x) 1 a) F 0
\<lbrakk>freeIn (i + x1) F; length (l @ init) = i + x1\<rbrakk> \<Longrightarrow> eval (lowerFm (i + x1) 1 F) ((l @ init) @ xs) = eval F ((l @ init) @ [x] @ xs)
freeIn i (ExN x1 F)
length init = i

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

goal (1 subgoal):
 1. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
case (AllN x1 F)
[PROOF STATE]
proof (state)
this:
\<lbrakk>freeIn ?i F; length ?init = ?i\<rbrakk> \<Longrightarrow> eval (lowerFm ?i 1 F) (?init @ xs) = eval F (?init @ [x] @ xs)
freeIn i (AllN x1 F)
length init = i

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

goal (1 subgoal):
 1. \<And>x1 F i init. \<lbrakk>\<And>i init. \<lbrakk>freeIn i F; length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 F) (init @ xs) = eval F (init @ [x] @ xs); freeIn i (AllN x1 F); length init = i\<rbrakk> \<Longrightarrow> eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (lowerFm i 1 (AllN x1 F)) (init @ xs) = eval (AllN x1 F) (init @ [x] @ xs)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>l. length l = x1 \<longrightarrow> eval (map_fm_binders (\<lambda>a x. lowerAtom (i + x) (Suc 0) a) F x1) (l @ init @ xs)) = (\<forall>l. length l = x1 \<longrightarrow> eval F (l @ init @ x # xs))
[PROOF STEP]
apply(rule all_cong1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. (length l = x1 \<longrightarrow> eval (map_fm_binders (\<lambda>a x. lowerAtom (i + x) (Suc 0) a) F x1) (l @ init @ xs)) = (length l = x1 \<longrightarrow> eval F (l @ init @ x # xs))
[PROOF STEP]
subgoal for l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (length l = x1 \<longrightarrow> eval (map_fm_binders (\<lambda>a x. lowerAtom (i + x) (Suc 0) a) F x1) (l @ init @ xs)) = (length l = x1 \<longrightarrow> eval F (l @ init @ x # xs))
[PROOF STEP]
using map[of 0] AllN(1)[of "i+x1" "l@init"] AllN(2) AllN(3)
[PROOF STATE]
proof (prove)
using this:
map_fm_binders (\<lambda>a x. lowerAtom (i + x) 1 a) F (0 + x1) = map_fm_binders (\<lambda>a x. lowerAtom (i + x1 + x) 1 a) F 0
\<lbrakk>freeIn (i + x1) F; length (l @ init) = i + x1\<rbrakk> \<Longrightarrow> eval (lowerFm (i + x1) 1 F) ((l @ init) @ xs) = eval F ((l @ init) @ [x] @ xs)
freeIn i (AllN x1 F)
length init = i

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval_lowerFm :
  assumes h : "freeIn 0 F"
  shows " \<forall>xs. (eval (lowerFm 0 1 F) xs = eval (ExQ F) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>xs. eval (lowerFm 0 1 F) xs = eval (ExQ F) xs
[PROOF STEP]
using eval_lowerFm_helper[OF h]
[PROOF STATE]
proof (prove)
using this:
length ?init = 0 \<Longrightarrow> eval (lowerFm 0 1 F) (?init @ ?xs) = eval F (?init @ [?x] @ ?xs)

goal (1 subgoal):
 1. \<forall>xs. eval (lowerFm 0 1 F) xs = eval (ExQ F) xs
[PROOF STEP]
by simp


[STATEMENT]
lemma higherPoly\<^sub>0_add : "higherPoly\<^sub>0 x y (p + q) = higherPoly\<^sub>0 x y p + higherPoly\<^sub>0 x y q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPoly\<^sub>0 x y (p + q) = higherPoly\<^sub>0 x y p + higherPoly\<^sub>0 x y q
[PROOF STEP]
using poly_mapping_eq_iff[where a = "higherPoly\<^sub>0 x y (p + q)", where b = "higherPoly\<^sub>0 x y p + higherPoly\<^sub>0 x y q"]
    plus_poly_mapping.rep_eq[where x = "higherPoly\<^sub>0 x y (p + q)", where xa = "higherPoly\<^sub>0 x y p + higherPoly\<^sub>0 x y q"]
[PROOF STATE]
proof (prove)
using this:
(higherPoly\<^sub>0 x y (p + q) = higherPoly\<^sub>0 x y p + higherPoly\<^sub>0 x y q) = (lookup (higherPoly\<^sub>0 x y (p + q)) = lookup (higherPoly\<^sub>0 x y p + higherPoly\<^sub>0 x y q))
lookup (higherPoly\<^sub>0 x y (p + q) + (higherPoly\<^sub>0 x y p + higherPoly\<^sub>0 x y q)) = (\<lambda>k. lookup (higherPoly\<^sub>0 x y (p + q)) k + lookup (higherPoly\<^sub>0 x y p + higherPoly\<^sub>0 x y q) k)

goal (1 subgoal):
 1. higherPoly\<^sub>0 x y (p + q) = higherPoly\<^sub>0 x y p + higherPoly\<^sub>0 x y q
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lookup (higherPoly\<^sub>0 x y (p + q) + (higherPoly\<^sub>0 x y p + higherPoly\<^sub>0 x y q)) = (\<lambda>k. lookup (higherPoly\<^sub>0 x y (p + q)) k + lookup (higherPoly\<^sub>0 x y p + higherPoly\<^sub>0 x y q) k); higherPoly\<^sub>0 x y (p + q) \<noteq> higherPoly\<^sub>0 x y p + higherPoly\<^sub>0 x y q; lookup (higherPoly\<^sub>0 x y (p + q)) \<noteq> lookup (higherPoly\<^sub>0 x y p + higherPoly\<^sub>0 x y q)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (simp add: higherPoly\<^sub>0.rep_eq lookup_add poly_mapping_eqI)


[STATEMENT]
lemma liftPoly_add: "liftPoly w z (a + b) = (liftPoly w z a) + (liftPoly w z b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. liftPoly w z (a + b) = liftPoly w z a + liftPoly w 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 w z (a + b) = map_fun id (map_fun id (map_fun mapping_of MPoly)) higherPoly\<^sub>0 w z a + map_fun id (map_fun id (map_fun mapping_of MPoly)) higherPoly\<^sub>0 w z b
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 w z (mapping_of (a + b))) = MPoly (higherPoly\<^sub>0 w z (mapping_of a)) + MPoly (higherPoly\<^sub>0 w z (mapping_of b))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 w z (mapping_of (a + b))) = MPoly (higherPoly\<^sub>0 w z (mapping_of a)) + MPoly (higherPoly\<^sub>0 w 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: plus_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 w z (mapping_of (a + b))) = MPoly (higherPoly\<^sub>0 w z (mapping_of a)) + MPoly (higherPoly\<^sub>0 w z (mapping_of b))
[PROOF STEP]
have h2: "MPoly (higherPoly\<^sub>0 w z (mapping_of a + mapping_of b)) =
    MPoly (higherPoly\<^sub>0 w z (mapping_of a)) + MPoly (higherPoly\<^sub>0 w z (mapping_of b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 w z (mapping_of a + mapping_of b)) = MPoly (higherPoly\<^sub>0 w z (mapping_of a)) + MPoly (higherPoly\<^sub>0 w z (mapping_of b))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 w z (mapping_of a + mapping_of b)) = MPoly (higherPoly\<^sub>0 w z (mapping_of a)) + MPoly (higherPoly\<^sub>0 w z (mapping_of b))
[PROOF STEP]
have h0a: "higherPoly\<^sub>0 w z (mapping_of a + mapping_of b) = (higherPoly\<^sub>0 w z (mapping_of a)) + (higherPoly\<^sub>0 w z (mapping_of b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPoly\<^sub>0 w z (mapping_of a + mapping_of b) = higherPoly\<^sub>0 w z (mapping_of a) + higherPoly\<^sub>0 w z (mapping_of b)
[PROOF STEP]
using higherPoly\<^sub>0_add[of w z _ _ ]
[PROOF STATE]
proof (prove)
using this:
higherPoly\<^sub>0 w z (?p + ?q) = higherPoly\<^sub>0 w z ?p + higherPoly\<^sub>0 w z ?q

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

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

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

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

goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 w z (mapping_of (a + b))) = MPoly (higherPoly\<^sub>0 w z (mapping_of a)) + MPoly (higherPoly\<^sub>0 w z (mapping_of b))
[PROOF STEP]
show "MPoly (higherPoly\<^sub>0 w z (mapping_of (a + b))) =
    MPoly (higherPoly\<^sub>0 w z (mapping_of a)) +
    MPoly (higherPoly\<^sub>0 w z (mapping_of b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly (higherPoly\<^sub>0 w z (mapping_of (a + b))) = MPoly (higherPoly\<^sub>0 w z (mapping_of a)) + MPoly (higherPoly\<^sub>0 w 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 w z (mapping_of a + mapping_of b)) = MPoly (higherPoly\<^sub>0 w z (mapping_of a)) + MPoly (higherPoly\<^sub>0 w z (mapping_of b))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vars_lift_add : "vars(liftPoly a b (p+q)) \<subseteq> vars(liftPoly a b (p))\<union> vars(liftPoly a b (q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (liftPoly a b (p + q)) \<subseteq> vars (liftPoly a b p) \<union> vars (liftPoly a b q)
[PROOF STEP]
using liftPoly_add[of a b p q]
[PROOF STATE]
proof (prove)
using this:
liftPoly a b (p + q) = liftPoly a b p + liftPoly a b q

goal (1 subgoal):
 1. vars (liftPoly a b (p + q)) \<subseteq> vars (liftPoly a b p) \<union> vars (liftPoly a b q)
[PROOF STEP]
using vars_add[of "liftPoly a b p" "liftPoly a b q"]
[PROOF STATE]
proof (prove)
using this:
liftPoly a b (p + q) = liftPoly a b p + liftPoly a b q
vars (liftPoly a b p + liftPoly a b q) \<subseteq> vars (liftPoly a b p) \<union> vars (liftPoly a b q)

goal (1 subgoal):
 1. vars (liftPoly a b (p + q)) \<subseteq> vars (liftPoly a b p) \<union> vars (liftPoly a b q)
[PROOF STEP]
by auto


[STATEMENT]
lemma mapping_of_lift_add : "mapping_of (liftPoly x y (a + b)) = mapping_of (liftPoly x y a) + mapping_of (liftPoly x y b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mapping_of (liftPoly x y (a + b)) = mapping_of (liftPoly x y a) + mapping_of (liftPoly x y b)
[PROOF STEP]
unfolding liftPoly.rep_eq plus_mpoly.rep_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. higherPoly\<^sub>0 x y (mapping_of a + mapping_of b) = higherPoly\<^sub>0 x y (mapping_of a) + higherPoly\<^sub>0 x y (mapping_of b)
[PROOF STEP]
using higherPoly\<^sub>0_add
[PROOF STATE]
proof (prove)
using this:
higherPoly\<^sub>0 ?x ?y (?p + ?q) = higherPoly\<^sub>0 ?x ?y ?p + higherPoly\<^sub>0 ?x ?y ?q

goal (1 subgoal):
 1. higherPoly\<^sub>0 x y (mapping_of a + mapping_of b) = higherPoly\<^sub>0 x y (mapping_of a) + higherPoly\<^sub>0 x y (mapping_of b)
[PROOF STEP]
.