[STATEMENT]
lemma eval_neg_neg : "eval (neg (neg f)) L \<longleftrightarrow> eval f L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (neg (neg f)) L = eval f L
[PROOF STEP]
by (simp add: neg_def)


[STATEMENT]
lemma eval_neg : "(\<not> eval (neg f) L) \<longleftrightarrow> eval f L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> eval (neg f) L) = eval f L
[PROOF STEP]
by (simp add: neg_def)


[STATEMENT]
lemma eval_and : "eval (and a b) L \<longleftrightarrow> (eval a L \<and> eval b L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (PolyAtoms.and a b) L = (eval a L \<and> eval b L)
[PROOF STEP]
by (simp add: and_def)


[STATEMENT]
lemma eval_or : "eval (or a b) L \<longleftrightarrow> (eval a L \<or> eval b L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (PolyAtoms.or a b) L = (eval a L \<or> eval b L)
[PROOF STEP]
by (simp add: or_def)


[STATEMENT]
lemma eval_Or : "eval (Or a b) L \<longleftrightarrow> (eval a L \<or> eval b L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Or a b) L = (eval a L \<or> eval b L)
[PROOF STEP]
by (simp)


[STATEMENT]
lemma eval_And : "eval (And a b) L \<longleftrightarrow> (eval a L \<and> eval b L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (And a b) L = (eval a L \<and> eval b L)
[PROOF STEP]
by (simp)


[STATEMENT]
lemma eval_not : "eval (neg a) L \<longleftrightarrow> \<not>(eval a L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (neg a) L = (\<not> eval a L)
[PROOF STEP]
by (simp add: neg_def)


[STATEMENT]
lemma eval_true : "eval TrueF L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval TrueF L
[PROOF STEP]
by simp


[STATEMENT]
lemma eval_false : "\<not>(eval FalseF L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> eval FalseF L
[PROOF STEP]
by simp


[STATEMENT]
lemma eval_Neg : "eval (Neg \<phi>) L = eval (neg \<phi>) L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Neg \<phi>) L = eval (neg \<phi>) L
[PROOF STEP]
by (simp add: eval_not)


[STATEMENT]
lemma eval_Neg_Neg : "eval (Neg (Neg \<phi>)) L = eval \<phi> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Neg (Neg \<phi>)) L = eval \<phi> L
[PROOF STEP]
by (simp add: eval_not)


[STATEMENT]
lemma eval_Neg_And : "eval (Neg (And \<phi> \<psi>)) L = eval (Or (Neg \<phi>) (Neg \<psi>)) L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Neg (And \<phi> \<psi>)) L = eval (Or (Neg \<phi>) (Neg \<psi>)) L
[PROOF STEP]
by simp


[STATEMENT]
lemma aEval_leq : "aEval (Leq p) L = (aEval (Less p) L \<or> aEval (Eq p) L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aEval (Leq p) L = (aEval (Less p) L \<or> aEval (Eq p) L)
[PROOF STEP]
by auto


[STATEMENT]
lemma sum_eq : "eval (Atom(Eq p)) L \<longrightarrow> eval (Atom(Eq q)) L \<longrightarrow> eval (Atom(Eq(p + q))) L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (fm.Atom (Eq p)) L \<longrightarrow> eval (fm.Atom (Eq q)) L \<longrightarrow> eval (fm.Atom (Eq (p + q))) L
[PROOF STEP]
by (simp add: insertion_add)


[STATEMENT]
lemma freeIn_list_conj : "(\<forall>f\<in>set(F). freeIn var f) \<Longrightarrow> freeIn var (list_conj F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f\<in>set F. freeIn var f \<Longrightarrow> freeIn var (list_conj F)
[PROOF STEP]
proof(induct F)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Ball (set []) (freeIn var) \<Longrightarrow> freeIn var (list_conj [])
 2. \<And>a F. \<lbrakk>Ball (set F) (freeIn var) \<Longrightarrow> freeIn var (list_conj F); Ball (set (a # F)) (freeIn var)\<rbrakk> \<Longrightarrow> freeIn var (list_conj (a # F))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set []. freeIn var a

goal (2 subgoals):
 1. Ball (set []) (freeIn var) \<Longrightarrow> freeIn var (list_conj [])
 2. \<And>a F. \<lbrakk>Ball (set F) (freeIn var) \<Longrightarrow> freeIn var (list_conj F); Ball (set (a # F)) (freeIn var)\<rbrakk> \<Longrightarrow> freeIn var (list_conj (a # F))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set []. freeIn var a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set []. freeIn var a

goal (1 subgoal):
 1. freeIn var (list_conj [])
[PROOF STEP]
by(simp add: list_conj_def)
[PROOF STATE]
proof (state)
this:
freeIn var (list_conj [])

goal (1 subgoal):
 1. \<And>a F. \<lbrakk>Ball (set F) (freeIn var) \<Longrightarrow> freeIn var (list_conj F); Ball (set (a # F)) (freeIn var)\<rbrakk> \<Longrightarrow> freeIn var (list_conj (a # F))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a F. \<lbrakk>Ball (set F) (freeIn var) \<Longrightarrow> freeIn var (list_conj F); Ball (set (a # F)) (freeIn var)\<rbrakk> \<Longrightarrow> freeIn var (list_conj (a # F))
[PROOF STEP]
case (Cons a F)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set F. freeIn var a \<Longrightarrow> freeIn var (list_conj F)
\<forall>a\<in>set (a # F). freeIn var a

goal (1 subgoal):
 1. \<And>a F. \<lbrakk>Ball (set F) (freeIn var) \<Longrightarrow> freeIn var (list_conj F); Ball (set (a # F)) (freeIn var)\<rbrakk> \<Longrightarrow> freeIn var (list_conj (a # F))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set F. freeIn var a \<Longrightarrow> freeIn var (list_conj F)
\<forall>a\<in>set (a # F). freeIn var a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set F. freeIn var a \<Longrightarrow> freeIn var (list_conj F)
\<forall>a\<in>set (a # F). freeIn var a

goal (1 subgoal):
 1. freeIn var (list_conj (a # F))
[PROOF STEP]
by (simp add: PolyAtoms.and_def list_conj_def)
[PROOF STATE]
proof (state)
this:
freeIn var (list_conj (a # F))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma freeIn_list_disj :
  assumes "\<forall>f\<in>set (L::atom fm list). freeIn var f"
  shows "freeIn var (list_disj L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (list_disj L)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>f\<in>set L. freeIn var f

goal (1 subgoal):
 1. freeIn var (list_disj L)
[PROOF STEP]
proof(induction L)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Ball (set []) (freeIn var) \<Longrightarrow> freeIn var (list_disj [])
 2. \<And>a L. \<lbrakk>Ball (set L) (freeIn var) \<Longrightarrow> freeIn var (list_disj L); Ball (set (a # L)) (freeIn var)\<rbrakk> \<Longrightarrow> freeIn var (list_disj (a # L))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set []. freeIn var a

goal (2 subgoals):
 1. Ball (set []) (freeIn var) \<Longrightarrow> freeIn var (list_disj [])
 2. \<And>a L. \<lbrakk>Ball (set L) (freeIn var) \<Longrightarrow> freeIn var (list_disj L); Ball (set (a # L)) (freeIn var)\<rbrakk> \<Longrightarrow> freeIn var (list_disj (a # L))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set []. freeIn var a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set []. freeIn var a

goal (1 subgoal):
 1. freeIn var (list_disj [])
[PROOF STEP]
unfolding list_disj_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set []. freeIn var a

goal (1 subgoal):
 1. freeIn var (foldr PolyAtoms.or [] FalseF)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
freeIn var (list_disj [])

goal (1 subgoal):
 1. \<And>a L. \<lbrakk>Ball (set L) (freeIn var) \<Longrightarrow> freeIn var (list_disj L); Ball (set (a # L)) (freeIn var)\<rbrakk> \<Longrightarrow> freeIn var (list_disj (a # L))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a L. \<lbrakk>Ball (set L) (freeIn var) \<Longrightarrow> freeIn var (list_disj L); Ball (set (a # L)) (freeIn var)\<rbrakk> \<Longrightarrow> freeIn var (list_disj (a # L))
[PROOF STEP]
case (Cons a L)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set L. freeIn var a \<Longrightarrow> freeIn var (list_disj L)
\<forall>a\<in>set (a # L). freeIn var a

goal (1 subgoal):
 1. \<And>a L. \<lbrakk>Ball (set L) (freeIn var) \<Longrightarrow> freeIn var (list_disj L); Ball (set (a # L)) (freeIn var)\<rbrakk> \<Longrightarrow> freeIn var (list_disj (a # L))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set L. freeIn var a \<Longrightarrow> freeIn var (list_disj L)
\<forall>a\<in>set (a # L). freeIn var a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set L. freeIn var a \<Longrightarrow> freeIn var (list_disj L)
\<forall>a\<in>set (a # L). freeIn var a

goal (1 subgoal):
 1. freeIn var (list_disj (a # L))
[PROOF STEP]
unfolding list_disj_def or_def
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set L. freeIn var a \<Longrightarrow> freeIn var (foldr (\<lambda>\<phi>\<^sub>1 \<phi>\<^sub>2. if \<phi>\<^sub>1 = FalseF then \<phi>\<^sub>2 else if \<phi>\<^sub>2 = FalseF then \<phi>\<^sub>1 else if \<phi>\<^sub>1 = TrueF \<or> \<phi>\<^sub>2 = TrueF then TrueF else Or \<phi>\<^sub>1 \<phi>\<^sub>2) L FalseF)
\<forall>a\<in>set (a # L). freeIn var a

goal (1 subgoal):
 1. freeIn var (foldr (\<lambda>\<phi>\<^sub>1 \<phi>\<^sub>2. if \<phi>\<^sub>1 = FalseF then \<phi>\<^sub>2 else if \<phi>\<^sub>2 = FalseF then \<phi>\<^sub>1 else if \<phi>\<^sub>1 = TrueF \<or> \<phi>\<^sub>2 = TrueF then TrueF else Or \<phi>\<^sub>1 \<phi>\<^sub>2) (a # L) FalseF)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
freeIn var (list_disj (a # L))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma var_not_in_aEval : "freeIn var (Atom \<phi>) \<Longrightarrow> (\<exists>x. aEval \<phi> (list_update L var x)) = (\<forall>x. aEval \<phi> (list_update L var x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn var (fm.Atom \<phi>) \<Longrightarrow> (\<exists>x. aEval \<phi> (L[var := x])) = (\<forall>x. aEval \<phi> (L[var := x]))
[PROOF STEP]
proof(induction \<phi>)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x. freeIn var (fm.Atom (Less x)) \<Longrightarrow> (\<exists>xa. aEval (Less x) (L[var := xa])) = (\<forall>xa. aEval (Less x) (L[var := xa]))
 2. \<And>x. freeIn var (fm.Atom (Eq x)) \<Longrightarrow> (\<exists>xa. aEval (Eq x) (L[var := xa])) = (\<forall>xa. aEval (Eq x) (L[var := xa]))
 3. \<And>x. freeIn var (fm.Atom (Leq x)) \<Longrightarrow> (\<exists>xa. aEval (Leq x) (L[var := xa])) = (\<forall>xa. aEval (Leq x) (L[var := xa]))
 4. \<And>x. freeIn var (fm.Atom (Neq x)) \<Longrightarrow> (\<exists>xa. aEval (Neq x) (L[var := xa])) = (\<forall>xa. aEval (Neq x) (L[var := xa]))
[PROOF STEP]
case (Less p)
[PROOF STATE]
proof (state)
this:
freeIn var (fm.Atom (Less p))

goal (4 subgoals):
 1. \<And>x. freeIn var (fm.Atom (Less x)) \<Longrightarrow> (\<exists>xa. aEval (Less x) (L[var := xa])) = (\<forall>xa. aEval (Less x) (L[var := xa]))
 2. \<And>x. freeIn var (fm.Atom (Eq x)) \<Longrightarrow> (\<exists>xa. aEval (Eq x) (L[var := xa])) = (\<forall>xa. aEval (Eq x) (L[var := xa]))
 3. \<And>x. freeIn var (fm.Atom (Leq x)) \<Longrightarrow> (\<exists>xa. aEval (Leq x) (L[var := xa])) = (\<forall>xa. aEval (Leq x) (L[var := xa]))
 4. \<And>x. freeIn var (fm.Atom (Neq x)) \<Longrightarrow> (\<exists>xa. aEval (Neq x) (L[var := xa])) = (\<forall>xa. aEval (Neq x) (L[var := xa]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
freeIn var (fm.Atom (Less p))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
freeIn var (fm.Atom (Less p))

goal (1 subgoal):
 1. (\<exists>x. aEval (Less p) (L[var := x])) = (\<forall>x. aEval (Less p) (L[var := x]))
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>var \<notin> vars p; insertion (nth_default 0 (L[var := x])) p < 0\<rbrakk> \<Longrightarrow> insertion (nth_default 0 (L[var := xa])) p < 0
[PROOF STEP]
using not_contains_insertion
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?var \<notin> vars ?p; insertion (nth_default 0 (?L[?var := ?x])) ?p = ?val\<rbrakk> \<Longrightarrow> insertion (nth_default 0 (?L[?var := ?y])) ?p = ?val

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>var \<notin> vars p; insertion (nth_default 0 (L[var := x])) p < 0\<rbrakk> \<Longrightarrow> insertion (nth_default 0 (L[var := xa])) p < 0
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<exists>x. aEval (Less p) (L[var := x])) = (\<forall>x. aEval (Less p) (L[var := x]))

goal (3 subgoals):
 1. \<And>x. freeIn var (fm.Atom (Eq x)) \<Longrightarrow> (\<exists>xa. aEval (Eq x) (L[var := xa])) = (\<forall>xa. aEval (Eq x) (L[var := xa]))
 2. \<And>x. freeIn var (fm.Atom (Leq x)) \<Longrightarrow> (\<exists>xa. aEval (Leq x) (L[var := xa])) = (\<forall>xa. aEval (Leq x) (L[var := xa]))
 3. \<And>x. freeIn var (fm.Atom (Neq x)) \<Longrightarrow> (\<exists>xa. aEval (Neq x) (L[var := xa])) = (\<forall>xa. aEval (Neq x) (L[var := xa]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. freeIn var (fm.Atom (Eq x)) \<Longrightarrow> (\<exists>xa. aEval (Eq x) (L[var := xa])) = (\<forall>xa. aEval (Eq x) (L[var := xa]))
 2. \<And>x. freeIn var (fm.Atom (Leq x)) \<Longrightarrow> (\<exists>xa. aEval (Leq x) (L[var := xa])) = (\<forall>xa. aEval (Leq x) (L[var := xa]))
 3. \<And>x. freeIn var (fm.Atom (Neq x)) \<Longrightarrow> (\<exists>xa. aEval (Neq x) (L[var := xa])) = (\<forall>xa. aEval (Neq x) (L[var := xa]))
[PROOF STEP]
case (Eq p)
[PROOF STATE]
proof (state)
this:
freeIn var (fm.Atom (Eq p))

goal (3 subgoals):
 1. \<And>x. freeIn var (fm.Atom (Eq x)) \<Longrightarrow> (\<exists>xa. aEval (Eq x) (L[var := xa])) = (\<forall>xa. aEval (Eq x) (L[var := xa]))
 2. \<And>x. freeIn var (fm.Atom (Leq x)) \<Longrightarrow> (\<exists>xa. aEval (Leq x) (L[var := xa])) = (\<forall>xa. aEval (Leq x) (L[var := xa]))
 3. \<And>x. freeIn var (fm.Atom (Neq x)) \<Longrightarrow> (\<exists>xa. aEval (Neq x) (L[var := xa])) = (\<forall>xa. aEval (Neq x) (L[var := xa]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
freeIn var (fm.Atom (Eq p))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
freeIn var (fm.Atom (Eq p))

goal (1 subgoal):
 1. (\<exists>x. aEval (Eq p) (L[var := x])) = (\<forall>x. aEval (Eq p) (L[var := x]))
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>var \<notin> vars p; insertion (nth_default 0 (L[var := x])) p = 0\<rbrakk> \<Longrightarrow> insertion (nth_default 0 (L[var := xa])) p = 0
[PROOF STEP]
using not_contains_insertion
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?var \<notin> vars ?p; insertion (nth_default 0 (?L[?var := ?x])) ?p = ?val\<rbrakk> \<Longrightarrow> insertion (nth_default 0 (?L[?var := ?y])) ?p = ?val

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>var \<notin> vars p; insertion (nth_default 0 (L[var := x])) p = 0\<rbrakk> \<Longrightarrow> insertion (nth_default 0 (L[var := xa])) p = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>x. aEval (Eq p) (L[var := x])) = (\<forall>x. aEval (Eq p) (L[var := x]))

goal (2 subgoals):
 1. \<And>x. freeIn var (fm.Atom (Leq x)) \<Longrightarrow> (\<exists>xa. aEval (Leq x) (L[var := xa])) = (\<forall>xa. aEval (Leq x) (L[var := xa]))
 2. \<And>x. freeIn var (fm.Atom (Neq x)) \<Longrightarrow> (\<exists>xa. aEval (Neq x) (L[var := xa])) = (\<forall>xa. aEval (Neq x) (L[var := xa]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. freeIn var (fm.Atom (Leq x)) \<Longrightarrow> (\<exists>xa. aEval (Leq x) (L[var := xa])) = (\<forall>xa. aEval (Leq x) (L[var := xa]))
 2. \<And>x. freeIn var (fm.Atom (Neq x)) \<Longrightarrow> (\<exists>xa. aEval (Neq x) (L[var := xa])) = (\<forall>xa. aEval (Neq x) (L[var := xa]))
[PROOF STEP]
case (Leq p)
[PROOF STATE]
proof (state)
this:
freeIn var (fm.Atom (Leq p))

goal (2 subgoals):
 1. \<And>x. freeIn var (fm.Atom (Leq x)) \<Longrightarrow> (\<exists>xa. aEval (Leq x) (L[var := xa])) = (\<forall>xa. aEval (Leq x) (L[var := xa]))
 2. \<And>x. freeIn var (fm.Atom (Neq x)) \<Longrightarrow> (\<exists>xa. aEval (Neq x) (L[var := xa])) = (\<forall>xa. aEval (Neq x) (L[var := xa]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
freeIn var (fm.Atom (Leq p))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
freeIn var (fm.Atom (Leq p))

goal (1 subgoal):
 1. (\<exists>x. aEval (Leq p) (L[var := x])) = (\<forall>x. aEval (Leq p) (L[var := x]))
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>var \<notin> vars p; insertion (nth_default 0 (L[var := x])) p \<le> 0\<rbrakk> \<Longrightarrow> insertion (nth_default 0 (L[var := xa])) p \<le> 0
[PROOF STEP]
using not_contains_insertion
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?var \<notin> vars ?p; insertion (nth_default 0 (?L[?var := ?x])) ?p = ?val\<rbrakk> \<Longrightarrow> insertion (nth_default 0 (?L[?var := ?y])) ?p = ?val

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>var \<notin> vars p; insertion (nth_default 0 (L[var := x])) p \<le> 0\<rbrakk> \<Longrightarrow> insertion (nth_default 0 (L[var := xa])) p \<le> 0
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<exists>x. aEval (Leq p) (L[var := x])) = (\<forall>x. aEval (Leq p) (L[var := x]))

goal (1 subgoal):
 1. \<And>x. freeIn var (fm.Atom (Neq x)) \<Longrightarrow> (\<exists>xa. aEval (Neq x) (L[var := xa])) = (\<forall>xa. aEval (Neq x) (L[var := xa]))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. freeIn var (fm.Atom (Neq x)) \<Longrightarrow> (\<exists>xa. aEval (Neq x) (L[var := xa])) = (\<forall>xa. aEval (Neq x) (L[var := xa]))
[PROOF STEP]
case (Neq p)
[PROOF STATE]
proof (state)
this:
freeIn var (fm.Atom (Neq p))

goal (1 subgoal):
 1. \<And>x. freeIn var (fm.Atom (Neq x)) \<Longrightarrow> (\<exists>xa. aEval (Neq x) (L[var := xa])) = (\<forall>xa. aEval (Neq x) (L[var := xa]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
freeIn var (fm.Atom (Neq p))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
freeIn var (fm.Atom (Neq p))

goal (1 subgoal):
 1. (\<exists>x. aEval (Neq p) (L[var := x])) = (\<forall>x. aEval (Neq p) (L[var := x]))
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>var \<notin> vars p; insertion (nth_default 0 (L[var := x])) p \<noteq> 0; insertion (nth_default 0 (L[var := xa])) p = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
using not_contains_insertion
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?var \<notin> vars ?p; insertion (nth_default 0 (?L[?var := ?x])) ?p = ?val\<rbrakk> \<Longrightarrow> insertion (nth_default 0 (?L[?var := ?y])) ?p = ?val

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>var \<notin> vars p; insertion (nth_default 0 (L[var := x])) p \<noteq> 0; insertion (nth_default 0 (L[var := xa])) p = 0\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<exists>x. aEval (Neq p) (L[var := x])) = (\<forall>x. aEval (Neq p) (L[var := x]))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma var_not_in_aEval2 : "freeIn 0 (Atom \<phi>) \<Longrightarrow> (\<exists>x. aEval \<phi> (x#L)) = (\<forall>x. aEval \<phi> (x#L))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. freeIn 0 (fm.Atom \<phi>) \<Longrightarrow> (\<exists>x. aEval \<phi> (x # L)) = (\<forall>x. aEval \<phi> (x # L))
[PROOF STEP]
by (metis list_update_code(2) var_not_in_aEval)


[STATEMENT]
lemma plugInLinear :
  assumes lLength : "length L>var"
  assumes nonzero : "B\<noteq>0"
  assumes hb : "\<forall>v. insertion (nth_default 0 (list_update L var v)) b = B"
  assumes hc : "\<forall>v. insertion (nth_default 0 (list_update L var v)) c = C"
  shows "aEval (Eq(b*Var var + c)) (list_update L var (-C/B))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aEval (Eq (b * Var var + c)) (L[var := - C / B])
[PROOF STEP]
by(simp add: lLength insertion_add insertion_mult nonzero hb hc insertion_var)


[STATEMENT]
lemma doubleExist : "eval (ExN 2 A) L = eval (ExQ (ExQ A)) L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (ExN 2 A) L = eval (ExQ (ExQ A)) L
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>l. length l = 2 \<and> eval A (l @ L)) = (\<exists>x xa. eval A (xa # x # L))
[PROOF STEP]
proof(safe)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>length l = 2; eval A (l @ L)\<rbrakk> \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
 2. \<And>x xa. eval A (xa # x # L) \<Longrightarrow> \<exists>l. length l = 2 \<and> eval A (l @ L)
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>length l = 2; eval A (l @ L)\<rbrakk> \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
 2. \<And>x xa. eval A (xa # x # L) \<Longrightarrow> \<exists>l. length l = 2 \<and> eval A (l @ L)
[PROOF STEP]
assume h : "length l = 2" "eval A (l @ L)"
[PROOF STATE]
proof (state)
this:
length l = 2
eval A (l @ L)

goal (2 subgoals):
 1. \<And>l. \<lbrakk>length l = 2; eval A (l @ L)\<rbrakk> \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
 2. \<And>x xa. eval A (xa # x # L) \<Longrightarrow> \<exists>l. length l = 2 \<and> eval A (l @ L)
[PROOF STEP]
show "\<exists>x xa. eval A (xa # x # L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
proof(cases l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l = [] \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
 2. \<And>a list. l = a # list \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
l = []

goal (2 subgoals):
 1. l = [] \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
 2. \<And>a list. l = a # list \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l = []

goal (1 subgoal):
 1. \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
l = []
length l = 2
eval A (l @ L)

goal (1 subgoal):
 1. \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x xa. eval A (xa # x # L)

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
case (Cons a list)
[PROOF STATE]
proof (state)
this:
l = a # list

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = a # list
[PROOF STEP]
have Cons' : "l = a # list"
[PROOF STATE]
proof (prove)
using this:
l = a # list

goal (1 subgoal):
 1. l = a # list
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = a # list

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = a # list
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l = a # list

goal (1 subgoal):
 1. \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
proof(cases list)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>l = a # list; list = []\<rbrakk> \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
 2. \<And>aa lista. \<lbrakk>l = a # list; list = aa # lista\<rbrakk> \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
list = []

goal (2 subgoals):
 1. \<lbrakk>l = a # list; list = []\<rbrakk> \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
 2. \<And>aa lista. \<lbrakk>l = a # list; list = aa # lista\<rbrakk> \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list = []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
list = []

goal (1 subgoal):
 1. \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
using h Cons
[PROOF STATE]
proof (prove)
using this:
list = []
length l = 2
eval A (l @ L)
l = a # list

goal (1 subgoal):
 1. \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x xa. eval A (xa # x # L)

goal (1 subgoal):
 1. \<And>aa lista. \<lbrakk>l = a # list; list = aa # lista\<rbrakk> \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa lista. \<lbrakk>l = a # list; list = aa # lista\<rbrakk> \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
case (Cons b list)
[PROOF STATE]
proof (state)
this:
list__ = b # list

goal (1 subgoal):
 1. \<And>aa lista. \<lbrakk>l = a # list__; list__ = aa # lista\<rbrakk> \<Longrightarrow> \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x xa. eval A (xa # x # L)
[PROOF STEP]
apply(rule exI[where x=b])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>xa. eval A (xa # b # L)
[PROOF STEP]
apply(rule exI[where x=a])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval A (a # b # L)
[PROOF STEP]
using h Cons' Cons
[PROOF STATE]
proof (prove)
using this:
length l = 2
eval A (l @ L)
l = a # list__
list__ = b # list

goal (1 subgoal):
 1. eval A (a # b # L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x xa. eval A (xa # x # L)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x xa. eval A (xa # x # L)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x xa. eval A (xa # x # L)

goal (1 subgoal):
 1. \<And>x xa. eval A (xa # x # L) \<Longrightarrow> \<exists>l. length l = 2 \<and> eval A (l @ L)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. eval A (xa # x # L) \<Longrightarrow> \<exists>l. length l = 2 \<and> eval A (l @ L)
[PROOF STEP]
fix x xa
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. eval A (xa # x # L) \<Longrightarrow> \<exists>l. length l = 2 \<and> eval A (l @ L)
[PROOF STEP]
assume h : "eval A (xa # x # L)"
[PROOF STATE]
proof (state)
this:
eval A (xa # x # L)

goal (1 subgoal):
 1. \<And>x xa. eval A (xa # x # L) \<Longrightarrow> \<exists>l. length l = 2 \<and> eval A (l @ L)
[PROOF STEP]
show "\<exists>l. length l = 2 \<and> eval A (l @ L)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l. length l = 2 \<and> eval A (l @ L)
[PROOF STEP]
apply(rule exI[where x="[xa,x]"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length [xa, x] = 2 \<and> eval A ([xa, x] @ L)
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
eval A (xa # x # L)

goal (1 subgoal):
 1. length [xa, x] = 2 \<and> eval A ([xa, x] @ L)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>l. length l = 2 \<and> eval A (l @ L)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma doubleForall : "eval (AllN 2 A) L = eval (AllQ (AllQ A)) L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (AllN 2 A) L = eval (AllQ (AllQ A)) L
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>l. length l = 2 \<longrightarrow> eval A (l @ L)) = (\<forall>x xa. eval A (xa # x # L))
[PROOF STEP]
using doubleExist eval_neg
[PROOF STATE]
proof (prove)
using this:
eval (ExN 2 ?A) ?L = eval (ExQ (ExQ ?A)) ?L
(\<not> eval (neg ?f) ?L) = eval ?f ?L

goal (1 subgoal):
 1. (\<forall>l. length l = 2 \<longrightarrow> eval A (l @ L)) = (\<forall>x xa. eval A (xa # x # L))
[PROOF STEP]
by fastforce


[STATEMENT]
lemma unwrapExist : "eval (ExN (j + 1) A) L = eval (ExQ (ExN j A)) L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (ExN (j + 1) A) L = eval (ExQ (ExN j A)) L
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>l. length l = Suc j \<and> eval A (l @ L)) = (\<exists>x l. length l = j \<and> eval A (l @ x # L))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>length l = Suc j; eval A (l @ L)\<rbrakk> \<Longrightarrow> \<exists>x l. length l = j \<and> eval A (l @ x # L)
 2. \<And>x l. \<lbrakk>eval A (l @ x # L); j = length l\<rbrakk> \<Longrightarrow> \<exists>la. length la = Suc (length l) \<and> eval A (la @ L)
[PROOF STEP]
subgoal for l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length l = Suc j; eval A (l @ L)\<rbrakk> \<Longrightarrow> \<exists>x l. length l = j \<and> eval A (l @ x # L)
[PROOF STEP]
apply(rule exI[where x="nth l j"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length l = Suc j; eval A (l @ L)\<rbrakk> \<Longrightarrow> \<exists>la. length la = j \<and> eval A (la @ l ! j # L)
[PROOF STEP]
apply(rule exI[where x="take j l"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length l = Suc j; eval A (l @ L)\<rbrakk> \<Longrightarrow> length (take j l) = j \<and> eval A (take j l @ l ! j # L)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length l = Suc j; eval A (l @ L)\<rbrakk> \<Longrightarrow> eval A (take j l @ l ! j # L)
[PROOF STEP]
by (metis Cons_nth_drop_Suc append.assoc append_Cons append_eq_append_conv_if append_take_drop_id lessI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x l. \<lbrakk>eval A (l @ x # L); j = length l\<rbrakk> \<Longrightarrow> \<exists>la. length la = Suc (length l) \<and> eval A (la @ L)
[PROOF STEP]
subgoal for x l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eval A (l @ x # L); j = length l\<rbrakk> \<Longrightarrow> \<exists>la. length la = Suc (length l) \<and> eval A (la @ L)
[PROOF STEP]
apply(rule exI[where x="l @ [x]"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eval A (l @ x # L); j = length l\<rbrakk> \<Longrightarrow> length (l @ [x]) = Suc (length l) \<and> eval A ((l @ [x]) @ L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma unwrapExist' : "eval (ExN (j + 1) A) L =  eval (ExN j (ExQ A)) L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (ExN (j + 1) A) L = eval (ExN j (ExQ A)) L
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>l. length l = Suc j \<and> eval A (l @ L)) = (\<exists>l. length l = j \<and> (\<exists>x. eval A (x # l @ L)))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>length l = Suc j; eval A (l @ L)\<rbrakk> \<Longrightarrow> \<exists>l. length l = j \<and> (\<exists>x. eval A (x # l @ L))
 2. \<And>l x. \<lbrakk>j = length l; eval A (x # l @ L)\<rbrakk> \<Longrightarrow> \<exists>la. length la = Suc (length l) \<and> eval A (la @ L)
[PROOF STEP]
subgoal for l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length l = Suc j; eval A (l @ L)\<rbrakk> \<Longrightarrow> \<exists>l. length l = j \<and> (\<exists>x. eval A (x # l @ L))
[PROOF STEP]
apply(rule exI[where x="drop 1 l"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length l = Suc j; eval A (l @ L)\<rbrakk> \<Longrightarrow> length (drop 1 l) = j \<and> (\<exists>x. eval A (x # drop 1 l @ L))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length l = Suc j; eval A (l @ L)\<rbrakk> \<Longrightarrow> \<exists>x. eval A (x # drop (Suc 0) l @ L)
[PROOF STEP]
apply(rule exI[where x="nth l 0"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length l = Suc j; eval A (l @ L)\<rbrakk> \<Longrightarrow> eval A (l ! 0 # drop (Suc 0) l @ L)
[PROOF STEP]
by (metis Cons_nth_drop_Suc append_Cons drop0 zero_less_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l x. \<lbrakk>j = length l; eval A (x # l @ L)\<rbrakk> \<Longrightarrow> \<exists>la. length la = Suc (length l) \<and> eval A (la @ L)
[PROOF STEP]
subgoal for l x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j = length l; eval A (x # l @ L)\<rbrakk> \<Longrightarrow> \<exists>la. length la = Suc (length l) \<and> eval A (la @ L)
[PROOF STEP]
apply(rule exI[where x="x#l"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j = length l; eval A (x # l @ L)\<rbrakk> \<Longrightarrow> length (x # l) = Suc (length l) \<and> eval A ((x # l) @ L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma unwrapExist'' : "eval (ExN (i + j) A) L = eval (ExN i(ExN j A)) L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (ExN (i + j) A) L = eval (ExN i (ExN j A)) L
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>l. length l = i + j \<and> eval A (l @ L)) = (\<exists>l. length l = i \<and> (\<exists>la. length la = j \<and> eval A (la @ l @ L)))
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>length l = i + j; eval A (l @ L)\<rbrakk> \<Longrightarrow> \<exists>l. length l = i \<and> (\<exists>la. length la = j \<and> eval A (la @ l @ L))
 2. \<And>l la. \<lbrakk>i = length l; eval A (la @ l @ L); j = length la\<rbrakk> \<Longrightarrow> \<exists>lb. length lb = length l + length la \<and> eval A (lb @ L)
[PROOF STEP]
subgoal for l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length l = i + j; eval A (l @ L)\<rbrakk> \<Longrightarrow> \<exists>l. length l = i \<and> (\<exists>la. length la = j \<and> eval A (la @ l @ L))
[PROOF STEP]
apply(rule exI[where x="drop j l"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length l = i + j; eval A (l @ L)\<rbrakk> \<Longrightarrow> length (drop j l) = i \<and> (\<exists>la. length la = j \<and> eval A (la @ drop j l @ L))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length l = i + j; eval A (l @ L)\<rbrakk> \<Longrightarrow> \<exists>la. length la = j \<and> eval A (la @ drop j l @ L)
[PROOF STEP]
apply(rule exI[where x="take j l"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length l = i + j; eval A (l @ L)\<rbrakk> \<Longrightarrow> length (take j l) = j \<and> eval A (take j l @ drop j l @ L)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length l = i + j; eval A (l @ L)\<rbrakk> \<Longrightarrow> eval A (take j l @ drop j l @ L)
[PROOF STEP]
by (metis append.assoc append_take_drop_id)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l la. \<lbrakk>i = length l; eval A (la @ l @ L); j = length la\<rbrakk> \<Longrightarrow> \<exists>lb. length lb = length l + length la \<and> eval A (lb @ L)
[PROOF STEP]
subgoal for l la
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = length l; eval A (la @ l @ L); j = length la\<rbrakk> \<Longrightarrow> \<exists>lb. length lb = length l + length la \<and> eval A (lb @ L)
[PROOF STEP]
apply(rule exI[where x="la@l"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = length l; eval A (la @ l @ L); j = length la\<rbrakk> \<Longrightarrow> length (la @ l) = length l + length la \<and> eval A ((la @ l) @ L)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma unwrapForall : "eval (AllN (j + 1) A) L = eval (AllQ (AllN j A)) L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (AllN (j + 1) A) L = eval (AllQ (AllN j A)) L
[PROOF STEP]
using unwrapExist[of j "neg A" L] eval_neg
[PROOF STATE]
proof (prove)
using this:
eval (ExN (j + 1) (neg A)) L = eval (ExQ (ExN j (neg A))) L
(\<not> eval (neg ?f) ?L) = eval ?f ?L

goal (1 subgoal):
 1. eval (AllN (j + 1) A) L = eval (AllQ (AllN j A)) L
[PROOF STEP]
by fastforce


[STATEMENT]
lemma unwrapForall' : "eval (AllN (j + 1) A) L =  eval (AllN j (AllQ A)) L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (AllN (j + 1) A) L = eval (AllN j (AllQ A)) L
[PROOF STEP]
using unwrapExist'[of j "neg A" L] eval_neg
[PROOF STATE]
proof (prove)
using this:
eval (ExN (j + 1) (neg A)) L = eval (ExN j (ExQ (neg A))) L
(\<not> eval (neg ?f) ?L) = eval ?f ?L

goal (1 subgoal):
 1. eval (AllN (j + 1) A) L = eval (AllN j (AllQ A)) L
[PROOF STEP]
by fastforce


[STATEMENT]
lemma unwrapForall'' : "eval (AllN (i + j) A) L = eval (AllN i(AllN j A)) L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (AllN (i + j) A) L = eval (AllN i (AllN j A)) L
[PROOF STEP]
using unwrapExist''[of i j "neg A" L] eval_neg
[PROOF STATE]
proof (prove)
using this:
eval (ExN (i + j) (neg A)) L = eval (ExN i (ExN j (neg A))) L
(\<not> eval (neg ?f) ?L) = eval ?f ?L

goal (1 subgoal):
 1. eval (AllN (i + j) A) L = eval (AllN i (AllN j A)) L
[PROOF STEP]
by fastforce