[STATEMENT]
lemma swap_fm :
  assumes "length L > a"
  assumes "length L > b"
  shows "eval F L = eval (swap_fm a b F) (swap_list a b L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval F L = eval (swap_fm a b F) (swap_list a b L)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a < length L
b < length L

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

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

goal (1 subgoal):
 1. eval TrueF L = eval (swap_fm a b TrueF) (swap_list a b L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval TrueF L = eval (swap_fm a b TrueF) (swap_list a b L)

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

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

goal (1 subgoal):
 1. eval FalseF L = eval (swap_fm a b FalseF) (swap_list a b L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval FalseF L = eval (swap_fm a b FalseF) (swap_list a b L)

goal (8 subgoals):
 1. \<And>x a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (fm.Atom x) L = eval (swap_fm a b (fm.Atom x)) (swap_list a b L)
 2. \<And>F1 F2 a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F1 L = eval (swap_fm a b F1) (swap_list a b L); \<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F2 L = eval (swap_fm a b F2) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (And F1 F2) L = eval (swap_fm a b (And F1 F2)) (swap_list a b L)
 3. \<And>F1 F2 a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F1 L = eval (swap_fm a b F1) (swap_list a b L); \<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F2 L = eval (swap_fm a b F2) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Or F1 F2) L = eval (swap_fm a b (Or F1 F2)) (swap_list a b L)
 4. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Neg F) L = eval (swap_fm a b (Neg F)) (swap_list a b L)
 5. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)
 6. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 7. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 8. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>x a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (fm.Atom x) L = eval (swap_fm a b (fm.Atom x)) (swap_list a b L)
 2. \<And>F1 F2 a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F1 L = eval (swap_fm a b F1) (swap_list a b L); \<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F2 L = eval (swap_fm a b F2) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (And F1 F2) L = eval (swap_fm a b (And F1 F2)) (swap_list a b L)
 3. \<And>F1 F2 a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F1 L = eval (swap_fm a b F1) (swap_list a b L); \<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F2 L = eval (swap_fm a b F2) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Or F1 F2) L = eval (swap_fm a b (Or F1 F2)) (swap_list a b L)
 4. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Neg F) L = eval (swap_fm a b (Neg F)) (swap_list a b L)
 5. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)
 6. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 7. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 8. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
case (Atom At)
[PROOF STATE]
proof (state)
this:
a < length L
b < length L

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

goal (1 subgoal):
 1. eval (fm.Atom At) L = eval (swap_fm a b (fm.Atom At)) (swap_list a b L)
[PROOF STEP]
apply(cases At)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>a < length L; b < length L; At = Less x1\<rbrakk> \<Longrightarrow> eval (fm.Atom At) L = eval (swap_fm a b (fm.Atom At)) (swap_list a b L)
 2. \<And>x2. \<lbrakk>a < length L; b < length L; At = Eq x2\<rbrakk> \<Longrightarrow> eval (fm.Atom At) L = eval (swap_fm a b (fm.Atom At)) (swap_list a b L)
 3. \<And>x3. \<lbrakk>a < length L; b < length L; At = Leq x3\<rbrakk> \<Longrightarrow> eval (fm.Atom At) L = eval (swap_fm a b (fm.Atom At)) (swap_list a b L)
 4. \<And>x4. \<lbrakk>a < length L; b < length L; At = Neq x4\<rbrakk> \<Longrightarrow> eval (fm.Atom At) L = eval (swap_fm a b (fm.Atom At)) (swap_list a b L)
[PROOF STEP]
using swap_poly[OF Atom(1) Atom(2)]
[PROOF STATE]
proof (prove)
using this:
insertion (nth_default 0 L) ?p = insertion (nth_default 0 (swap_list a b L)) (swap_poly a b ?p)

goal (4 subgoals):
 1. \<And>x1. \<lbrakk>a < length L; b < length L; At = Less x1\<rbrakk> \<Longrightarrow> eval (fm.Atom At) L = eval (swap_fm a b (fm.Atom At)) (swap_list a b L)
 2. \<And>x2. \<lbrakk>a < length L; b < length L; At = Eq x2\<rbrakk> \<Longrightarrow> eval (fm.Atom At) L = eval (swap_fm a b (fm.Atom At)) (swap_list a b L)
 3. \<And>x3. \<lbrakk>a < length L; b < length L; At = Leq x3\<rbrakk> \<Longrightarrow> eval (fm.Atom At) L = eval (swap_fm a b (fm.Atom At)) (swap_list a b L)
 4. \<And>x4. \<lbrakk>a < length L; b < length L; At = Neq x4\<rbrakk> \<Longrightarrow> eval (fm.Atom At) L = eval (swap_fm a b (fm.Atom At)) (swap_list a b L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (fm.Atom At) L = eval (swap_fm a b (fm.Atom At)) (swap_list a b L)

goal (7 subgoals):
 1. \<And>F1 F2 a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F1 L = eval (swap_fm a b F1) (swap_list a b L); \<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F2 L = eval (swap_fm a b F2) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (And F1 F2) L = eval (swap_fm a b (And F1 F2)) (swap_list a b L)
 2. \<And>F1 F2 a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F1 L = eval (swap_fm a b F1) (swap_list a b L); \<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F2 L = eval (swap_fm a b F2) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Or F1 F2) L = eval (swap_fm a b (Or F1 F2)) (swap_list a b L)
 3. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Neg F) L = eval (swap_fm a b (Neg F)) (swap_list a b L)
 4. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)
 5. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 6. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 7. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>F1 F2 a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F1 L = eval (swap_fm a b F1) (swap_list a b L); \<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F2 L = eval (swap_fm a b F2) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (And F1 F2) L = eval (swap_fm a b (And F1 F2)) (swap_list a b L)
 2. \<And>F1 F2 a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F1 L = eval (swap_fm a b F1) (swap_list a b L); \<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F2 L = eval (swap_fm a b F2) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Or F1 F2) L = eval (swap_fm a b (Or F1 F2)) (swap_list a b L)
 3. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Neg F) L = eval (swap_fm a b (Neg F)) (swap_list a b L)
 4. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)
 5. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 6. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 7. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
case (And F1 F2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F1 ?L = eval (swap_fm ?a ?b F1) (swap_list ?a ?b ?L)
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F2 ?L = eval (swap_fm ?a ?b F2) (swap_list ?a ?b ?L)
a < length L
b < length L

goal (7 subgoals):
 1. \<And>F1 F2 a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F1 L = eval (swap_fm a b F1) (swap_list a b L); \<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F2 L = eval (swap_fm a b F2) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (And F1 F2) L = eval (swap_fm a b (And F1 F2)) (swap_list a b L)
 2. \<And>F1 F2 a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F1 L = eval (swap_fm a b F1) (swap_list a b L); \<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F2 L = eval (swap_fm a b F2) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Or F1 F2) L = eval (swap_fm a b (Or F1 F2)) (swap_list a b L)
 3. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Neg F) L = eval (swap_fm a b (Neg F)) (swap_list a b L)
 4. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)
 5. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 6. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 7. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (And F1 F2) L = eval (swap_fm a b (And F1 F2)) (swap_list a b L)
[PROOF STEP]
using And(1)[OF And(3-4)] And(2)[OF And(3-4)]
[PROOF STATE]
proof (prove)
using this:
eval F1 L = eval (swap_fm a b F1) (swap_list a b L)
eval F2 L = eval (swap_fm a b F2) (swap_list a b L)

goal (1 subgoal):
 1. eval (And F1 F2) L = eval (swap_fm a b (And F1 F2)) (swap_list a b L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (And F1 F2) L = eval (swap_fm a b (And F1 F2)) (swap_list a b L)

goal (6 subgoals):
 1. \<And>F1 F2 a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F1 L = eval (swap_fm a b F1) (swap_list a b L); \<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F2 L = eval (swap_fm a b F2) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Or F1 F2) L = eval (swap_fm a b (Or F1 F2)) (swap_list a b L)
 2. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Neg F) L = eval (swap_fm a b (Neg F)) (swap_list a b L)
 3. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)
 4. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 5. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 6. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>F1 F2 a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F1 L = eval (swap_fm a b F1) (swap_list a b L); \<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F2 L = eval (swap_fm a b F2) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Or F1 F2) L = eval (swap_fm a b (Or F1 F2)) (swap_list a b L)
 2. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Neg F) L = eval (swap_fm a b (Neg F)) (swap_list a b L)
 3. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)
 4. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 5. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 6. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
case (Or F1 F2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F1 ?L = eval (swap_fm ?a ?b F1) (swap_list ?a ?b ?L)
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F2 ?L = eval (swap_fm ?a ?b F2) (swap_list ?a ?b ?L)
a < length L
b < length L

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

goal (1 subgoal):
 1. eval (Or F1 F2) L = eval (swap_fm a b (Or F1 F2)) (swap_list a b L)
[PROOF STEP]
using Or(1)[OF Or(3-4)] Or(2)[OF Or(3-4)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F1 ?L = eval (swap_fm ?a ?b F1) (swap_list ?a ?b ?L)
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F2 ?L = eval (swap_fm ?a ?b F2) (swap_list ?a ?b ?L)
a < length L
b < length L
eval F1 L = eval (swap_fm a b F1) (swap_list a b L)
eval F2 L = eval (swap_fm a b F2) (swap_list a b L)

goal (1 subgoal):
 1. eval (Or F1 F2) L = eval (swap_fm a b (Or F1 F2)) (swap_list a b L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (Or F1 F2) L = eval (swap_fm a b (Or F1 F2)) (swap_list a b L)

goal (5 subgoals):
 1. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Neg F) L = eval (swap_fm a b (Neg F)) (swap_list a b L)
 2. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)
 3. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 4. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 5. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Neg F) L = eval (swap_fm a b (Neg F)) (swap_list a b L)
 2. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)
 3. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 4. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 5. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
case (Neg F)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F ?L = eval (swap_fm ?a ?b F) (swap_list ?a ?b ?L)
a < length L
b < length L

goal (5 subgoals):
 1. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (Neg F) L = eval (swap_fm a b (Neg F)) (swap_list a b L)
 2. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)
 3. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 4. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 5. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F ?L = eval (swap_fm ?a ?b F) (swap_list ?a ?b ?L)
a < length L
b < length L
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F ?L = eval (swap_fm ?a ?b F) (swap_list ?a ?b ?L)
a < length L
b < length L

goal (1 subgoal):
 1. eval (Neg F) L = eval (swap_fm a b (Neg F)) (swap_list a b L)
[PROOF STEP]
using Neg(1)[OF Neg(2-3)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F ?L = eval (swap_fm ?a ?b F) (swap_list ?a ?b ?L)
a < length L
b < length L
eval F L = eval (swap_fm a b F) (swap_list a b L)

goal (1 subgoal):
 1. eval (Neg F) L = eval (swap_fm a b (Neg F)) (swap_list a b L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (Neg F) L = eval (swap_fm a b (Neg F)) (swap_list a b L)

goal (4 subgoals):
 1. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)
 2. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 3. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 4. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)
 2. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 3. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 4. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
case (ExQ F)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F ?L = eval (swap_fm ?a ?b F) (swap_list ?a ?b ?L)
a < length L
b < length L

goal (4 subgoals):
 1. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)
 2. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 3. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 4. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. eval F (x # L)) = (\<exists>x. eval (swap_fm (Suc a) (Suc b) F) (x # L[b := L ! a, a := L ! b]))
[PROOF STEP]
apply(rule ex_cong1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (x # L[b := L ! a, a := L ! b])
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (x # L[b := L ! a, a := L ! b])
[PROOF STEP]
using ExQ(1)[of "Suc a" "x#L" "Suc b"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Suc a < length (x # L); Suc b < length (x # L)\<rbrakk> \<Longrightarrow> eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (swap_list (Suc a) (Suc b) (x # L))

goal (1 subgoal):
 1. eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (x # L[b := L ! a, a := L ! b])
[PROOF STEP]
unfolding swap_list_cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Suc a < length (x # L); Suc b < length (x # L)\<rbrakk> \<Longrightarrow> eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (x # swap_list a b L)

goal (1 subgoal):
 1. eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (x # L[b := L ! a, a := L ! b])
[PROOF STEP]
using ExQ(2-3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Suc a < length (x # L); Suc b < length (x # L)\<rbrakk> \<Longrightarrow> eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (x # swap_list a b L)
a < length L
b < length L

goal (1 subgoal):
 1. eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (x # L[b := L ! a, a := L ! b])
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
eval (ExQ F) L = eval (swap_fm a b (ExQ F)) (swap_list a b L)

goal (3 subgoals):
 1. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 2. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 3. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 2. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 3. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
case (AllQ F)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F ?L = eval (swap_fm ?a ?b F) (swap_list ?a ?b ?L)
a < length L
b < length L

goal (3 subgoals):
 1. \<And>F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
 2. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 3. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F ?L = eval (swap_fm ?a ?b F) (swap_list ?a ?b ?L)
a < length L
b < length L
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F ?L = eval (swap_fm ?a ?b F) (swap_list ?a ?b ?L)
a < length L
b < length L

goal (1 subgoal):
 1. eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a L b. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (L[b := L ! a, a := L ! b]); a < length L; b < length L\<rbrakk> \<Longrightarrow> (\<forall>x. eval F (x # L)) = (\<forall>x. eval (swap_fm (Suc a) (Suc b) F) (x # L[b := L ! a, a := L ! b]))
[PROOF STEP]
apply(rule all_cong1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>a L b. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (L[b := L ! a, a := L ! b]); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (x # L[b := L ! a, a := L ! b])
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a L b. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (L[b := L ! a, a := L ! b]); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (x # L[b := L ! a, a := L ! b])
[PROOF STEP]
using AllQ(1)[of "Suc a" "x#L" "Suc b"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Suc a < length (x # L); Suc b < length (x # L)\<rbrakk> \<Longrightarrow> eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (swap_list (Suc a) (Suc b) (x # L))

goal (1 subgoal):
 1. \<lbrakk>\<And>a L b. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (L[b := L ! a, a := L ! b]); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (x # L[b := L ! a, a := L ! b])
[PROOF STEP]
unfolding swap_list_cons
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Suc a < length (x # L); Suc b < length (x # L)\<rbrakk> \<Longrightarrow> eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (x # swap_list a b L)

goal (1 subgoal):
 1. \<lbrakk>\<And>a L b. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (L[b := L ! a, a := L ! b]); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (x # L[b := L ! a, a := L ! b])
[PROOF STEP]
using AllQ(2-3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Suc a < length (x # L); Suc b < length (x # L)\<rbrakk> \<Longrightarrow> eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (x # swap_list a b L)
a < length L
b < length L

goal (1 subgoal):
 1. \<lbrakk>\<And>a L b. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (L[b := L ! a, a := L ! b]); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F (x # L) = eval (swap_fm (Suc a) (Suc b) F) (x # L[b := L ! a, a := L ! b])
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
eval (AllQ F) L = eval (swap_fm a b (AllQ F)) (swap_list a b L)

goal (2 subgoals):
 1. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 2. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 2. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
case (ExN i F)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F ?L = eval (swap_fm ?a ?b F) (swap_list ?a ?b ?L)
a < length L
b < length L

goal (2 subgoals):
 1. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (ExN x1 F) L = eval (swap_fm a b (ExN x1 F)) (swap_list a b L)
 2. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (ExN i F) L = eval (swap_fm a b (ExN i F)) (swap_list a b L)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>l. length l = i \<and> eval F (l @ L)) = (\<exists>l. length l = i \<and> eval (swap_fm (a + i) (b + i) F) (l @ L[b := L ! a, a := L ! b]))
[PROOF STEP]
apply(rule ex_cong1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. (length l = i \<and> eval F (l @ L)) = (length l = i \<and> eval (swap_fm (a + i) (b + i) F) (l @ L[b := L ! a, a := L ! b]))
[PROOF STEP]
subgoal for l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (length l = i \<and> eval F (l @ L)) = (length l = i \<and> eval (swap_fm (a + i) (b + i) F) (l @ L[b := L ! a, a := L ! b]))
[PROOF STEP]
using ExN(1)[of "a+i" "l@L" "b+i"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a + i < length (l @ L); b + i < length (l @ L)\<rbrakk> \<Longrightarrow> eval F (l @ L) = eval (swap_fm (a + i) (b + i) F) (swap_list (a + i) (b + i) (l @ L))

goal (1 subgoal):
 1. (length l = i \<and> eval F (l @ L)) = (length l = i \<and> eval (swap_fm (a + i) (b + i) F) (l @ L[b := L ! a, a := L ! b]))
[PROOF STEP]
by (smt (verit, del_insts) ExN.prems(1) ExN.prems(2) add.commute add_diff_cancel_right' add_less_cancel_left length_append list_update_append not_add_less2 nth_append swap_list.elims)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
eval (ExN i F) L = eval (swap_fm a b (ExN i F)) (swap_list a b L)

goal (1 subgoal):
 1. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
case (AllN i F)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F ?L = eval (swap_fm ?a ?b F) (swap_list ?a ?b ?L)
a < length L
b < length L

goal (1 subgoal):
 1. \<And>x1 F a b L. \<lbrakk>\<And>a b L. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (swap_list a b L); a < length L; b < length L\<rbrakk> \<Longrightarrow> eval (AllN x1 F) L = eval (swap_fm a b (AllN x1 F)) (swap_list a b L)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F ?L = eval (swap_fm ?a ?b F) (swap_list ?a ?b ?L)
a < length L
b < length L
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a < length ?L; ?b < length ?L\<rbrakk> \<Longrightarrow> eval F ?L = eval (swap_fm ?a ?b F) (swap_list ?a ?b ?L)
a < length L
b < length L

goal (1 subgoal):
 1. eval (AllN i F) L = eval (swap_fm a b (AllN i F)) (swap_list a b L)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a L b. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (L[b := L ! a, a := L ! b]); a < length L; b < length L\<rbrakk> \<Longrightarrow> (\<forall>l. length l = i \<longrightarrow> eval F (l @ L)) = (\<forall>l. length l = i \<longrightarrow> eval (swap_fm (a + i) (b + i) F) (l @ L[b := L ! a, a := L ! b]))
[PROOF STEP]
apply(rule all_cong1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>\<And>a L b. \<lbrakk>a < length L; b < length L\<rbrakk> \<Longrightarrow> eval F L = eval (swap_fm a b F) (L[b := L ! a, a := L ! b]); a < length L; b < length L\<rbrakk> \<Longrightarrow> (length l = i \<longrightarrow> eval F (l @ L)) = (length l = i \<longrightarrow> eval (swap_fm (a + i) (b + i) F) (l @ L[b := L ! a, a := L ! b]))
[PROOF STEP]
by (smt (z3) add.commute add_diff_cancel_right' le_add2 length_append less_diff_conv2 list_update_append not_add_less2 nth_append)
[PROOF STATE]
proof (state)
this:
eval (AllN i F) L = eval (swap_fm a b (AllN i F)) (swap_list a b L)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "eval (ExQ (ExQ F)) L = eval (ExQ (ExQ (swap_fm 0 1 F))) L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (ExQ (ExQ F)) L = eval (ExQ (ExQ (swap_fm 0 1 F))) L
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x xa. eval F (xa # x # L)) = (\<exists>x xa. eval (swap_fm 0 (Suc 0) F) (xa # x # L))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xa. eval F (xa # x # L) \<Longrightarrow> \<exists>x xa. eval (swap_fm 0 (Suc 0) F) (xa # x # L)
 2. \<And>x xa. eval (swap_fm 0 (Suc 0) F) (xa # x # L) \<Longrightarrow> \<exists>x xa. eval F (xa # x # L)
[PROOF STEP]
subgoal for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval F (j # i # L) \<Longrightarrow> \<exists>x xa. eval (swap_fm 0 (Suc 0) F) (xa # x # L)
[PROOF STEP]
apply(rule exI[where x=j])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval F (j # i # L) \<Longrightarrow> \<exists>x. eval (swap_fm 0 (Suc 0) F) (x # j # L)
[PROOF STEP]
apply(rule exI[where x=i])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval F (j # i # L) \<Longrightarrow> eval (swap_fm 0 (Suc 0) F) (i # j # L)
[PROOF STEP]
using swap_fm[of 0 "j # i # L" "Suc 0" F]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < length (j # i # L); Suc 0 < length (j # i # L)\<rbrakk> \<Longrightarrow> eval F (j # i # L) = eval (swap_fm 0 (Suc 0) F) (swap_list 0 (Suc 0) (j # i # L))

goal (1 subgoal):
 1. eval F (j # i # L) \<Longrightarrow> eval (swap_fm 0 (Suc 0) F) (i # j # L)
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. eval (swap_fm 0 (Suc 0) F) (xa # x # L) \<Longrightarrow> \<exists>x xa. eval F (xa # x # L)
[PROOF STEP]
subgoal for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (swap_fm 0 (Suc 0) F) (j # i # L) \<Longrightarrow> \<exists>x xa. eval F (xa # x # L)
[PROOF STEP]
apply(rule exI[where x=j])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (swap_fm 0 (Suc 0) F) (j # i # L) \<Longrightarrow> \<exists>x. eval F (x # j # L)
[PROOF STEP]
apply(rule exI[where x=i])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (swap_fm 0 (Suc 0) F) (j # i # L) \<Longrightarrow> eval F (i # j # L)
[PROOF STEP]
using swap_fm[of 0 "i # j # L" "Suc 0" F]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < length (i # j # L); Suc 0 < length (i # j # L)\<rbrakk> \<Longrightarrow> eval F (i # j # L) = eval (swap_fm 0 (Suc 0) F) (swap_list 0 (Suc 0) (i # j # L))

goal (1 subgoal):
 1. eval (swap_fm 0 (Suc 0) F) (j # i # L) \<Longrightarrow> eval F (i # j # L)
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma swap_atom:
  assumes "length L > a"
  assumes "length L > b"
  shows "aEval F L = aEval (swap_atom a b F) (swap_list a b L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aEval F L = aEval (swap_atom a b F) (swap_list a b L)
[PROOF STEP]
using swap_fm[OF assms, of "Atom F"]
[PROOF STATE]
proof (prove)
using this:
eval (fm.Atom F) L = eval (swap_fm a b (fm.Atom F)) (swap_list a b L)

goal (1 subgoal):
 1. aEval F L = aEval (swap_atom a b F) (swap_list a b L)
[PROOF STEP]
by auto


[STATEMENT]
lemma "check_eqv (Abs_idx (1, 0)) (FAnd (FEq_Const 0 100000) (FEq_Const 0 0)) FFalse"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_eqv (Abs_idx (1, 0)) (x\<^sub>0 = 100000 \<and> x\<^sub>0 = 0) \<bottom>
[PROOF STEP]
by check_equiv


[STATEMENT]
lemma "check_eqv (Abs_idx (1, 0)) (FEq_Plus 0 0 1) FFalse"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_eqv (Abs_idx (1, 0)) (x\<^sub>0 = x\<^sub>0 + 1) \<bottom>
[PROOF STEP]
by check_equiv


[STATEMENT]
lemma "check_eqv (Abs_idx (0, 1)) (FSuc_SO 0 0) (FBase (Empty 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_eqv (Abs_idx (0, 1)) (X\<^sub>0 = X\<^sub>0 + 1) (FBase (Empty 0))
[PROOF STEP]
by check_equiv


[STATEMENT]
lemma "check_eqv (Abs_idx (0, 2))
  (FEx SO (FAnd (FBase (Subset 1 0)) (FSuc_SO 0 2)))
  (FAll FO (FImp (FIn 0 0) (FEx FO (FAnd (FEq_Plus 1 0 1) (FIn 0 1)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. check_eqv (Abs_idx (0, 2)) (\<exists>\<^sub>2 FBase (Subset 1 0) \<and> X\<^sub>0 = X\<^sub>2 + 1) (\<forall>\<^sub>1 \<not> x\<^sub>0 \<in> X\<^bsub>0\<^esub> \<or> (\<exists>\<^sub>1 x\<^sub>1 = x\<^sub>0 + 1 \<and> x\<^sub>0 \<in> X\<^bsub>1\<^esub>))
[PROOF STEP]
by check_equiv


[STATEMENT]
lemma "Thm (Abs_idx (0, 1)) (FNot M2L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Thm (Abs_idx (0, 1)) (\<not> M2L)
[PROOF STEP]
by (simp add: Thm_def M2L_def) check_equiv


[STATEMENT]
lemma "Thm (Abs_idx (0, 0)) \<Phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Thm (Abs_idx (0, 0)) \<Phi>
[PROOF STEP]
by (simp add: Thm_def \<Phi>_def) check_equiv


[STATEMENT]
lemma "Thm (Abs_idx (0, 1)) (\<Psi> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Thm (Abs_idx (0, 1)) (\<Psi> 0)
[PROOF STEP]
by (simp add: Thm_def \<Psi>_def) check_equiv


[STATEMENT]
lemma "Thm (Abs_idx (0, 2)) (\<Psi> 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Thm (Abs_idx (0, 2)) (\<Psi> 1)
[PROOF STEP]
by (simp add: Thm_def \<Psi>_def) check_equiv


[STATEMENT]
lemma "Thm (Abs_idx (0, 3)) (\<Psi> 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Thm (Abs_idx (0, 3)) (\<Psi> 2)
[PROOF STEP]
by (simp add: Thm_def \<Psi>_def numeral_nat) check_equiv


[STATEMENT]
lemma "Thm (Abs_idx (0, 4)) (\<Psi> 3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Thm (Abs_idx (0, 4)) (\<Psi> 3)
[PROOF STEP]
by (simp add: Thm_def \<Psi>_def numeral_nat) check_equiv


[STATEMENT]
lemma "Thm (Abs_idx (0, 5)) (\<Psi> 4)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Thm (Abs_idx (0, 5)) (\<Psi> 4)
[PROOF STEP]
by (simp add: Thm_def \<Psi>_def numeral_nat) check_equiv


[STATEMENT]
lemma "Thm (Abs_idx (0, 6)) (\<Psi> 5)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Thm (Abs_idx (0, 6)) (\<Psi> 5)
[PROOF STEP]
by (simp add: Thm_def \<Psi>_def numeral_nat) check_equiv


[STATEMENT]
lemma "Thm (Abs_idx (0, 11)) (\<Psi> 10)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Thm (Abs_idx (0, 11)) (\<Psi> 10)
[PROOF STEP]
by (simp add: Thm_def \<Psi>_def numeral_nat) check_equiv


[STATEMENT]
lemma "Thm (Abs_idx (0, 16)) (\<Psi> 15)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Thm (Abs_idx (0, 16)) (\<Psi> 15)
[PROOF STEP]
by (simp add: Thm_def \<Psi>_def numeral_nat) check_equiv


[STATEMENT]
lemma d_b_c_a: "d_aux b c a = d_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux b c a = d_aux a b c
[PROOF STEP]
by (metis d_aux_def sup.assoc sup_commute)


[STATEMENT]
lemma d_c_a_b: "d_aux c a b = d_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux c a b = d_aux a b c
[PROOF STEP]
by (metis d_aux_def sup.assoc sup_commute)


[STATEMENT]
lemma e_b_c_a: "e_aux b c a = e_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_aux b c a = e_aux a b c
[PROOF STEP]
by (simp add: e_aux_def ac_simps)


[STATEMENT]
lemma e_c_a_b: "e_aux c a b = e_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e_aux c a b = e_aux a b c
[PROOF STEP]
by (simp add: e_aux_def ac_simps)


[STATEMENT]
lemma b_a: "b_aux a b c = a_aux b c a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_aux a b c = a_aux b c a
[PROOF STEP]
by (simp add: a_aux_def b_aux_def e_b_c_a d_b_c_a)


[STATEMENT]
lemma c_a: "c_aux a b c = a_aux c a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_aux a b c = a_aux c a b
[PROOF STEP]
by (simp add: a_aux_def c_aux_def e_c_a_b d_c_a_b)


[STATEMENT]
lemma [simp]: "a_aux a b c \<le> e_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_aux a b c \<le> e_aux a b c
[PROOF STEP]
apply (simp add: a_aux_def e_aux_def d_aux_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> ((a \<squnion> b) \<sqinter> (b \<squnion> c) \<sqinter> (c \<squnion> a)) \<le> b \<squnion> c
[PROOF STEP]
apply (rule_tac y = "(a \<squnion> b) \<sqinter> (b \<squnion> c) \<sqinter> (c \<squnion> a)" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a \<sqinter> ((a \<squnion> b) \<sqinter> (b \<squnion> c) \<sqinter> (c \<squnion> a)) \<le> (a \<squnion> b) \<sqinter> (b \<squnion> c) \<sqinter> (c \<squnion> a)
 2. (a \<squnion> b) \<sqinter> (b \<squnion> c) \<sqinter> (c \<squnion> a) \<le> b \<squnion> c
[PROOF STEP]
apply (rule inf_le2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<squnion> b) \<sqinter> (b \<squnion> c) \<sqinter> (c \<squnion> a) \<le> b \<squnion> c
[PROOF STEP]
by simp


[STATEMENT]
lemma [simp]: "b_aux a b c \<le> e_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_aux a b c \<le> e_aux a b c
[PROOF STEP]
apply (unfold b_a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_aux b c a \<le> e_aux a b c
[PROOF STEP]
apply (subst e_b_c_a [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_aux b c a \<le> e_aux b c a
[PROOF STEP]
by simp


[STATEMENT]
lemma [simp]: "c_aux a b c \<le> e_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_aux a b c \<le> e_aux a b c
[PROOF STEP]
apply (unfold c_a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_aux c a b \<le> e_aux a b c
[PROOF STEP]
apply (subst e_c_a_b [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_aux c a b \<le> e_aux c a b
[PROOF STEP]
by simp


[STATEMENT]
lemma [simp]: "d_aux a b c \<le> a_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> a_aux a b c
[PROOF STEP]
by (simp add: a_aux_def e_aux_def d_aux_def)


[STATEMENT]
lemma [simp]: "d_aux a b c \<le> b_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> b_aux a b c
[PROOF STEP]
apply (unfold b_a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> a_aux b c a
[PROOF STEP]
apply (subst d_b_c_a [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux b c a \<le> a_aux b c a
[PROOF STEP]
by simp


[STATEMENT]
lemma [simp]: "d_aux a b c \<le> c_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> c_aux a b c
[PROOF STEP]
apply (unfold c_a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> a_aux c a b
[PROOF STEP]
apply (subst d_c_a_b [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux c a b \<le> a_aux c a b
[PROOF STEP]
by simp


[STATEMENT]
lemma a_meet_e: "a \<sqinter> (e_aux a b c) = a \<sqinter> (b \<squnion> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> e_aux a b c = a \<sqinter> (b \<squnion> c)
[PROOF STEP]
by (rule order.antisym) (simp_all add: e_aux_def le_infI2)


[STATEMENT]
lemma b_meet_e: "b \<sqinter> (e_aux a b c) = b \<sqinter> (c \<squnion> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<sqinter> e_aux a b c = b \<sqinter> (c \<squnion> a)
[PROOF STEP]
by (simp add: a_meet_e [THEN sym] e_b_c_a)


[STATEMENT]
lemma c_meet_e: "c \<sqinter> (e_aux a b c) = c \<sqinter> (a \<squnion> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<sqinter> e_aux a b c = c \<sqinter> (a \<squnion> b)
[PROOF STEP]
by (simp add: a_meet_e [THEN sym] e_c_a_b)


[STATEMENT]
lemma a_join_d: "a \<squnion> d_aux a b c = a \<squnion> (b \<sqinter> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<squnion> d_aux a b c = a \<squnion> b \<sqinter> c
[PROOF STEP]
by (rule order.antisym) (simp_all add: d_aux_def le_supI2)


[STATEMENT]
lemma b_join_d: "b \<squnion> d_aux a b c = b \<squnion> (c \<sqinter> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<squnion> d_aux a b c = b \<squnion> c \<sqinter> a
[PROOF STEP]
by (simp add: a_join_d [THEN sym] d_b_c_a)


[STATEMENT]
lemma M5_lattice_incomp: "M5_lattice a b c \<Longrightarrow> incomp a b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M5_lattice a b c \<Longrightarrow> incomp a b
[PROOF STEP]
apply (simp add: M5_lattice_def incomp_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sqinter> b = b \<sqinter> c \<and> c \<sqinter> a = b \<sqinter> c \<and> a \<squnion> b = b \<squnion> c \<and> c \<squnion> a = b \<squnion> c \<and> a \<sqinter> b < a \<squnion> b \<Longrightarrow> \<not> a \<le> b \<and> \<not> b \<le> a
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<sqinter> b = b \<sqinter> c; c \<sqinter> a = b \<sqinter> c; a \<squnion> b = b \<squnion> c; c \<squnion> a = b \<squnion> c; a \<sqinter> b < a \<squnion> b; a \<le> b\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>a \<sqinter> b = b \<sqinter> c; c \<sqinter> a = b \<sqinter> c; a \<squnion> b = b \<squnion> c; c \<squnion> a = b \<squnion> c; a \<sqinter> b < a \<squnion> b; b \<le> a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp_all add: inf_absorb1 inf_absorb2 )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a = b \<sqinter> c; b \<sqinter> c \<squnion> b = b \<squnion> c; c \<squnion> b \<sqinter> c = b \<squnion> c; b \<sqinter> c < b \<squnion> c\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>b = b \<sqinter> c; c \<sqinter> a = b; a \<squnion> b = b \<squnion> c; c \<squnion> a = b \<squnion> c; b < b \<squnion> c; b \<le> a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (simp_all add: sup_absorb1 sup_absorb2 )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b = b \<sqinter> c; c \<sqinter> (b \<squnion> c) = b; a = b \<squnion> c; b < b \<squnion> c\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (subgoal_tac "c \<sqinter> (b \<squnion> c) = c")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b = b \<sqinter> c; c \<sqinter> (b \<squnion> c) = b; a = b \<squnion> c; b < b \<squnion> c; c \<sqinter> (b \<squnion> c) = c\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>b = b \<sqinter> c; c \<sqinter> (b \<squnion> c) = b; a = b \<squnion> c; b < b \<squnion> c\<rbrakk> \<Longrightarrow> c \<sqinter> (b \<squnion> c) = c
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b = b \<sqinter> c; c \<sqinter> (b \<squnion> c) = b; a = b \<squnion> c; b < b \<squnion> c\<rbrakk> \<Longrightarrow> c \<sqinter> (b \<squnion> c) = c
[PROOF STEP]
apply (subst sup_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b = b \<sqinter> c; c \<sqinter> (b \<squnion> c) = b; a = b \<squnion> c; b < b \<squnion> c\<rbrakk> \<Longrightarrow> c \<sqinter> (c \<squnion> b) = c
[PROOF STEP]
by simp


[STATEMENT]
lemma b_meet_d: "b \<sqinter> (d_aux a b c) = (b \<sqinter> c) \<squnion> (a \<sqinter> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<sqinter> d_aux a b c = b \<sqinter> c \<squnion> a \<sqinter> b
[PROOF STEP]
by (simp add: a_meet_d [THEN sym] d_b_c_a)


[STATEMENT]
lemma c_meet_d: "c \<sqinter> (d_aux a b c) = (c \<sqinter> a) \<squnion> (b \<sqinter> c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<sqinter> d_aux a b c = c \<sqinter> a \<squnion> b \<sqinter> c
[PROOF STEP]
by (simp add: a_meet_d [THEN sym] d_c_a_b)


[STATEMENT]
lemma d_less_e: "no_distrib a b c \<Longrightarrow> d_aux a b c < e_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_distrib a b c \<Longrightarrow> d_aux a b c < e_aux a b c
[PROOF STEP]
apply (subst less_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. no_distrib a b c \<Longrightarrow> d_aux a b c \<le> e_aux a b c \<and> d_aux a b c \<noteq> e_aux a b c
[PROOF STEP]
apply(case_tac "d_aux a b c = e_aux a b c")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_distrib a b c; d_aux a b c = e_aux a b c\<rbrakk> \<Longrightarrow> d_aux a b c \<le> e_aux a b c \<and> d_aux a b c \<noteq> e_aux a b c
 2. \<lbrakk>no_distrib a b c; d_aux a b c \<noteq> e_aux a b c\<rbrakk> \<Longrightarrow> d_aux a b c \<le> e_aux a b c \<and> d_aux a b c \<noteq> e_aux a b c
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_distrib a b c; d_aux a b c = e_aux a b c\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>no_distrib a b c; d_aux a b c \<noteq> e_aux a b c\<rbrakk> \<Longrightarrow> d_aux a b c \<le> e_aux a b c
[PROOF STEP]
apply (simp add: no_distrib_def a_meet_e [THEN sym] a_meet_d [THEN sym])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_distrib a b c; d_aux a b c \<noteq> e_aux a b c\<rbrakk> \<Longrightarrow> d_aux a b c \<le> e_aux a b c
[PROOF STEP]
apply (rule_tac y = "a_aux a b c" in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_distrib a b c; d_aux a b c \<noteq> e_aux a b c\<rbrakk> \<Longrightarrow> d_aux a b c \<le> a_aux a b c
 2. \<lbrakk>no_distrib a b c; d_aux a b c \<noteq> e_aux a b c\<rbrakk> \<Longrightarrow> a_aux a b c \<le> e_aux a b c
[PROOF STEP]
by simp_all


[STATEMENT]
lemma a_meet_b_eq_d: " d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
assume d_less_e: " d_aux a b c \<le> e_aux a b c"
[PROOF STATE]
proof (state)
this:
d_aux a b c \<le> e_aux a b c

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
have "(a \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) = (b \<sqinter> e_aux a b c \<squnion>  d_aux a b c) \<sqinter> (d_aux a b c \<squnion> a \<sqinter> e_aux a b c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) = (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (d_aux a b c \<squnion> a \<sqinter> e_aux a b c)
[PROOF STEP]
by (simp add: inf_commute sup_commute)
[PROOF STATE]
proof (state)
this:
(a \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) = (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (d_aux a b c \<squnion> a \<sqinter> e_aux a b c)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(a \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) = (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (d_aux a b c \<squnion> a \<sqinter> e_aux a b c)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
have "\<dots> = d_aux a b c \<squnion> ((b \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (a \<sqinter> e_aux a b c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (d_aux a b c \<squnion> a \<sqinter> e_aux a b c) = d_aux a b c \<squnion> (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (a \<sqinter> e_aux a b c)
[PROOF STEP]
by (simp add: modular)
[PROOF STATE]
proof (state)
this:
(b \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (d_aux a b c \<squnion> a \<sqinter> e_aux a b c) = d_aux a b c \<squnion> (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (a \<sqinter> e_aux a b c)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(b \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (d_aux a b c \<squnion> a \<sqinter> e_aux a b c) = d_aux a b c \<squnion> (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (a \<sqinter> e_aux a b c)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
have "\<dots> = d_aux a b c \<squnion> (d_aux a b c \<squnion> e_aux a b c \<sqinter> b) \<sqinter> (a \<sqinter> e_aux a b c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<squnion> (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (a \<sqinter> e_aux a b c) = d_aux a b c \<squnion> (d_aux a b c \<squnion> e_aux a b c \<sqinter> b) \<sqinter> (a \<sqinter> e_aux a b c)
[PROOF STEP]
by (simp add: inf_commute sup_commute)
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (a \<sqinter> e_aux a b c) = d_aux a b c \<squnion> (d_aux a b c \<squnion> e_aux a b c \<sqinter> b) \<sqinter> (a \<sqinter> e_aux a b c)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (a \<sqinter> e_aux a b c) = d_aux a b c \<squnion> (d_aux a b c \<squnion> e_aux a b c \<sqinter> b) \<sqinter> (a \<sqinter> e_aux a b c)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
have "\<dots> = d_aux a b c \<squnion> (e_aux a b c \<sqinter> (d_aux a b c \<squnion> b)) \<sqinter> (a \<sqinter> e_aux a b c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<squnion> (d_aux a b c \<squnion> e_aux a b c \<sqinter> b) \<sqinter> (a \<sqinter> e_aux a b c) = d_aux a b c \<squnion> e_aux a b c \<sqinter> (d_aux a b c \<squnion> b) \<sqinter> (a \<sqinter> e_aux a b c)
[PROOF STEP]
by (cut_tac d_less_e, simp add: modular [THEN sym] less_le)
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> (d_aux a b c \<squnion> e_aux a b c \<sqinter> b) \<sqinter> (a \<sqinter> e_aux a b c) = d_aux a b c \<squnion> e_aux a b c \<sqinter> (d_aux a b c \<squnion> b) \<sqinter> (a \<sqinter> e_aux a b c)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> (d_aux a b c \<squnion> e_aux a b c \<sqinter> b) \<sqinter> (a \<sqinter> e_aux a b c) = d_aux a b c \<squnion> e_aux a b c \<sqinter> (d_aux a b c \<squnion> b) \<sqinter> (a \<sqinter> e_aux a b c)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
have "\<dots> =  d_aux a b c \<squnion> ((a \<sqinter> e_aux a b c) \<sqinter> (e_aux a b c \<sqinter> (b \<squnion> d_aux a b c)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<squnion> e_aux a b c \<sqinter> (d_aux a b c \<squnion> b) \<sqinter> (a \<sqinter> e_aux a b c) = d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (e_aux a b c \<sqinter> (b \<squnion> d_aux a b c))
[PROOF STEP]
by (simp add: inf_commute sup_commute)
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> e_aux a b c \<sqinter> (d_aux a b c \<squnion> b) \<sqinter> (a \<sqinter> e_aux a b c) = d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (e_aux a b c \<sqinter> (b \<squnion> d_aux a b c))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> e_aux a b c \<sqinter> (d_aux a b c \<squnion> b) \<sqinter> (a \<sqinter> e_aux a b c) = d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (e_aux a b c \<sqinter> (b \<squnion> d_aux a b c))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
have "\<dots> = d_aux a b c \<squnion> (a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> d_aux a b c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (e_aux a b c \<sqinter> (b \<squnion> d_aux a b c)) = d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> d_aux a b c)
[PROOF STEP]
by (simp add: inf_assoc)
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (e_aux a b c \<sqinter> (b \<squnion> d_aux a b c)) = d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> d_aux a b c)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (e_aux a b c \<sqinter> (b \<squnion> d_aux a b c)) = d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> d_aux a b c)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
have "\<dots> = d_aux a b c \<squnion> (a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> (c \<sqinter> a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> d_aux a b c) = d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> c \<sqinter> a)
[PROOF STEP]
by (simp add: b_join_d)
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> d_aux a b c) = d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> c \<sqinter> a)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> d_aux a b c) = d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> c \<sqinter> a)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
have "\<dots> = d_aux a b c \<squnion> (a \<sqinter> (b \<squnion> c) \<sqinter> (b \<squnion> (c \<sqinter> a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> c \<sqinter> a) = d_aux a b c \<squnion> a \<sqinter> (b \<squnion> c) \<sqinter> (b \<squnion> c \<sqinter> a)
[PROOF STEP]
by (simp add: a_meet_e)
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> c \<sqinter> a) = d_aux a b c \<squnion> a \<sqinter> (b \<squnion> c) \<sqinter> (b \<squnion> c \<sqinter> a)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> e_aux a b c \<sqinter> (b \<squnion> c \<sqinter> a) = d_aux a b c \<squnion> a \<sqinter> (b \<squnion> c) \<sqinter> (b \<squnion> c \<sqinter> a)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
have "\<dots> = d_aux a b c \<squnion> (a \<sqinter> ((b \<squnion> c) \<sqinter> (b \<squnion> (c \<sqinter> a))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<squnion> a \<sqinter> (b \<squnion> c) \<sqinter> (b \<squnion> c \<sqinter> a) = d_aux a b c \<squnion> a \<sqinter> ((b \<squnion> c) \<sqinter> (b \<squnion> c \<sqinter> a))
[PROOF STEP]
by (simp add: inf_assoc)
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> (b \<squnion> c) \<sqinter> (b \<squnion> c \<sqinter> a) = d_aux a b c \<squnion> a \<sqinter> ((b \<squnion> c) \<sqinter> (b \<squnion> c \<sqinter> a))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> (b \<squnion> c) \<sqinter> (b \<squnion> c \<sqinter> a) = d_aux a b c \<squnion> a \<sqinter> ((b \<squnion> c) \<sqinter> (b \<squnion> c \<sqinter> a))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
have "\<dots> = d_aux a b c \<squnion> (a \<sqinter> (b \<squnion> ((b \<squnion> c) \<sqinter> (c \<sqinter> a))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<squnion> a \<sqinter> ((b \<squnion> c) \<sqinter> (b \<squnion> c \<sqinter> a)) = d_aux a b c \<squnion> a \<sqinter> (b \<squnion> (b \<squnion> c) \<sqinter> (c \<sqinter> a))
[PROOF STEP]
by (simp add: modular)
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> ((b \<squnion> c) \<sqinter> (b \<squnion> c \<sqinter> a)) = d_aux a b c \<squnion> a \<sqinter> (b \<squnion> (b \<squnion> c) \<sqinter> (c \<sqinter> a))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> ((b \<squnion> c) \<sqinter> (b \<squnion> c \<sqinter> a)) = d_aux a b c \<squnion> a \<sqinter> (b \<squnion> (b \<squnion> c) \<sqinter> (c \<sqinter> a))

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
have "\<dots> = d_aux a b c \<squnion> (a \<sqinter> (b \<squnion> (c \<sqinter> a)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<squnion> a \<sqinter> (b \<squnion> (b \<squnion> c) \<sqinter> (c \<sqinter> a)) = d_aux a b c \<squnion> a \<sqinter> (b \<squnion> c \<sqinter> a)
[PROOF STEP]
by (simp add: inf_absorb2)
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> (b \<squnion> (b \<squnion> c) \<sqinter> (c \<sqinter> a)) = d_aux a b c \<squnion> a \<sqinter> (b \<squnion> c \<sqinter> a)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> (b \<squnion> (b \<squnion> c) \<sqinter> (c \<sqinter> a)) = d_aux a b c \<squnion> a \<sqinter> (b \<squnion> c \<sqinter> a)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
have "\<dots> = d_aux a b c \<squnion> (a \<sqinter> ((c \<sqinter> a) \<squnion> b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<squnion> a \<sqinter> (b \<squnion> c \<sqinter> a) = d_aux a b c \<squnion> a \<sqinter> (c \<sqinter> a \<squnion> b)
[PROOF STEP]
by (simp add: sup_commute inf_commute)
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> (b \<squnion> c \<sqinter> a) = d_aux a b c \<squnion> a \<sqinter> (c \<sqinter> a \<squnion> b)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> (b \<squnion> c \<sqinter> a) = d_aux a b c \<squnion> a \<sqinter> (c \<sqinter> a \<squnion> b)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
have "\<dots> = d_aux a b c \<squnion> ((c \<sqinter> a) \<squnion> (a \<sqinter> b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<squnion> a \<sqinter> (c \<sqinter> a \<squnion> b) = d_aux a b c \<squnion> (c \<sqinter> a \<squnion> a \<sqinter> b)
[PROOF STEP]
by (simp add: modular)
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> (c \<sqinter> a \<squnion> b) = d_aux a b c \<squnion> (c \<sqinter> a \<squnion> a \<sqinter> b)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> a \<sqinter> (c \<sqinter> a \<squnion> b) = d_aux a b c \<squnion> (c \<sqinter> a \<squnion> a \<sqinter> b)

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
have "\<dots> = d_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<squnion> (c \<sqinter> a \<squnion> a \<sqinter> b) = d_aux a b c
[PROOF STEP]
by (rule order.antisym, simp_all add: d_aux_def)
[PROOF STATE]
proof (state)
this:
d_aux a b c \<squnion> (c \<sqinter> a \<squnion> a \<sqinter> b) = d_aux a b c

goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(a \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) = d_aux a b c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(a \<sqinter> e_aux a b c \<squnion> d_aux a b c) \<sqinter> (b \<sqinter> e_aux a b c \<squnion> d_aux a b c) = d_aux a b c

goal (1 subgoal):
 1. a_aux a b c \<sqinter> b_aux a b c = d_aux a b c
[PROOF STEP]
by (simp add: a_aux_def b_aux_def)
[PROOF STATE]
proof (state)
this:
a_aux a b c \<sqinter> b_aux a b c = d_aux a b c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma b_meet_c_eq_d: " d_aux a b c \<le> e_aux a b c \<Longrightarrow> b_aux a b c \<sqinter> c_aux a b c = d_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> b_aux a b c \<sqinter> c_aux a b c = d_aux a b c
[PROOF STEP]
apply (subst b_a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux b c a \<sqinter> c_aux a b c = d_aux a b c
[PROOF STEP]
apply (subgoal_tac "c_aux a b c = b_aux b c a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>d_aux a b c \<le> e_aux a b c; c_aux a b c = b_aux b c a\<rbrakk> \<Longrightarrow> a_aux b c a \<sqinter> c_aux a b c = d_aux a b c
 2. d_aux a b c \<le> e_aux a b c \<Longrightarrow> c_aux a b c = b_aux b c a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>d_aux a b c \<le> e_aux a b c; c_aux a b c = b_aux b c a\<rbrakk> \<Longrightarrow> a_aux b c a \<sqinter> b_aux b c a = d_aux a b c
 2. d_aux a b c \<le> e_aux a b c \<Longrightarrow> c_aux a b c = b_aux b c a
[PROOF STEP]
apply (subst a_meet_b_eq_d)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>d_aux a b c \<le> e_aux a b c; c_aux a b c = b_aux b c a\<rbrakk> \<Longrightarrow> d_aux b c a \<le> e_aux b c a
 2. \<lbrakk>d_aux a b c \<le> e_aux a b c; c_aux a b c = b_aux b c a\<rbrakk> \<Longrightarrow> d_aux b c a = d_aux a b c
 3. d_aux a b c \<le> e_aux a b c \<Longrightarrow> c_aux a b c = b_aux b c a
[PROOF STEP]
by (simp_all add: c_aux_def b_aux_def d_b_c_a e_b_c_a)


[STATEMENT]
lemma c_meet_a_eq_d: "d_aux a b c \<le> e_aux a b c \<Longrightarrow> c_aux a b c \<sqinter> a_aux a b c = d_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> c_aux a b c \<sqinter> a_aux a b c = d_aux a b c
[PROOF STEP]
apply (subst c_a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux c a b \<sqinter> a_aux a b c = d_aux a b c
[PROOF STEP]
apply (subgoal_tac "a_aux a b c = b_aux c a b")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>d_aux a b c \<le> e_aux a b c; a_aux a b c = b_aux c a b\<rbrakk> \<Longrightarrow> a_aux c a b \<sqinter> a_aux a b c = d_aux a b c
 2. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c = b_aux c a b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>d_aux a b c \<le> e_aux a b c; a_aux a b c = b_aux c a b\<rbrakk> \<Longrightarrow> a_aux c a b \<sqinter> b_aux c a b = d_aux a b c
 2. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c = b_aux c a b
[PROOF STEP]
apply (subst a_meet_b_eq_d)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>d_aux a b c \<le> e_aux a b c; a_aux a b c = b_aux c a b\<rbrakk> \<Longrightarrow> d_aux c a b \<le> e_aux c a b
 2. \<lbrakk>d_aux a b c \<le> e_aux a b c; a_aux a b c = b_aux c a b\<rbrakk> \<Longrightarrow> d_aux c a b = d_aux a b c
 3. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c = b_aux c a b
[PROOF STEP]
by (simp_all add: a_aux_def b_aux_def d_b_c_a e_b_c_a)


[STATEMENT]
lemma a_def_equiv: "d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c = (a \<squnion> d_aux a b c) \<sqinter> e_aux a b c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a_aux a b c = (a \<squnion> d_aux a b c) \<sqinter> e_aux a b c
[PROOF STEP]
apply (simp add: a_aux_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> a \<sqinter> e_aux a b c \<squnion> d_aux a b c = (a \<squnion> d_aux a b c) \<sqinter> e_aux a b c
[PROOF STEP]
apply (subst inf_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> e_aux a b c \<sqinter> a \<squnion> d_aux a b c = (a \<squnion> d_aux a b c) \<sqinter> e_aux a b c
[PROOF STEP]
apply (subst sup_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> d_aux a b c \<squnion> e_aux a b c \<sqinter> a = (a \<squnion> d_aux a b c) \<sqinter> e_aux a b c
[PROOF STEP]
apply (simp add: modular)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_aux a b c \<le> e_aux a b c \<Longrightarrow> e_aux a b c \<sqinter> (d_aux a b c \<squnion> a) = (a \<squnion> d_aux a b c) \<sqinter> e_aux a b c
[PROOF STEP]
by (simp add: inf_commute sup_commute)