[STATEMENT]
lemma rightInvertible:
(*<*)fixes \<Gamma> :: "'a form multiset"(*>*)

assumes (*<*)rules:(*>*) "R' \<subseteq> upRules \<and> R = Ax \<union> R'"
and   (*<*)a:(*>*) "(\<Gamma> \<Rightarrow>* Compound F Fs,n) \<in> derivable R*"
and   (*<*)b:(*>*) "\<forall> r' \<in> R. rightPrincipal r' (Compound F Fs) \<longrightarrow> (\<Gamma>' \<Rightarrow>* E) \<in> set (fst r')"
and (*<*)nonEm:(*>*) "E \<noteq> Em"
shows "\<exists> m\<le>n. (\<Gamma> +\<Gamma>' \<Rightarrow>* E,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
R' \<subseteq> upRules \<and> R = Ax \<union> R'
( \<Gamma> \<Rightarrow>* Compound F Fs, n) \<in> derivable R*
\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')
E \<noteq> Em

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
proof (induct n arbitrary:\<Gamma> rule:nat_less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n \<Gamma>. \<lbrakk>\<forall>m<n. R' \<subseteq> upRules \<and> R = Ax \<union> R' \<longrightarrow> (\<forall>x. ( x \<Rightarrow>* Compound F Fs, m) \<in> derivable R* \<longrightarrow> (\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')) \<longrightarrow> E \<noteq> Em \<longrightarrow> (\<exists>ma\<le>m. ( x + \<Gamma>' \<Rightarrow>* E, ma) \<in> derivable R*)); R' \<subseteq> upRules \<and> R = Ax \<union> R'; ( \<Gamma> \<Rightarrow>* Compound F Fs, n) \<in> derivable R*; \<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r'); E \<noteq> Em\<rbrakk> \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
case (1 n \<Gamma>)
[PROOF STATE]
proof (state)
this:
\<forall>m<n. R' \<subseteq> upRules \<and> R = Ax \<union> R' \<longrightarrow> (\<forall>x. ( x \<Rightarrow>* Compound F Fs, m) \<in> derivable R* \<longrightarrow> (\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')) \<longrightarrow> E \<noteq> Em \<longrightarrow> (\<exists>ma\<le>m. ( x + \<Gamma>' \<Rightarrow>* E, ma) \<in> derivable R*))
R' \<subseteq> upRules \<and> R = Ax \<union> R'
( \<Gamma> \<Rightarrow>* Compound F Fs, n) \<in> derivable R*
\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')
E \<noteq> Em

goal (1 subgoal):
 1. \<And>n \<Gamma>. \<lbrakk>\<forall>m<n. R' \<subseteq> upRules \<and> R = Ax \<union> R' \<longrightarrow> (\<forall>x. ( x \<Rightarrow>* Compound F Fs, m) \<in> derivable R* \<longrightarrow> (\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')) \<longrightarrow> E \<noteq> Em \<longrightarrow> (\<exists>ma\<le>m. ( x + \<Gamma>' \<Rightarrow>* E, ma) \<in> derivable R*)); R' \<subseteq> upRules \<and> R = Ax \<union> R'; ( \<Gamma> \<Rightarrow>* Compound F Fs, n) \<in> derivable R*; \<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r'); E \<noteq> Em\<rbrakk> \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m<n. R' \<subseteq> upRules \<and> R = Ax \<union> R' \<longrightarrow> (\<forall>x. ( x \<Rightarrow>* Compound F Fs, m) \<in> derivable R* \<longrightarrow> (\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')) \<longrightarrow> E \<noteq> Em \<longrightarrow> (\<exists>ma\<le>m. ( x + \<Gamma>' \<Rightarrow>* E, ma) \<in> derivable R*))
R' \<subseteq> upRules \<and> R = Ax \<union> R'
( \<Gamma> \<Rightarrow>* Compound F Fs, n) \<in> derivable R*
\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')
E \<noteq> Em
[PROOF STEP]
have IH:"\<forall>m<n. \<forall>\<Gamma>. ( \<Gamma> \<Rightarrow>* Compound F Fs, m) \<in> derivable R* \<longrightarrow>
              (\<forall>r' \<in> R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')) \<longrightarrow>
              (\<exists>m'\<le>m. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m') \<in> derivable R*)"
     and a': "(\<Gamma> \<Rightarrow>* Compound F Fs,n) \<in> derivable R*"
     and b': "\<forall> r' \<in> R. rightPrincipal r' (Compound F Fs) \<longrightarrow> (\<Gamma>' \<Rightarrow>* E) \<in> set (fst r')"
[PROOF STATE]
proof (prove)
using this:
\<forall>m<n. R' \<subseteq> upRules \<and> R = Ax \<union> R' \<longrightarrow> (\<forall>x. ( x \<Rightarrow>* Compound F Fs, m) \<in> derivable R* \<longrightarrow> (\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')) \<longrightarrow> E \<noteq> Em \<longrightarrow> (\<exists>ma\<le>m. ( x + \<Gamma>' \<Rightarrow>* E, ma) \<in> derivable R*))
R' \<subseteq> upRules \<and> R = Ax \<union> R'
( \<Gamma> \<Rightarrow>* Compound F Fs, n) \<in> derivable R*
\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')
E \<noteq> Em

goal (1 subgoal):
 1. \<forall>m<n. \<forall>\<Gamma>. ( \<Gamma> \<Rightarrow>* Compound F Fs, m) \<in> derivable R* \<longrightarrow> (\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')) \<longrightarrow> (\<exists>m'\<le>m. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m') \<in> derivable R*) &&& ( \<Gamma> \<Rightarrow>* Compound F Fs, n) \<in> derivable R* &&& \<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>m<n. \<forall>\<Gamma>. ( \<Gamma> \<Rightarrow>* Compound F Fs, m) \<in> derivable R* \<longrightarrow> (\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')) \<longrightarrow> (\<exists>m'\<le>m. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m') \<in> derivable R*)
( \<Gamma> \<Rightarrow>* Compound F Fs, n) \<in> derivable R*
\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')

goal (1 subgoal):
 1. \<And>n \<Gamma>. \<lbrakk>\<forall>m<n. R' \<subseteq> upRules \<and> R = Ax \<union> R' \<longrightarrow> (\<forall>x. ( x \<Rightarrow>* Compound F Fs, m) \<in> derivable R* \<longrightarrow> (\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')) \<longrightarrow> E \<noteq> Em \<longrightarrow> (\<exists>ma\<le>m. ( x + \<Gamma>' \<Rightarrow>* E, ma) \<in> derivable R*)); R' \<subseteq> upRules \<and> R = Ax \<union> R'; ( \<Gamma> \<Rightarrow>* Compound F Fs, n) \<in> derivable R*; \<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r'); E \<noteq> Em\<rbrakk> \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
proof (cases n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 0
[PROOF STEP]
have "(\<Gamma> \<Rightarrow>* Compound F Fs,0) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* Compound F Fs, 0) \<in> derivable R*
[PROOF STEP]
using a'
[PROOF STATE]
proof (prove)
using this:
n = 0
( \<Gamma> \<Rightarrow>* Compound F Fs, n) \<in> derivable R*

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* Compound F Fs, 0) \<in> derivable R*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
( \<Gamma> \<Rightarrow>* Compound F Fs, 0) \<in> derivable R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
( \<Gamma> \<Rightarrow>* Compound F Fs, 0) \<in> derivable R*
[PROOF STEP]
have "([],\<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*"
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> \<Rightarrow>* Compound F Fs, 0) \<in> derivable R*

goal (1 subgoal):
 1. ([],  \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*
[PROOF STEP]
by (cases) (auto)
[PROOF STATE]
proof (state)
this:
([],  \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
([],  \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*
[PROOF STEP]
have "\<exists> r S. extendRule S r = ([],\<Gamma> \<Rightarrow>* Compound F Fs) \<and> (r \<in> Ax \<or> r \<in> R')"
[PROOF STATE]
proof (prove)
using this:
([],  \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*

goal (1 subgoal):
 1. \<exists>r S. extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs) \<and> (r \<in> Ax \<or> r \<in> R')
[PROOF STEP]
using rules and ruleSet[where R'=R' and R=R and Ps="[]" and C="\<Gamma> \<Rightarrow>* Compound F Fs"]
[PROOF STATE]
proof (prove)
using this:
([],  \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*
R' \<subseteq> upRules \<and> R = Ax \<union> R'
\<lbrakk>R' \<subseteq> upRules; R = Ax \<union> R'; ([],  \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*\<rbrakk> \<Longrightarrow> \<exists>S r. extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs) \<and> (r \<in> R' \<or> r \<in> Ax)

goal (1 subgoal):
 1. \<exists>r S. extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs) \<and> (r \<in> Ax \<or> r \<in> R')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r S. extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs) \<and> (r \<in> Ax \<or> r \<in> R')

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r S. extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs) \<and> (r \<in> Ax \<or> r \<in> R')
[PROOF STEP]
obtain r S where "extendRule S r = ([],\<Gamma> \<Rightarrow>* Compound F Fs)" and "r \<in> Ax \<or> r \<in> R'"
[PROOF STATE]
proof (prove)
using this:
\<exists>r S. extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs) \<and> (r \<in> Ax \<or> r \<in> R')

goal (1 subgoal):
 1. (\<And>S r. \<lbrakk>extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs); r \<in> Ax \<or> r \<in> R'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs)
r \<in> Ax \<or> r \<in> R'

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs)
r \<in> Ax \<or> r \<in> R'

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs)
r \<in> Ax \<or> r \<in> R'

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
assume "r \<in> Ax"
[PROOF STATE]
proof (state)
this:
r \<in> Ax

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> Ax
[PROOF STEP]
have "r = ([], \<LM> ff \<RM> \<Rightarrow>* Em)"
[PROOF STATE]
proof (prove)
using this:
r \<in> Ax

goal (1 subgoal):
 1. r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em)
[PROOF STEP]
using characteriseAx[where r=r] and \<open>extendRule S r = ([],\<Gamma> \<Rightarrow>* Compound F Fs)\<close>
[PROOF STATE]
proof (prove)
using this:
r \<in> Ax
r \<in> Ax \<Longrightarrow> r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<or> (\<exists>i. r = ([],  \<LM> At i  \<RM> \<Rightarrow>* At i))
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em)
[PROOF STEP]
by (auto simp add:extendRule_def extend_def)
[PROOF STATE]
proof (state)
this:
r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
with \<open>extendRule S r = ([],\<Gamma> \<Rightarrow>* Compound F Fs)\<close>
[PROOF STATE]
proof (chain)
picking this:
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs)
r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em)
[PROOF STEP]
have "extend S (\<LM> ff \<RM> \<Rightarrow>* Em) = (\<Gamma> \<Rightarrow>* Compound F Fs)"
[PROOF STATE]
proof (prove)
using this:
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs)
r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em)

goal (1 subgoal):
 1. extend S ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* Compound F Fs)
[PROOF STEP]
using extendRule_def[where R="([],\<LM>ff\<RM>\<Rightarrow>* Em)" and forms=S]
[PROOF STATE]
proof (prove)
using this:
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs)
r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em)
extendRule S ([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<equiv> (map (extend S) (fst ([],  \<LM> ff  \<RM> \<Rightarrow>* Em)), extend S (snd ([],  \<LM> ff  \<RM> \<Rightarrow>* Em)))

goal (1 subgoal):
 1. extend S ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* Compound F Fs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extend S ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* Compound F Fs)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
extend S ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* Compound F Fs)
[PROOF STEP]
have "ff \<in># \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
extend S ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. ff \<in># \<Gamma>
[PROOF STEP]
using extendFalsum[where S=S and \<Gamma>=\<Gamma> and \<Delta>="Compound F Fs"]
[PROOF STATE]
proof (prove)
using this:
extend S ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* Compound F Fs)
extend S ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* Compound F Fs) \<Longrightarrow> ff \<in># \<Gamma>

goal (1 subgoal):
 1. ff \<in># \<Gamma>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ff \<in># \<Gamma>

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ff \<in># \<Gamma>
[PROOF STEP]
have "ff \<in># \<Gamma> + \<Gamma>'"
[PROOF STATE]
proof (prove)
using this:
ff \<in># \<Gamma>

goal (1 subgoal):
 1. ff \<in># \<Gamma> + \<Gamma>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ff \<in># \<Gamma> + \<Gamma>'

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ff \<in># \<Gamma> + \<Gamma>'
[PROOF STEP]
have "(\<Gamma> + \<Gamma>' \<Rightarrow>* E,0) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
ff \<in># \<Gamma> + \<Gamma>'

goal (1 subgoal):
 1. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
[PROOF STEP]
using rules
            and containFalsum[where \<Gamma>="\<Gamma> + \<Gamma>'" and R=R]
[PROOF STATE]
proof (prove)
using this:
ff \<in># \<Gamma> + \<Gamma>'
R' \<subseteq> upRules \<and> R = Ax \<union> R'
\<lbrakk>ff \<in># \<Gamma> + \<Gamma>'; Ax \<subseteq> R\<rbrakk> \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* ?C, 0) \<in> derivable R*

goal (1 subgoal):
 1. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
[PROOF STEP]
have "(\<Gamma> + \<Gamma>' \<Rightarrow>* E,0) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*

goal (1 subgoal):
 1. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
r \<in> Ax \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r \<in> Ax \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
r \<in> Ax \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
assume "r \<in> R'"
[PROOF STATE]
proof (state)
this:
r \<in> R'

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> R'
[PROOF STEP]
have "r \<in> upRules"
[PROOF STATE]
proof (prove)
using this:
r \<in> R'

goal (1 subgoal):
 1. r \<in> upRules
[PROOF STEP]
using rules
[PROOF STATE]
proof (prove)
using this:
r \<in> R'
R' \<subseteq> upRules \<and> R = Ax \<union> R'

goal (1 subgoal):
 1. r \<in> upRules
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> upRules

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> upRules
[PROOF STEP]
have "\<exists> Ps C. Ps \<noteq> [] \<and> r = (Ps,C)"
[PROOF STATE]
proof (prove)
using this:
r \<in> upRules

goal (1 subgoal):
 1. \<exists>Ps C. Ps \<noteq> [] \<and> r = (Ps, C)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<in> upRules \<Longrightarrow> \<exists>Ps C. Ps \<noteq> [] \<and> r = (Ps, C)
[PROOF STEP]
obtain x y where "r = (x,y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. r = (x, y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases r)
[PROOF STATE]
proof (state)
this:
r = (x, y)

goal (1 subgoal):
 1. r \<in> upRules \<Longrightarrow> \<exists>Ps C. Ps \<noteq> [] \<and> r = (Ps, C)
[PROOF STEP]
with \<open>r \<in> upRules\<close>
[PROOF STATE]
proof (chain)
picking this:
r \<in> upRules
r = (x, y)
[PROOF STEP]
have "(x,y) \<in> upRules"
[PROOF STATE]
proof (prove)
using this:
r \<in> upRules
r = (x, y)

goal (1 subgoal):
 1. (x, y) \<in> upRules
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x, y) \<in> upRules

goal (1 subgoal):
 1. r \<in> upRules \<Longrightarrow> \<exists>Ps C. Ps \<noteq> [] \<and> r = (Ps, C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> upRules
[PROOF STEP]
obtain Ps where "(Ps :: 'a sequent list) \<noteq> []" and "x=Ps"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> upRules

goal (1 subgoal):
 1. (\<And>Ps. \<lbrakk>Ps \<noteq> []; x = Ps\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases) (auto)
[PROOF STATE]
proof (state)
this:
Ps \<noteq> []
x = Ps

goal (1 subgoal):
 1. r \<in> upRules \<Longrightarrow> \<exists>Ps C. Ps \<noteq> [] \<and> r = (Ps, C)
[PROOF STEP]
with \<open>r = (x,y)\<close>
[PROOF STATE]
proof (chain)
picking this:
r = (x, y)
Ps \<noteq> []
x = Ps
[PROOF STEP]
have "r = (Ps, y)"
[PROOF STATE]
proof (prove)
using this:
r = (x, y)
Ps \<noteq> []
x = Ps

goal (1 subgoal):
 1. r = (Ps, y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r = (Ps, y)

goal (1 subgoal):
 1. r \<in> upRules \<Longrightarrow> \<exists>Ps C. Ps \<noteq> [] \<and> r = (Ps, C)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = (Ps, y)
[PROOF STEP]
show "\<exists> Ps C. Ps \<noteq> [] \<and> r = (Ps,C)"
[PROOF STATE]
proof (prove)
using this:
r = (Ps, y)

goal (1 subgoal):
 1. \<exists>Ps C. Ps \<noteq> [] \<and> r = (Ps, C)
[PROOF STEP]
using \<open>Ps \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
r = (Ps, y)
Ps \<noteq> []

goal (1 subgoal):
 1. \<exists>Ps C. Ps \<noteq> [] \<and> r = (Ps, C)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>Ps C. Ps \<noteq> [] \<and> r = (Ps, C)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Ps C. Ps \<noteq> [] \<and> r = (Ps, C)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Ps C. Ps \<noteq> [] \<and> r = (Ps, C)
[PROOF STEP]
obtain Ps C where "Ps \<noteq> []" and "r = (Ps,C)"
[PROOF STATE]
proof (prove)
using this:
\<exists>Ps C. Ps \<noteq> [] \<and> r = (Ps, C)

goal (1 subgoal):
 1. (\<And>Ps C. \<lbrakk>Ps \<noteq> []; r = (Ps, C)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ps \<noteq> []
r = (Ps, C)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Ps \<noteq> []
r = (Ps, C)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
from \<open>extendRule S r = ([], \<Gamma> \<Rightarrow>* Compound F Fs)\<close>
[PROOF STATE]
proof (chain)
picking this:
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs)
[PROOF STEP]
have "\<exists> S. r = ([],S)"
[PROOF STATE]
proof (prove)
using this:
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. \<exists>S. r = ([], S)
[PROOF STEP]
using extendRule_def[where forms=S and R=r]
[PROOF STATE]
proof (prove)
using this:
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs)
extendRule S r \<equiv> (map (extend S) (fst r), extend S (snd r))

goal (1 subgoal):
 1. \<exists>S. r = ([], S)
[PROOF STEP]
by (cases r) (auto)
[PROOF STATE]
proof (state)
this:
\<exists>S. r = ([], S)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>S. r = ([], S)
[PROOF STEP]
obtain S where "r = ([],S)"
[PROOF STATE]
proof (prove)
using this:
\<exists>S. r = ([], S)

goal (1 subgoal):
 1. (\<And>S. r = ([], S) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r = ([], S)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Ps \<noteq> []
r = (Ps, C)
r = ([], S)
[PROOF STEP]
have "(\<Gamma> + \<Gamma>' \<Rightarrow>* E,0) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
Ps \<noteq> []
r = (Ps, C)
r = ([], S)

goal (1 subgoal):
 1. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
[PROOF STEP]
using rules
[PROOF STATE]
proof (prove)
using this:
Ps \<noteq> []
r = (Ps, C)
r = ([], S)
R' \<subseteq> upRules \<and> R = Ax \<union> R'

goal (1 subgoal):
 1. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
r \<in> R' \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs)
r \<in> Ax \<or> r \<in> R'
r \<in> Ax \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
r \<in> R' \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
[PROOF STEP]
show "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* E,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs)
r \<in> Ax \<or> r \<in> R'
r \<in> Ax \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
r \<in> R' \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
using \<open>n=0\<close>
[PROOF STATE]
proof (prove)
using this:
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Compound F Fs)
r \<in> Ax \<or> r \<in> R'
r \<in> Ax \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
r \<in> R' \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
n = 0

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
case (Suc n')
[PROOF STATE]
proof (state)
this:
n = Suc n'

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = Suc n'
[PROOF STEP]
have "(\<Gamma> \<Rightarrow>* Compound F Fs,n'+1) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
n = Suc n'

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* Compound F Fs, n' + 1) \<in> derivable R*
[PROOF STEP]
using a'
[PROOF STATE]
proof (prove)
using this:
n = Suc n'
( \<Gamma> \<Rightarrow>* Compound F Fs, n) \<in> derivable R*

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* Compound F Fs, n' + 1) \<in> derivable R*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
( \<Gamma> \<Rightarrow>* Compound F Fs, n' + 1) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
( \<Gamma> \<Rightarrow>* Compound F Fs, n' + 1) \<in> derivable R*
[PROOF STEP]
obtain Ps where "(Ps, \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*" and
                          "Ps \<noteq> []" and
                          derv: "\<forall> p \<in> set Ps. \<exists> n\<le>n'. (p,n) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> \<Rightarrow>* Compound F Fs, n' + 1) \<in> derivable R*

goal (1 subgoal):
 1. (\<And>Ps. \<lbrakk>(Ps,  \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*; Ps \<noteq> []; \<forall>p\<in>set Ps. \<exists>n\<le>n'. (p, n) \<in> derivable R*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using characteriseLast[where C="\<Gamma> \<Rightarrow>* Compound F Fs" and m=n' and R="R*"]
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> \<Rightarrow>* Compound F Fs, n' + 1) \<in> derivable R*
( \<Gamma> \<Rightarrow>* Compound F Fs, n' + 1) \<in> derivable R* \<Longrightarrow> \<exists>Ps. Ps \<noteq> [] \<and> (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R* \<and> (\<forall>p\<in>set Ps. \<exists>n\<le>n'. (p, n) \<in> derivable R*)

goal (1 subgoal):
 1. (\<And>Ps. \<lbrakk>(Ps,  \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*; Ps \<noteq> []; \<forall>p\<in>set Ps. \<exists>n\<le>n'. (p, n) \<in> derivable R*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Ps,  \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*
Ps \<noteq> []
\<forall>p\<in>set Ps. \<exists>n\<le>n'. (p, n) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(Ps,  \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*
Ps \<noteq> []
\<forall>p\<in>set Ps. \<exists>n\<le>n'. (p, n) \<in> derivable R*
[PROOF STEP]
have "\<exists> r S. (r \<in> Ax \<or> r \<in> R') \<and> extendRule S r = (Ps, \<Gamma> \<Rightarrow>* Compound F Fs)"
[PROOF STATE]
proof (prove)
using this:
(Ps,  \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*
Ps \<noteq> []
\<forall>p\<in>set Ps. \<exists>n\<le>n'. (p, n) \<in> derivable R*

goal (1 subgoal):
 1. \<exists>r S. (r \<in> Ax \<or> r \<in> R') \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
[PROOF STEP]
using rules and ruleSet[where R'=R' and R=R and Ps=Ps and C="\<Gamma> \<Rightarrow>* Compound F Fs"]
[PROOF STATE]
proof (prove)
using this:
(Ps,  \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*
Ps \<noteq> []
\<forall>p\<in>set Ps. \<exists>n\<le>n'. (p, n) \<in> derivable R*
R' \<subseteq> upRules \<and> R = Ax \<union> R'
\<lbrakk>R' \<subseteq> upRules; R = Ax \<union> R'; (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs) \<in> R*\<rbrakk> \<Longrightarrow> \<exists>S r. extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs) \<and> (r \<in> R' \<or> r \<in> Ax)

goal (1 subgoal):
 1. \<exists>r S. (r \<in> Ax \<or> r \<in> R') \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r S. (r \<in> Ax \<or> r \<in> R') \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>r S. (r \<in> Ax \<or> r \<in> R') \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
[PROOF STEP]
obtain r S where "r \<in> Ax \<or> r \<in> R'" and ext: "extendRule S r = (Ps, \<Gamma> \<Rightarrow>* Compound F Fs)"
[PROOF STATE]
proof (prove)
using this:
\<exists>r S. (r \<in> Ax \<or> r \<in> R') \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. (\<And>r S. \<lbrakk>r \<in> Ax \<or> r \<in> R'; extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> Ax \<or> r \<in> R'
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r \<in> Ax \<or> r \<in> R'
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
r \<in> Ax \<or> r \<in> R'
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
assume "r \<in> Ax"
[PROOF STATE]
proof (state)
this:
r \<in> Ax

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> Ax
[PROOF STEP]
have "fst r = []"
[PROOF STATE]
proof (prove)
using this:
r \<in> Ax

goal (1 subgoal):
 1. fst r = []
[PROOF STEP]
apply (cases r)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>r \<in> Ax; r = (a, b)\<rbrakk> \<Longrightarrow> fst r = []
[PROOF STEP]
by (rule Ax.cases) auto
[PROOF STATE]
proof (state)
this:
fst r = []

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst r = []

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
obtain x y where "r = (x,y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. r = (x, y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases r)
[PROOF STATE]
proof (state)
this:
r = (x, y)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = (x, y)
[PROOF STEP]
have "x \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
r = (x, y)

goal (1 subgoal):
 1. x \<noteq> []
[PROOF STEP]
using \<open>Ps \<noteq> []\<close> and ext
                            and extendRule_def[where forms=S and R=r]
                            and extend_def[where forms=S and seq="snd r"]
[PROOF STATE]
proof (prove)
using this:
r = (x, y)
Ps \<noteq> []
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
extendRule S r \<equiv> (map (extend S) (fst r), extend S (snd r))
extend S (snd r) \<equiv> if succ (snd r) = Em then  antec S + antec (snd r) \<Rightarrow>* succ S else ( antec S + antec (snd r) \<Rightarrow>* succ (snd r))

goal (1 subgoal):
 1. x \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> []

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fst r = []
x \<noteq> []
[PROOF STEP]
have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* E,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
fst r = []
x \<noteq> []

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
using \<open>r=(x,y)\<close>
[PROOF STATE]
proof (prove)
using this:
fst r = []
x \<noteq> []
r = (x, y)

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
r \<in> Ax \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r \<in> Ax \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
r \<in> Ax \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
assume "r \<in> R'"
[PROOF STATE]
proof (state)
this:
r \<in> R'

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
obtain ps c where "r = (ps,c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ps c. r = (ps, c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases r) auto
[PROOF STATE]
proof (state)
this:
r = (ps, c)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = (ps, c)
[PROOF STEP]
have "r \<in> upRules"
[PROOF STATE]
proof (prove)
using this:
r = (ps, c)

goal (1 subgoal):
 1. r \<in> upRules
[PROOF STEP]
using rules and \<open>r \<in> R'\<close>
[PROOF STATE]
proof (prove)
using this:
r = (ps, c)
R' \<subseteq> upRules \<and> R = Ax \<union> R'
r \<in> R'

goal (1 subgoal):
 1. r \<in> upRules
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r \<in> upRules

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> upRules
[PROOF STEP]
have "\<exists> T Ts. c = (\<LM>Compound T Ts\<RM> \<Rightarrow>* Em) \<or> c = (\<Empt> \<Rightarrow>* Compound T Ts)"
[PROOF STATE]
proof (prove)
using this:
r \<in> upRules

goal (1 subgoal):
 1. \<exists>T Ts. c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound T Ts)
[PROOF STEP]
using \<open>r=(ps,c)\<close>
              and upRuleCharacterise[where Ps=ps and C=c]
[PROOF STATE]
proof (prove)
using this:
r \<in> upRules
r = (ps, c)
(ps, c) \<in> upRules \<Longrightarrow> \<exists>F Fs. c = ( \<Empt> \<Rightarrow>* Compound F Fs) \<or> c = ( \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em)

goal (1 subgoal):
 1. \<exists>T Ts. c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound T Ts)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>T Ts. c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound T Ts)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>T Ts. c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound T Ts)
[PROOF STEP]
obtain T Ts where "c = (\<LM>Compound T Ts\<RM> \<Rightarrow>* Em) \<or> c = (\<Empt> \<Rightarrow>* Compound T Ts)"
[PROOF STATE]
proof (prove)
using this:
\<exists>T Ts. c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound T Ts)

goal (1 subgoal):
 1. (\<And>T Ts. c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound T Ts) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound T Ts)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound T Ts)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound T Ts)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
assume "c = (\<Empt> \<Rightarrow>* Compound T Ts)"
[PROOF STATE]
proof (state)
this:
c = ( \<Empt> \<Rightarrow>* Compound T Ts)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
with ext
[PROOF STATE]
proof (chain)
picking this:
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
c = ( \<Empt> \<Rightarrow>* Compound T Ts)
[PROOF STEP]
have "Compound T Ts = Compound F Fs"
[PROOF STATE]
proof (prove)
using this:
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
c = ( \<Empt> \<Rightarrow>* Compound T Ts)

goal (1 subgoal):
 1. Compound T Ts = Compound F Fs
[PROOF STEP]
using \<open>r = (ps,c)\<close>
[PROOF STATE]
proof (prove)
using this:
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
c = ( \<Empt> \<Rightarrow>* Compound T Ts)
r = (ps, c)

goal (1 subgoal):
 1. Compound T Ts = Compound F Fs
[PROOF STEP]
by (auto simp add:extendRule_def extend_def)
[PROOF STATE]
proof (state)
this:
Compound T Ts = Compound F Fs

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Compound T Ts = Compound F Fs
[PROOF STEP]
have "rightPrincipal r (Compound F Fs)"
[PROOF STATE]
proof (prove)
using this:
Compound T Ts = Compound F Fs

goal (1 subgoal):
 1. rightPrincipal r (Compound F Fs)
[PROOF STEP]
using \<open>c = (\<Empt> \<Rightarrow>* Compound T Ts)\<close> and \<open>r = (ps,c)\<close>
[PROOF STATE]
proof (prove)
using this:
Compound T Ts = Compound F Fs
c = ( \<Empt> \<Rightarrow>* Compound T Ts)
r = (ps, c)

goal (1 subgoal):
 1. rightPrincipal r (Compound F Fs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rightPrincipal r (Compound F Fs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rightPrincipal r (Compound F Fs)
[PROOF STEP]
have "(\<Gamma>' \<Rightarrow>* E) \<in> set ps"
[PROOF STATE]
proof (prove)
using this:
rightPrincipal r (Compound F Fs)

goal (1 subgoal):
 1. ( \<Gamma>' \<Rightarrow>* E) \<in> set ps
[PROOF STEP]
using b' and \<open>r = (ps,c)\<close> and \<open>r \<in> R'\<close> and rules
[PROOF STATE]
proof (prove)
using this:
rightPrincipal r (Compound F Fs)
\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')
r = (ps, c)
r \<in> R'
R' \<subseteq> upRules \<and> R = Ax \<union> R'

goal (1 subgoal):
 1. ( \<Gamma>' \<Rightarrow>* E) \<in> set ps
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
( \<Gamma>' \<Rightarrow>* E) \<in> set ps

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
( \<Gamma>' \<Rightarrow>* E) \<in> set ps
[PROOF STEP]
have "extend S (\<Gamma>' \<Rightarrow>* E) \<in> set Ps"
[PROOF STATE]
proof (prove)
using this:
( \<Gamma>' \<Rightarrow>* E) \<in> set ps

goal (1 subgoal):
 1. extend S ( \<Gamma>' \<Rightarrow>* E) \<in> set Ps
[PROOF STEP]
using \<open>extendRule S r = (Ps,\<Gamma> \<Rightarrow>* Compound F Fs)\<close>
                  and \<open>r = (ps,c)\<close>
[PROOF STATE]
proof (prove)
using this:
( \<Gamma>' \<Rightarrow>* E) \<in> set ps
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
r = (ps, c)

goal (1 subgoal):
 1. extend S ( \<Gamma>' \<Rightarrow>* E) \<in> set Ps
[PROOF STEP]
by (simp add:extendContain)
[PROOF STATE]
proof (state)
this:
extend S ( \<Gamma>' \<Rightarrow>* E) \<in> set Ps

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
extend S ( \<Gamma>' \<Rightarrow>* E) \<in> set Ps

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
from \<open>rightPrincipal r (Compound F Fs)\<close>
[PROOF STATE]
proof (chain)
picking this:
rightPrincipal r (Compound F Fs)
[PROOF STEP]
have "c = (\<Empt> \<Rightarrow>* Compound F Fs)"
[PROOF STATE]
proof (prove)
using this:
rightPrincipal r (Compound F Fs)

goal (1 subgoal):
 1. c = ( \<Empt> \<Rightarrow>* Compound F Fs)
[PROOF STEP]
using \<open>r = (ps,c)\<close>
[PROOF STATE]
proof (prove)
using this:
rightPrincipal r (Compound F Fs)
r = (ps, c)

goal (1 subgoal):
 1. c = ( \<Empt> \<Rightarrow>* Compound F Fs)
[PROOF STEP]
by (cases) auto
[PROOF STATE]
proof (state)
this:
c = ( \<Empt> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
with ext
[PROOF STATE]
proof (chain)
picking this:
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
c = ( \<Empt> \<Rightarrow>* Compound F Fs)
[PROOF STEP]
have "antec S = \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
c = ( \<Empt> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. antec S = \<Gamma>
[PROOF STEP]
using \<open>r = (ps,c)\<close>
[PROOF STATE]
proof (prove)
using this:
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
c = ( \<Empt> \<Rightarrow>* Compound F Fs)
r = (ps, c)

goal (1 subgoal):
 1. antec S = \<Gamma>
[PROOF STEP]
by (auto simp add:extendRule_def extend_def)
[PROOF STATE]
proof (state)
this:
antec S = \<Gamma>

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
extend S ( \<Gamma>' \<Rightarrow>* E) \<in> set Ps
antec S = \<Gamma>
[PROOF STEP]
have "(\<Gamma> + \<Gamma>' \<Rightarrow>* E) \<in> set Ps"
[PROOF STATE]
proof (prove)
using this:
extend S ( \<Gamma>' \<Rightarrow>* E) \<in> set Ps
antec S = \<Gamma>

goal (1 subgoal):
 1. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E) \<in> set Ps
[PROOF STEP]
using nonEm
[PROOF STATE]
proof (prove)
using this:
extend S ( \<Gamma>' \<Rightarrow>* E) \<in> set Ps
antec S = \<Gamma>
E \<noteq> Em

goal (1 subgoal):
 1. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E) \<in> set Ps
[PROOF STEP]
by (simp add:extend_def)
[PROOF STATE]
proof (state)
this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E) \<in> set Ps

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E) \<in> set Ps
[PROOF STEP]
have "\<exists> m\<le>n'. (\<Gamma> + \<Gamma>' \<Rightarrow>* E,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E) \<in> set Ps

goal (1 subgoal):
 1. \<exists>m\<le>n'. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
using \<open>\<forall> p \<in> set Ps. \<exists> n\<le>n'. (p,n) \<in> derivable R*\<close>
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E) \<in> set Ps
\<forall>p\<in>set Ps. \<exists>n\<le>n'. (p, n) \<in> derivable R*

goal (1 subgoal):
 1. \<exists>m\<le>n'. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n'. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m\<le>n'. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* E,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
\<exists>m\<le>n'. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
using \<open>n = Suc n'\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>m\<le>n'. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
n = Suc n'

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
by (auto,rule_tac x=m in exI) (simp)
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c = ( \<Empt> \<Rightarrow>* Compound T Ts) \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c = ( \<Empt> \<Rightarrow>* Compound T Ts) \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c = ( \<Empt> \<Rightarrow>* Compound T Ts) \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
assume "c = (\<LM>Compound T Ts\<RM> \<Rightarrow>* Em)"
[PROOF STATE]
proof (state)
this:
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
with ext and \<open>r = (ps,c)\<close>
[PROOF STATE]
proof (chain)
picking this:
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
r = (ps, c)
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em)
[PROOF STEP]
have "Compound T Ts \<in># \<Gamma>"
[PROOF STATE]
proof (prove)
using this:
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
r = (ps, c)
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em)

goal (1 subgoal):
 1. Compound T Ts \<in># \<Gamma>
[PROOF STEP]
by (auto simp add:extendRule_def extend_def)
[PROOF STATE]
proof (state)
this:
Compound T Ts \<in># \<Gamma>

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Compound T Ts \<in># \<Gamma>
[PROOF STEP]
have "\<exists> \<Gamma>1. \<Gamma> = \<Gamma>1 \<oplus> Compound T Ts"
[PROOF STATE]
proof (prove)
using this:
Compound T Ts \<in># \<Gamma>

goal (1 subgoal):
 1. \<exists>\<Gamma>1. \<Gamma> = \<Gamma>1 \<oplus> Compound T Ts
[PROOF STEP]
by (rule_tac x="\<Gamma> \<ominus> Compound T Ts" in exI) (auto simp add:multiset_eq_iff)
[PROOF STATE]
proof (state)
this:
\<exists>\<Gamma>1. \<Gamma> = \<Gamma>1 \<oplus> Compound T Ts

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<Gamma>1. \<Gamma> = \<Gamma>1 \<oplus> Compound T Ts
[PROOF STEP]
obtain \<Gamma>1 where "\<Gamma> = \<Gamma>1 \<oplus> Compound T Ts"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<Gamma>1. \<Gamma> = \<Gamma>1 \<oplus> Compound T Ts

goal (1 subgoal):
 1. (\<And>\<Gamma>1. \<Gamma> = \<Gamma>1 \<oplus> Compound T Ts \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Gamma> = \<Gamma>1 \<oplus> Compound T Ts

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma> = \<Gamma>1 \<oplus> Compound T Ts

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
from \<open>c = (\<LM>Compound T Ts\<RM> \<Rightarrow>* Em)\<close> and \<open>r = (ps,c)\<close> and ext
[PROOF STATE]
proof (chain)
picking this:
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em)
r = (ps, c)
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
[PROOF STEP]
have "succ S = Compound F Fs"
[PROOF STATE]
proof (prove)
using this:
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em)
r = (ps, c)
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. succ S = Compound F Fs
[PROOF STEP]
by (auto simp add:extendRule_def extend_def)
[PROOF STATE]
proof (state)
this:
succ S = Compound F Fs

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> = \<Gamma>1 \<oplus> Compound T Ts
succ S = Compound F Fs
[PROOF STEP]
have "S = (\<Gamma>1 \<Rightarrow>* Compound F Fs)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> = \<Gamma>1 \<oplus> Compound T Ts
succ S = Compound F Fs

goal (1 subgoal):
 1. S = ( \<Gamma>1 \<Rightarrow>* Compound F Fs)
[PROOF STEP]
using ext
                  and \<open>r = (ps,c)\<close> and \<open>c = (\<LM>Compound T Ts\<RM> \<Rightarrow>* Em)\<close>
[PROOF STATE]
proof (prove)
using this:
\<Gamma> = \<Gamma>1 \<oplus> Compound T Ts
succ S = Compound F Fs
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
r = (ps, c)
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em)

goal (1 subgoal):
 1. S = ( \<Gamma>1 \<Rightarrow>* Compound F Fs)
[PROOF STEP]
apply (auto simp add:extendRule_def extend_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> = add_mset (Compound T Ts) (antec S); succ S = Compound F Fs; r = (ps,  \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em); c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em); Ps = map (extend S) ps; \<Gamma>1 = antec S\<rbrakk> \<Longrightarrow> S = ( antec S \<Rightarrow>* Compound F Fs)
[PROOF STEP]
by (cases S) auto
[PROOF STATE]
proof (state)
this:
S = ( \<Gamma>1 \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
with derv
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set Ps. \<exists>n\<le>n'. (p, n) \<in> derivable R*
S = ( \<Gamma>1 \<Rightarrow>* Compound F Fs)
[PROOF STEP]
have pms: "\<forall> p \<in> set ps. \<exists> m\<le>n'. (extend (\<Gamma>1 \<Rightarrow>* Compound F Fs) p,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set Ps. \<exists>n\<le>n'. (p, n) \<in> derivable R*
S = ( \<Gamma>1 \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p, m) \<in> derivable R*
[PROOF STEP]
using ext
                  and \<open>r= (ps,c)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set Ps. \<exists>n\<le>n'. (p, n) \<in> derivable R*
S = ( \<Gamma>1 \<Rightarrow>* Compound F Fs)
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
r = (ps, c)

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p, m) \<in> derivable R*
[PROOF STEP]
by (auto simp add:extendRule_def)
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
have "\<forall> p \<in> set ps. \<exists> m\<le>n'. (extend (\<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
assume "p \<in> set ps"
[PROOF STATE]
proof (state)
this:
p \<in> set ps

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
obtain \<Gamma>i \<delta>i where p: "p = (\<Gamma>i \<Rightarrow>* \<delta>i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<Gamma>i \<delta>i. p = ( \<Gamma>i \<Rightarrow>* \<delta>i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases p) auto
[PROOF STATE]
proof (state)
this:
p = ( \<Gamma>i \<Rightarrow>* \<delta>i)

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
have "\<delta>i = Em \<or> \<delta>i \<noteq> Em"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<delta>i = Em \<or> \<delta>i \<noteq> Em
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<delta>i = Em \<or> \<delta>i \<noteq> Em

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<delta>i = Em \<or> \<delta>i \<noteq> Em

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<delta>i = Em \<or> \<delta>i \<noteq> Em

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
assume "\<delta>i = Em"
[PROOF STATE]
proof (state)
this:
\<delta>i = Em

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<delta>i = Em
[PROOF STEP]
have "extend (\<Gamma>1 \<Rightarrow>* Compound F Fs) p = (\<Gamma>1 + \<Gamma>i \<Rightarrow>* Compound F Fs)"
[PROOF STATE]
proof (prove)
using this:
\<delta>i = Em

goal (1 subgoal):
 1. extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p = ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* Compound F Fs)
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
\<delta>i = Em
p = ( \<Gamma>i \<Rightarrow>* \<delta>i)

goal (1 subgoal):
 1. extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p = ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* Compound F Fs)
[PROOF STEP]
by (auto simp add:extend_def)
[PROOF STATE]
proof (state)
this:
extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p = ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
with pms
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p, m) \<in> derivable R*
extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p = ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* Compound F Fs)
[PROOF STEP]
obtain m where "m \<le>n'" and "(\<Gamma>1 + \<Gamma>i \<Rightarrow>* Compound F Fs,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p, m) \<in> derivable R*
extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p = ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m \<le> n'; ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* Compound F Fs, m) \<in> derivable R*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>p \<in> set ps\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p, m) \<in> derivable R*
extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p = ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* Compound F Fs)
p \<in> set ps

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m \<le> n'; ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* Compound F Fs, m) \<in> derivable R*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m \<le> n'
( \<Gamma>1 + \<Gamma>i \<Rightarrow>* Compound F Fs, m) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
with IH and \<open>n = Suc n'\<close> and b'
[PROOF STATE]
proof (chain)
picking this:
\<forall>m<n. \<forall>\<Gamma>. ( \<Gamma> \<Rightarrow>* Compound F Fs, m) \<in> derivable R* \<longrightarrow> (\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')) \<longrightarrow> (\<exists>m'\<le>m. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m') \<in> derivable R*)
n = Suc n'
\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')
m \<le> n'
( \<Gamma>1 + \<Gamma>i \<Rightarrow>* Compound F Fs, m) \<in> derivable R*
[PROOF STEP]
have "\<exists> m'\<le>m. (\<Gamma>1 + \<Gamma>i + \<Gamma>' \<Rightarrow>* E,m') \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
\<forall>m<n. \<forall>\<Gamma>. ( \<Gamma> \<Rightarrow>* Compound F Fs, m) \<in> derivable R* \<longrightarrow> (\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')) \<longrightarrow> (\<exists>m'\<le>m. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m') \<in> derivable R*)
n = Suc n'
\<forall>r'\<in>R. rightPrincipal r' (Compound F Fs) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* E) \<in> set (fst r')
m \<le> n'
( \<Gamma>1 + \<Gamma>i \<Rightarrow>* Compound F Fs, m) \<in> derivable R*

goal (1 subgoal):
 1. \<exists>m'\<le>m. ( \<Gamma>1 + \<Gamma>i + \<Gamma>' \<Rightarrow>* E, m') \<in> derivable R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m'\<le>m. ( \<Gamma>1 + \<Gamma>i + \<Gamma>' \<Rightarrow>* E, m') \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m'\<le>m. ( \<Gamma>1 + \<Gamma>i + \<Gamma>' \<Rightarrow>* E, m') \<in> derivable R*
[PROOF STEP]
have "\<exists> m\<le>n'. (extend (\<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
\<exists>m'\<le>m. ( \<Gamma>1 + \<Gamma>i + \<Gamma>' \<Rightarrow>* E, m') \<in> derivable R*

goal (1 subgoal):
 1. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
using \<open>m\<le>n'\<close>
                           and p and \<open>\<delta>i = Em\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>m'\<le>m. ( \<Gamma>1 + \<Gamma>i + \<Gamma>' \<Rightarrow>* E, m') \<in> derivable R*
m \<le> n'
p = ( \<Gamma>i \<Rightarrow>* \<delta>i)
\<delta>i = Em

goal (1 subgoal):
 1. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
apply (auto simp add:extend_def union_ac)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m'. \<lbrakk>m \<le> n'; p = ( \<Gamma>i \<Rightarrow>* Em); \<delta>i = Em; m' \<le> m; ( \<Gamma>' + (\<Gamma>1 + \<Gamma>i) \<Rightarrow>* E, m') \<in> derivable R*\<rbrakk> \<Longrightarrow> \<exists>m\<le>n'. ( \<Gamma>' + (\<Gamma>1 + \<Gamma>i) \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
by (rule_tac x="m'" in exI) auto
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<delta>i = Em \<Longrightarrow> \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<delta>i = Em \<Longrightarrow> \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<delta>i = Em \<Longrightarrow> \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
assume "\<delta>i \<noteq> Em"
[PROOF STATE]
proof (state)
this:
\<delta>i \<noteq> Em

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<delta>i \<noteq> Em
[PROOF STEP]
have "extend (\<Gamma>1 \<Rightarrow>* Compound F Fs) p = (\<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i)"
[PROOF STATE]
proof (prove)
using this:
\<delta>i \<noteq> Em

goal (1 subgoal):
 1. extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p = ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i)
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
\<delta>i \<noteq> Em
p = ( \<Gamma>i \<Rightarrow>* \<delta>i)

goal (1 subgoal):
 1. extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p = ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i)
[PROOF STEP]
by (auto simp add:extend_def)
[PROOF STATE]
proof (state)
this:
extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p = ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i)

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
with pms
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p, m) \<in> derivable R*
extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p = ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i)
[PROOF STEP]
obtain m where "m\<le>n'" and "(\<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p, m) \<in> derivable R*
extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p = ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i)

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m \<le> n'; ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i, m) \<in> derivable R*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>p \<in> set ps\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p, m) \<in> derivable R*
extend ( \<Gamma>1 \<Rightarrow>* Compound F Fs) p = ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i)
p \<in> set ps

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m \<le> n'; ( \<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i, m) \<in> derivable R*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m \<le> n'
( \<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i, m) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<le> n'
( \<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i, m) \<in> derivable R*
[PROOF STEP]
have "(\<Gamma>1 + \<Gamma>i + \<Gamma>' \<Rightarrow>* \<delta>i,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
m \<le> n'
( \<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i, m) \<in> derivable R*

goal (1 subgoal):
 1. ( \<Gamma>1 + \<Gamma>i + \<Gamma>' \<Rightarrow>* \<delta>i, m) \<in> derivable R*
[PROOF STEP]
using rules
                           and dpWeak[where \<Gamma>="\<Gamma>1 + \<Gamma>i" and E="\<delta>i" and n=m and R=R and R'=R']
[PROOF STATE]
proof (prove)
using this:
m \<le> n'
( \<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i, m) \<in> derivable R*
R' \<subseteq> upRules \<and> R = Ax \<union> R'
\<lbrakk>( \<Gamma>1 + \<Gamma>i \<Rightarrow>* \<delta>i, m) \<in> derivable R*; R' \<subseteq> upRules; R = Ax \<union> R'\<rbrakk> \<Longrightarrow> ( \<Gamma>1 + \<Gamma>i + ?\<Gamma>' \<Rightarrow>* \<delta>i, m) \<in> derivable R*

goal (1 subgoal):
 1. ( \<Gamma>1 + \<Gamma>i + \<Gamma>' \<Rightarrow>* \<delta>i, m) \<in> derivable R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
( \<Gamma>1 + \<Gamma>i + \<Gamma>' \<Rightarrow>* \<delta>i, m) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
( \<Gamma>1 + \<Gamma>i + \<Gamma>' \<Rightarrow>* \<delta>i, m) \<in> derivable R*
[PROOF STEP]
have "\<exists> m\<le>n'. (extend (\<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
( \<Gamma>1 + \<Gamma>i + \<Gamma>' \<Rightarrow>* \<delta>i, m) \<in> derivable R*

goal (1 subgoal):
 1. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
using \<open>m\<le>n'\<close>
                           and p and \<open>\<delta>i \<noteq> Em\<close>
[PROOF STATE]
proof (prove)
using this:
( \<Gamma>1 + \<Gamma>i + \<Gamma>' \<Rightarrow>* \<delta>i, m) \<in> derivable R*
m \<le> n'
p = ( \<Gamma>i \<Rightarrow>* \<delta>i)
\<delta>i \<noteq> Em

goal (1 subgoal):
 1. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
by (auto simp add:extend_def union_ac)
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<delta>i \<noteq> Em \<Longrightarrow> \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<delta>i = Em \<or> \<delta>i \<noteq> Em
\<delta>i = Em \<Longrightarrow> \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
\<delta>i \<noteq> Em \<Longrightarrow> \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
have "\<exists> m\<le>n'. (extend (\<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
\<delta>i = Em \<or> \<delta>i \<noteq> Em
\<delta>i = Em \<Longrightarrow> \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
\<delta>i \<noteq> Em \<Longrightarrow> \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?p2 \<in> set ps \<Longrightarrow> \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) ?p2, m) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?p2 \<in> set ps \<Longrightarrow> \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) ?p2, m) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
[PROOF STEP]
have "\<forall> p \<in> set (fst (extendRule (\<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r)).
                          \<exists> m\<le>n'. (p,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set (fst (extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r)). \<exists>m\<le>n'. (p, m) \<in> derivable R*
[PROOF STEP]
using \<open>r = (ps,c)\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) p, m) \<in> derivable R*
r = (ps, c)

goal (1 subgoal):
 1. \<forall>p\<in>set (fst (extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r)). \<exists>m\<le>n'. (p, m) \<in> derivable R*
[PROOF STEP]
by (auto simp add:extendRule_def)
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set (fst (extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r)). \<exists>m\<le>n'. (p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>p\<in>set (fst (extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r)). \<exists>m\<le>n'. (p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
have "extendRule (\<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r \<in> R*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r \<in> R*
[PROOF STEP]
using \<open>r \<in> R'\<close> and rules
[PROOF STATE]
proof (prove)
using this:
r \<in> R'
R' \<subseteq> upRules \<and> R = Ax \<union> R'

goal (1 subgoal):
 1. extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r \<in> R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r \<in> R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r \<in> R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
from \<open>S = (\<Gamma>1 \<Rightarrow>* Compound F Fs)\<close> and ext and \<open>c = (\<LM>Compound T Ts\<RM> \<Rightarrow>* Em)\<close>
                 and \<open>\<Gamma> = \<Gamma>1 \<oplus> Compound T Ts\<close> and \<open>r = (ps,c)\<close>
[PROOF STATE]
proof (chain)
picking this:
S = ( \<Gamma>1 \<Rightarrow>* Compound F Fs)
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em)
\<Gamma> = \<Gamma>1 \<oplus> Compound T Ts
r = (ps, c)
[PROOF STEP]
have "extend (\<Gamma>1 + \<Gamma>' \<Rightarrow>* E) (snd r) = (\<Gamma> + \<Gamma>' \<Rightarrow>* E)"
[PROOF STATE]
proof (prove)
using this:
S = ( \<Gamma>1 \<Rightarrow>* Compound F Fs)
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em)
\<Gamma> = \<Gamma>1 \<oplus> Compound T Ts
r = (ps, c)

goal (1 subgoal):
 1. extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) (snd r) = ( \<Gamma> + \<Gamma>' \<Rightarrow>* E)
[PROOF STEP]
by (auto simp add:extend_def union_ac)
[PROOF STATE]
proof (state)
this:
extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) (snd r) = ( \<Gamma> + \<Gamma>' \<Rightarrow>* E)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) (snd r) = ( \<Gamma> + \<Gamma>' \<Rightarrow>* E)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
from ext and \<open>r = (ps,c)\<close> and \<open>Ps \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
r = (ps, c)
Ps \<noteq> []
[PROOF STEP]
have "fst r \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
r = (ps, c)
Ps \<noteq> []

goal (1 subgoal):
 1. fst r \<noteq> []
[PROOF STEP]
by (auto simp add:extendRule_def)
[PROOF STATE]
proof (state)
this:
fst r \<noteq> []

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set (fst (extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r)). \<exists>m\<le>n'. (p, m) \<in> derivable R*
extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r \<in> R*
extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) (snd r) = ( \<Gamma> + \<Gamma>' \<Rightarrow>* E)
fst r \<noteq> []
[PROOF STEP]
have "(\<Gamma> + \<Gamma>' \<Rightarrow>* E,n'+1) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set (fst (extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r)). \<exists>m\<le>n'. (p, m) \<in> derivable R*
extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r \<in> R*
extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) (snd r) = ( \<Gamma> + \<Gamma>' \<Rightarrow>* E)
fst r \<noteq> []

goal (1 subgoal):
 1. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n' + 1) \<in> derivable R*
[PROOF STEP]
using
                 derivable.step[where r="extendRule (\<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r" and m="n'" and R="R*"]
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set (fst (extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r)). \<exists>m\<le>n'. (p, m) \<in> derivable R*
extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r \<in> R*
extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) (snd r) = ( \<Gamma> + \<Gamma>' \<Rightarrow>* E)
fst r \<noteq> []
\<lbrakk>extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r \<in> R*; fst (extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r) \<noteq> []; \<forall>p\<in>set (fst (extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r)). \<exists>n\<le>n'. (p, n) \<in> derivable R*\<rbrakk> \<Longrightarrow> (snd (extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* E) r), n' + 1) \<in> derivable R*

goal (1 subgoal):
 1. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n' + 1) \<in> derivable R*
[PROOF STEP]
by (cases r) (auto simp add:map_is_Nil_conv extendRule_def)
[PROOF STATE]
proof (state)
this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n' + 1) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n' + 1) \<in> derivable R*
[PROOF STEP]
have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* E,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n' + 1) \<in> derivable R*

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
using \<open>n = Suc n'\<close>
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n' + 1) \<in> derivable R*
n = Suc n'

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em) \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound T Ts)
c = ( \<Empt> \<Rightarrow>* Compound T Ts) \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em) \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* E,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound T Ts)
c = ( \<Empt> \<Rightarrow>* Compound T Ts) \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
c = ( \<LM> Compound T Ts  \<RM> \<Rightarrow>* Em) \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
r \<in> R' \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r \<in> Ax \<or> r \<in> R'
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
r \<in> Ax \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
r \<in> R' \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
show "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* E,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
r \<in> Ax \<or> r \<in> R'
extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Compound F Fs)
r \<in> Ax \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
r \<in> R' \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*

goal:
No subgoals!
[PROOF STEP]
qed