[STATEMENT]
lemma Special_ax_imp_special_axioms:
  assumes "x \<in> Special_ax" shows "\<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> special_axioms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> special_axioms
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> Special_ax

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> special_axioms
[PROOF STEP]
proof (induction rule: Special_ax.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v x ax y sx. \<lbrakk>AbstForm v 0 x ax; SubstForm v y x sx; Form x; is_Var v; Term y\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp sx (q_Ex ax) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> special_axioms
[PROOF STEP]
case (I v x ax y sx)
[PROOF STATE]
proof (state)
this:
AbstForm v 0 x ax
SubstForm v y x sx
Form x
is_Var v
Term y

goal (1 subgoal):
 1. \<And>v x ax y sx. \<lbrakk>AbstForm v 0 x ax; SubstForm v y x sx; Form x; is_Var v; Term y\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp sx (q_Ex ax) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> special_axioms
[PROOF STEP]
obtain fm::fm and u::tm where fm: "x = \<lbrakk>\<guillemotleft>fm\<guillemotright>\<rbrakk>e" and  u: "y = \<lbrakk>\<guillemotleft>u\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>fm u. \<lbrakk>x = \<lbrakk>\<guillemotleft>fm\<guillemotright>\<rbrakk>e; y = \<lbrakk>\<guillemotleft>u\<guillemotright>\<rbrakk>e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
AbstForm v 0 x ax
SubstForm v y x sx
Form x
is_Var v
Term y

goal (1 subgoal):
 1. (\<And>fm u. \<lbrakk>x = \<lbrakk>\<guillemotleft>fm\<guillemotright>\<rbrakk>e; y = \<lbrakk>\<guillemotleft>u\<guillemotright>\<rbrakk>e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim!: Form_imp_is_fm Term_imp_is_tm)
[PROOF STATE]
proof (state)
this:
x = \<lbrakk>\<guillemotleft>fm\<guillemotright>\<rbrakk>e
y = \<lbrakk>\<guillemotleft>u\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. \<And>v x ax y sx. \<lbrakk>AbstForm v 0 x ax; SubstForm v y x sx; Form x; is_Var v; Term y\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp sx (q_Ex ax) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> special_axioms
[PROOF STEP]
obtain B where x: "x  = \<lbrakk>quot_dbfm B\<rbrakk>e"
            and ax: "ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 B)\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B. \<lbrakk>x = \<lbrakk>quot_dbfm B\<rbrakk>e; ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 B)\<rbrakk>e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using I AbstForm_imp_abst_dbfm
[PROOF STATE]
proof (prove)
using this:
AbstForm v 0 x ax
SubstForm v y x sx
Form x
is_Var v
Term y
AbstForm ?v ?i ?x ?x' \<Longrightarrow> \<exists>A. ?x = \<lbrakk>quot_dbfm A\<rbrakk>?e \<and> ?x' = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var ?v) (nat_of_ord ?i) A)\<rbrakk>?e

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>x = \<lbrakk>quot_dbfm B\<rbrakk>e; ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 B)\<rbrakk>e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
x = \<lbrakk>quot_dbfm B\<rbrakk>e
ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 B)\<rbrakk>e

goal (1 subgoal):
 1. \<And>v x ax y sx. \<lbrakk>AbstForm v 0 x ax; SubstForm v y x sx; Form x; is_Var v; Term y\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp sx (q_Ex ax) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> special_axioms
[PROOF STEP]
obtain B' where x': "x = \<lbrakk>quot_dbfm B'\<rbrakk>e"
             and sx: "sx = \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] u) (decode_Var v) B')\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B'. \<lbrakk>x = \<lbrakk>quot_dbfm B'\<rbrakk>e; sx = \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] u) (decode_Var v) B')\<rbrakk>e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
AbstForm v 0 x ax
SubstForm v y x sx
Form x
is_Var v
Term y

goal (1 subgoal):
 1. (\<And>B'. \<lbrakk>x = \<lbrakk>quot_dbfm B'\<rbrakk>e; sx = \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] u) (decode_Var v) B')\<rbrakk>e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis u SubstForm_imp_subst_dbfm_lemma quot_tm_def)
[PROOF STATE]
proof (state)
this:
x = \<lbrakk>quot_dbfm B'\<rbrakk>e
sx = \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] u) (decode_Var v) B')\<rbrakk>e

goal (1 subgoal):
 1. \<And>v x ax y sx. \<lbrakk>AbstForm v 0 x ax; SubstForm v y x sx; Form x; is_Var v; Term y\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp sx (q_Ex ax) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> special_axioms
[PROOF STEP]
have eq: "B'=B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B' = B
[PROOF STEP]
by (metis quot_dbfm_inject_lemma x x')
[PROOF STATE]
proof (state)
this:
B' = B

goal (1 subgoal):
 1. \<And>v x ax y sx. \<lbrakk>AbstForm v 0 x ax; SubstForm v y x sx; Form x; is_Var v; Term y\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp sx (q_Ex ax) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> special_axioms
[PROOF STEP]
have "fm(decode_Var v::=u) IMP SyntaxN.Ex (decode_Var v) fm \<in> special_axioms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fm(decode_Var v::=u) IMP SyntaxN.Ex (decode_Var v) fm \<in> special_axioms
[PROOF STEP]
by (metis special_axioms.intros)
[PROOF STATE]
proof (state)
this:
fm(decode_Var v::=u) IMP SyntaxN.Ex (decode_Var v) fm \<in> special_axioms

goal (1 subgoal):
 1. \<And>v x ax y sx. \<lbrakk>AbstForm v 0 x ax; SubstForm v y x sx; Form x; is_Var v; Term y\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp sx (q_Ex ax) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> special_axioms
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
fm(decode_Var v::=u) IMP SyntaxN.Ex (decode_Var v) fm \<in> special_axioms

goal (1 subgoal):
 1. \<exists>A. q_Imp sx (q_Ex ax) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> special_axioms
[PROOF STEP]
using eq
[PROOF STATE]
proof (prove)
using this:
fm(decode_Var v::=u) IMP SyntaxN.Ex (decode_Var v) fm \<in> special_axioms
B' = B

goal (1 subgoal):
 1. \<exists>A. q_Imp sx (q_Ex ax) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> special_axioms
[PROOF STEP]
apply (auto simp: quot_simps q_defs
                intro!: exI [where x = "fm((decode_Var v)::=u) IMP (Ex (decode_Var v) fm)"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fm(decode_Var v::=u) IMP SyntaxN.Ex (decode_Var v) fm \<in> special_axioms; B' = B\<rbrakk> \<Longrightarrow> sx = \<lbrakk>\<guillemotleft>fm(decode_Var v::=u)\<guillemotright>\<rbrakk>e
 2. \<lbrakk>fm(decode_Var v::=u) IMP SyntaxN.Ex (decode_Var v) fm \<in> special_axioms; B' = B\<rbrakk> \<Longrightarrow> ax = \<lbrakk>quot_dbfm (trans_fm [decode_Var v] fm)\<rbrakk>e
[PROOF STEP]
apply (metis fm quot_dbfm_inject_lemma quot_fm_def subst_fm_trans_commute sx x')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fm(decode_Var v::=u) IMP SyntaxN.Ex (decode_Var v) fm \<in> special_axioms; B' = B\<rbrakk> \<Longrightarrow> ax = \<lbrakk>quot_dbfm (trans_fm [decode_Var v] fm)\<rbrakk>e
[PROOF STEP]
apply (metis abst_trans_fm ax fm quot_dbfm_inject_lemma quot_fm_def x)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>A. q_Imp sx (q_Ex ax) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> special_axioms

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma special_axioms_into_Special_ax: "A \<in> special_axioms \<Longrightarrow> \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<in> Special_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> special_axioms \<Longrightarrow> \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<in> Special_ax
[PROOF STEP]
proof (induct rule: special_axioms.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A i x. \<lbrakk>\<guillemotleft>A(i::=x) IMP SyntaxN.Ex i A\<guillemotright>\<rbrakk>e \<in> Special_ax
[PROOF STEP]
case (I A i t)
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>A i x. \<lbrakk>\<guillemotleft>A(i::=x) IMP SyntaxN.Ex i A\<guillemotright>\<rbrakk>e \<in> Special_ax
[PROOF STEP]
have "\<lbrakk>\<guillemotleft>A(i::=t) IMP SyntaxN.Ex i A\<guillemotright>\<rbrakk>e =
        q_Imp \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] t) i (trans_fm [] A))\<rbrakk>e
              (q_Ex \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>A(i::=t) IMP SyntaxN.Ex i A\<guillemotright>\<rbrakk>e = q_Imp \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] t) i (trans_fm [] A))\<rbrakk>e (q_Ex \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e)
[PROOF STEP]
by (simp add: quot_fm_def q_defs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<guillemotleft>A(i::=t) IMP SyntaxN.Ex i A\<guillemotright>\<rbrakk>e = q_Imp \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] t) i (trans_fm [] A))\<rbrakk>e (q_Ex \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e)

goal (1 subgoal):
 1. \<And>A i x. \<lbrakk>\<guillemotleft>A(i::=x) IMP SyntaxN.Ex i A\<guillemotright>\<rbrakk>e \<in> Special_ax
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<guillemotleft>A(i::=t) IMP SyntaxN.Ex i A\<guillemotright>\<rbrakk>e = q_Imp \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] t) i (trans_fm [] A))\<rbrakk>e (q_Ex \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e)

goal (1 subgoal):
 1. \<And>A i x. \<lbrakk>\<guillemotleft>A(i::=x) IMP SyntaxN.Ex i A\<guillemotright>\<rbrakk>e \<in> Special_ax
[PROOF STEP]
have "... \<in> Special_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q_Imp \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] t) i (trans_fm [] A))\<rbrakk>e (q_Ex \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e) \<in> Special_ax
[PROOF STEP]
apply (rule Special_ax.intros [OF AbstForm_trans_fm])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. SubstForm (q_Var i) ?y \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] t) i (trans_fm [] A))\<rbrakk>e
 2. Form \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
 3. is_Var (q_Var i)
 4. Term ?y
[PROOF STEP]
apply (auto simp: quot_fm_def [symmetric] intro: SubstForm_quot [unfolded eval_Var_q])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
q_Imp \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] t) i (trans_fm [] A))\<rbrakk>e (q_Ex \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e) \<in> Special_ax

goal (1 subgoal):
 1. \<And>A i x. \<lbrakk>\<guillemotleft>A(i::=x) IMP SyntaxN.Ex i A\<guillemotright>\<rbrakk>e \<in> Special_ax
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<guillemotleft>A(i::=t) IMP SyntaxN.Ex i A\<guillemotright>\<rbrakk>e \<in> Special_ax
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<guillemotleft>A(i::=t) IMP SyntaxN.Ex i A\<guillemotright>\<rbrakk>e \<in> Special_ax

goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>A(i::=t) IMP SyntaxN.Ex i A\<guillemotright>\<rbrakk>e \<in> Special_ax
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<guillemotleft>A(i::=t) IMP SyntaxN.Ex i A\<guillemotright>\<rbrakk>e \<in> Special_ax

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Induction_ax_imp_induction_axioms:
  assumes "x \<in> Induction_ax" shows "\<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> Induction_ax

goal (1 subgoal):
 1. \<exists>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
proof (induction rule: Induction_ax.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
case (I v x x0 w xw xevw allw allvw ax)
[PROOF STATE]
proof (state)
this:
SubstForm v 0 x x0
SubstForm v w x xw
SubstForm v (q_Eats v w) x xevw
AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw
AbstForm v 0 (q_All allw) allvw
AbstForm v 0 x ax
v \<noteq> w
VarNonOccForm w x

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
SubstForm v 0 x x0
SubstForm v w x xw
SubstForm v (q_Eats v w) x xevw
AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw
AbstForm v 0 (q_All allw) allvw
AbstForm v 0 x ax
v \<noteq> w
VarNonOccForm w x
[PROOF STEP]
have v: "is_Var v" and w: "is_Var w"
        and dvw [simp]: "decode_Var v \<noteq> decode_Var w"  "atom (decode_Var w) \<sharp> [decode_Var v]"
[PROOF STATE]
proof (prove)
using this:
SubstForm v 0 x x0
SubstForm v w x xw
SubstForm v (q_Eats v w) x xevw
AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw
AbstForm v 0 (q_All allw) allvw
AbstForm v 0 x ax
v \<noteq> w
VarNonOccForm w x

goal (1 subgoal):
 1. is_Var v &&& is_Var w &&& decode_Var v \<noteq> decode_Var w &&& atom (decode_Var w) \<sharp> [decode_Var v]
[PROOF STEP]
by (auto simp: AbstForm_def fresh_Cons)
[PROOF STATE]
proof (state)
this:
is_Var v
is_Var w
decode_Var v \<noteq> decode_Var w
atom (decode_Var w) \<sharp> [decode_Var v]

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
obtain A::fm where A: "x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e" and wfresh: "atom (decode_Var w) \<sharp> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. \<lbrakk>x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; atom (decode_Var w) \<sharp> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using I VarNonOccForm_imp_fresh
[PROOF STATE]
proof (prove)
using this:
SubstForm v 0 x x0
SubstForm v w x xw
SubstForm v (q_Eats v w) x xevw
AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw
AbstForm v 0 (q_All allw) allvw
AbstForm v 0 x ax
v \<noteq> w
VarNonOccForm w x
\<lbrakk>VarNonOccForm ?v ?x; \<And>A. \<lbrakk>?x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>?e; atom (decode_Var ?v) \<sharp> A\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; atom (decode_Var w) \<sharp> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
atom (decode_Var w) \<sharp> A

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
atom (decode_Var w) \<sharp> A
[PROOF STEP]
obtain A' A'' where A': "q_Imp (\<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e) (q_Imp xw xevw) = \<lbrakk>quot_dbfm A'\<rbrakk>e"
                       and A'': "q_All allw = \<lbrakk>quot_dbfm A''\<rbrakk>e"
[PROOF STATE]
proof (prove)
using this:
x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
atom (decode_Var w) \<sharp> A

goal (1 subgoal):
 1. (\<And>A' A''. \<lbrakk>q_Imp \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e (q_Imp xw xevw) = \<lbrakk>quot_dbfm A'\<rbrakk>e; q_All allw = \<lbrakk>quot_dbfm A''\<rbrakk>e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using I VarNonOccForm_imp_fresh
[PROOF STATE]
proof (prove)
using this:
x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
atom (decode_Var w) \<sharp> A
SubstForm v 0 x x0
SubstForm v w x xw
SubstForm v (q_Eats v w) x xevw
AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw
AbstForm v 0 (q_All allw) allvw
AbstForm v 0 x ax
v \<noteq> w
VarNonOccForm w x
\<lbrakk>VarNonOccForm ?v ?x; \<And>A. \<lbrakk>?x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>?e; atom (decode_Var ?v) \<sharp> A\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>A' A''. \<lbrakk>q_Imp \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e (q_Imp xw xevw) = \<lbrakk>quot_dbfm A'\<rbrakk>e; q_All allw = \<lbrakk>quot_dbfm A''\<rbrakk>e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto dest!: AbstForm_imp_abst_dbfm)
[PROOF STATE]
proof (state)
this:
q_Imp \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e (q_Imp xw xevw) = \<lbrakk>quot_dbfm A'\<rbrakk>e
q_All allw = \<lbrakk>quot_dbfm A''\<rbrakk>e

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
define Aw where "Aw = A(decode_Var v::=Var (decode_Var w))"
[PROOF STATE]
proof (state)
this:
Aw = A(decode_Var v::=Var (decode_Var w))

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
define Ae where "Ae = A(decode_Var v::= Eats (Var (decode_Var v)) (Var (decode_Var w)))"
[PROOF STATE]
proof (state)
this:
Ae = A(decode_Var v::=Eats (Var (decode_Var v)) (Var (decode_Var w)))

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
have x0: "x0 = \<lbrakk>\<guillemotleft>A(decode_Var v::=Zero)\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x0 = \<lbrakk>\<guillemotleft>A(decode_Var v::=Zero)\<guillemotright>\<rbrakk>e
[PROOF STEP]
using I SubstForm_imp_subst_fm
[PROOF STATE]
proof (prove)
using this:
SubstForm v 0 x x0
SubstForm v w x xw
SubstForm v (q_Eats v w) x xevw
AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw
AbstForm v 0 (q_All allw) allvw
AbstForm v 0 x ax
v \<noteq> w
VarNonOccForm w x
\<lbrakk>SubstForm ?v \<lbrakk>\<guillemotleft>?u\<guillemotright>\<rbrakk>?e ?x ?x'; Form ?x; \<And>A. \<lbrakk>?x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>?e; ?x' = \<lbrakk>\<guillemotleft>A(decode_Var ?v::=?u)\<guillemotright>\<rbrakk>?e\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. x0 = \<lbrakk>\<guillemotleft>A(decode_Var v::=Zero)\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (metis A Form_quot_fm eval_fm_inject eval_tm.simps(1) quot_Zero)
[PROOF STATE]
proof (state)
this:
x0 = \<lbrakk>\<guillemotleft>A(decode_Var v::=Zero)\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
have xw: "xw = \<lbrakk>\<guillemotleft>Aw\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xw = \<lbrakk>\<guillemotleft>Aw\<guillemotright>\<rbrakk>e
[PROOF STEP]
using I SubstForm_imp_subst_fm
[PROOF STATE]
proof (prove)
using this:
SubstForm v 0 x x0
SubstForm v w x xw
SubstForm v (q_Eats v w) x xevw
AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw
AbstForm v 0 (q_All allw) allvw
AbstForm v 0 x ax
v \<noteq> w
VarNonOccForm w x
\<lbrakk>SubstForm ?v \<lbrakk>\<guillemotleft>?u\<guillemotright>\<rbrakk>?e ?x ?x'; Form ?x; \<And>A. \<lbrakk>?x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>?e; ?x' = \<lbrakk>\<guillemotleft>A(decode_Var ?v::=?u)\<guillemotright>\<rbrakk>?e\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. xw = \<lbrakk>\<guillemotleft>Aw\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (metis A Form_quot_fm eval_fm_inject is_Var_imp_decode_Var w Aw_def)
[PROOF STATE]
proof (state)
this:
xw = \<lbrakk>\<guillemotleft>Aw\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
have "SubstForm v (\<lbrakk>\<guillemotleft>Eats (Var (decode_Var v)) (Var (decode_Var w))\<guillemotright>\<rbrakk>e) x xevw"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SubstForm v \<lbrakk>\<guillemotleft>Eats (Var (decode_Var v)) (Var (decode_Var w))\<guillemotright>\<rbrakk>e x xevw
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
SubstForm v 0 x x0
SubstForm v w x xw
SubstForm v (q_Eats v w) x xevw
AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw
AbstForm v 0 (q_All allw) allvw
AbstForm v 0 x ax
v \<noteq> w
VarNonOccForm w x

goal (1 subgoal):
 1. SubstForm v \<lbrakk>\<guillemotleft>Eats (Var (decode_Var v)) (Var (decode_Var w))\<guillemotright>\<rbrakk>e x xevw
[PROOF STEP]
by (simp add: quot_simps q_defs) (metis is_Var_iff v w)
[PROOF STATE]
proof (state)
this:
SubstForm v \<lbrakk>\<guillemotleft>Eats (Var (decode_Var v)) (Var (decode_Var w))\<guillemotright>\<rbrakk>e x xevw

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
hence xevw: "xevw = \<lbrakk>\<guillemotleft>Ae\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
using this:
SubstForm v \<lbrakk>\<guillemotleft>Eats (Var (decode_Var v)) (Var (decode_Var w))\<guillemotright>\<rbrakk>e x xevw

goal (1 subgoal):
 1. xevw = \<lbrakk>\<guillemotleft>Ae\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (metis A Ae_def Form_quot_fm SubstForm_imp_subst_fm eval_fm_inject)
[PROOF STATE]
proof (state)
this:
xevw = \<lbrakk>\<guillemotleft>Ae\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
have ax: "ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] A))\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] A))\<rbrakk>e
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
SubstForm v 0 x x0
SubstForm v w x xw
SubstForm v (q_Eats v w) x xevw
AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw
AbstForm v 0 (q_All allw) allvw
AbstForm v 0 x ax
v \<noteq> w
VarNonOccForm w x

goal (1 subgoal):
 1. ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] A))\<rbrakk>e
[PROOF STEP]
by (metis A AbstForm_imp_abst_dbfm nat_of_ord_0 quot_dbfm_inject_lemma quot_fm_def)
[PROOF STATE]
proof (state)
this:
ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] A))\<rbrakk>e

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
have evw: "q_Imp x (q_Imp xw xevw) =
             \<lbrakk>quot_dbfm (trans_fm [] (A IMP (Aw IMP Ae)))\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q_Imp x (q_Imp xw xevw) = \<lbrakk>quot_dbfm (trans_fm [] (A IMP Aw IMP Ae))\<rbrakk>e
[PROOF STEP]
using A xw xevw
[PROOF STATE]
proof (prove)
using this:
x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
xw = \<lbrakk>\<guillemotleft>Aw\<guillemotright>\<rbrakk>e
xevw = \<lbrakk>\<guillemotleft>Ae\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. q_Imp x (q_Imp xw xevw) = \<lbrakk>quot_dbfm (trans_fm [] (A IMP Aw IMP Ae))\<rbrakk>e
[PROOF STEP]
by (auto simp: quot_simps q_defs quot_fm_def)
[PROOF STATE]
proof (state)
this:
q_Imp x (q_Imp xw xevw) = \<lbrakk>quot_dbfm (trans_fm [] (A IMP Aw IMP Ae))\<rbrakk>e

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
hence allw: "allw = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var w) 0
                                    (trans_fm [] (A IMP (Aw IMP Ae))))\<rbrakk>e"
[PROOF STATE]
proof (prove)
using this:
q_Imp x (q_Imp xw xevw) = \<lbrakk>quot_dbfm (trans_fm [] (A IMP Aw IMP Ae))\<rbrakk>e

goal (1 subgoal):
 1. allw = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var w) 0 (trans_fm [] (A IMP Aw IMP Ae)))\<rbrakk>e
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
q_Imp x (q_Imp xw xevw) = \<lbrakk>quot_dbfm (trans_fm [] (A IMP Aw IMP Ae))\<rbrakk>e
SubstForm v 0 x x0
SubstForm v w x xw
SubstForm v (q_Eats v w) x xevw
AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw
AbstForm v 0 (q_All allw) allvw
AbstForm v 0 x ax
v \<noteq> w
VarNonOccForm w x

goal (1 subgoal):
 1. allw = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var w) 0 (trans_fm [] (A IMP Aw IMP Ae)))\<rbrakk>e
[PROOF STEP]
by (metis AbstForm_imp_abst_dbfm nat_of_ord_0 quot_dbfm_inject_lemma)
[PROOF STATE]
proof (state)
this:
allw = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var w) 0 (trans_fm [] (A IMP Aw IMP Ae)))\<rbrakk>e

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
allw = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var w) 0 (trans_fm [] (A IMP Aw IMP Ae)))\<rbrakk>e
[PROOF STEP]
have evw: "q_All allw = \<lbrakk>quot_dbfm (trans_fm [] (All (decode_Var w) (A IMP (Aw IMP Ae))))\<rbrakk>e"
[PROOF STATE]
proof (prove)
using this:
allw = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var w) 0 (trans_fm [] (A IMP Aw IMP Ae)))\<rbrakk>e

goal (1 subgoal):
 1. q_All allw = \<lbrakk>quot_dbfm (trans_fm [] (SyntaxN.All (decode_Var w) (A IMP Aw IMP Ae)))\<rbrakk>e
[PROOF STEP]
by (auto simp: q_defs abst_trans_fm)
[PROOF STATE]
proof (state)
this:
q_All allw = \<lbrakk>quot_dbfm (trans_fm [] (SyntaxN.All (decode_Var w) (A IMP Aw IMP Ae)))\<rbrakk>e

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
hence allvw: "allvw = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0
                                     (trans_fm [] (All (decode_Var w) (A IMP (Aw IMP Ae)))))\<rbrakk>e"
[PROOF STATE]
proof (prove)
using this:
q_All allw = \<lbrakk>quot_dbfm (trans_fm [] (SyntaxN.All (decode_Var w) (A IMP Aw IMP Ae)))\<rbrakk>e

goal (1 subgoal):
 1. allvw = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] (SyntaxN.All (decode_Var w) (A IMP Aw IMP Ae))))\<rbrakk>e
[PROOF STEP]
using I
[PROOF STATE]
proof (prove)
using this:
q_All allw = \<lbrakk>quot_dbfm (trans_fm [] (SyntaxN.All (decode_Var w) (A IMP Aw IMP Ae)))\<rbrakk>e
SubstForm v 0 x x0
SubstForm v w x xw
SubstForm v (q_Eats v w) x xevw
AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw
AbstForm v 0 (q_All allw) allvw
AbstForm v 0 x ax
v \<noteq> w
VarNonOccForm w x

goal (1 subgoal):
 1. allvw = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] (SyntaxN.All (decode_Var w) (A IMP Aw IMP Ae))))\<rbrakk>e
[PROOF STEP]
by (metis AbstForm_imp_abst_dbfm nat_of_ord_0 quot_dbfm_inject_lemma)
[PROOF STATE]
proof (state)
this:
allvw = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] (SyntaxN.All (decode_Var w) (A IMP Aw IMP Ae))))\<rbrakk>e

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
define ind_ax
    where "ind_ax =
        A(decode_Var v::=Zero) IMP
        ((All (decode_Var v) (All (decode_Var w) (A IMP (Aw IMP Ae)))) IMP
        (All (decode_Var v) A))"
[PROOF STATE]
proof (state)
this:
ind_ax = A(decode_Var v::=Zero) IMP SyntaxN.All (decode_Var v) (SyntaxN.All (decode_Var w) (A IMP Aw IMP Ae)) IMP SyntaxN.All (decode_Var v) A

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
have "atom (decode_Var w) \<sharp> (decode_Var v, A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom (decode_Var w) \<sharp> (decode_Var v, A)
[PROOF STEP]
using I wfresh v w
[PROOF STATE]
proof (prove)
using this:
SubstForm v 0 x x0
SubstForm v w x xw
SubstForm v (q_Eats v w) x xevw
AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw
AbstForm v 0 (q_All allw) allvw
AbstForm v 0 x ax
v \<noteq> w
VarNonOccForm w x
atom (decode_Var w) \<sharp> A
is_Var v
is_Var w

goal (1 subgoal):
 1. atom (decode_Var w) \<sharp> (decode_Var v, A)
[PROOF STEP]
by (metis atom_eq_iff decode_Var_inject fresh_Pair fresh_ineq_at_base)
[PROOF STATE]
proof (state)
this:
atom (decode_Var w) \<sharp> (decode_Var v, A)

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
hence "ind_ax \<in> induction_axioms"
[PROOF STATE]
proof (prove)
using this:
atom (decode_Var w) \<sharp> (decode_Var v, A)

goal (1 subgoal):
 1. ind_ax \<in> induction_axioms
[PROOF STEP]
by (auto simp: ind_ax_def Aw_def Ae_def induction_axioms.intros)
[PROOF STATE]
proof (state)
this:
ind_ax \<in> induction_axioms

goal (1 subgoal):
 1. \<And>v x x0 w xw xevw allw allvw ax. \<lbrakk>SubstForm v 0 x x0; SubstForm v w x xw; SubstForm v (q_Eats v w) x xevw; AbstForm w 0 (q_Imp x (q_Imp xw xevw)) allw; AbstForm v 0 (q_All allw) allvw; AbstForm v 0 x ax; v \<noteq> w; VarNonOccForm w x\<rbrakk> \<Longrightarrow> \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ind_ax \<in> induction_axioms

goal (1 subgoal):
 1. \<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms
[PROOF STEP]
by (force simp: quot_simps q_defs ind_ax_def allvw ax x0 abst_trans_fm2 abst_trans_fm)
[PROOF STATE]
proof (state)
this:
\<exists>A. q_Imp x0 (q_Imp (q_All allvw) (q_All ax)) = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> A \<in> induction_axioms

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma induction_axioms_into_Induction_ax:
  "A \<in> induction_axioms \<Longrightarrow> \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<in> Induction_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> induction_axioms \<Longrightarrow> \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<in> Induction_ax
[PROOF STEP]
proof (induct rule: induction_axioms.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j i A. atom j \<sharp> (i, A) \<Longrightarrow> \<lbrakk>\<guillemotleft>A(i::=Zero) IMP SyntaxN.All i (SyntaxN.All j (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j)))) IMP SyntaxN.All i A\<guillemotright>\<rbrakk>e \<in> Induction_ax
[PROOF STEP]
case (ind j i A)
[PROOF STATE]
proof (state)
this:
atom j \<sharp> (i, A)

goal (1 subgoal):
 1. \<And>j i A. atom j \<sharp> (i, A) \<Longrightarrow> \<lbrakk>\<guillemotleft>A(i::=Zero) IMP SyntaxN.All i (SyntaxN.All j (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j)))) IMP SyntaxN.All i A\<guillemotright>\<rbrakk>e \<in> Induction_ax
[PROOF STEP]
hence eq: "\<lbrakk>\<guillemotleft>A(i::=Zero) IMP All i (All j (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j)))) IMP All i A\<guillemotright>\<rbrakk>e =
            q_Imp \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] Zero) i (trans_fm [] A))\<rbrakk>e
            (q_Imp (q_All (q_All
                  (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e
                    (q_Imp
                      \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e
                      \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e))))
              (q_All \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e))"
[PROOF STATE]
proof (prove)
using this:
atom j \<sharp> (i, A)

goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>A(i::=Zero) IMP SyntaxN.All i (SyntaxN.All j (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j)))) IMP SyntaxN.All i A\<guillemotright>\<rbrakk>e = q_Imp \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] Zero) i (trans_fm [] A))\<rbrakk>e (q_Imp (q_All (q_All (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)))) (q_All \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e))
[PROOF STEP]
by (simp add: quot_simps q_defs quot_subst_eq fresh_Cons fresh_Pair)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<guillemotleft>A(i::=Zero) IMP SyntaxN.All i (SyntaxN.All j (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j)))) IMP SyntaxN.All i A\<guillemotright>\<rbrakk>e = q_Imp \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] Zero) i (trans_fm [] A))\<rbrakk>e (q_Imp (q_All (q_All (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)))) (q_All \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e))

goal (1 subgoal):
 1. \<And>j i A. atom j \<sharp> (i, A) \<Longrightarrow> \<lbrakk>\<guillemotleft>A(i::=Zero) IMP SyntaxN.All i (SyntaxN.All j (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j)))) IMP SyntaxN.All i A\<guillemotright>\<rbrakk>e \<in> Induction_ax
[PROOF STEP]
have [simp]: "atom j \<sharp> [i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom j \<sharp> [i]
[PROOF STEP]
using ind
[PROOF STATE]
proof (prove)
using this:
atom j \<sharp> (i, A)

goal (1 subgoal):
 1. atom j \<sharp> [i]
[PROOF STEP]
by (metis fresh_Cons fresh_Nil fresh_Pair)
[PROOF STATE]
proof (state)
this:
atom j \<sharp> [i]

goal (1 subgoal):
 1. \<And>j i A. atom j \<sharp> (i, A) \<Longrightarrow> \<lbrakk>\<guillemotleft>A(i::=Zero) IMP SyntaxN.All i (SyntaxN.All j (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j)))) IMP SyntaxN.All i A\<guillemotright>\<rbrakk>e \<in> Induction_ax
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>A(i::=Zero) IMP SyntaxN.All i (SyntaxN.All j (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j)))) IMP SyntaxN.All i A\<guillemotright>\<rbrakk>e \<in> Induction_ax
[PROOF STEP]
proof (simp only: eq, rule Induction_ax.intros [where v = "q_Var i" and w = "q_Var j"])
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. SubstForm (q_Var i) 0 ?x1 \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] Zero) i (trans_fm [] A))\<rbrakk>e
 2. SubstForm (q_Var i) (q_Var j) ?x1 ?xw1
 3. SubstForm (q_Var i) (q_Eats (q_Var i) (q_Var j)) ?x1 ?xevw1
 4. AbstForm (q_Var j) 0 (q_Imp ?x1 (q_Imp ?xw1 ?xevw1)) ?allw1
 5. AbstForm (q_Var i) 0 (q_All ?allw1) (q_All (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)))
 6. AbstForm (q_Var i) 0 ?x1 \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e
 7. q_Var i \<noteq> q_Var j
 8. VarNonOccForm (q_Var j) ?x1
[PROOF STEP]
show "SubstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
           \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] Zero) i (trans_fm [] A))\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SubstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] Zero) i (trans_fm [] A))\<rbrakk>e
[PROOF STEP]
by (metis SubstForm_subst_dbfm_eq Term_quot_tm eval_tm.simps(1) quot_Zero quot_fm_def quot_tm_def)
[PROOF STATE]
proof (state)
this:
SubstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (subst_dbfm (trans_tm [] Zero) i (trans_fm [] A))\<rbrakk>e

goal (7 subgoals):
 1. SubstForm (q_Var i) (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e ?xw1
 2. SubstForm (q_Var i) (q_Eats (q_Var i) (q_Var j)) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e ?xevw1
 3. AbstForm (q_Var j) 0 (q_Imp \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e (q_Imp ?xw1 ?xevw1)) ?allw1
 4. AbstForm (q_Var i) 0 (q_All ?allw1) (q_All (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)))
 5. AbstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e
 6. q_Var i \<noteq> q_Var j
 7. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. SubstForm (q_Var i) (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e ?xw1
 2. SubstForm (q_Var i) (q_Eats (q_Var i) (q_Var j)) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e ?xevw1
 3. AbstForm (q_Var j) 0 (q_Imp \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e (q_Imp ?xw1 ?xevw1)) ?allw1
 4. AbstForm (q_Var i) 0 (q_All ?allw1) (q_All (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)))
 5. AbstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e
 6. q_Var i \<noteq> q_Var j
 7. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
show "SubstForm (q_Var i) (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (subst_dbfm (DBVar j) i (trans_fm [] A))\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SubstForm (q_Var i) (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (subst_dbfm (DBVar j) i (trans_fm [] A))\<rbrakk>e
[PROOF STEP]
by (auto simp: quot_fm_def intro!: SubstForm_subst_dbfm_eq Term_Var)
         (metis q_Var_def)
[PROOF STATE]
proof (state)
this:
SubstForm (q_Var i) (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (subst_dbfm (DBVar j) i (trans_fm [] A))\<rbrakk>e

goal (6 subgoals):
 1. SubstForm (q_Var i) (q_Eats (q_Var i) (q_Var j)) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e ?xevw1
 2. AbstForm (q_Var j) 0 (q_Imp \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (subst_dbfm (DBVar j) i (trans_fm [] A))\<rbrakk>e ?xevw1)) ?allw1
 3. AbstForm (q_Var i) 0 (q_All ?allw1) (q_All (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)))
 4. AbstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e
 5. q_Var i \<noteq> q_Var j
 6. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. SubstForm (q_Var i) (q_Eats (q_Var i) (q_Var j)) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e ?xevw1
 2. AbstForm (q_Var j) 0 (q_Imp \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (subst_dbfm (DBVar j) i (trans_fm [] A))\<rbrakk>e ?xevw1)) ?allw1
 3. AbstForm (q_Var i) 0 (q_All ?allw1) (q_All (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)))
 4. AbstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e
 5. q_Var i \<noteq> q_Var j
 6. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
show "SubstForm (q_Var i) (q_Eats (q_Var i) (q_Var j)) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
              \<lbrakk>quot_dbfm (subst_dbfm (DBEats (DBVar i) (DBVar j)) i (trans_fm [] A))\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SubstForm (q_Var i) (q_Eats (q_Var i) (q_Var j)) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (subst_dbfm (DBEats (DBVar i) (DBVar j)) i (trans_fm [] A))\<rbrakk>e
[PROOF STEP]
unfolding quot_fm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SubstForm (q_Var i) (q_Eats (q_Var i) (q_Var j)) \<lbrakk>quot_dbfm (trans_fm [] A)\<rbrakk>e \<lbrakk>quot_dbfm (subst_dbfm (DBEats (DBVar i) (DBVar j)) i (trans_fm [] A))\<rbrakk>e
[PROOF STEP]
by (auto intro!: SubstForm_subst_dbfm_eq Term_Eats Term_Var) (simp add: q_defs)
[PROOF STATE]
proof (state)
this:
SubstForm (q_Var i) (q_Eats (q_Var i) (q_Var j)) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (subst_dbfm (DBEats (DBVar i) (DBVar j)) i (trans_fm [] A))\<rbrakk>e

goal (5 subgoals):
 1. AbstForm (q_Var j) 0 (q_Imp \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (subst_dbfm (DBVar j) i (trans_fm [] A))\<rbrakk>e \<lbrakk>quot_dbfm (subst_dbfm (DBEats (DBVar i) (DBVar j)) i (trans_fm [] A))\<rbrakk>e)) ?allw1
 2. AbstForm (q_Var i) 0 (q_All ?allw1) (q_All (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)))
 3. AbstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e
 4. q_Var i \<noteq> q_Var j
 5. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. AbstForm (q_Var j) 0 (q_Imp \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (subst_dbfm (DBVar j) i (trans_fm [] A))\<rbrakk>e \<lbrakk>quot_dbfm (subst_dbfm (DBEats (DBVar i) (DBVar j)) i (trans_fm [] A))\<rbrakk>e)) ?allw1
 2. AbstForm (q_Var i) 0 (q_All ?allw1) (q_All (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)))
 3. AbstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e
 4. q_Var i \<noteq> q_Var j
 5. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
show "AbstForm (q_Var j) 0
           (q_Imp \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
              (q_Imp \<lbrakk>quot_dbfm (subst_dbfm (DBVar j) i (trans_fm [] A))\<rbrakk>e
                     \<lbrakk>quot_dbfm (subst_dbfm (DBEats (DBVar i) (DBVar j)) i (trans_fm [] A))\<rbrakk>e))
           \<lbrakk>quot_dbfm (trans_fm [j] (A IMP (A(i::= Var j) IMP A(i::= Eats(Var i)(Var j)))))\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AbstForm (q_Var j) 0 (q_Imp \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (subst_dbfm (DBVar j) i (trans_fm [] A))\<rbrakk>e \<lbrakk>quot_dbfm (subst_dbfm (DBEats (DBVar i) (DBVar j)) i (trans_fm [] A))\<rbrakk>e)) \<lbrakk>quot_dbfm (trans_fm [j] (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j))))\<rbrakk>e
[PROOF STEP]
by (rule AbstForm_trans_fm_eq [where A = "(A IMP A(i::= Var j) IMP A(i::= Eats(Var i)(Var j)))"])
         (auto simp: quot_simps q_defs quot_fm_def subst_fm_trans_commute_eq)
[PROOF STATE]
proof (state)
this:
AbstForm (q_Var j) 0 (q_Imp \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (subst_dbfm (DBVar j) i (trans_fm [] A))\<rbrakk>e \<lbrakk>quot_dbfm (subst_dbfm (DBEats (DBVar i) (DBVar j)) i (trans_fm [] A))\<rbrakk>e)) \<lbrakk>quot_dbfm (trans_fm [j] (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j))))\<rbrakk>e

goal (4 subgoals):
 1. AbstForm (q_Var i) 0 (q_All \<lbrakk>quot_dbfm (trans_fm [j] (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j))))\<rbrakk>e) (q_All (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)))
 2. AbstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e
 3. q_Var i \<noteq> q_Var j
 4. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. AbstForm (q_Var i) 0 (q_All \<lbrakk>quot_dbfm (trans_fm [j] (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j))))\<rbrakk>e) (q_All (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)))
 2. AbstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e
 3. q_Var i \<noteq> q_Var j
 4. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
show "AbstForm (q_Var i) 0
     (q_All \<lbrakk>quot_dbfm (trans_fm [j] (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j))))\<rbrakk>e)
     (q_All
       (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e
         (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e
                \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AbstForm (q_Var i) 0 (q_All \<lbrakk>quot_dbfm (trans_fm [j] (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j))))\<rbrakk>e) (q_All (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)))
[PROOF STEP]
apply (rule AbstForm_trans_fm_eq
               [where A = "All j (A IMP (A(i::= Var j) IMP A(i::= Eats(Var i)(Var j))))"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. q_All \<lbrakk>quot_dbfm (trans_fm [j] (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j))))\<rbrakk>e = \<lbrakk>\<guillemotleft>SyntaxN.All j (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j)))\<guillemotright>\<rbrakk>?e
 2. q_All (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)) = \<lbrakk>quot_dbfm (trans_fm [i] (SyntaxN.All j (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j)))))\<rbrakk>?e
[PROOF STEP]
apply (auto simp: q_defs quot_fm_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
AbstForm (q_Var i) 0 (q_All \<lbrakk>quot_dbfm (trans_fm [j] (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j))))\<rbrakk>e) (q_All (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] A)\<rbrakk>e (q_Imp \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Var j)))\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [j, i] (A(i::=Eats (Var i) (Var j))))\<rbrakk>e)))

goal (3 subgoals):
 1. AbstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e
 2. q_Var i \<noteq> q_Var j
 3. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. AbstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e
 2. q_Var i \<noteq> q_Var j
 3. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
show "AbstForm (q_Var i) 0 (\<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e) \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AbstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e
[PROOF STEP]
by (metis AbstForm_trans_fm)
[PROOF STATE]
proof (state)
this:
AbstForm (q_Var i) 0 \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<lbrakk>quot_dbfm (trans_fm [i] A)\<rbrakk>e

goal (2 subgoals):
 1. q_Var i \<noteq> q_Var j
 2. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. q_Var i \<noteq> q_Var j
 2. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
show "q_Var i \<noteq> q_Var j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q_Var i \<noteq> q_Var j
[PROOF STEP]
using ind
[PROOF STATE]
proof (prove)
using this:
atom j \<sharp> (i, A)

goal (1 subgoal):
 1. q_Var i \<noteq> q_Var j
[PROOF STEP]
by (simp add: q_Var_def)
[PROOF STATE]
proof (state)
this:
q_Var i \<noteq> q_Var j

goal (1 subgoal):
 1. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
show "VarNonOccForm (q_Var j) (\<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (metis fresh_Pair fresh_imp_VarNonOccForm ind)
[PROOF STATE]
proof (state)
this:
VarNonOccForm (q_Var j) \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<guillemotleft>A(i::=Zero) IMP SyntaxN.All i (SyntaxN.All j (A IMP A(i::=Var j) IMP A(i::=Eats (Var i) (Var j)))) IMP SyntaxN.All i A\<guillemotright>\<rbrakk>e \<in> Induction_ax

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma AxiomP_eqvt [eqvt]: "(p \<bullet> AxiomP x) = AxiomP (p \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> AxiomP x = AxiomP (p \<bullet> x)
[PROOF STEP]
by (simp add: AxiomP_def)


[STATEMENT]
lemma AxiomP_fresh_iff [simp]: "a \<sharp> AxiomP x \<longleftrightarrow> a \<sharp> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> AxiomP x = a \<sharp> x
[PROOF STEP]
by (auto simp: AxiomP_def)


[STATEMENT]
lemma eval_fm_AxiomP [simp]: "eval_fm e (AxiomP x) \<longleftrightarrow> \<lbrakk>x\<rbrakk>e \<in> Axiom"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fm e (AxiomP x) = (\<lbrakk>x\<rbrakk>e \<in> Axiom)
[PROOF STEP]
unfolding AxiomP_def Axiom_def Extra_ax_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fm e (x EQ \<guillemotleft>extra_axiom\<guillemotright> OR SentP x OR Equality_axP x OR HF_axP x OR Special_axP x OR Induction_axP x) = (\<lbrakk>x\<rbrakk>e \<in> {\<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e0} \<union> Sent \<union> Equality_ax \<union> HF_ax \<union> Special_ax \<union> Induction_ax)
[PROOF STEP]
by (auto simp del: Equality_axP.simps HF_axP.simps intro: eval_quot_fm_ignore)


[STATEMENT]
lemma AxiomP_sf [iff]: "Sigma_fm (AxiomP t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_fm (AxiomP t)
[PROOF STEP]
by (auto simp: AxiomP_def)


[STATEMENT]
lemma ModPonP_eqvt [eqvt]: "(p \<bullet> ModPonP x y z) = ModPonP (p \<bullet> x) (p \<bullet> y) (p \<bullet> z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> ModPonP x y z = ModPonP (p \<bullet> x) (p \<bullet> y) (p \<bullet> z)
[PROOF STEP]
by (simp add: ModPonP_def)


[STATEMENT]
lemma ModPonP_fresh_iff [simp]: "a \<sharp> ModPonP x y z \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> y \<and> a \<sharp> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<sharp> ModPonP x y z = (a \<sharp> x \<and> a \<sharp> y \<and> a \<sharp> z)
[PROOF STEP]
by (auto simp: ModPonP_def)


[STATEMENT]
lemma eval_fm_ModPonP [simp]: "eval_fm e (ModPonP x y z) \<longleftrightarrow> ModPon \<lbrakk>x\<rbrakk>e \<lbrakk>y\<rbrakk>e \<lbrakk>z\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fm e (ModPonP x y z) = ModPon \<lbrakk>x\<rbrakk>e \<lbrakk>y\<rbrakk>e \<lbrakk>z\<rbrakk>e
[PROOF STEP]
by (auto simp: ModPon_def ModPonP_def q_defs)


[STATEMENT]
lemma ModPonP_sf [iff]: "Sigma_fm (ModPonP t u v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sigma_fm (ModPonP t u v)
[PROOF STEP]
by (auto simp: ModPonP_def)


[STATEMENT]
lemma ModPonP_subst [simp]:
  "(ModPonP t u v)(i::=w) = ModPonP (subst i w t) (subst i w u) (subst i w v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ModPonP t u v)(i::=w) = ModPonP (subst i w t) (subst i w u) (subst i w v)
[PROOF STEP]
by (auto simp: ModPonP_def)


[STATEMENT]
lemma ExistsP_subst [simp]: "(ExistsP p q)(j::=w) = ExistsP (subst j w p) (subst j w q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ExistsP p q)(j::=w) = ExistsP (subst j w p) (subst j w q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (ExistsP p q)(j::=w) = ExistsP (subst j w p) (subst j w q)
[PROOF STEP]
obtain x::name and x'::name and y::name and v::name
    where "atom x \<sharp> (j,w,p,q,v,y,x')"   "atom x' \<sharp> (j,w,p,q,v,y)"
          "atom y \<sharp> (j,w,p,q,v)"   "atom v \<sharp> (j,w,p,q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x v y x'. \<lbrakk>atom x \<sharp> (j, w, p, q, v, y, x'); atom x' \<sharp> (j, w, p, q, v, y); atom y \<sharp> (j, w, p, q, v); atom v \<sharp> (j, w, p, q)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom x \<sharp> (j, w, p, q, v, y, x')
atom x' \<sharp> (j, w, p, q, v, y)
atom y \<sharp> (j, w, p, q, v)
atom v \<sharp> (j, w, p, q)

goal (1 subgoal):
 1. (ExistsP p q)(j::=w) = ExistsP (subst j w p) (subst j w q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> (j, w, p, q, v, y, x')
atom x' \<sharp> (j, w, p, q, v, y)
atom y \<sharp> (j, w, p, q, v)
atom v \<sharp> (j, w, p, q)

goal (1 subgoal):
 1. (ExistsP p q)(j::=w) = ExistsP (subst j w p) (subst j w q)
[PROOF STEP]
by (auto simp: ExistsP.simps [of x _ _ x' y v])
[PROOF STATE]
proof (state)
this:
(ExistsP p q)(j::=w) = ExistsP (subst j w p) (subst j w q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Exists_imp_exists:
  assumes "Exists p q"
  shows "\<exists>A B i. p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>(Ex i A) IMP B\<guillemotright>\<rbrakk>e \<and> atom i \<sharp> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A B i. p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e \<and> atom i \<sharp> B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A B i. p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e \<and> atom i \<sharp> B
[PROOF STEP]
obtain x ax y v
    where x:    "Form x"
      and noc:  "VarNonOccForm v y"
      and abst: "AbstForm v 0 x ax"
      and p: "p = q_Imp x y"
      and q: "q = q_Imp (q_Ex ax) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x v y ax. \<lbrakk>Form x; VarNonOccForm v y; AbstForm v 0 x ax; p = q_Imp x y; q = q_Imp (q_Ex ax) y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Exists p q

goal (1 subgoal):
 1. (\<And>x v y ax. \<lbrakk>Form x; VarNonOccForm v y; AbstForm v 0 x ax; p = q_Imp x y; q = q_Imp (q_Ex ax) y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: Exists_def)
[PROOF STATE]
proof (state)
this:
Form x
VarNonOccForm v y
AbstForm v 0 x ax
p = q_Imp x y
q = q_Imp (q_Ex ax) y

goal (1 subgoal):
 1. \<exists>A B i. p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e \<and> atom i \<sharp> B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Form x
VarNonOccForm v y
AbstForm v 0 x ax
p = q_Imp x y
q = q_Imp (q_Ex ax) y
[PROOF STEP]
obtain B::fm where B: "y = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e" and vfresh: "atom (decode_Var v) \<sharp> B"
[PROOF STATE]
proof (prove)
using this:
Form x
VarNonOccForm v y
AbstForm v 0 x ax
p = q_Imp x y
q = q_Imp (q_Ex ax) y

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>y = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e; atom (decode_Var v) \<sharp> B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis VarNonOccForm_imp_fresh)
[PROOF STATE]
proof (state)
this:
y = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
atom (decode_Var v) \<sharp> B

goal (1 subgoal):
 1. \<exists>A B i. p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e \<and> atom i \<sharp> B
[PROOF STEP]
obtain A::fm where A: "x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A. x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Form_imp_is_fm x)
[PROOF STATE]
proof (state)
this:
x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. \<exists>A B i. p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e \<and> atom i \<sharp> B
[PROOF STEP]
with AbstForm_imp_abst_dbfm [OF abst, of e]
[PROOF STATE]
proof (chain)
picking this:
\<exists>A. x = \<lbrakk>quot_dbfm A\<rbrakk>e \<and> ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) (nat_of_ord 0) A)\<rbrakk>e
x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
[PROOF STEP]
have ax: "ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] A))\<rbrakk>e"
           "p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
using this:
\<exists>A. x = \<lbrakk>quot_dbfm A\<rbrakk>e \<and> ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) (nat_of_ord 0) A)\<rbrakk>e
x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] A))\<rbrakk>e &&& p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
using p A B
[PROOF STATE]
proof (prove)
using this:
\<exists>A. x = \<lbrakk>quot_dbfm A\<rbrakk>e \<and> ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) (nat_of_ord 0) A)\<rbrakk>e
x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
p = q_Imp x y
x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
y = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] A))\<rbrakk>e &&& p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (auto simp: quot_simps quot_fm_def q_defs)
[PROOF STATE]
proof (state)
this:
ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] A))\<rbrakk>e
p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. \<exists>A B i. p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e \<and> atom i \<sharp> B
[PROOF STEP]
have "q = \<lbrakk>\<guillemotleft>(Ex (decode_Var v) A) IMP B\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q = \<lbrakk>\<guillemotleft>SyntaxN.Ex (decode_Var v) A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
using q A B ax
[PROOF STATE]
proof (prove)
using this:
q = q_Imp (q_Ex ax) y
x = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
y = \<lbrakk>\<guillemotleft>B\<guillemotright>\<rbrakk>e
ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] A))\<rbrakk>e
p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. q = \<lbrakk>\<guillemotleft>SyntaxN.Ex (decode_Var v) A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (auto simp: abst_trans_fm quot_simps q_defs)
[PROOF STATE]
proof (state)
this:
q = \<lbrakk>\<guillemotleft>SyntaxN.Ex (decode_Var v) A IMP B\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. \<exists>A B i. p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e \<and> atom i \<sharp> B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q = \<lbrakk>\<guillemotleft>SyntaxN.Ex (decode_Var v) A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
q = \<lbrakk>\<guillemotleft>SyntaxN.Ex (decode_Var v) A IMP B\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. \<exists>A B i. p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e \<and> atom i \<sharp> B
[PROOF STEP]
using vfresh ax
[PROOF STATE]
proof (prove)
using this:
q = \<lbrakk>\<guillemotleft>SyntaxN.Ex (decode_Var v) A IMP B\<guillemotright>\<rbrakk>e
atom (decode_Var v) \<sharp> B
ax = \<lbrakk>quot_dbfm (abst_dbfm (decode_Var v) 0 (trans_fm [] A))\<rbrakk>e
p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. \<exists>A B i. p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e \<and> atom i \<sharp> B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A B i. p = \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e \<and> atom i \<sharp> B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Exists_intro: "atom i \<sharp> B \<Longrightarrow> Exists (\<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e) \<lbrakk>\<guillemotleft>(Ex i A) IMP B\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atom i \<sharp> B \<Longrightarrow> Exists \<lbrakk>\<guillemotleft>A IMP B\<guillemotright>\<rbrakk>e \<lbrakk>\<guillemotleft>SyntaxN.Ex i A IMP B\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (simp add: Exists_def quot_simps q_defs)
     (metis AbstForm_trans_fm Form_quot_fm fresh_imp_VarNonOccForm)


[STATEMENT]
lemma SubstP_subst [simp]: "(SubstP p q)(j::=w) = SubstP (subst j w p) (subst j w q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SubstP p q)(j::=w) = SubstP (subst j w p) (subst j w q)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (SubstP p q)(j::=w) = SubstP (subst j w p) (subst j w q)
[PROOF STEP]
obtain u::name and v::name  where "atom u \<sharp> (j,w,p,q,v)"  "atom v \<sharp> (j,w,p,q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u v. \<lbrakk>atom u \<sharp> (j, w, p, q, v); atom v \<sharp> (j, w, p, q)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom u \<sharp> (j, w, p, q, v)
atom v \<sharp> (j, w, p, q)

goal (1 subgoal):
 1. (SubstP p q)(j::=w) = SubstP (subst j w p) (subst j w q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom u \<sharp> (j, w, p, q, v)
atom v \<sharp> (j, w, p, q)

goal (1 subgoal):
 1. (SubstP p q)(j::=w) = SubstP (subst j w p) (subst j w q)
[PROOF STEP]
by (simp add: SubstP.simps [of u _ _ v])
[PROOF STATE]
proof (state)
this:
(SubstP p q)(j::=w) = SubstP (subst j w p) (subst j w q)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Subst_imp_subst:
  assumes "Subst p q" "Form p"
  shows "\<exists>A::fm. \<exists>i t. p = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>A(i::=t)\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A i t. p = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>A(i::=t)\<guillemotright>\<rbrakk>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A i t. p = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>A(i::=t)\<guillemotright>\<rbrakk>e
[PROOF STEP]
obtain v u where subst: "SubstForm v u p q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v u. SubstForm v u p q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Subst p q
Form p

goal (1 subgoal):
 1. (\<And>v u. SubstForm v u p q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: Subst_def)
[PROOF STATE]
proof (state)
this:
SubstForm v u p q

goal (1 subgoal):
 1. \<exists>A i t. p = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>A(i::=t)\<guillemotright>\<rbrakk>e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
SubstForm v u p q
[PROOF STEP]
obtain t::tm where substt: "SubstForm v \<lbrakk>\<guillemotleft>t\<guillemotright>\<rbrakk>e p q"
[PROOF STATE]
proof (prove)
using this:
SubstForm v u p q

goal (1 subgoal):
 1. (\<And>t. SubstForm v \<lbrakk>\<guillemotleft>t\<guillemotright>\<rbrakk>e p q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis SubstForm_def Term_imp_is_tm)
[PROOF STATE]
proof (state)
this:
SubstForm v \<lbrakk>\<guillemotleft>t\<guillemotright>\<rbrakk>e p q

goal (1 subgoal):
 1. \<exists>A i t. p = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>A(i::=t)\<guillemotright>\<rbrakk>e
[PROOF STEP]
with SubstForm_imp_subst_fm [OF substt] assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>Form p; \<And>A. \<lbrakk>p = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; q = \<lbrakk>\<guillemotleft>A(decode_Var v::=t)\<guillemotright>\<rbrakk>e\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
Subst p q
Form p
SubstForm v \<lbrakk>\<guillemotleft>t\<guillemotright>\<rbrakk>e p q
[PROOF STEP]
obtain A where "p = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e"  "q = \<lbrakk>\<guillemotleft>A(decode_Var v::=t)\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Form p; \<And>A. \<lbrakk>p = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; q = \<lbrakk>\<guillemotleft>A(decode_Var v::=t)\<guillemotright>\<rbrakk>e\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
Subst p q
Form p
SubstForm v \<lbrakk>\<guillemotleft>t\<guillemotright>\<rbrakk>e p q

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>p = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e; q = \<lbrakk>\<guillemotleft>A(decode_Var v::=t)\<guillemotright>\<rbrakk>e\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
q = \<lbrakk>\<guillemotleft>A(decode_Var v::=t)\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. \<exists>A i t. p = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>A(i::=t)\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
p = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e
q = \<lbrakk>\<guillemotleft>A(decode_Var v::=t)\<guillemotright>\<rbrakk>e

goal (1 subgoal):
 1. \<exists>A i t. p = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>A(i::=t)\<guillemotright>\<rbrakk>e
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A i t. p = \<lbrakk>\<guillemotleft>A\<guillemotright>\<rbrakk>e \<and> q = \<lbrakk>\<guillemotleft>A(i::=t)\<guillemotright>\<rbrakk>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma PrfP_subst [simp]:
     "(PrfP t u v)(j::=w) = PrfP (subst j w t) (subst j w u) (subst j w v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (PrfP t u v)(j::=w) = PrfP (subst j w t) (subst j w u) (subst j w v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (PrfP t u v)(j::=w) = PrfP (subst j w t) (subst j w u) (subst j w v)
[PROOF STEP]
obtain l::name and sl::name and m::name and n::name and sm::name and sn::name
    where "atom l \<sharp> (t,u,v,j,w,sl,m,n,sm,sn)"   "atom sl \<sharp> (t,u,v,j,w,m,n,sm,sn)"
          "atom m \<sharp> (t,u,v,j,w,n,sm,sn)"   "atom n \<sharp> (t,u,v,j,w,sm,sn)"
          "atom sm \<sharp> (t,u,v,j,w,sn)"   "atom sn \<sharp> (t,u,v,j,w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l sl m n sm sn. \<lbrakk>atom l \<sharp> (t, u, v, j, w, sl, m, n, sm, sn); atom sl \<sharp> (t, u, v, j, w, m, n, sm, sn); atom m \<sharp> (t, u, v, j, w, n, sm, sn); atom n \<sharp> (t, u, v, j, w, sm, sn); atom sm \<sharp> (t, u, v, j, w, sn); atom sn \<sharp> (t, u, v, j, w)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom l \<sharp> (t, u, v, j, w, sl, m, n, sm, sn)
atom sl \<sharp> (t, u, v, j, w, m, n, sm, sn)
atom m \<sharp> (t, u, v, j, w, n, sm, sn)
atom n \<sharp> (t, u, v, j, w, sm, sn)
atom sm \<sharp> (t, u, v, j, w, sn)
atom sn \<sharp> (t, u, v, j, w)

goal (1 subgoal):
 1. (PrfP t u v)(j::=w) = PrfP (subst j w t) (subst j w u) (subst j w v)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom l \<sharp> (t, u, v, j, w, sl, m, n, sm, sn)
atom sl \<sharp> (t, u, v, j, w, m, n, sm, sn)
atom m \<sharp> (t, u, v, j, w, n, sm, sn)
atom n \<sharp> (t, u, v, j, w, sm, sn)
atom sm \<sharp> (t, u, v, j, w, sn)
atom sn \<sharp> (t, u, v, j, w)

goal (1 subgoal):
 1. (PrfP t u v)(j::=w) = PrfP (subst j w t) (subst j w u) (subst j w v)
[PROOF STEP]
by (simp add: PrfP.simps [of l _ sl m n sm sn])
[PROOF STATE]
proof (state)
this:
(PrfP t u v)(j::=w) = PrfP (subst j w t) (subst j w u) (subst j w v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma PfP_subst [simp]: "(PfP t)(j::=w) = PfP (subst j w t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (PfP t)(j::=w) = PfP (subst j w t)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (PfP t)(j::=w) = PfP (subst j w t)
[PROOF STEP]
obtain k::name and s::name where "atom k \<sharp> (s,t,j,w)" "atom s \<sharp> (t,j,w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k s. \<lbrakk>atom k \<sharp> (s, t, j, w); atom s \<sharp> (t, j, w)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom k \<sharp> (s, t, j, w)
atom s \<sharp> (t, j, w)

goal (1 subgoal):
 1. (PfP t)(j::=w) = PfP (subst j w t)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom k \<sharp> (s, t, j, w)
atom s \<sharp> (t, j, w)

goal (1 subgoal):
 1. (PfP t)(j::=w) = PfP (subst j w t)
[PROOF STEP]
by (auto simp: PfP.simps [of k s])
[PROOF STATE]
proof (state)
this:
(PfP t)(j::=w) = PfP (subst j w t)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extra_axiom_imp_Pf: "Pf \<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e
[PROOF STEP]
have "\<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e \<in> Extra_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e \<in> Extra_ax
[PROOF STEP]
by (simp add: Extra_ax_def) (rule eval_quot_fm_ignore)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e \<in> Extra_ax

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e \<in> Extra_ax

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (force simp add: Pf_def Prf_def Axiom_def intro: BuildSeq_exI)
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>extra_axiom\<guillemotright>\<rbrakk>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma boolean_axioms_imp_Pf:
  assumes "\<alpha> \<in> boolean_axioms" shows "Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
have "\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Sent"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Sent
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in> boolean_axioms

goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Sent
[PROOF STEP]
by (rule boolean_axioms.cases)
       (auto simp: Sent_def Sent_axioms_def quot_Disj quot_Neg q_defs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Sent

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Sent

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (force simp add: Pf_def Prf_def Axiom_def intro: BuildSeq_exI)
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma equality_axioms_imp_Pf:
  assumes "\<alpha> \<in> equality_axioms" shows "Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
have "\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Equality_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Equality_ax
[PROOF STEP]
using assms [unfolded equality_axioms_def]
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in> {refl_ax, eq_cong_ax, mem_cong_ax, eats_cong_ax}

goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Equality_ax
[PROOF STEP]
by (auto simp: Equality_ax_def eval_quot_fm_ignore)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Equality_ax

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Equality_ax

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (force simp add: Pf_def Prf_def Axiom_def intro: BuildSeq_exI)
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma HF_axioms_imp_Pf:
  assumes "\<alpha> \<in> HF_axioms" shows "Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
have "\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> HF_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> HF_ax
[PROOF STEP]
using assms [unfolded HF_axioms_def]
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in> {HF1, HF2}

goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> HF_ax
[PROOF STEP]
by (auto simp: HF_ax_def eval_quot_fm_ignore)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> HF_ax

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> HF_ax

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (force simp add: Pf_def Prf_def Axiom_def intro: BuildSeq_exI)
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma special_axioms_imp_Pf:
  assumes "\<alpha> \<in> special_axioms" shows "Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
have "\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Special_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Special_ax
[PROOF STEP]
by (metis special_axioms_into_Special_ax assms)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Special_ax

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Special_ax

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (force simp add: Pf_def Prf_def Axiom_def intro: BuildSeq_exI)
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma induction_axioms_imp_Pf:
  assumes "\<alpha> \<in> induction_axioms" shows "Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
have "\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Induction_ax"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Induction_ax
[PROOF STEP]
by (metis induction_axioms_into_Induction_ax assms)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Induction_ax

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e \<in> Induction_ax

goal (1 subgoal):
 1. Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (force simp add: Pf_def Prf_def Axiom_def intro: BuildSeq_exI)
[PROOF STATE]
proof (state)
this:
Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ModPon_imp_Pf: "\<lbrakk>Pf \<lbrakk>Q_Imp x y\<rbrakk>e; Pf \<lbrakk>x\<rbrakk>e\<rbrakk> \<Longrightarrow> Pf \<lbrakk>y\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Pf \<lbrakk>Q_Imp x y\<rbrakk>e; Pf \<lbrakk>x\<rbrakk>e\<rbrakk> \<Longrightarrow> Pf \<lbrakk>y\<rbrakk>e
[PROOF STEP]
by (auto simp: Pf_def Prf_def ModPon_def q_defs intro: BuildSeq_combine)


[STATEMENT]
lemma quot_ModPon_imp_Pf: "\<lbrakk>Pf \<lbrakk>\<guillemotleft>\<alpha> IMP \<beta>\<guillemotright>\<rbrakk>e; Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>\<beta>\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Pf \<lbrakk>\<guillemotleft>\<alpha> IMP \<beta>\<guillemotright>\<rbrakk>e; Pf \<lbrakk>\<guillemotleft>\<alpha>\<guillemotright>\<rbrakk>e\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>\<beta>\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (simp add: ModPon_imp_Pf quot_fm_def quot_simps q_defs)


[STATEMENT]
lemma quot_Exists_imp_Pf: "\<lbrakk>Pf \<lbrakk>\<guillemotleft>\<alpha> IMP \<beta>\<guillemotright>\<rbrakk>e; atom i \<sharp> \<beta>\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>Ex i \<alpha> IMP \<beta>\<guillemotright>\<rbrakk>e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Pf \<lbrakk>\<guillemotleft>\<alpha> IMP \<beta>\<guillemotright>\<rbrakk>e; atom i \<sharp> \<beta>\<rbrakk> \<Longrightarrow> Pf \<lbrakk>\<guillemotleft>SyntaxN.Ex i \<alpha> IMP \<beta>\<guillemotright>\<rbrakk>e
[PROOF STEP]
by (force simp: Pf_def Prf_def Exists_def quot_simps q_defs
            intro: BuildSeq_combine AbstForm_trans_fm_eq fresh_imp_VarNonOccForm)