[STATEMENT]
lemma SeqStTermP_lemma:
  assumes "atom m \<sharp> (v,i,t,u,s,k,n,sm,sm',sn,sn')" "atom n \<sharp> (v,i,t,u,s,k,sm,sm',sn,sn')"
          "atom sm \<sharp> (v,i,t,u,s,k,sm',sn,sn')" "atom sm' \<sharp> (v,i,t,u,s,k,sn,sn')"
          "atom sn \<sharp> (v,i,t,u,s,k,sn')" "atom sn' \<sharp> (v,i,t,u,s,k)"
    shows "{ SeqStTermP v i t u s k }
           \<turnstile> ((t EQ v AND u EQ i) OR
              ((IndP t OR t NEQ v) AND u EQ t)) OR
              Ex m (Ex n (Ex sm (Ex sm' (Ex sn (Ex sn' (Var m IN k AND Var n IN k AND
                       SeqStTermP v i (Var sm) (Var sm') s (Var m) AND
                       SeqStTermP v i (Var sn) (Var sn') s (Var n) AND
                       t EQ Q_Eats (Var sm) (Var sn) AND
                       u EQ Q_Eats (Var sm') (Var sn')))))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {SeqStTermP v i t u s k} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {SeqStTermP v i t u s k} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
[PROOF STEP]
obtain l::name and sl::name and sl'::name
    where "atom l \<sharp> (v,i,t,u,s,k,sl,sl',m,n,sm,sm',sn,sn')"
          "atom sl \<sharp> (v,i,t,u,s,k,sl',m,n,sm,sm',sn,sn')"
          "atom sl' \<sharp> (v,i,t,u,s,k,m,n,sm,sm',sn,sn')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l sl sl'. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis obtain_fresh)
[PROOF STATE]
proof (state)
this:
atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn')
atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn')
atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn')

goal (1 subgoal):
 1. {SeqStTermP v i t u s k} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn')
atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn')
atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn')

goal (1 subgoal):
 1. {SeqStTermP v i t u s k} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn')
atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn')
atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn')
atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn')
atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn')
atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn')
atom sm' \<sharp> (v, i, t, u, s, k, sn, sn')
atom sn \<sharp> (v, i, t, u, s, k, sn')
atom sn' \<sharp> (v, i, t, u, s, k)

goal (1 subgoal):
 1. {SeqStTermP v i t u s k} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
[PROOF STEP]
apply (simp add: SeqStTermP.simps [of l s k v i sl sl' m n sm sm' sn sn'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {VarP v AND LstSeqP s k (HPair t u) AND All2 l (SUCC k) (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn')))))))))))} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
[PROOF STEP]
apply (rule Conj_EH Ex_EH All2_SUCC_E [THEN rotate2] | simp)+
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {HPair k (HPair (Var sl) (Var sl')) IN s, (Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))), All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl' \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 3. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl' \<sharp> C
 4. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 5. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl \<sharp> C
[PROOF STEP]
apply (rule cut_same [where A = "HPair t u EQ HPair (Var sl) (Var sl')"])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {HPair k (HPair (Var sl) (Var sl')) IN s, (Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))), All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> HPair t u EQ HPair (Var sl) (Var sl')
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {HPair t u EQ HPair (Var sl) (Var sl'), HPair k (HPair (Var sl) (Var sl')) IN s, (Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))), All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 3. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl' \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 4. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl' \<sharp> C
 5. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 6. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl \<sharp> C
[PROOF STEP]
apply (metis Assume AssumeH(4) LstSeqP_EQ)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {HPair t u EQ HPair (Var sl) (Var sl'), HPair k (HPair (Var sl) (Var sl')) IN s, (Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))), All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl' \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 3. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl' \<sharp> C
 4. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 5. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl \<sharp> C
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, (Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))), All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl' \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 3. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl' \<sharp> C
 4. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 5. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl \<sharp> C
[PROOF STEP]
apply (rule Disj_EH)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))), t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 3. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl' \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 4. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl' \<sharp> C
 5. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 6. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl \<sharp> C
[PROOF STEP]
apply (rule Disj_I1)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))), t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 3. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl' \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 4. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl' \<sharp> C
 5. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 6. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl \<sharp> C
[PROOF STEP]
apply (rule anti_deduction)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl IMP t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))), t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 3. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl' \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 4. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl' \<sharp> C
 5. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 6. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl \<sharp> C
[PROOF STEP]
apply (rule Var_Eq_subst_Iff [THEN Sym_L, THEN Iff_MP_same])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl IMP t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t)(sl::=t)
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))), t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 3. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl' \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 4. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl' \<sharp> C
 5. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 6. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl \<sharp> C
[PROOF STEP]
apply (rule Sym_L [THEN rotate2])
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl' EQ u, t EQ Var sl, HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl IMP t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t)(sl::=t)
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))), t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 3. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl' \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 4. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl' \<sharp> C
 5. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 6. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl \<sharp> C
[PROOF STEP]
apply (rule Var_Eq_subst_Iff [THEN Iff_MP_same], force)
    \<comment> \<open>now the quantified case\<close>
    \<comment> \<open>auto could be used but is VERY SLOW\<close>
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))), t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl' \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 3. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl' \<sharp> C
 4. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sl \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 5. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sl \<sharp> C
[PROOF STEP]
apply (rule Ex_EH Conj_EH)+
[PROOF STATE]
proof (prove)
goal (17 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sn' \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 3. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sn' \<sharp> C
 4. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sn \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 5. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sn \<sharp> C
 6. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sm' \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 7. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sm' \<sharp> C
 8. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom sm \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
 9. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> \<forall>C\<in>{t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v}. atom sm \<sharp> C
 10. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom n \<sharp> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
A total of 17 subgoals...
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
[PROOF STEP]
apply (rule Disj_I2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))
[PROOF STEP]
apply (rule Ex_I [where x = "Var m"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn'))))))
[PROOF STEP]
apply (rule Ex_I [where x = "Var n"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))
[PROOF STEP]
apply (rule Ex_I [where x = "Var sm"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn'))))
[PROOF STEP]
apply (rule Ex_I [where x = "Var sm'"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))
[PROOF STEP]
apply (rule Ex_I [where x = "Var sn"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn'))
[PROOF STEP]
apply (rule Ex_I [where x = "Var sn'"], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')
[PROOF STEP]
apply (simp_all add: SeqStTermP.simps [of l s _ v i sl sl' m n sm sm' sn sn'])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> Var m IN k AND Var n IN k AND (VarP v AND LstSeqP s (Var m) (HPair (Var sm) (Var sm')) AND All2 l (SUCC (Var m)) (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn')))))))))))) AND (VarP v AND LstSeqP s (Var n) (HPair (Var sn) (Var sn')) AND All2 l (SUCC (Var n)) (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn')))))))))))) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')
[PROOF STEP]
apply ((rule Conj_I)+, blast intro: LstSeqP_Mem)+
    \<comment> \<open>first SeqStTermP subgoal\<close>
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> All2 l (SUCC (Var m)) (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn')))))))))))
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (VarP v AND LstSeqP s (Var n) (HPair (Var sn) (Var sn')) AND All2 l (SUCC (Var n)) (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn')))))))))))) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')
[PROOF STEP]
apply (rule All2_Subset [OF Hyp], blast)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> SUCC (Var m) SUBS k
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))} \<turnstile> SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))
 3. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom l \<sharp> (SUCC (Var m), k)
 4. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (VarP v AND LstSeqP s (Var n) (HPair (Var sn) (Var sn')) AND All2 l (SUCC (Var n)) (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn')))))))))))) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')
[PROOF STEP]
apply (blast intro!: SUCC_Subset_Ord LstSeqP_OrdP, blast, simp)
    \<comment> \<open>next SeqStTermP subgoal\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> (VarP v AND LstSeqP s (Var n) (HPair (Var sn) (Var sn')) AND All2 l (SUCC (Var n)) (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn')))))))))))) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')
[PROOF STEP]
apply ((rule Conj_I)+, blast intro: LstSeqP_Mem)+
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> All2 l (SUCC (Var n)) (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn')))))))))))
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')
[PROOF STEP]
apply (rule All2_Subset [OF Hyp], blast)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> SUCC (Var n) SUBS k
 2. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))} \<turnstile> SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))
 3. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> atom l \<sharp> (SUCC (Var n), k)
 4. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')
[PROOF STEP]
apply (blast intro!: SUCC_Subset_Ord LstSeqP_OrdP, blast, simp)
    \<comment> \<open>finally, the equality pair\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>atom l \<sharp> (v, i, t, u, s, k, sl, sl', m, n, sm, sm', sn, sn'); atom sl \<sharp> (v, i, t, u, s, k, sl', m, n, sm, sm', sn, sn'); atom sl' \<sharp> (v, i, t, u, s, k, m, n, sm, sm', sn, sn'); atom m \<sharp> (v, i, t, u, s, k, n, sm, sm', sn, sn'); atom n \<sharp> (v, i, t, u, s, k, sm, sm', sn, sn'); atom sm \<sharp> (v, i, t, u, s, k, sm', sn, sn'); atom sm' \<sharp> (v, i, t, u, s, k, sn, sn'); atom sn \<sharp> (v, i, t, u, s, k, sn'); atom sn' \<sharp> (v, i, t, u, s, k)\<rbrakk> \<Longrightarrow> {Var sl EQ Q_Eats (Var sm) (Var sn), Var sl' EQ Q_Eats (Var sm') (Var sn'), HPair (Var n) (HPair (Var sn) (Var sn')) IN s, HPair (Var m) (HPair (Var sm) (Var sm')) IN s, Var n IN k, Var m IN k, t EQ Var sl, u EQ Var sl', HPair k (HPair (Var sl) (Var sl')) IN s, All2 l k (SyntaxN.Ex sl (SyntaxN.Ex sl' (HPair (Var l) (HPair (Var sl) (Var sl')) IN s AND ((Var sl EQ v AND Var sl' EQ i OR (IndP (Var sl) OR Var sl NEQ v) AND Var sl' EQ Var sl) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN Var l AND Var n IN Var l AND HPair (Var m) (HPair (Var sm) (Var sm')) IN s AND HPair (Var n) (HPair (Var sn) (Var sn')) IN s AND Var sl EQ Q_Eats (Var sm) (Var sn) AND Var sl' EQ Q_Eats (Var sm') (Var sn'))))))))))), LstSeqP s k (HPair t u), VarP v} \<turnstile> t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')
[PROOF STEP]
apply (blast intro: Trans)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
{SeqStTermP v i t u s k} \<turnstile> (t EQ v AND u EQ i OR (IndP t OR t NEQ v) AND u EQ t) OR SyntaxN.Ex m (SyntaxN.Ex n (SyntaxN.Ex sm (SyntaxN.Ex sm' (SyntaxN.Ex sn (SyntaxN.Ex sn' (Var m IN k AND Var n IN k AND SeqStTermP v i (Var sm) (Var sm') s (Var m) AND SeqStTermP v i (Var sn) (Var sn') s (Var n) AND t EQ Q_Eats (Var sm) (Var sn) AND u EQ Q_Eats (Var sm') (Var sn')))))))

goal:
No subgoals!
[PROOF STEP]
qed