[STATEMENT]
lemma dpWeakR:
assumes (*<*)a:(*>*)"(\<Gamma> \<Rightarrow>* Em,n) \<in> derivable R*"
and  (*<*)b:(*>*) "R' \<subseteq> upRules"
and  (*<*)c:(*>*) "R = Ax \<union> R'"
shows "(\<Gamma> \<Rightarrow>* C,n) \<in> derivable R*"   \<comment> \<open>Proof omitted\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> \<Rightarrow>* Em, n) \<in> derivable R*

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, n) \<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. \<forall>x. ( x \<Rightarrow>* Em, m) \<in> derivable R* \<longrightarrow> ( x \<Rightarrow>* C, m) \<in> derivable R*; ( \<Gamma> \<Rightarrow>* Em, n) \<in> derivable R*\<rbrakk> \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
case (1 n \<Gamma>)
[PROOF STATE]
proof (state)
this:
\<forall>m<n. \<forall>x. ( x \<Rightarrow>* Em, m) \<in> derivable R* \<longrightarrow> ( x \<Rightarrow>* C, m) \<in> derivable R*
( \<Gamma> \<Rightarrow>* Em, n) \<in> derivable R*

goal (1 subgoal):
 1. \<And>n \<Gamma>. \<lbrakk>\<forall>m<n. \<forall>x. ( x \<Rightarrow>* Em, m) \<in> derivable R* \<longrightarrow> ( x \<Rightarrow>* C, m) \<in> derivable R*; ( \<Gamma> \<Rightarrow>* Em, n) \<in> derivable R*\<rbrakk> \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>m<n. \<forall>x. ( x \<Rightarrow>* Em, m) \<in> derivable R* \<longrightarrow> ( x \<Rightarrow>* C, m) \<in> derivable R*
( \<Gamma> \<Rightarrow>* Em, n) \<in> derivable R*
[PROOF STEP]
have IH: "\<forall>m<n. \<forall> \<Gamma>. ( \<Gamma> \<Rightarrow>* Em, m) \<in> derivable R* \<longrightarrow> ( \<Gamma> \<Rightarrow>* C, m) \<in> derivable R*"
      and a': "( \<Gamma> \<Rightarrow>* Em, n) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
\<forall>m<n. \<forall>x. ( x \<Rightarrow>* Em, m) \<in> derivable R* \<longrightarrow> ( x \<Rightarrow>* C, m) \<in> derivable R*
( \<Gamma> \<Rightarrow>* Em, n) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>m<n. \<forall>\<Gamma>. ( \<Gamma> \<Rightarrow>* Em, m) \<in> derivable R* \<longrightarrow> ( \<Gamma> \<Rightarrow>* C, m) \<in> derivable R* &&& ( \<Gamma> \<Rightarrow>* Em, n) \<in> derivable R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>m<n. \<forall>\<Gamma>. ( \<Gamma> \<Rightarrow>* Em, m) \<in> derivable R* \<longrightarrow> ( \<Gamma> \<Rightarrow>* C, m) \<in> derivable R*
( \<Gamma> \<Rightarrow>* Em, n) \<in> derivable R*

goal (1 subgoal):
 1. \<And>n \<Gamma>. \<lbrakk>\<forall>m<n. \<forall>x. ( x \<Rightarrow>* Em, m) \<in> derivable R* \<longrightarrow> ( x \<Rightarrow>* C, m) \<in> derivable R*; ( \<Gamma> \<Rightarrow>* Em, n) \<in> derivable R*\<rbrakk> \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
proof (cases n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
n = 0

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

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

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

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

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

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
([],  \<Gamma> \<Rightarrow>* Em) \<in> R*
[PROOF STEP]
obtain  r S where "r \<in> R" and split:"extendRule S r = ([],\<Gamma> \<Rightarrow>* Em)"
[PROOF STATE]
proof (prove)
using this:
([],  \<Gamma> \<Rightarrow>* Em) \<in> R*

goal (1 subgoal):
 1. (\<And>r S. \<lbrakk>r \<in> R; extendRule S r = ([],  \<Gamma> \<Rightarrow>* Em)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule extRules.cases) auto
[PROOF STATE]
proof (state)
this:
r \<in> R
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Em)

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

goal (1 subgoal):
 1. (\<And>c. r = ([], c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases r) (auto simp add:extendRule_def)
[PROOF STATE]
proof (state)
this:
r = ([], c)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
with \<open>r \<in> R\<close>
[PROOF STATE]
proof (chain)
picking this:
r \<in> R
r = ([], c)
[PROOF STEP]
have "r \<in> Ax \<or> r \<in> upRules"
[PROOF STATE]
proof (prove)
using this:
r \<in> R
r = ([], c)

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

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

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
with \<open>r = ([],c)\<close>
[PROOF STATE]
proof (chain)
picking this:
r = ([], c)
r \<in> Ax \<or> r \<in> upRules
[PROOF STEP]
have "r \<in> Ax"
[PROOF STATE]
proof (prove)
using this:
r = ([], c)
r \<in> Ax \<or> r \<in> upRules

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

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
with \<open>r = ([],c)\<close>
[PROOF STATE]
proof (chain)
picking this:
r = ([], c)
r \<in> Ax
[PROOF STEP]
obtain i where "c = (\<LM>At i\<RM> \<Rightarrow>* At i) \<or> c = (\<LM>ff\<RM> \<Rightarrow>* Em)"
[PROOF STATE]
proof (prove)
using this:
r = ([], c)
r \<in> Ax

goal (1 subgoal):
 1. (\<And>i. c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<or> c = ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using characteriseAx[where r=r]
[PROOF STATE]
proof (prove)
using this:
r = ([], c)
r \<in> Ax
r \<in> Ax \<Longrightarrow> r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<or> (\<exists>i. r = ([],  \<LM> At i  \<RM> \<Rightarrow>* At i))

goal (1 subgoal):
 1. (\<And>i. c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<or> c = ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<or> c = ( \<LM> ff  \<RM> \<Rightarrow>* Em)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<or> c = ( \<LM> ff  \<RM> \<Rightarrow>* Em)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<or> c = ( \<LM> ff  \<RM> \<Rightarrow>* Em)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
assume "c = (\<LM>At i\<RM> \<Rightarrow>* At i)"
[PROOF STATE]
proof (state)
this:
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
with split and \<open>r = ([],c)\<close>
[PROOF STATE]
proof (chain)
picking this:
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Em)
r = ([], c)
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i)
[PROOF STEP]
have "(\<Gamma> \<Rightarrow>* C,0) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Em)
r = ([], c)
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i)

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*
[PROOF STEP]
by (auto simp add:extendRule_def extend_def)
[PROOF STATE]
proof (state)
this:
( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
assume "c = (\<LM>ff\<RM> \<Rightarrow>* Em)"
[PROOF STATE]
proof (state)
this:
c = ( \<LM> ff  \<RM> \<Rightarrow>* Em)

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c = ( \<LM> ff  \<RM> \<Rightarrow>* Em)
[PROOF STEP]
have "extend S (\<LM>ff\<RM> \<Rightarrow>* Em) = (\<Gamma> \<Rightarrow>* Em)"
[PROOF STATE]
proof (prove)
using this:
c = ( \<LM> ff  \<RM> \<Rightarrow>* Em)

goal (1 subgoal):
 1. extend S ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* Em)
[PROOF STEP]
using split and \<open>r = ([],c)\<close>
[PROOF STATE]
proof (prove)
using this:
c = ( \<LM> ff  \<RM> \<Rightarrow>* Em)
extendRule S r = ([],  \<Gamma> \<Rightarrow>* Em)
r = ([], c)

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

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

goal (1 subgoal):
 1. ff \<in># \<Gamma>
[PROOF STEP]
using extendFalsum
[PROOF STATE]
proof (prove)
using this:
extend S ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* Em)
extend ?S ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( ?\<Gamma> \<Rightarrow>* ?\<Delta>) \<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> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ff \<in># \<Gamma>
[PROOF STEP]
have "(\<Gamma> \<Rightarrow>* C,0) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
ff \<in># \<Gamma>

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

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

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c = ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<or> c = ( \<LM> ff  \<RM> \<Rightarrow>* Em)
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*
c = ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*
[PROOF STEP]
show "(\<Gamma> \<Rightarrow>* C,n) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<or> c = ( \<LM> ff  \<RM> \<Rightarrow>* Em)
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*
c = ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
using \<open>n=0\<close>
[PROOF STATE]
proof (prove)
using this:
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<or> c = ( \<LM> ff  \<RM> \<Rightarrow>* Em)
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*
c = ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*
n = 0

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<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> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = Suc n'
[PROOF STEP]
have "(\<Gamma> \<Rightarrow>* Em, n'+1) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
n = Suc n'

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

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

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

goal (1 subgoal):
 1. (\<And>Ps. \<lbrakk>Ps \<noteq> []; (Ps,  \<Gamma> \<Rightarrow>* Em) \<in> R*; \<forall>p\<in>set Ps. \<exists>m\<le>n'. (p, m) \<in> derivable R*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using characteriseLast[where C="\<Gamma> \<Rightarrow>* Em" and m=n' and R="R*"]
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> \<Rightarrow>* Em, n' + 1) \<in> derivable R*
( \<Gamma> \<Rightarrow>* Em, n' + 1) \<in> derivable R* \<Longrightarrow> \<exists>Ps. Ps \<noteq> [] \<and> (Ps,  \<Gamma> \<Rightarrow>* Em) \<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 \<noteq> []; (Ps,  \<Gamma> \<Rightarrow>* Em) \<in> R*; \<forall>p\<in>set Ps. \<exists>m\<le>n'. (p, m) \<in> derivable R*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ps \<noteq> []
(Ps,  \<Gamma> \<Rightarrow>* Em) \<in> R*
\<forall>p\<in>set Ps. \<exists>m\<le>n'. (p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
from g c
[PROOF STATE]
proof (chain)
picking this:
(Ps,  \<Gamma> \<Rightarrow>* Em) \<in> R*
R = Ax \<union> R'
[PROOF STEP]
obtain S r where "r \<in> R" and split: "(r \<in> Ax \<or> r \<in> R') \<and> extendRule S r = (Ps, \<Gamma> \<Rightarrow>* Em)"
[PROOF STATE]
proof (prove)
using this:
(Ps,  \<Gamma> \<Rightarrow>* Em) \<in> R*
R = Ax \<union> R'

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
with b
[PROOF STATE]
proof (chain)
picking this:
R' \<subseteq> upRules
r \<in> R
(r \<in> Ax \<or> r \<in> R') \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Em)
[PROOF STEP]
have as: "(r \<in> Ax \<or> r \<in> upRules) \<and> extendRule S r = (Ps, \<Gamma> \<Rightarrow>* Em)"
[PROOF STATE]
proof (prove)
using this:
R' \<subseteq> upRules
r \<in> R
(r \<in> Ax \<or> r \<in> R') \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Em)

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
from as f
[PROOF STATE]
proof (chain)
picking this:
(r \<in> Ax \<or> r \<in> upRules) \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Em)
Ps \<noteq> []
[PROOF STEP]
have "fst r \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
(r \<in> Ax \<or> r \<in> upRules) \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Em)
Ps \<noteq> []

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
with as
[PROOF STATE]
proof (chain)
picking this:
(r \<in> Ax \<or> r \<in> upRules) \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Em)
fst r \<noteq> []
[PROOF STEP]
have "r \<in> upRules"
[PROOF STATE]
proof (prove)
using this:
(r \<in> Ax \<or> r \<in> upRules) \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Em)
fst r \<noteq> []

goal (1 subgoal):
 1. r \<in> upRules
[PROOF STEP]
apply (cases r,auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<noteq> []; r = (a, b); extendRule S (a, b) = (Ps,  \<Gamma> \<Rightarrow>* Em); (a, b) \<in> Ax\<rbrakk> \<Longrightarrow> (a, b) \<in> upRules
[PROOF STEP]
by (rule Ax.cases) auto
[PROOF STATE]
proof (state)
this:
r \<in> upRules

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r \<in> upRules

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<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> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r \<in> upRules
r = (ps, c)
[PROOF STEP]
have "(ps,c) \<in> upRules"
[PROOF STATE]
proof (prove)
using this:
r \<in> upRules
r = (ps, c)

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(ps, c) \<in> upRules
[PROOF STEP]
obtain F Fs where "c = (\<LM>Compound F Fs\<RM> \<Rightarrow>* Em) \<or> c = (\<Empt> \<Rightarrow>* Compound F Fs)"
[PROOF STATE]
proof (prove)
using this:
(ps, c) \<in> upRules

goal (1 subgoal):
 1. (\<And>F Fs. c = ( \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound F Fs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule upRules.cases) auto
[PROOF STATE]
proof (state)
this:
c = ( \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c = ( \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c = ( \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
assume "c = (\<Empt> \<Rightarrow>* Compound F Fs)"
[PROOF STATE]
proof (state)
this:
c = ( \<Empt> \<Rightarrow>* Compound F Fs)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
with \<open>r = (ps,c)\<close> and split
[PROOF STATE]
proof (chain)
picking this:
r = (ps, c)
(r \<in> Ax \<or> r \<in> R') \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Em)
c = ( \<Empt> \<Rightarrow>* Compound F Fs)
[PROOF STEP]
have "(\<Gamma> \<Rightarrow>* C,n'+1) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
r = (ps, c)
(r \<in> Ax \<or> r \<in> R') \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Em)
c = ( \<Empt> \<Rightarrow>* Compound F Fs)

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

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

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

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
assume "c = (\<LM> Compound F Fs \<RM> \<Rightarrow>* Em)"
[PROOF STATE]
proof (state)
this:
c = ( \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c = ( \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
obtain \<Gamma>1 \<delta> where "S = (\<Gamma>1 \<Rightarrow>* \<delta>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<Gamma>1 \<delta>. S = ( \<Gamma>1 \<Rightarrow>* \<delta>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases S) auto
[PROOF STATE]
proof (state)
this:
S = ( \<Gamma>1 \<Rightarrow>* \<delta>)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c = ( \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em)
S = ( \<Gamma>1 \<Rightarrow>* \<delta>)
[PROOF STEP]
have "\<delta> = Em"
[PROOF STATE]
proof (prove)
using this:
c = ( \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em)
S = ( \<Gamma>1 \<Rightarrow>* \<delta>)

goal (1 subgoal):
 1. \<delta> = Em
[PROOF STEP]
using split and \<open>r= (ps,c)\<close>
[PROOF STATE]
proof (prove)
using this:
c = ( \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em)
S = ( \<Gamma>1 \<Rightarrow>* \<delta>)
(r \<in> Ax \<or> r \<in> R') \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Em)
r = (ps, c)

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<delta> = Em
[PROOF STEP]
have "S = (\<Gamma>1 \<Rightarrow>* Em)"
[PROOF STATE]
proof (prove)
using this:
\<delta> = Em

goal (1 subgoal):
 1. S = ( \<Gamma>1 \<Rightarrow>* Em)
[PROOF STEP]
using \<open>S = (\<Gamma>1 \<Rightarrow>* \<delta>)\<close>
[PROOF STATE]
proof (prove)
using this:
\<delta> = Em
S = ( \<Gamma>1 \<Rightarrow>* \<delta>)

goal (1 subgoal):
 1. S = ( \<Gamma>1 \<Rightarrow>* Em)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S = ( \<Gamma>1 \<Rightarrow>* Em)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
with h as \<open>r = (ps,c)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set Ps. \<exists>m\<le>n'. (p, m) \<in> derivable R*
(r \<in> Ax \<or> r \<in> upRules) \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Em)
r = (ps, c)
S = ( \<Gamma>1 \<Rightarrow>* Em)
[PROOF STEP]
have pms: "\<forall> p \<in> set ps. \<exists> m\<le>n'. (extend (\<Gamma>1 \<Rightarrow>* Em) p,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set Ps. \<exists>m\<le>n'. (p, m) \<in> derivable R*
(r \<in> Ax \<or> r \<in> upRules) \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Em)
r = (ps, c)
S = ( \<Gamma>1 \<Rightarrow>* Em)

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 \<Rightarrow>* Em) 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>* Em) p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
have "\<forall> p \<in> set ps. \<exists> m\<le>n'. (extend (\<Gamma>1  \<Rightarrow>* C) 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 \<Rightarrow>* C) 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 \<Rightarrow>* C) 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 \<Rightarrow>* C) 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 \<Rightarrow>* C) 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 \<Rightarrow>* C) 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>* Em) p, m) \<in> derivable R*
p \<in> set ps
[PROOF STEP]
obtain m where "m\<le>n'" and aa: "(extend (\<Gamma>1 \<Rightarrow>* Em) p,m) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
\<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 \<Rightarrow>* Em) p, m) \<in> derivable R*
p \<in> set ps

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. ( \<Gamma>1 + \<Gamma>2 \<Rightarrow>* Em, m) \<in> derivable R*
[PROOF STEP]
using aa
[PROOF STATE]
proof (prove)
using this:
extend ( \<Gamma>1 \<Rightarrow>* Em) p = ( \<Gamma>1 + \<Gamma>2 \<Rightarrow>* Em)
(extend ( \<Gamma>1 \<Rightarrow>* Em) p, m) \<in> derivable R*

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

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

goal (1 subgoal):
 1. ( \<Gamma>1 + \<Gamma>2 \<Rightarrow>* C, m) \<in> derivable R*
[PROOF STEP]
using IH and \<open>n = Suc n'\<close> and \<open>m\<le>n'\<close>
[PROOF STATE]
proof (prove)
using this:
( \<Gamma>1 + \<Gamma>2 \<Rightarrow>* Em, m) \<in> derivable R*
\<forall>m<n. \<forall>\<Gamma>. ( \<Gamma> \<Rightarrow>* Em, m) \<in> derivable R* \<longrightarrow> ( \<Gamma> \<Rightarrow>* C, m) \<in> derivable R*
n = Suc n'
m \<le> n'

goal (1 subgoal):
 1. ( \<Gamma>1 + \<Gamma>2 \<Rightarrow>* C, m) \<in> derivable R*
[PROOF STEP]
apply-
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>( \<Gamma>1 + \<Gamma>2 \<Rightarrow>* Em, m) \<in> derivable R*; \<forall>m<n. \<forall>\<Gamma>. ( \<Gamma> \<Rightarrow>* Em, m) \<in> derivable R* \<longrightarrow> ( \<Gamma> \<Rightarrow>* C, m) \<in> derivable R*; n = Suc n'; m \<le> n'\<rbrakk> \<Longrightarrow> ( \<Gamma>1 + \<Gamma>2 \<Rightarrow>* C, m) \<in> derivable R*
[PROOF STEP]
apply (drule_tac x=m in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>( \<Gamma>1 + \<Gamma>2 \<Rightarrow>* Em, m) \<in> derivable R*; n = Suc n'; m \<le> n'; m < n \<longrightarrow> (\<forall>\<Gamma>. ( \<Gamma> \<Rightarrow>* Em, m) \<in> derivable R* \<longrightarrow> ( \<Gamma> \<Rightarrow>* C, m) \<in> derivable R*)\<rbrakk> \<Longrightarrow> ( \<Gamma>1 + \<Gamma>2 \<Rightarrow>* C, m) \<in> derivable R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
( \<Gamma>1 + \<Gamma>2 \<Rightarrow>* C, m) \<in> derivable R*

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. ( \<Gamma>1 + \<Gamma>2 \<Rightarrow>* \<delta>', m) \<in> derivable R*
[PROOF STEP]
using aa
[PROOF STATE]
proof (prove)
using this:
extend ( \<Gamma>1 \<Rightarrow>* Em) p = ( \<Gamma>1 + \<Gamma>2 \<Rightarrow>* \<delta>')
(extend ( \<Gamma>1 \<Rightarrow>* Em) p, m) \<in> derivable R*

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

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

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

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

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

goal (1 subgoal):
 1. (extend ( \<Gamma>1 \<Rightarrow>* C) p, m) \<in> derivable R*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(extend ( \<Gamma>1 \<Rightarrow>* C) p, m) \<in> derivable R*

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 \<Rightarrow>* C) 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 \<Rightarrow>* C) 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 \<Rightarrow>* C) p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>p\<in>set ps. \<exists>m\<le>n'. (extend ( \<Gamma>1 \<Rightarrow>* C) p, m) \<in> derivable R*
[PROOF STEP]
have "\<forall> p \<in> set (fst (extendRule (\<Gamma>1  \<Rightarrow>* C) 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 \<Rightarrow>* C) p, m) \<in> derivable R*

goal (1 subgoal):
 1. \<forall>p\<in>set (fst (extendRule ( \<Gamma>1 \<Rightarrow>* C) 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 \<Rightarrow>* C) p, m) \<in> derivable R*
r = (ps, c)

goal (1 subgoal):
 1. \<forall>p\<in>set (fst (extendRule ( \<Gamma>1 \<Rightarrow>* C) 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 \<Rightarrow>* C) r)). \<exists>m\<le>n'. (p, m) \<in> derivable R*

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
have "extendRule (\<Gamma>1  \<Rightarrow>* C) r \<in> R*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extendRule ( \<Gamma>1 \<Rightarrow>* C) r \<in> R*
[PROOF STEP]
using \<open>r \<in> upRules\<close> and \<open>r \<in> R\<close>
[PROOF STATE]
proof (prove)
using this:
r \<in> upRules
r \<in> R

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

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
from \<open>S = (\<Gamma>1 \<Rightarrow>* Em)\<close> and as
[PROOF STATE]
proof (chain)
picking this:
S = ( \<Gamma>1 \<Rightarrow>* Em)
(r \<in> Ax \<or> r \<in> upRules) \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Em)
[PROOF STEP]
have "extend (\<Gamma>1  \<Rightarrow>* C) (snd r) = (\<Gamma> \<Rightarrow>* C)"
[PROOF STATE]
proof (prove)
using this:
S = ( \<Gamma>1 \<Rightarrow>* Em)
(r \<in> Ax \<or> r \<in> upRules) \<and> extendRule S r = (Ps,  \<Gamma> \<Rightarrow>* Em)

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

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

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

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, 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> \<Rightarrow>* C, n' + 1) \<in> derivable R*

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

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

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*
[PROOF STEP]
using \<open>n = Suc n'\<close>
[PROOF STATE]
proof (prove)
using this:
c = ( \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em) \<or> c = ( \<Empt> \<Rightarrow>* Compound F Fs)
c = ( \<Empt> \<Rightarrow>* Compound F Fs) \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n' + 1) \<in> derivable R*
c = ( \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em) \<Longrightarrow> ( \<Gamma> \<Rightarrow>* C, n' + 1) \<in> derivable R*
n = Suc n'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
( \<Gamma> \<Rightarrow>* C, n) \<in> derivable R*

goal:
No subgoals!
[PROOF STEP]
qed