[STATEMENT]
lemma eval_fmla_correct:
  fixes \<phi> :: "('a :: infinite, 'b) fo_fmla"
  assumes "wf_fo_intp \<phi> I"
  shows "wf \<phi> I (eval_fmla \<phi> I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf \<phi> I (eval_fmla \<phi> I)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp \<phi> I

goal (1 subgoal):
 1. wf \<phi> I (eval_fmla \<phi> I)
[PROOF STEP]
proof (induction \<phi> I rule: eval_fmla.induct)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>r ts I. wf_fo_intp (Pred r ts) I \<Longrightarrow> wf (Pred r ts) I (eval_fmla (Pred r ts) I)
 2. \<And>b I. wf_fo_intp (Bool b) I \<Longrightarrow> wf (Bool b) I (eval_fmla (Bool b) I)
 3. \<And>t t' I. wf_fo_intp (Eqa t t') I \<Longrightarrow> wf (Eqa t t') I (eval_fmla (Eqa t t') I)
 4. \<And>\<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Neg \<phi>) I\<rbrakk> \<Longrightarrow> wf (Neg \<phi>) I (eval_fmla (Neg \<phi>) I)
 5. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 6. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 7. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 8. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
case (1 r ts I)
[PROOF STATE]
proof (state)
this:
wf_fo_intp (Pred r ts) I

goal (8 subgoals):
 1. \<And>r ts I. wf_fo_intp (Pred r ts) I \<Longrightarrow> wf (Pred r ts) I (eval_fmla (Pred r ts) I)
 2. \<And>b I. wf_fo_intp (Bool b) I \<Longrightarrow> wf (Bool b) I (eval_fmla (Bool b) I)
 3. \<And>t t' I. wf_fo_intp (Eqa t t') I \<Longrightarrow> wf (Eqa t t') I (eval_fmla (Eqa t t') I)
 4. \<And>\<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Neg \<phi>) I\<rbrakk> \<Longrightarrow> wf (Neg \<phi>) I (eval_fmla (Neg \<phi>) I)
 5. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 6. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 7. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 8. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_fo_intp (Pred r ts) I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp (Pred r ts) I

goal (1 subgoal):
 1. wf (Pred r ts) I (eval_fmla (Pred r ts) I)
[PROOF STEP]
using fo_abs
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp (Pred r ts) I
finite (?I (?r, length ?ts)) \<Longrightarrow> wf (Pred ?r ?ts) ?I (abs ?ts (?I (?r, length ?ts)))

goal (1 subgoal):
 1. wf (Pred r ts) I (eval_fmla (Pred r ts) I)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf (Pred r ts) I (eval_fmla (Pred r ts) I)

goal (7 subgoals):
 1. \<And>b I. wf_fo_intp (Bool b) I \<Longrightarrow> wf (Bool b) I (eval_fmla (Bool b) I)
 2. \<And>t t' I. wf_fo_intp (Eqa t t') I \<Longrightarrow> wf (Eqa t t') I (eval_fmla (Eqa t t') I)
 3. \<And>\<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Neg \<phi>) I\<rbrakk> \<Longrightarrow> wf (Neg \<phi>) I (eval_fmla (Neg \<phi>) I)
 4. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 5. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 6. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 7. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>b I. wf_fo_intp (Bool b) I \<Longrightarrow> wf (Bool b) I (eval_fmla (Bool b) I)
 2. \<And>t t' I. wf_fo_intp (Eqa t t') I \<Longrightarrow> wf (Eqa t t') I (eval_fmla (Eqa t t') I)
 3. \<And>\<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Neg \<phi>) I\<rbrakk> \<Longrightarrow> wf (Neg \<phi>) I (eval_fmla (Neg \<phi>) I)
 4. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 5. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 6. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 7. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
case (2 b I)
[PROOF STATE]
proof (state)
this:
wf_fo_intp (Bool b) I

goal (7 subgoals):
 1. \<And>b I. wf_fo_intp (Bool b) I \<Longrightarrow> wf (Bool b) I (eval_fmla (Bool b) I)
 2. \<And>t t' I. wf_fo_intp (Eqa t t') I \<Longrightarrow> wf (Eqa t t') I (eval_fmla (Eqa t t') I)
 3. \<And>\<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Neg \<phi>) I\<rbrakk> \<Longrightarrow> wf (Neg \<phi>) I (eval_fmla (Neg \<phi>) I)
 4. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 5. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 6. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 7. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_fo_intp (Bool b) I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp (Bool b) I

goal (1 subgoal):
 1. wf (Bool b) I (eval_fmla (Bool b) I)
[PROOF STEP]
using fo_bool
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp (Bool b) I
wf (Bool ?b) ?I (eval_bool ?b)

goal (1 subgoal):
 1. wf (Bool b) I (eval_fmla (Bool b) I)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf (Bool b) I (eval_fmla (Bool b) I)

goal (6 subgoals):
 1. \<And>t t' I. wf_fo_intp (Eqa t t') I \<Longrightarrow> wf (Eqa t t') I (eval_fmla (Eqa t t') I)
 2. \<And>\<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Neg \<phi>) I\<rbrakk> \<Longrightarrow> wf (Neg \<phi>) I (eval_fmla (Neg \<phi>) I)
 3. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 4. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 5. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 6. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>t t' I. wf_fo_intp (Eqa t t') I \<Longrightarrow> wf (Eqa t t') I (eval_fmla (Eqa t t') I)
 2. \<And>\<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Neg \<phi>) I\<rbrakk> \<Longrightarrow> wf (Neg \<phi>) I (eval_fmla (Neg \<phi>) I)
 3. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 4. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 5. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 6. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
case (3 t t' I)
[PROOF STATE]
proof (state)
this:
wf_fo_intp (Eqa t t') I

goal (6 subgoals):
 1. \<And>t t' I. wf_fo_intp (Eqa t t') I \<Longrightarrow> wf (Eqa t t') I (eval_fmla (Eqa t t') I)
 2. \<And>\<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Neg \<phi>) I\<rbrakk> \<Longrightarrow> wf (Neg \<phi>) I (eval_fmla (Neg \<phi>) I)
 3. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 4. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 5. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 6. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_fo_intp (Eqa t t') I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp (Eqa t t') I

goal (1 subgoal):
 1. wf (Eqa t t') I (eval_fmla (Eqa t t') I)
[PROOF STEP]
using fo_eq
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp (Eqa t t') I
wf (Eqa ?trm ?trm') ?I (eval_eq ?trm ?trm')

goal (1 subgoal):
 1. wf (Eqa t t') I (eval_fmla (Eqa t t') I)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf (Eqa t t') I (eval_fmla (Eqa t t') I)

goal (5 subgoals):
 1. \<And>\<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Neg \<phi>) I\<rbrakk> \<Longrightarrow> wf (Neg \<phi>) I (eval_fmla (Neg \<phi>) I)
 2. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 3. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 4. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 5. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>\<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Neg \<phi>) I\<rbrakk> \<Longrightarrow> wf (Neg \<phi>) I (eval_fmla (Neg \<phi>) I)
 2. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 3. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 4. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 5. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
case (4 \<phi> I)
[PROOF STATE]
proof (state)
this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp (Neg \<phi>) I

goal (5 subgoals):
 1. \<And>\<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Neg \<phi>) I\<rbrakk> \<Longrightarrow> wf (Neg \<phi>) I (eval_fmla (Neg \<phi>) I)
 2. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 3. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 4. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 5. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp (Neg \<phi>) I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp (Neg \<phi>) I

goal (1 subgoal):
 1. wf (Neg \<phi>) I (eval_fmla (Neg \<phi>) I)
[PROOF STEP]
using fo_neg
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp (Neg \<phi>) I
wf ?\<phi> ?I ?t \<Longrightarrow> wf (Neg ?\<phi>) ?I (eval_neg (fv_fo_fmla_list ?\<phi>) ?t)

goal (1 subgoal):
 1. wf (Neg \<phi>) I (eval_fmla (Neg \<phi>) I)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf (Neg \<phi>) I (eval_fmla (Neg \<phi>) I)

goal (4 subgoals):
 1. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 2. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 3. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 4. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 2. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 3. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 4. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
case (5 \<phi> \<psi> I)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Pred ?x11.0 ?x12.0; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Bool ?x2.0; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Eqa ?x31.0 ?x32.0; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Neg ?x4.0; wf_fo_intp ?x4.0 I\<rbrakk> \<Longrightarrow> wf ?x4.0 I (eval_fmla ?x4.0 I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Conj ?x51.0 ?x52.0; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Disj ?x61.0 ?x62.0; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Exists ?x71.0 ?x72.0; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Forall ?x81.0 ?x82.0; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
wf_fo_intp (Conj \<phi> \<psi>) I

goal (4 subgoals):
 1. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 2. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 3. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 4. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
have fins: "wf_fo_intp \<phi> I" "wf_fo_intp \<psi> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fo_intp \<phi> I &&& wf_fo_intp \<psi> I
[PROOF STEP]
using 5(10)
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp (Conj \<phi> \<psi>) I

goal (1 subgoal):
 1. wf_fo_intp \<phi> I &&& wf_fo_intp \<psi> I
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf_fo_intp \<phi> I
wf_fo_intp \<psi> I

goal (4 subgoals):
 1. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 2. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 3. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 4. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
have eval\<phi>: "wf \<phi> I (eval_fmla \<phi> I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf \<phi> I (eval_fmla \<phi> I)
[PROOF STEP]
using 5(1)[OF _ _ fins(1)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)

goal (1 subgoal):
 1. wf \<phi> I (eval_fmla \<phi> I)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf \<phi> I (eval_fmla \<phi> I)

goal (4 subgoals):
 1. \<And>\<phi> \<psi> I. \<lbrakk>\<And>x xa. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); \<And>x xa xb x11 x12. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Pred x11 x12; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x2. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Bool x2; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x31 x32. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Eqa x31 x32; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x4. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Neg x4; wf_fo_intp x4 I\<rbrakk> \<Longrightarrow> wf x4 I (eval_fmla x4 I); \<And>x xa xb x51 x52. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Conj x51 x52; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x61 x62. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Disj x61 x62; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x71 x72. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Exists x71 x72; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); \<And>x xa xb x81 x82. \<lbrakk>x = fv_fo_fmla_list \<phi>; xa = fv_fo_fmla_list \<psi>; xb = eval_fmla \<phi> I; \<psi> = Forall x81 x82; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Conj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 2. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 3. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 4. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
[PROOF STEP]
proof (cases "\<exists>\<psi>'. \<psi> = Neg \<psi>'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 2. \<nexists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>\<psi>'. \<psi> = Neg \<psi>'

goal (2 subgoals):
 1. \<exists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 2. \<nexists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<psi>'. \<psi> = Neg \<psi>'
[PROOF STEP]
obtain \<psi>' where \<psi>_def: "\<psi> = Neg \<psi>'"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<psi>'. \<psi> = Neg \<psi>'

goal (1 subgoal):
 1. (\<And>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<psi> = Neg \<psi>'

goal (2 subgoals):
 1. \<exists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 2. \<nexists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
[PROOF STEP]
have fin: "wf_fo_intp \<psi>' I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fo_intp \<psi>' I
[PROOF STEP]
using fins(2)
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp \<psi> I

goal (1 subgoal):
 1. wf_fo_intp \<psi>' I
[PROOF STEP]
by (auto simp: \<psi>_def)
[PROOF STATE]
proof (state)
this:
wf_fo_intp \<psi>' I

goal (2 subgoals):
 1. \<exists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 2. \<nexists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
[PROOF STEP]
have eval\<psi>': "wf \<psi>' I (eval_fmla \<psi>' I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf \<psi>' I (eval_fmla \<psi>' I)
[PROOF STEP]
using 5(5)[OF _ _ _ \<psi>_def fin]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I\<rbrakk> \<Longrightarrow> wf \<psi>' I (eval_fmla \<psi>' I)

goal (1 subgoal):
 1. wf \<psi>' I (eval_fmla \<psi>' I)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf \<psi>' I (eval_fmla \<psi>' I)

goal (2 subgoals):
 1. \<exists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
 2. \<nexists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
[PROOF STEP]
unfolding \<psi>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (Conj \<phi> (Neg \<psi>')) I (eval_fmla (Conj \<phi> (Neg \<psi>')) I)
[PROOF STEP]
using fo_ajoin[OF eval\<phi> eval\<psi>']
[PROOF STATE]
proof (prove)
using this:
wf (Conj \<phi> (Neg \<psi>')) I (eval_ajoin (fv_fo_fmla_list \<phi>) (eval_fmla \<phi> I) (fv_fo_fmla_list \<psi>') (eval_fmla \<psi>' I))

goal (1 subgoal):
 1. wf (Conj \<phi> (Neg \<psi>')) I (eval_fmla (Conj \<phi> (Neg \<psi>')) I)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)

goal (1 subgoal):
 1. \<nexists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>\<psi>'. \<psi> = Neg \<psi>'

goal (1 subgoal):
 1. \<nexists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<nexists>\<psi>'. \<psi> = Neg \<psi>'
[PROOF STEP]
have eval\<psi>: "wf \<psi> I (eval_fmla \<psi> I)"
[PROOF STATE]
proof (prove)
using this:
\<nexists>\<psi>'. \<psi> = Neg \<psi>'

goal (1 subgoal):
 1. wf \<psi> I (eval_fmla \<psi> I)
[PROOF STEP]
using 5 fins(2)
[PROOF STATE]
proof (prove)
using this:
\<nexists>\<psi>'. \<psi> = Neg \<psi>'
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; wf_fo_intp \<phi> I\<rbrakk> \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Pred ?x11.0 ?x12.0; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Bool ?x2.0; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Eqa ?x31.0 ?x32.0; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Neg ?x4.0; wf_fo_intp ?x4.0 I\<rbrakk> \<Longrightarrow> wf ?x4.0 I (eval_fmla ?x4.0 I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Conj ?x51.0 ?x52.0; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Disj ?x61.0 ?x62.0; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Exists ?x71.0 ?x72.0; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
\<lbrakk>?x = fv_fo_fmla_list \<phi>; ?xa = fv_fo_fmla_list \<psi>; ?xb = eval_fmla \<phi> I; \<psi> = Forall ?x81.0 ?x82.0; wf_fo_intp \<psi> I\<rbrakk> \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
wf_fo_intp (Conj \<phi> \<psi>) I
wf_fo_intp \<psi> I

goal (1 subgoal):
 1. wf \<psi> I (eval_fmla \<psi> I)
[PROOF STEP]
by (cases \<psi>) auto
[PROOF STATE]
proof (state)
this:
wf \<psi> I (eval_fmla \<psi> I)

goal (1 subgoal):
 1. \<nexists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
[PROOF STEP]
have eval: "eval_fmla (Conj \<phi> \<psi>) I = eval_conj (fv_fo_fmla_list \<phi>) (eval_fmla \<phi> I)
      (fv_fo_fmla_list \<psi>) (eval_fmla \<psi> I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval_fmla (Conj \<phi> \<psi>) I = eval_conj (fv_fo_fmla_list \<phi>) (eval_fmla \<phi> I) (fv_fo_fmla_list \<psi>) (eval_fmla \<psi> I)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<nexists>\<psi>'. \<psi> = Neg \<psi>'

goal (1 subgoal):
 1. eval_fmla (Conj \<phi> \<psi>) I = eval_conj (fv_fo_fmla_list \<phi>) (eval_fmla \<phi> I) (fv_fo_fmla_list \<psi>) (eval_fmla \<psi> I)
[PROOF STEP]
by (auto simp: Let_def split: fo_fmla.splits)
[PROOF STATE]
proof (state)
this:
eval_fmla (Conj \<phi> \<psi>) I = eval_conj (fv_fo_fmla_list \<phi>) (eval_fmla \<phi> I) (fv_fo_fmla_list \<psi>) (eval_fmla \<psi> I)

goal (1 subgoal):
 1. \<nexists>\<psi>'. \<psi> = Neg \<psi>' \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
[PROOF STEP]
show "wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
[PROOF STEP]
using fo_conj[OF eval\<phi> eval\<psi>, folded eval] False
[PROOF STATE]
proof (prove)
using this:
case \<psi> of Neg \<psi>' \<Rightarrow> False | _ \<Rightarrow> True \<Longrightarrow> wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
\<nexists>\<psi>'. \<psi> = Neg \<psi>'

goal (1 subgoal):
 1. wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)
[PROOF STEP]
by (auto split: fo_fmla.splits)
[PROOF STATE]
proof (state)
this:
wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wf (Conj \<phi> \<psi>) I (eval_fmla (Conj \<phi> \<psi>) I)

goal (3 subgoals):
 1. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 2. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 3. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 2. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 3. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
case (6 \<phi> \<psi> I)
[PROOF STATE]
proof (state)
this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
wf_fo_intp (Disj \<phi> \<psi>) I

goal (3 subgoals):
 1. \<And>\<phi> \<psi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I); wf_fo_intp (Disj \<phi> \<psi>) I\<rbrakk> \<Longrightarrow> wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
 2. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 3. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
wf_fo_intp (Disj \<phi> \<psi>) I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
wf_fo_intp (Disj \<phi> \<psi>) I

goal (1 subgoal):
 1. wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
[PROOF STEP]
using fo_disj
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp \<psi> I \<Longrightarrow> wf \<psi> I (eval_fmla \<psi> I)
wf_fo_intp (Disj \<phi> \<psi>) I
\<lbrakk>wf ?\<phi> ?I ?t\<phi>; wf ?\<psi> ?I ?t\<psi>\<rbrakk> \<Longrightarrow> wf (Disj ?\<phi> ?\<psi>) ?I (eval_disj (fv_fo_fmla_list ?\<phi>) ?t\<phi> (fv_fo_fmla_list ?\<psi>) ?t\<psi>)

goal (1 subgoal):
 1. wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf (Disj \<phi> \<psi>) I (eval_fmla (Disj \<phi> \<psi>) I)

goal (2 subgoals):
 1. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 2. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 2. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
case (7 i \<phi> I)
[PROOF STATE]
proof (state)
this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp (Exists i \<phi>) I

goal (2 subgoals):
 1. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Exists i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
 2. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp (Exists i \<phi>) I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp (Exists i \<phi>) I

goal (1 subgoal):
 1. wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
[PROOF STEP]
using fo_exists
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp (Exists i \<phi>) I
wf ?\<phi> ?I ?t \<Longrightarrow> wf (Exists ?i ?\<phi>) ?I (eval_exists ?i (fv_fo_fmla_list ?\<phi>) ?t)

goal (1 subgoal):
 1. wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf (Exists i \<phi>) I (eval_fmla (Exists i \<phi>) I)

goal (1 subgoal):
 1. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
case (8 i \<phi> I)
[PROOF STATE]
proof (state)
this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp (Forall i \<phi>) I

goal (1 subgoal):
 1. \<And>i \<phi> I. \<lbrakk>wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I); wf_fo_intp (Forall i \<phi>) I\<rbrakk> \<Longrightarrow> wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp (Forall i \<phi>) I
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp (Forall i \<phi>) I

goal (1 subgoal):
 1. wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
using fo_forall
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp \<phi> I \<Longrightarrow> wf \<phi> I (eval_fmla \<phi> I)
wf_fo_intp (Forall i \<phi>) I
wf ?\<phi> ?I ?t \<Longrightarrow> wf (Forall ?i ?\<phi>) ?I (eval_forall ?i (fv_fo_fmla_list ?\<phi>) ?t)

goal (1 subgoal):
 1. wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wf (Forall i \<phi>) I (eval_fmla (Forall i \<phi>) I)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval_fmla_proj_sat:
  fixes \<phi> :: "('a :: infinite, 'b) fo_fmla"
  assumes "wf_fo_intp \<phi> I"
  shows "rep (eval_fmla \<phi> I) = proj_sat \<phi> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rep (eval_fmla \<phi> I) = proj_sat \<phi> I
[PROOF STEP]
using eval_fmla_correct[OF assms]
[PROOF STATE]
proof (prove)
using this:
wf \<phi> I (eval_fmla \<phi> I)

goal (1 subgoal):
 1. rep (eval_fmla \<phi> I) = proj_sat \<phi> I
[PROOF STEP]
by (auto simp: fo_rep)


[STATEMENT]
lemma eval_sound:
  fixes \<phi> :: "('a :: infinite, 'b) fo_fmla"
  assumes "eval \<phi> I = Fin Z"
  shows "Z = proj_sat \<phi> I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Z = proj_sat \<phi> I
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Z = proj_sat \<phi> I
[PROOF STEP]
have "wf \<phi> I (eval_fmla \<phi> I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf \<phi> I (eval_fmla \<phi> I)
[PROOF STEP]
using eval_fmla_correct assms
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp ?\<phi> ?I \<Longrightarrow> wf ?\<phi> ?I (eval_fmla ?\<phi> ?I)
eval \<phi> I = Fin Z

goal (1 subgoal):
 1. wf \<phi> I (eval_fmla \<phi> I)
[PROOF STEP]
by (auto simp: eval_def split: if_splits)
[PROOF STATE]
proof (state)
this:
wf \<phi> I (eval_fmla \<phi> I)

goal (1 subgoal):
 1. Z = proj_sat \<phi> I
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf \<phi> I (eval_fmla \<phi> I)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf \<phi> I (eval_fmla \<phi> I)

goal (1 subgoal):
 1. Z = proj_sat \<phi> I
[PROOF STEP]
using assms fo_res_fin fo_res_infin
[PROOF STATE]
proof (prove)
using this:
wf \<phi> I (eval_fmla \<phi> I)
eval \<phi> I = Fin Z
\<lbrakk>wf ?\<phi> ?I ?t; finite (rep ?t)\<rbrakk> \<Longrightarrow> res ?t = Fin (rep ?t)
\<lbrakk>wf ?\<phi> ?I ?t; infinite (rep ?t)\<rbrakk> \<Longrightarrow> res ?t = Infin

goal (1 subgoal):
 1. Z = proj_sat \<phi> I
[PROOF STEP]
by (fastforce simp: eval_def fo_rep split: if_splits)
[PROOF STATE]
proof (state)
this:
Z = proj_sat \<phi> I

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eval_complete:
  fixes \<phi> :: "('a :: infinite, 'b) fo_fmla"
  assumes "eval \<phi> I = Infin"
  shows "infinite (proj_sat \<phi> I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite (proj_sat \<phi> I)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite (proj_sat \<phi> I)
[PROOF STEP]
have "wf \<phi> I (eval_fmla \<phi> I)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf \<phi> I (eval_fmla \<phi> I)
[PROOF STEP]
using eval_fmla_correct assms
[PROOF STATE]
proof (prove)
using this:
wf_fo_intp ?\<phi> ?I \<Longrightarrow> wf ?\<phi> ?I (eval_fmla ?\<phi> ?I)
eval \<phi> I = Infin

goal (1 subgoal):
 1. wf \<phi> I (eval_fmla \<phi> I)
[PROOF STEP]
by (auto simp: eval_def split: if_splits)
[PROOF STATE]
proof (state)
this:
wf \<phi> I (eval_fmla \<phi> I)

goal (1 subgoal):
 1. infinite (proj_sat \<phi> I)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
wf \<phi> I (eval_fmla \<phi> I)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
wf \<phi> I (eval_fmla \<phi> I)

goal (1 subgoal):
 1. infinite (proj_sat \<phi> I)
[PROOF STEP]
using assms fo_res_fin
[PROOF STATE]
proof (prove)
using this:
wf \<phi> I (eval_fmla \<phi> I)
eval \<phi> I = Infin
\<lbrakk>wf ?\<phi> ?I ?t; finite (rep ?t)\<rbrakk> \<Longrightarrow> res ?t = Fin (rep ?t)

goal (1 subgoal):
 1. infinite (proj_sat \<phi> I)
[PROOF STEP]
by (auto simp: eval_def fo_rep split: if_splits)
[PROOF STATE]
proof (state)
this:
infinite (proj_sat \<phi> I)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closeSubstI:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "\<And>\<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> (\<Psi>, P[<\<sigma>>], Q[<\<sigma>>]) \<in> Rel"

  shows "(\<Psi>, P, Q) \<in> closeSubst Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Psi>, P, Q) \<in> closeSubst Rel
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wellFormedSubst ?\<sigma> \<Longrightarrow> (\<Psi>, P[<?\<sigma>>], Q[<?\<sigma>>]) \<in> Rel

goal (1 subgoal):
 1. (\<Psi>, P, Q) \<in> closeSubst Rel
[PROOF STEP]
by(unfold closeSubst_def) auto


[STATEMENT]
lemma closeSubstE:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   \<sigma> :: "(name list \<times> 'a list) list"

  assumes "(\<Psi>, P, Q) \<in> closeSubst Rel"
  and     "wellFormedSubst \<sigma>"

  shows "(\<Psi>, P[<\<sigma>>], Q[<\<sigma>>]) \<in> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Psi>, P[<\<sigma>>], Q[<\<sigma>>]) \<in> Rel
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P, Q) \<in> closeSubst Rel
wellFormedSubst \<sigma>

goal (1 subgoal):
 1. (\<Psi>, P[<\<sigma>>], Q[<\<sigma>>]) \<in> Rel
[PROOF STEP]
by(unfold closeSubst_def) auto


[STATEMENT]
lemma closeSubstClosed:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   p :: "name prm"

  assumes "eqvt Rel"
  and     "(\<Psi>, P, Q) \<in> closeSubst Rel"

  shows "(p \<bullet> \<Psi>, p \<bullet> P, p \<bullet> Q) \<in> closeSubst Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<bullet> \<Psi>, p \<bullet> P, p \<bullet> Q) \<in> closeSubst Rel
[PROOF STEP]
proof(rule closeSubstI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> (p \<bullet> \<Psi>, p \<bullet> P[<\<sigma>>], p \<bullet> Q[<\<sigma>>]) \<in> Rel
[PROOF STEP]
fix \<sigma>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> (p \<bullet> \<Psi>, p \<bullet> P[<\<sigma>>], p \<bullet> Q[<\<sigma>>]) \<in> Rel
[PROOF STEP]
assume "wellFormedSubst(\<sigma>::(name list \<times> 'a list) list)"
[PROOF STATE]
proof (state)
this:
wellFormedSubst \<sigma>

goal (1 subgoal):
 1. \<And>\<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> (p \<bullet> \<Psi>, p \<bullet> P[<\<sigma>>], p \<bullet> Q[<\<sigma>>]) \<in> Rel
[PROOF STEP]
with \<open>(\<Psi>, P, Q) \<in> closeSubst Rel\<close> \<open>wellFormedSubst \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P, Q) \<in> closeSubst Rel
wellFormedSubst \<sigma>
wellFormedSubst \<sigma>
[PROOF STEP]
have "(\<Psi>, P[<(rev p \<bullet> \<sigma>)>], Q[<(rev p \<bullet> \<sigma>)>]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P, Q) \<in> closeSubst Rel
wellFormedSubst \<sigma>
wellFormedSubst \<sigma>

goal (1 subgoal):
 1. (\<Psi>, P[<rev p \<bullet> \<sigma>>], Q[<rev p \<bullet> \<sigma>>]) \<in> Rel
[PROOF STEP]
by(rule_tac closeSubstE) auto
[PROOF STATE]
proof (state)
this:
(\<Psi>, P[<rev p \<bullet> \<sigma>>], Q[<rev p \<bullet> \<sigma>>]) \<in> Rel

goal (1 subgoal):
 1. \<And>\<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> (p \<bullet> \<Psi>, p \<bullet> P[<\<sigma>>], p \<bullet> Q[<\<sigma>>]) \<in> Rel
[PROOF STEP]
hence "(p \<bullet> \<Psi>, p \<bullet> (P[<(rev p \<bullet> \<sigma>)>]), p \<bullet> (Q[<(rev p \<bullet> \<sigma>)>])) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P[<rev p \<bullet> \<sigma>>], Q[<rev p \<bullet> \<sigma>>]) \<in> Rel

goal (1 subgoal):
 1. (p \<bullet> \<Psi>, p \<bullet> P[<rev p \<bullet> \<sigma>>], p \<bullet> Q[<rev p \<bullet> \<sigma>>]) \<in> Rel
[PROOF STEP]
by(drule_tac p=p in eqvtI[OF \<open>eqvt Rel\<close>]) (simp add: eqvts)
[PROOF STATE]
proof (state)
this:
(p \<bullet> \<Psi>, p \<bullet> P[<rev p \<bullet> \<sigma>>], p \<bullet> Q[<rev p \<bullet> \<sigma>>]) \<in> Rel

goal (1 subgoal):
 1. \<And>\<sigma>. wellFormedSubst \<sigma> \<Longrightarrow> (p \<bullet> \<Psi>, p \<bullet> P[<\<sigma>>], p \<bullet> Q[<\<sigma>>]) \<in> Rel
[PROOF STEP]
thus "(p \<bullet> \<Psi>, (p \<bullet> P)[<\<sigma>>], (p \<bullet> Q)[<\<sigma>>]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> \<Psi>, p \<bullet> P[<rev p \<bullet> \<sigma>>], p \<bullet> Q[<rev p \<bullet> \<sigma>>]) \<in> Rel

goal (1 subgoal):
 1. (p \<bullet> \<Psi>, p \<bullet> P[<\<sigma>>], p \<bullet> Q[<\<sigma>>]) \<in> Rel
[PROOF STEP]
by(simp del: seqSubs_def add: eqvts)
[PROOF STATE]
proof (state)
this:
(p \<bullet> \<Psi>, p \<bullet> P[<\<sigma>>], p \<bullet> Q[<\<sigma>>]) \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closeSubstEqvt:
  assumes "eqvt Rel"

  shows "eqvt(closeSubst Rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt (closeSubst Rel)
[PROOF STEP]
proof(auto simp add: eqvt_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b p. (a, aa, b) \<in> closeSubst Rel \<Longrightarrow> (p \<bullet> a, p \<bullet> aa, p \<bullet> b) \<in> closeSubst Rel
[PROOF STEP]
fix \<Psi> P Q p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa b p. (a, aa, b) \<in> closeSubst Rel \<Longrightarrow> (p \<bullet> a, p \<bullet> aa, p \<bullet> b) \<in> closeSubst Rel
[PROOF STEP]
assume "(\<Psi>, P, Q) \<in> closeSubst Rel"
[PROOF STATE]
proof (state)
this:
(\<Psi>, P, Q) \<in> closeSubst Rel

goal (1 subgoal):
 1. \<And>a aa b p. (a, aa, b) \<in> closeSubst Rel \<Longrightarrow> (p \<bullet> a, p \<bullet> aa, p \<bullet> b) \<in> closeSubst Rel
[PROOF STEP]
thus "((p::name prm) \<bullet> \<Psi>, p \<bullet> P, p \<bullet> Q) \<in> closeSubst Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P, Q) \<in> closeSubst Rel

goal (1 subgoal):
 1. (p \<bullet> \<Psi>, p \<bullet> P, p \<bullet> Q) \<in> closeSubst Rel
[PROOF STEP]
by(drule_tac p=p in closeSubstClosed[OF \<open>eqvt Rel\<close>]) (simp add: eqvts)
[PROOF STATE]
proof (state)
this:
(p \<bullet> \<Psi>, p \<bullet> P, p \<bullet> Q) \<in> closeSubst Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma closeSubstUnfold:
  fixes \<Psi> :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   \<sigma> :: "(name list \<times> 'a list) list"

  assumes "(\<Psi>, P, Q) \<in> closeSubst Rel"
  and     "wellFormedSubst \<sigma>"

  shows "(\<Psi>, P[<\<sigma>>], Q[<\<sigma>>]) \<in> closeSubst Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Psi>, P[<\<sigma>>], Q[<\<sigma>>]) \<in> closeSubst Rel
[PROOF STEP]
proof(rule closeSubstI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>'. wellFormedSubst \<sigma>' \<Longrightarrow> (\<Psi>, P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel
[PROOF STEP]
fix \<sigma>'::"(name list \<times> 'a list) list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<sigma>'. wellFormedSubst \<sigma>' \<Longrightarrow> (\<Psi>, P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel
[PROOF STEP]
assume "wellFormedSubst \<sigma>'"
[PROOF STATE]
proof (state)
this:
wellFormedSubst \<sigma>'

goal (1 subgoal):
 1. \<And>\<sigma>'. wellFormedSubst \<sigma>' \<Longrightarrow> (\<Psi>, P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel
[PROOF STEP]
with \<open>wellFormedSubst \<sigma>\<close>
[PROOF STATE]
proof (chain)
picking this:
wellFormedSubst \<sigma>
wellFormedSubst \<sigma>'
[PROOF STEP]
have "wellFormedSubst(\<sigma>@\<sigma>')"
[PROOF STATE]
proof (prove)
using this:
wellFormedSubst \<sigma>
wellFormedSubst \<sigma>'

goal (1 subgoal):
 1. wellFormedSubst (\<sigma> @ \<sigma>')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wellFormedSubst (\<sigma> @ \<sigma>')

goal (1 subgoal):
 1. \<And>\<sigma>'. wellFormedSubst \<sigma>' \<Longrightarrow> (\<Psi>, P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel
[PROOF STEP]
with \<open>(\<Psi>, P, Q) \<in> closeSubst Rel\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P, Q) \<in> closeSubst Rel
wellFormedSubst (\<sigma> @ \<sigma>')
[PROOF STEP]
have "(\<Psi>, P[<(\<sigma>@\<sigma>')>], Q[<(\<sigma>@\<sigma>')>]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P, Q) \<in> closeSubst Rel
wellFormedSubst (\<sigma> @ \<sigma>')

goal (1 subgoal):
 1. (\<Psi>, P[<(\<sigma> @ \<sigma>')>], Q[<(\<sigma> @ \<sigma>')>]) \<in> Rel
[PROOF STEP]
by(rule closeSubstE)
[PROOF STATE]
proof (state)
this:
(\<Psi>, P[<(\<sigma> @ \<sigma>')>], Q[<(\<sigma> @ \<sigma>')>]) \<in> Rel

goal (1 subgoal):
 1. \<And>\<sigma>'. wellFormedSubst \<sigma>' \<Longrightarrow> (\<Psi>, P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel
[PROOF STEP]
thus "(\<Psi>, P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P[<(\<sigma> @ \<sigma>')>], Q[<(\<sigma> @ \<sigma>')>]) \<in> Rel

goal (1 subgoal):
 1. (\<Psi>, P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Psi>, P[<\<sigma>>][<\<sigma>'>], Q[<\<sigma>>][<\<sigma>'>]) \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Fvars_tm_simps[simp]:
  "Fvars Zero = {}"
  "Fvars (Var a) = {a}"
  "Fvars (Eats x y) = Fvars x \<union> Fvars y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fvars Zero = {} &&& Fvars (Var a) = {a} &&& Fvars (Eats x y) = Fvars x \<union> Fvars y
[PROOF STEP]
by (auto simp: Fvars_def fresh_at_base(2))


[STATEMENT]
lemma finite_Fvars_tm[simp]:
  fixes t :: tm
  shows "finite (Fvars t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Fvars t)
[PROOF STEP]
by (induct t rule: tm.induct) auto


[STATEMENT]
lemma Fvars_fm_simps[simp]:
  "Fvars (x IN y) = Fvars x \<union> Fvars y"
  "Fvars (x EQ y) = Fvars x \<union> Fvars y"
  "Fvars (A OR B) = Fvars A \<union> Fvars B"
  "Fvars (A AND B) = Fvars A \<union> Fvars B"
  "Fvars (A IMP B) = Fvars A \<union> Fvars B"
  "Fvars Fls = {}"
  "Fvars (Neg A) = Fvars A"
  "Fvars (Ex a A) = Fvars A - {a}"
  "Fvars (All a A) = Fvars A - {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((Fvars (x IN y) = Fvars x \<union> Fvars y &&& Fvars (x EQ y) = Fvars x \<union> Fvars y) &&& Fvars (A OR B) = Fvars A \<union> Fvars B &&& Fvars (A AND B) = Fvars A \<union> Fvars B) &&& (Fvars (A IMP B) = Fvars A \<union> Fvars B &&& Fvars Fls = {}) &&& Fvars (Neg A) = Fvars A &&& Fvars (SyntaxN.Ex a A) = Fvars A - {a} &&& Fvars (SyntaxN.All a A) = Fvars A - {a}
[PROOF STEP]
by (auto simp: Fvars_def fresh_at_base(2))


[STATEMENT]
lemma finite_Fvars_fm[simp]:
  fixes A :: fm
  shows "finite (Fvars A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Fvars A)
[PROOF STEP]
by (induct A rule: fm.induct) auto


[STATEMENT]
lemma subst_tm_subst_tm[simp]:
  "x \<noteq> y \<Longrightarrow> atom x \<sharp> u \<Longrightarrow> subst y u (subst x t v) = subst x (subst y u t) (subst y u v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; atom x \<sharp> u\<rbrakk> \<Longrightarrow> subst y u (subst x t v) = subst x (subst y u t) (subst y u v)
[PROOF STEP]
by (induct v rule: tm.induct) auto


[STATEMENT]
lemma subst_fm_subst_fm[simp]:
  "x \<noteq> y \<Longrightarrow> atom x \<sharp> u \<Longrightarrow> (A(x::=t))(y::=u) = (A(y::=u))(x::=subst y u t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; atom x \<sharp> u\<rbrakk> \<Longrightarrow> (A(x::=t))(y::=u) = (A(y::=u))(x::=subst y u t)
[PROOF STEP]
by (nominal_induct A avoiding: x t y u rule: fm.strong_induct) auto


[STATEMENT]
lemma Fvars_ground_aux: "Fvars t \<subseteq> B \<Longrightarrow> ground_aux t (atom ` B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fvars t \<subseteq> B \<Longrightarrow> ground_aux t (atom ` B)
[PROOF STEP]
by (induct t rule: tm.induct) auto


[STATEMENT]
lemma ground_Fvars: "ground t \<longleftrightarrow> Fvars t = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground t = (Fvars t = {})
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ground t \<Longrightarrow> Fvars t = {}
 2. Fvars t = {} \<Longrightarrow> ground t
[PROOF STEP]
apply (auto simp only: Fvars_def ground_fresh) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fvars t = {} \<Longrightarrow> ground t
[PROOF STEP]
apply (auto intro: Fvars_ground_aux[of t "{}", simplified])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Fvars_ground_fm_aux: "Fvars A \<subseteq> B \<Longrightarrow> ground_fm_aux A (atom ` B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fvars A \<subseteq> B \<Longrightarrow> ground_fm_aux A (atom ` B)
[PROOF STEP]
apply (induct A arbitrary: B rule: fm.induct)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x1 x2 B. Fvars (x1 IN x2) \<subseteq> B \<Longrightarrow> ground_fm_aux (x1 IN x2) (atom ` B)
 2. \<And>x1 x2 B. Fvars (x1 EQ x2) \<subseteq> B \<Longrightarrow> ground_fm_aux (x1 EQ x2) (atom ` B)
 3. \<And>x1 x2 B. \<lbrakk>\<And>B. Fvars x1 \<subseteq> B \<Longrightarrow> ground_fm_aux x1 (atom ` B); \<And>B. Fvars x2 \<subseteq> B \<Longrightarrow> ground_fm_aux x2 (atom ` B); Fvars (x1 OR x2) \<subseteq> B\<rbrakk> \<Longrightarrow> ground_fm_aux (x1 OR x2) (atom ` B)
 4. \<And>x B. \<lbrakk>\<And>B. Fvars x \<subseteq> B \<Longrightarrow> ground_fm_aux x (atom ` B); Fvars (Neg x) \<subseteq> B\<rbrakk> \<Longrightarrow> ground_fm_aux (Neg x) (atom ` B)
 5. \<And>x1 x2 B. \<lbrakk>\<And>B. Fvars x2 \<subseteq> B \<Longrightarrow> ground_fm_aux x2 (atom ` B); Fvars (SyntaxN.Ex x1 x2) \<subseteq> B\<rbrakk> \<Longrightarrow> ground_fm_aux (SyntaxN.Ex x1 x2) (atom ` B)
[PROOF STEP]
apply (auto simp: Diff_subset_conv Fvars_ground_aux)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 B. \<lbrakk>\<And>B. Fvars x2 \<subseteq> B \<Longrightarrow> ground_fm_aux x2 (atom ` B); Fvars x2 \<subseteq> insert x1 B\<rbrakk> \<Longrightarrow> ground_fm_aux x2 (insert (atom x1) (atom ` B))
[PROOF STEP]
apply (drule meta_spec, drule meta_mp, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 B. \<lbrakk>Fvars x2 \<subseteq> insert x1 B; ground_fm_aux x2 (atom ` insert x1 B)\<rbrakk> \<Longrightarrow> ground_fm_aux x2 (insert (atom x1) (atom ` B))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma ground_fm_Fvars: "ground_fm A \<longleftrightarrow> Fvars A = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground_fm A = (Fvars A = {})
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ground_fm A \<Longrightarrow> Fvars A = {}
 2. Fvars A = {} \<Longrightarrow> ground_fm A
[PROOF STEP]
apply (auto simp only: Fvars_def ground_fresh) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fvars A = {} \<Longrightarrow> ground_fm A
[PROOF STEP]
apply (auto intro: Fvars_ground_fm_aux[of A "{}", simplified])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma coding_tm_Fvars_empty[simp]: "coding_tm t \<Longrightarrow> Fvars t = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coding_tm t \<Longrightarrow> Fvars t = {}
[PROOF STEP]
by (induct t rule: coding_tm.induct) (auto simp: Fvars_def)


[STATEMENT]
lemma Fvars_empty_ground[simp]: "Fvars t = {} \<Longrightarrow> ground t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fvars t = {} \<Longrightarrow> ground t
[PROOF STEP]
by (induct t rule: tm.induct) auto


[STATEMENT]
theorem Goedel_II: "\<not> {} \<turnstile> Fls \<Longrightarrow> \<not> {} \<turnstile> neg (PfP \<guillemotleft>Fls\<guillemotright>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> {} \<turnstile> Fls \<Longrightarrow> \<not> {} \<turnstile> neg (PfP \<guillemotleft>Fls\<guillemotright>)
[PROOF STEP]
by (rule g2.goedel_second[unfolded consistent_def PP_def PfP_subst subst.simps simp_thms if_True])


[STATEMENT]
lemma ground_fm_PrfP[simp]:
  "ground_fm (PrfP s k t) \<longleftrightarrow> ground s \<and> ground k \<and> ground t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground_fm (PrfP s k t) = (ground s \<and> ground k \<and> ground t)
[PROOF STEP]
by (auto simp add: ground_aux_def ground_fm_aux_def supp_conv_fresh)


[STATEMENT]
lemma Fvars_HPair[simp]: "Fvars (HPair t u) = Fvars t \<union> Fvars u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fvars (HPair t u) = Fvars t \<union> Fvars u
[PROOF STEP]
unfolding Fvars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a. \<not> atom a \<sharp> HPair t u} = {a. \<not> atom a \<sharp> t} \<union> {a. \<not> atom a \<sharp> u}
[PROOF STEP]
by auto


[STATEMENT]
lemma ground_HPair[simp]: "ground (HPair t u) \<longleftrightarrow> ground t \<and> ground u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground (HPair t u) = (ground t \<and> ground u)
[PROOF STEP]
unfolding ground_Fvars
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Fvars (HPair t u) = {}) = (Fvars t = {} \<and> Fvars u = {})
[PROOF STEP]
by auto


[STATEMENT]
lemma neg_Neg:
  "{} \<turnstile> neg \<phi> IFF Neg \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> neg \<phi> IFF Neg \<phi>
[PROOF STEP]
unfolding neg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<turnstile> (\<phi> IMP Fls) IFF Neg \<phi>
[PROOF STEP]
by (auto simp: Fls_def intro: ContraAssume)


[STATEMENT]
lemma ground_aux_mono: "A \<subseteq> B \<Longrightarrow> ground_aux t A \<Longrightarrow> ground_aux t B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> B; ground_aux t A\<rbrakk> \<Longrightarrow> ground_aux t B
[PROOF STEP]
unfolding ground_aux_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<subseteq> B; supp t \<subseteq> A\<rbrakk> \<Longrightarrow> supp t \<subseteq> B
[PROOF STEP]
by auto


[STATEMENT]
theorem Goedel_I: "\<exists>\<phi>. \<not> {} \<turnstile> \<phi> \<and> \<not> {} \<turnstile> Neg \<phi> \<and> eval_fm e0 \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<phi>. \<not> {} \<turnstile> \<phi> \<and> \<not> {} \<turnstile> Neg \<phi> \<and> eval_fm e0 \<phi>
[PROOF STEP]
by (meson Iff_MP2_same g1.recover_proofs.goedel_first_classic_strong[OF consistent] neg_Neg)


[STATEMENT]
theorem Goedel_I': "\<exists>\<phi>. \<not> {} \<turnstile> \<phi> \<and> \<not> {} \<turnstile> Neg \<phi> \<and> isTrue \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<phi>. \<not> {} \<turnstile> \<phi> \<and> \<not> {} \<turnstile> Neg \<phi> \<and> isTrue \<phi>
[PROOF STEP]
by (meson Iff_MP2_same g1'.goedel_first_classic_strong[OF consistent] neg_Neg)


[STATEMENT]
lemma prefix_finI_item[intro!]:
    assumes "a = b" "u \<le> v"
    shows "a # u \<le> b # v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a # u \<le> b # v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = b
u \<le> v

goal (1 subgoal):
 1. a # u \<le> b # v
[PROOF STEP]
by force


[STATEMENT]
lemma prefix_finE_item[elim!]:
    assumes "a # u \<le> b # v"
    obtains "a = b" "u \<le> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>a = b; u \<le> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a # u \<le> b # v

goal (1 subgoal):
 1. (\<lbrakk>a = b; u \<le> v\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force


[STATEMENT]
lemma prefix_fin_append[intro]: "u \<le> u @ v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<le> u @ v
[PROOF STEP]
by auto


[STATEMENT]
lemma pprefix_fin_length[dest]:
    assumes "u < v"
    shows "length u < length v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length u < length v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length u < length v
[PROOF STEP]
obtain a w where 1: "v = u @ a # w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a w. v = u @ a # w \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u < v

goal (1 subgoal):
 1. (\<And>a w. v = u @ a # w \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
v = u @ a # w

goal (1 subgoal):
 1. length u < length v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length u < length v
[PROOF STEP]
unfolding 1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length u < length (u @ a # w)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length u < length v

goal:
No subgoals!
[PROOF STEP]
qed