[STATEMENT]
lemma var_not_in_eval : "\<forall>var. \<forall>L. (freeIn var \<phi> \<longrightarrow> ((\<exists>x. eval \<phi> (list_update L var x)) = (\<forall>x. eval \<phi> (list_update L var x))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x]))
[PROOF STEP]
proof(induction \<phi>)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<forall>var L. freeIn var TrueF \<longrightarrow> (\<exists>x. eval TrueF (L[var := x])) = (\<forall>x. eval TrueF (L[var := x]))
 2. \<forall>var L. freeIn var FalseF \<longrightarrow> (\<exists>x. eval FalseF (L[var := x])) = (\<forall>x. eval FalseF (L[var := x]))
 3. \<And>x. \<forall>var L. freeIn var (fm.Atom x) \<longrightarrow> (\<exists>xa. eval (fm.Atom x) (L[var := xa])) = (\<forall>xa. eval (fm.Atom x) (L[var := xa]))
 4. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (And \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (And \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (And \<phi>1 \<phi>2) (L[var := x]))
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
 6. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 7. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 8. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 9. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 10. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
case TrueF
[PROOF STATE]
proof (state)
this:

goal (10 subgoals):
 1. \<forall>var L. freeIn var TrueF \<longrightarrow> (\<exists>x. eval TrueF (L[var := x])) = (\<forall>x. eval TrueF (L[var := x]))
 2. \<forall>var L. freeIn var FalseF \<longrightarrow> (\<exists>x. eval FalseF (L[var := x])) = (\<forall>x. eval FalseF (L[var := x]))
 3. \<And>x. \<forall>var L. freeIn var (fm.Atom x) \<longrightarrow> (\<exists>xa. eval (fm.Atom x) (L[var := xa])) = (\<forall>xa. eval (fm.Atom x) (L[var := xa]))
 4. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (And \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (And \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (And \<phi>1 \<phi>2) (L[var := x]))
 5. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
 6. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 7. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 8. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 9. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 10. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>var L. freeIn var TrueF \<longrightarrow> (\<exists>x. eval TrueF (L[var := x])) = (\<forall>x. eval TrueF (L[var := x]))
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var TrueF \<longrightarrow> (\<exists>x. eval TrueF (L[var := x])) = (\<forall>x. eval TrueF (L[var := x]))

goal (9 subgoals):
 1. \<forall>var L. freeIn var FalseF \<longrightarrow> (\<exists>x. eval FalseF (L[var := x])) = (\<forall>x. eval FalseF (L[var := x]))
 2. \<And>x. \<forall>var L. freeIn var (fm.Atom x) \<longrightarrow> (\<exists>xa. eval (fm.Atom x) (L[var := xa])) = (\<forall>xa. eval (fm.Atom x) (L[var := xa]))
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (And \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (And \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (And \<phi>1 \<phi>2) (L[var := x]))
 4. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
 5. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 6. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 7. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 8. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 9. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<forall>var L. freeIn var FalseF \<longrightarrow> (\<exists>x. eval FalseF (L[var := x])) = (\<forall>x. eval FalseF (L[var := x]))
 2. \<And>x. \<forall>var L. freeIn var (fm.Atom x) \<longrightarrow> (\<exists>xa. eval (fm.Atom x) (L[var := xa])) = (\<forall>xa. eval (fm.Atom x) (L[var := xa]))
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (And \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (And \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (And \<phi>1 \<phi>2) (L[var := x]))
 4. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
 5. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 6. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 7. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 8. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 9. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
case FalseF
[PROOF STATE]
proof (state)
this:

goal (9 subgoals):
 1. \<forall>var L. freeIn var FalseF \<longrightarrow> (\<exists>x. eval FalseF (L[var := x])) = (\<forall>x. eval FalseF (L[var := x]))
 2. \<And>x. \<forall>var L. freeIn var (fm.Atom x) \<longrightarrow> (\<exists>xa. eval (fm.Atom x) (L[var := xa])) = (\<forall>xa. eval (fm.Atom x) (L[var := xa]))
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (And \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (And \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (And \<phi>1 \<phi>2) (L[var := x]))
 4. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
 5. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 6. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 7. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 8. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 9. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>var L. freeIn var FalseF \<longrightarrow> (\<exists>x. eval FalseF (L[var := x])) = (\<forall>x. eval FalseF (L[var := x]))
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var FalseF \<longrightarrow> (\<exists>x. eval FalseF (L[var := x])) = (\<forall>x. eval FalseF (L[var := x]))

goal (8 subgoals):
 1. \<And>x. \<forall>var L. freeIn var (fm.Atom x) \<longrightarrow> (\<exists>xa. eval (fm.Atom x) (L[var := xa])) = (\<forall>xa. eval (fm.Atom x) (L[var := xa]))
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (And \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (And \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (And \<phi>1 \<phi>2) (L[var := x]))
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
 4. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 5. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 6. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 7. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 8. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>x. \<forall>var L. freeIn var (fm.Atom x) \<longrightarrow> (\<exists>xa. eval (fm.Atom x) (L[var := xa])) = (\<forall>xa. eval (fm.Atom x) (L[var := xa]))
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (And \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (And \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (And \<phi>1 \<phi>2) (L[var := x]))
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
 4. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 5. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 6. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 7. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 8. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
case (Atom x)
[PROOF STATE]
proof (state)
this:

goal (8 subgoals):
 1. \<And>x. \<forall>var L. freeIn var (fm.Atom x) \<longrightarrow> (\<exists>xa. eval (fm.Atom x) (L[var := xa])) = (\<forall>xa. eval (fm.Atom x) (L[var := xa]))
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (And \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (And \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (And \<phi>1 \<phi>2) (L[var := x]))
 3. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
 4. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 5. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 6. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 7. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 8. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>var L. freeIn var (fm.Atom x) \<longrightarrow> (\<exists>xa. eval (fm.Atom x) (L[var := xa])) = (\<forall>xa. eval (fm.Atom x) (L[var := xa]))
[PROOF STEP]
using var_not_in_aEval eval.simps(1)
[PROOF STATE]
proof (prove)
using this:
freeIn ?var (fm.Atom ?\<phi>) \<Longrightarrow> (\<exists>x. aEval ?\<phi> (?L[?var := x])) = (\<forall>x. aEval ?\<phi> (?L[?var := x]))
eval (fm.Atom ?a) ?\<Gamma> = aEval ?a ?\<Gamma>

goal (1 subgoal):
 1. \<forall>var L. freeIn var (fm.Atom x) \<longrightarrow> (\<exists>xa. eval (fm.Atom x) (L[var := xa])) = (\<forall>xa. eval (fm.Atom x) (L[var := xa]))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var (fm.Atom x) \<longrightarrow> (\<exists>xa. eval (fm.Atom x) (L[var := xa])) = (\<forall>xa. eval (fm.Atom x) (L[var := xa]))

goal (7 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (And \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (And \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (And \<phi>1 \<phi>2) (L[var := x]))
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
 3. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 4. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 5. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 6. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 7. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (And \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (And \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (And \<phi>1 \<phi>2) (L[var := x]))
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
 3. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 4. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 5. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 6. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 7. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
case (And \<phi>1 \<phi>2)
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x]))
\<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))

goal (7 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (And \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (And \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (And \<phi>1 \<phi>2) (L[var := x]))
 2. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
 3. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 4. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 5. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 6. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 7. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x]))
\<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x]))
\<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))

goal (1 subgoal):
 1. \<forall>var L. freeIn var (And \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (And \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (And \<phi>1 \<phi>2) (L[var := x]))
[PROOF STEP]
by (meson eval.simps(4) freeIn.simps(7))
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var (And \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (And \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (And \<phi>1 \<phi>2) (L[var := x]))

goal (6 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
 2. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 3. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 4. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 5. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 6. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
 2. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 3. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 4. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 5. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 6. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
case (Or \<phi>1 \<phi>2)
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x]))
\<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))

goal (6 subgoals):
 1. \<And>\<phi>1 \<phi>2. \<lbrakk>\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x])); \<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))\<rbrakk> \<Longrightarrow> \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
 2. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 3. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 4. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 5. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 6. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x]))
\<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>var L. freeIn var \<phi>1 \<longrightarrow> (\<exists>x. eval \<phi>1 (L[var := x])) = (\<forall>x. eval \<phi>1 (L[var := x]))
\<forall>var L. freeIn var \<phi>2 \<longrightarrow> (\<exists>x. eval \<phi>2 (L[var := x])) = (\<forall>x. eval \<phi>2 (L[var := x]))

goal (1 subgoal):
 1. \<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var (Or \<phi>1 \<phi>2) \<longrightarrow> (\<exists>x. eval (Or \<phi>1 \<phi>2) (L[var := x])) = (\<forall>x. eval (Or \<phi>1 \<phi>2) (L[var := x]))

goal (5 subgoals):
 1. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 2. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 3. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 4. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 5. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 2. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 3. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 4. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 5. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
case (Neg \<phi>)
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x]))

goal (5 subgoals):
 1. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
 2. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 3. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 4. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 5. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x]))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x]))

goal (1 subgoal):
 1. \<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))
[PROOF STEP]
by (meson eval.simps(6) freeIn.simps(9))
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var (Neg \<phi>) \<longrightarrow> (\<exists>x. eval (Neg \<phi>) (L[var := x])) = (\<forall>x. eval (Neg \<phi>) (L[var := x]))

goal (4 subgoals):
 1. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 2. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 3. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 4. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 2. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 3. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 4. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
case (ExQ \<phi>)
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x]))

goal (4 subgoals):
 1. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 2. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 3. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 4. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
fix xa L var x
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 2. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 3. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 4. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
have  "(xa::real) # L[var := x] = (xa#L)[var+1:=x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa # L[var := x] = (xa # L)[var + 1 := x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xa # L[var := x] = (xa # L)[var + 1 := x]

goal (4 subgoals):
 1. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
 2. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 3. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 4. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xa # L[var := x] = (xa # L)[var + 1 := x]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
xa # L[var := x] = (xa # L)[var + 1 := x]

goal (1 subgoal):
 1. \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
[PROOF STEP]
using ExQ
[PROOF STATE]
proof (prove)
using this:
xa # L[var := x] = (xa # L)[var + 1 := x]
\<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x]))

goal (1 subgoal):
 1. \<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))
[PROOF STEP]
by (metis Suc_eq_plus1 eval.simps(7) freeIn.simps(10) list_update_code(3))
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var (ExQ \<phi>) \<longrightarrow> (\<exists>x. eval (ExQ \<phi>) (L[var := x])) = (\<forall>x. eval (ExQ \<phi>) (L[var := x]))

goal (3 subgoals):
 1. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 2. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 3. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 2. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 3. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
case (AllQ \<phi>)
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x]))

goal (3 subgoals):
 1. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 2. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 3. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
fix xa L var x
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 2. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 3. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
have  "(xa::real) # L[var := x] = (xa#L)[var+1:=x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa # L[var := x] = (xa # L)[var + 1 := x]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xa # L[var := x] = (xa # L)[var + 1 := x]

goal (3 subgoals):
 1. \<And>\<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
 2. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 3. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xa # L[var := x] = (xa # L)[var + 1 := x]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
xa # L[var := x] = (xa # L)[var + 1 := x]

goal (1 subgoal):
 1. \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
[PROOF STEP]
using AllQ
[PROOF STATE]
proof (prove)
using this:
xa # L[var := x] = (xa # L)[var + 1 := x]
\<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x]))

goal (1 subgoal):
 1. \<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))
[PROOF STEP]
by (metis Suc_eq_plus1 eval.simps(8) freeIn.simps(11) list_update_code(3))
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var (AllQ \<phi>) \<longrightarrow> (\<exists>x. eval (AllQ \<phi>) (L[var := x])) = (\<forall>x. eval (AllQ \<phi>) (L[var := x]))

goal (2 subgoals):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 2. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 2. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
case (ExN i \<phi>)
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x]))

goal (2 subgoals):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 2. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x]))

goal (2 subgoals):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 2. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
fix xa L var x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 2. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
assume "length (xa::real list) = i"
[PROOF STATE]
proof (state)
this:
length xa = i

goal (2 subgoals):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 2. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
have  "xa @ L[var := x] = (xa@L)[var+i:=x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa @ L[var := x] = (xa @ L)[var + i := x]
[PROOF STEP]
by (simp add: \<open>length xa = i\<close> list_update_append)
[PROOF STATE]
proof (state)
this:
xa @ L[var := x] = (xa @ L)[var + i := x]

goal (2 subgoals):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 2. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
length ?xa2 = i \<Longrightarrow> ?xa2 @ ?L2[?var2 := ?x2] = (?xa2 @ ?L2)[?var2 + i := ?x2]

goal (2 subgoals):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (ExN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (ExN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (ExN x1 \<phi>) (L[var := x]))
 2. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length ?xa2 = i \<Longrightarrow> ?xa2 @ ?L2[?var2 := ?x2] = (?xa2 @ ?L2)[?var2 + i := ?x2]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length ?xa2 = i \<Longrightarrow> ?xa2 @ ?L2[?var2 := ?x2] = (?xa2 @ ?L2)[?var2 + i := ?x2]

goal (1 subgoal):
 1. \<forall>var L. freeIn var (ExN i \<phi>) \<longrightarrow> (\<exists>x. eval (ExN i \<phi>) (L[var := x])) = (\<forall>x. eval (ExN i \<phi>) (L[var := x]))
[PROOF STEP]
using ExN
[PROOF STATE]
proof (prove)
using this:
length ?xa2 = i \<Longrightarrow> ?xa2 @ ?L2[?var2 := ?x2] = (?xa2 @ ?L2)[?var2 + i := ?x2]
\<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x]))

goal (1 subgoal):
 1. \<forall>var L. freeIn var (ExN i \<phi>) \<longrightarrow> (\<exists>x. eval (ExN i \<phi>) (L[var := x])) = (\<forall>x. eval (ExN i \<phi>) (L[var := x]))
[PROOF STEP]
by (metis eval.simps(10) freeIn.simps(13))
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var (ExN i \<phi>) \<longrightarrow> (\<exists>x. eval (ExN i \<phi>) (L[var := x])) = (\<forall>x. eval (ExN i \<phi>) (L[var := x]))

goal (1 subgoal):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
case (AllN i \<phi>)
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x]))

goal (1 subgoal):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x]))

goal (1 subgoal):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
fix xa L var x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
assume "length (xa::real list) = i"
[PROOF STATE]
proof (state)
this:
length xa = i

goal (1 subgoal):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
have  "xa @ L[var := x] = (xa@L)[var+i:=x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xa @ L[var := x] = (xa @ L)[var + i := x]
[PROOF STEP]
by (simp add: \<open>length xa = i\<close> list_update_append)
[PROOF STATE]
proof (state)
this:
xa @ L[var := x] = (xa @ L)[var + i := x]

goal (1 subgoal):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
length ?xa2 = i \<Longrightarrow> ?xa2 @ ?L2[?var2 := ?x2] = (?xa2 @ ?L2)[?var2 + i := ?x2]

goal (1 subgoal):
 1. \<And>x1 \<phi>. \<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x])) \<Longrightarrow> \<forall>var L. freeIn var (AllN x1 \<phi>) \<longrightarrow> (\<exists>x. eval (AllN x1 \<phi>) (L[var := x])) = (\<forall>x. eval (AllN x1 \<phi>) (L[var := x]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length ?xa2 = i \<Longrightarrow> ?xa2 @ ?L2[?var2 := ?x2] = (?xa2 @ ?L2)[?var2 + i := ?x2]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length ?xa2 = i \<Longrightarrow> ?xa2 @ ?L2[?var2 := ?x2] = (?xa2 @ ?L2)[?var2 + i := ?x2]

goal (1 subgoal):
 1. \<forall>var L. freeIn var (AllN i \<phi>) \<longrightarrow> (\<exists>x. eval (AllN i \<phi>) (L[var := x])) = (\<forall>x. eval (AllN i \<phi>) (L[var := x]))
[PROOF STEP]
using AllN
[PROOF STATE]
proof (prove)
using this:
length ?xa2 = i \<Longrightarrow> ?xa2 @ ?L2[?var2 := ?x2] = (?xa2 @ ?L2)[?var2 + i := ?x2]
\<forall>var L. freeIn var \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (L[var := x])) = (\<forall>x. eval \<phi> (L[var := x]))

goal (1 subgoal):
 1. \<forall>var L. freeIn var (AllN i \<phi>) \<longrightarrow> (\<exists>x. eval (AllN i \<phi>) (L[var := x])) = (\<forall>x. eval (AllN i \<phi>) (L[var := x]))
[PROOF STEP]
by (metis eval.simps(9) freeIn.simps(12))
[PROOF STATE]
proof (state)
this:
\<forall>var L. freeIn var (AllN i \<phi>) \<longrightarrow> (\<exists>x. eval (AllN i \<phi>) (L[var := x])) = (\<forall>x. eval (AllN i \<phi>) (L[var := x]))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma var_not_in_eval2 : "\<forall>L. (freeIn 0 \<phi> \<longrightarrow> ((\<exists>x. eval \<phi> (x#L)) = (\<forall>x. eval \<phi> (x#L))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>L. freeIn 0 \<phi> \<longrightarrow> (\<exists>x. eval \<phi> (x # L)) = (\<forall>x. eval \<phi> (x # L))
[PROOF STEP]
by (metis list_update_code(2) var_not_in_eval)


[STATEMENT]
lemma var_not_in_eval3 :
  assumes "freeIn var \<phi>"
  assumes "length xs' = var"
  shows "((\<exists>x. eval \<phi> (xs'@x#L)) = (\<forall>x. eval \<phi> (xs'@x#L)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. eval \<phi> (xs' @ x # L)) = (\<forall>x. eval \<phi> (xs' @ x # L))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
freeIn var \<phi>
length xs' = var

goal (1 subgoal):
 1. (\<exists>x. eval \<phi> (xs' @ x # L)) = (\<forall>x. eval \<phi> (xs' @ x # L))
[PROOF STEP]
by (metis list_update_length var_not_in_eval)


[STATEMENT]
lemma eval_list_conj : "eval (list_conj F) L = (\<forall>f\<in>set(F). eval f L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (list_conj F) L = (\<forall>f\<in>set F. eval f L)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval (list_conj F) L = (\<forall>f\<in>set F. eval f L)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval (list_conj F) L = (\<forall>f\<in>set F. eval f L)
[PROOF STEP]
fix f F
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval (list_conj F) L = (\<forall>f\<in>set F. eval f L)
[PROOF STEP]
have h : "eval (foldr and F f) L = (eval f L \<and> (\<forall>f \<in> set F. eval f L))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (foldr PolyAtoms.and F f) L = (eval f L \<and> (\<forall>f\<in>set F. eval f L))
[PROOF STEP]
apply(induct F)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. eval (foldr PolyAtoms.and [] f) L = (eval f L \<and> (\<forall>f\<in>set []. eval f L))
 2. \<And>a F. eval (foldr PolyAtoms.and F f) L = (eval f L \<and> (\<forall>f\<in>set F. eval f L)) \<Longrightarrow> eval (foldr PolyAtoms.and (a # F) f) L = (eval f L \<and> (\<forall>f\<in>set (a # F). eval f L))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a F. eval (foldr PolyAtoms.and F f) L = (eval f L \<and> (\<forall>f\<in>set F. eval f L)) \<Longrightarrow> eval (foldr PolyAtoms.and (a # F) f) L = (eval f L \<and> (\<forall>f\<in>set (a # F). eval f L))
[PROOF STEP]
using eval_and
[PROOF STATE]
proof (prove)
using this:
eval (PolyAtoms.and ?a ?b) ?L = (eval ?a ?L \<and> eval ?b ?L)

goal (1 subgoal):
 1. \<And>a F. eval (foldr PolyAtoms.and F f) L = (eval f L \<and> (\<forall>f\<in>set F. eval f L)) \<Longrightarrow> eval (foldr PolyAtoms.and (a # F) f) L = (eval f L \<and> (\<forall>f\<in>set (a # F). eval f L))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (foldr PolyAtoms.and F f) L = (eval f L \<and> (\<forall>f\<in>set F. eval f L))

goal (1 subgoal):
 1. eval (list_conj F) L = (\<forall>f\<in>set F. eval f L)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
eval (foldr PolyAtoms.and ?Fa2 ?f2) L = (eval ?f2 L \<and> (\<forall>f\<in>set ?Fa2. eval f L))

goal (1 subgoal):
 1. eval (list_conj F) L = (\<forall>f\<in>set F. eval f L)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval (foldr PolyAtoms.and ?Fa2 ?f2) L = (eval ?f2 L \<and> (\<forall>f\<in>set ?Fa2. eval f L))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval (foldr PolyAtoms.and ?Fa2 ?f2) L = (eval ?f2 L \<and> (\<forall>f\<in>set ?Fa2. eval f L))

goal (1 subgoal):
 1. eval (list_conj F) L = (\<forall>f\<in>set F. eval f L)
[PROOF STEP]
by(simp add:list_conj_def)
[PROOF STATE]
proof (state)
this:
eval (list_conj F) L = (\<forall>f\<in>set F. eval f L)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval_list_disj : "eval (list_disj F) L = (\<exists>f\<in>set(F). eval f L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (list_disj F) L = (\<exists>f\<in>set F. eval f L)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval (list_disj F) L = (\<exists>f\<in>set F. eval f L)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval (list_disj F) L = (\<exists>f\<in>set F. eval f L)
[PROOF STEP]
fix f F
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval (list_disj F) L = (\<exists>f\<in>set F. eval f L)
[PROOF STEP]
have h : "eval (foldr or F f) L = (eval f L \<or> (\<exists>f \<in> set F. eval f L))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (foldr PolyAtoms.or F f) L = (eval f L \<or> (\<exists>f\<in>set F. eval f L))
[PROOF STEP]
apply(induct F)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. eval (foldr PolyAtoms.or [] f) L = (eval f L \<or> (\<exists>f\<in>set []. eval f L))
 2. \<And>a F. eval (foldr PolyAtoms.or F f) L = (eval f L \<or> (\<exists>f\<in>set F. eval f L)) \<Longrightarrow> eval (foldr PolyAtoms.or (a # F) f) L = (eval f L \<or> (\<exists>f\<in>set (a # F). eval f L))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a F. eval (foldr PolyAtoms.or F f) L = (eval f L \<or> (\<exists>f\<in>set F. eval f L)) \<Longrightarrow> eval (foldr PolyAtoms.or (a # F) f) L = (eval f L \<or> (\<exists>f\<in>set (a # F). eval f L))
[PROOF STEP]
using eval_or
[PROOF STATE]
proof (prove)
using this:
eval (PolyAtoms.or ?a ?b) ?L = (eval ?a ?L \<or> eval ?b ?L)

goal (1 subgoal):
 1. \<And>a F. eval (foldr PolyAtoms.or F f) L = (eval f L \<or> (\<exists>f\<in>set F. eval f L)) \<Longrightarrow> eval (foldr PolyAtoms.or (a # F) f) L = (eval f L \<or> (\<exists>f\<in>set (a # F). eval f L))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval (foldr PolyAtoms.or F f) L = (eval f L \<or> (\<exists>f\<in>set F. eval f L))

goal (1 subgoal):
 1. eval (list_disj F) L = (\<exists>f\<in>set F. eval f L)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
eval (foldr PolyAtoms.or ?Fa2 ?f2) L = (eval ?f2 L \<or> (\<exists>f\<in>set ?Fa2. eval f L))

goal (1 subgoal):
 1. eval (list_disj F) L = (\<exists>f\<in>set F. eval f L)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval (foldr PolyAtoms.or ?Fa2 ?f2) L = (eval ?f2 L \<or> (\<exists>f\<in>set ?Fa2. eval f L))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval (foldr PolyAtoms.or ?Fa2 ?f2) L = (eval ?f2 L \<or> (\<exists>f\<in>set ?Fa2. eval f L))

goal (1 subgoal):
 1. eval (list_disj F) L = (\<exists>f\<in>set F. eval f L)
[PROOF STEP]
by(simp add:list_disj_def)
[PROOF STATE]
proof (state)
this:
eval (list_disj F) L = (\<exists>f\<in>set F. eval f L)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma befaf: assumes "q\<in>set s" "distinct s"
shows "before q s \<union> {q} \<union> after q s = set s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. before q s \<union> {q} \<union> after q s = set s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. before q s \<union> {q} \<union> after q s = set s
[PROOF STEP]
have "before q s \<union> {y. index s y = index s q \<and> q \<in> set s}
      = {y. index s y \<le> index s q \<and> q \<in> set s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. before q s \<union> {y. index s y = index s q \<and> q \<in> set s} = {y. index s y \<le> index s q \<and> q \<in> set s}
[PROOF STEP]
unfolding before_in_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. index s y < index s q \<and> q \<in> set s} \<union> {y. index s y = index s q \<and> q \<in> set s} = {y. index s y \<le> index s q \<and> q \<in> set s}
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>index s x \<le> index s q; q \<in> set s; x \<noteq> q\<rbrakk> \<Longrightarrow> index s x < index s q
[PROOF STEP]
by (simp add: le_neq_implies_less)
[PROOF STATE]
proof (state)
this:
before q s \<union> {y. index s y = index s q \<and> q \<in> set s} = {y. index s y \<le> index s q \<and> q \<in> set s}

goal (1 subgoal):
 1. before q s \<union> {q} \<union> after q s = set s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
before q s \<union> {y. index s y = index s q \<and> q \<in> set s} = {y. index s y \<le> index s q \<and> q \<in> set s}

goal (1 subgoal):
 1. before q s \<union> {q} \<union> after q s = set s
[PROOF STEP]
have "\<dots> =  {y. index s y \<le> index s q \<and> y\<in> set s \<and> q \<in> set s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. index s y \<le> index s q \<and> q \<in> set s} = {y. index s y \<le> index s q \<and> y \<in> set s \<and> q \<in> set s}
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>index s x \<le> index s q; q \<in> set s\<rbrakk> \<Longrightarrow> x \<in> set s
[PROOF STEP]
by (metis index_conv_size_if_notin index_less_size_conv not_less)
[PROOF STATE]
proof (state)
this:
{y. index s y \<le> index s q \<and> q \<in> set s} = {y. index s y \<le> index s q \<and> y \<in> set s \<and> q \<in> set s}

goal (1 subgoal):
 1. before q s \<union> {q} \<union> after q s = set s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{y. index s y \<le> index s q \<and> q \<in> set s} = {y. index s y \<le> index s q \<and> y \<in> set s \<and> q \<in> set s}

goal (1 subgoal):
 1. before q s \<union> {q} \<union> after q s = set s
[PROOF STEP]
with \<open>q \<in> set s\<close>
[PROOF STATE]
proof (chain)
picking this:
q \<in> set s
{y. index s y \<le> index s q \<and> q \<in> set s} = {y. index s y \<le> index s q \<and> y \<in> set s \<and> q \<in> set s}
[PROOF STEP]
have "\<dots> = {y. index s y \<le> index s q \<and> y\<in> set s}"
[PROOF STATE]
proof (prove)
using this:
q \<in> set s
{y. index s y \<le> index s q \<and> q \<in> set s} = {y. index s y \<le> index s q \<and> y \<in> set s \<and> q \<in> set s}

goal (1 subgoal):
 1. {y. index s y \<le> index s q \<and> y \<in> set s \<and> q \<in> set s} = {y. index s y \<le> index s q \<and> y \<in> set s}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{y. index s y \<le> index s q \<and> y \<in> set s \<and> q \<in> set s} = {y. index s y \<le> index s q \<and> y \<in> set s}

goal (1 subgoal):
 1. before q s \<union> {q} \<union> after q s = set s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
before q s \<union> {y. index s y = index s q \<and> q \<in> set s} = {y. index s y \<le> index s q \<and> y \<in> set s}
[PROOF STEP]
have "before q s \<union> {y. index s y = index s q \<and> q \<in> set s} \<union> after q s
      = {y. index s y \<le> index s q \<and> y\<in> set s} \<union> {y. index s y > index s q \<and> y \<in> set s}"
[PROOF STATE]
proof (prove)
using this:
before q s \<union> {y. index s y = index s q \<and> q \<in> set s} = {y. index s y \<le> index s q \<and> y \<in> set s}

goal (1 subgoal):
 1. before q s \<union> {y. index s y = index s q \<and> q \<in> set s} \<union> after q s = {y. index s y \<le> index s q \<and> y \<in> set s} \<union> {y. index s q < index s y \<and> y \<in> set s}
[PROOF STEP]
unfolding before_in_def
[PROOF STATE]
proof (prove)
using this:
{y. index s y < index s q \<and> q \<in> set s} \<union> {y. index s y = index s q \<and> q \<in> set s} = {y. index s y \<le> index s q \<and> y \<in> set s}

goal (1 subgoal):
 1. {y. index s y < index s q \<and> q \<in> set s} \<union> {y. index s y = index s q \<and> q \<in> set s} \<union> {y. index s q < index s y \<and> y \<in> set s} = {y. index s y \<le> index s q \<and> y \<in> set s} \<union> {y. index s q < index s y \<and> y \<in> set s}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
before q s \<union> {y. index s y = index s q \<and> q \<in> set s} \<union> after q s = {y. index s y \<le> index s q \<and> y \<in> set s} \<union> {y. index s q < index s y \<and> y \<in> set s}

goal (1 subgoal):
 1. before q s \<union> {q} \<union> after q s = set s
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
before q s \<union> {y. index s y = index s q \<and> q \<in> set s} \<union> after q s = {y. index s y \<le> index s q \<and> y \<in> set s} \<union> {y. index s q < index s y \<and> y \<in> set s}

goal (1 subgoal):
 1. before q s \<union> {q} \<union> after q s = set s
[PROOF STEP]
have "\<dots> = set s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {y. index s y \<le> index s q \<and> y \<in> set s} \<union> {y. index s q < index s y \<and> y \<in> set s} = set s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{y. index s y \<le> index s q \<and> y \<in> set s} \<union> {y. index s q < index s y \<and> y \<in> set s} = set s

goal (1 subgoal):
 1. before q s \<union> {q} \<union> after q s = set s
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
before q s \<union> {y. index s y = index s q \<and> q \<in> set s} \<union> after q s = set s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
before q s \<union> {y. index s y = index s q \<and> q \<in> set s} \<union> after q s = set s

goal (1 subgoal):
 1. before q s \<union> {q} \<union> after q s = set s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
before q s \<union> {y. index s y = index s q \<and> q \<in> set s} \<union> after q s = set s
q \<in> set s
distinct s

goal (1 subgoal):
 1. before q s \<union> {q} \<union> after q s = set s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
before q s \<union> {q} \<union> after q s = set s

goal:
No subgoals!
[PROOF STEP]
qed