[STATEMENT]
lemma containFalsum:
assumes a: "ff \<in># \<Gamma>"
   and  b: "Ax \<subseteq> R"
shows "(\<Gamma> \<Rightarrow>* C,0) \<in> derivable R*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
ff \<in># \<Gamma>
[PROOF STEP]
have "\<Gamma> = \<Gamma> \<ominus> ff \<oplus> ff"
[PROOF STATE]
proof (prove)
using this:
ff \<in># \<Gamma>

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

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> = \<Gamma> \<ominus> ff \<oplus> ff
[PROOF STEP]
have "extend (\<Gamma> \<ominus> ff \<Rightarrow>* C) (\<LM>ff\<RM> \<Rightarrow>* Em) = (\<Gamma> \<Rightarrow>* C)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> = \<Gamma> \<ominus> ff \<oplus> ff

goal (1 subgoal):
 1. extend ( \<Gamma> \<ominus> ff \<Rightarrow>* C) ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* C)
[PROOF STEP]
using extend_def[where forms="\<Gamma> \<ominus> ff \<Rightarrow>* C" and seq="\<LM>ff\<RM> \<Rightarrow>* Em"]
[PROOF STATE]
proof (prove)
using this:
\<Gamma> = \<Gamma> \<ominus> ff \<oplus> ff
extend ( \<Gamma> \<ominus> ff \<Rightarrow>* C) ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<equiv> if succ ( \<LM> ff  \<RM> \<Rightarrow>* Em) = Em then  antec ( \<Gamma> \<ominus> ff \<Rightarrow>* C) + antec ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<Rightarrow>* succ ( \<Gamma> \<ominus> ff \<Rightarrow>* C) else ( antec ( \<Gamma> \<ominus> ff \<Rightarrow>* C) + antec ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<Rightarrow>* succ ( \<LM> ff  \<RM> \<Rightarrow>* Em))

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

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
extend ( \<Gamma> \<ominus> ff \<Rightarrow>* C) ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* C)

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*
[PROOF STEP]
have "([],\<LM>ff\<RM> \<Rightarrow>* Em) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<in> R
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
Ax \<subseteq> R

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

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
extend ( \<Gamma> \<ominus> ff \<Rightarrow>* C) ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* C)
([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<in> R
[PROOF STEP]
have "([],\<Gamma> \<Rightarrow>* C) \<in> R*"
[PROOF STATE]
proof (prove)
using this:
extend ( \<Gamma> \<ominus> ff \<Rightarrow>* C) ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* C)
([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<in> R

goal (1 subgoal):
 1. ([],  \<Gamma> \<Rightarrow>* C) \<in> R*
[PROOF STEP]
using extRules.I[where R=R and r="([],  \<LM>ff\<RM> \<Rightarrow>* Em)" and seq="\<Gamma> \<ominus> ff \<Rightarrow>* C"]
       and extendRule_def[where forms="\<Gamma> \<ominus> ff \<Rightarrow>* C" and R="([],  \<LM>ff\<RM> \<Rightarrow>* Em)"]
[PROOF STATE]
proof (prove)
using this:
extend ( \<Gamma> \<ominus> ff \<Rightarrow>* C) ( \<LM> ff  \<RM> \<Rightarrow>* Em) = ( \<Gamma> \<Rightarrow>* C)
([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<in> R
([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<in> R \<Longrightarrow> extendRule ( \<Gamma> \<ominus> ff \<Rightarrow>* C) ([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<in> R*
extendRule ( \<Gamma> \<ominus> ff \<Rightarrow>* C) ([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<equiv> (map (extend ( \<Gamma> \<ominus> ff \<Rightarrow>* C)) (fst ([],  \<LM> ff  \<RM> \<Rightarrow>* Em)), extend ( \<Gamma> \<ominus> ff \<Rightarrow>* C) (snd ([],  \<LM> ff  \<RM> \<Rightarrow>* Em)))

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

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
([],  \<Gamma> \<Rightarrow>* C) \<in> R*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
([],  \<Gamma> \<Rightarrow>* C) \<in> R*

goal (1 subgoal):
 1. ( \<Gamma> \<Rightarrow>* C, 0) \<in> derivable R*
[PROOF STEP]
using derivable.base[where R="R*" and C="\<Gamma> \<Rightarrow>* C"]
[PROOF STATE]
proof (prove)
using this:
([],  \<Gamma> \<Rightarrow>* C) \<in> R*
([],  \<Gamma> \<Rightarrow>* C) \<in> R* \<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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma characteriseAx:
shows "r \<in> Ax \<Longrightarrow> r = ([],\<LM> ff \<RM> \<Rightarrow>* Em) \<or> (\<exists> i. r = ([], \<LM> At i \<RM> \<Rightarrow>* At i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r \<in> Ax \<Longrightarrow> r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<or> (\<exists>i. r = ([],  \<LM> At i  \<RM> \<Rightarrow>* At i))
[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> r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<or> (\<exists>i. r = ([],  \<LM> At i  \<RM> \<Rightarrow>* At i))
[PROOF STEP]
by (rule Ax.cases) auto


[STATEMENT]
lemma characteriseLast:
assumes "(C,m+1) \<in> derivable R"
shows "\<exists> Ps. Ps \<noteq> [] \<and>
             (Ps,C) \<in> R \<and>
             (\<forall> p \<in> set Ps. \<exists> n\<le>m. (p,n) \<in> derivable R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Ps. Ps \<noteq> [] \<and> (Ps, C) \<in> R \<and> (\<forall>p\<in>set Ps. \<exists>n\<le>m. (p, n) \<in> derivable R)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(C, m + 1) \<in> derivable R

goal (1 subgoal):
 1. \<exists>Ps. Ps \<noteq> [] \<and> (Ps, C) \<in> R \<and> (\<forall>p\<in>set Ps. \<exists>n\<le>m. (p, n) \<in> derivable R)
[PROOF STEP]
by (cases) auto


[STATEMENT]
lemma upRuleCharacterise:
assumes "(Ps,C) \<in> upRules"
shows "\<exists> F Fs. C = (\<Empt> \<Rightarrow>* Compound F Fs) \<or> C = (\<LM>Compound F Fs\<RM> \<Rightarrow>* Em)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>F Fs. C = ( \<Empt> \<Rightarrow>* Compound F Fs) \<or> C = ( \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(Ps, C) \<in> upRules

goal (1 subgoal):
 1. \<exists>F Fs. C = ( \<Empt> \<Rightarrow>* Compound F Fs) \<or> C = ( \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em)
[PROOF STEP]
by (cases) auto


[STATEMENT]
lemma extendEmpty:
shows "extend (\<Empt> \<Rightarrow>* Em) C = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend ( \<Empt> \<Rightarrow>* Em) C = C
[PROOF STEP]
apply (auto simp add:extend_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. succ C = Em \<Longrightarrow> ( antec C \<Rightarrow>* Em) = C
 2. succ C \<noteq> Em \<Longrightarrow> ( antec C \<Rightarrow>* succ C) = C
[PROOF STEP]
apply (cases C)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>succ C = Em; C = ( x1 \<Rightarrow>* x2)\<rbrakk> \<Longrightarrow> ( antec C \<Rightarrow>* Em) = C
 2. succ C \<noteq> Em \<Longrightarrow> ( antec C \<Rightarrow>* succ C) = C
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. succ C \<noteq> Em \<Longrightarrow> ( antec C \<Rightarrow>* succ C) = C
[PROOF STEP]
by (cases C) auto


[STATEMENT]
lemma extendContain:
assumes "r = (ps,c)"
    and "(Ps,C) = extendRule S r"
    and "p \<in> set ps"
shows "extend S p \<in> set Ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend S p \<in> set Ps
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. extend S p \<in> set Ps
[PROOF STEP]
from \<open>p \<in> set ps\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<in> set ps
[PROOF STEP]
have "extend S p \<in> set (map (extend S) ps)"
[PROOF STATE]
proof (prove)
using this:
p \<in> set ps

goal (1 subgoal):
 1. extend S p \<in> set (map (extend S) ps)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extend S p \<in> set (map (extend S) ps)

goal (1 subgoal):
 1. extend S p \<in> set Ps
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
extend S p \<in> set (map (extend S) ps)

goal (1 subgoal):
 1. extend S p \<in> set Ps
[PROOF STEP]
from \<open>(Ps,C) = extendRule S r\<close> and \<open>r = (ps,c)\<close>
[PROOF STATE]
proof (chain)
picking this:
(Ps, C) = extendRule S r
r = (ps, c)
[PROOF STEP]
have "map (extend S) ps = Ps"
[PROOF STATE]
proof (prove)
using this:
(Ps, C) = extendRule S r
r = (ps, c)

goal (1 subgoal):
 1. map (extend S) ps = Ps
[PROOF STEP]
by (simp add:extendRule_def)
[PROOF STATE]
proof (state)
this:
map (extend S) ps = Ps

goal (1 subgoal):
 1. extend S p \<in> set Ps
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
extend S p \<in> set (map (extend S) ps)
map (extend S) ps = Ps
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
extend S p \<in> set (map (extend S) ps)
map (extend S) ps = Ps

goal (1 subgoal):
 1. extend S p \<in> set Ps
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extend S p \<in> set Ps

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nonPrincipalID:
fixes A :: "'a form"
assumes "r \<in> Ax"
shows "\<not> rightPrincipal r A \<and> \<not> leftPrincipal r A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
r \<in> Ax
[PROOF STEP]
obtain i where r1:"r = ([], \<LM> ff \<RM> \<Rightarrow>* Em) \<or> r = ([], \<LM> At i \<RM> \<Rightarrow>* At i)"
[PROOF STATE]
proof (prove)
using this:
r \<in> Ax

goal (1 subgoal):
 1. (\<And>i. r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<or> r = ([],  \<LM> At i  \<RM> \<Rightarrow>* At i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using characteriseAx[where r=r]
[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))

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

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<or> r = ([],  \<LM> At i  \<RM> \<Rightarrow>* At i)

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
assume "rightPrincipal r A"
[PROOF STATE]
proof (state)
this:
rightPrincipal r A

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rightPrincipal r A
[PROOF STEP]
obtain Ps where r2:"r = (Ps, \<Empt> \<Rightarrow>* A)"
[PROOF STATE]
proof (prove)
using this:
rightPrincipal r A

goal (1 subgoal):
 1. (\<And>Ps. r = (Ps,  \<Empt> \<Rightarrow>* A) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases r) auto
[PROOF STATE]
proof (state)
this:
r = (Ps,  \<Empt> \<Rightarrow>* A)

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
with r1
[PROOF STATE]
proof (chain)
picking this:
r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<or> r = ([],  \<LM> At i  \<RM> \<Rightarrow>* At i)
r = (Ps,  \<Empt> \<Rightarrow>* A)
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<or> r = ([],  \<LM> At i  \<RM> \<Rightarrow>* At i)
r = (Ps,  \<Empt> \<Rightarrow>* A)

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
rightPrincipal r A \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rightPrincipal r A \<Longrightarrow> False
[PROOF STEP]
have "\<not> rightPrincipal r A"
[PROOF STATE]
proof (prove)
using this:
rightPrincipal r A \<Longrightarrow> False

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

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> rightPrincipal r A

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> rightPrincipal r A

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
assume "leftPrincipal r A"
[PROOF STATE]
proof (state)
this:
leftPrincipal r A

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
leftPrincipal r A
[PROOF STEP]
obtain Ps' F Fs where r3:"r = (Ps', \<LM>Compound F Fs\<RM> \<Rightarrow>* Em)"
[PROOF STATE]
proof (prove)
using this:
leftPrincipal r A

goal (1 subgoal):
 1. (\<And>Ps' F Fs. r = (Ps',  \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases r) auto
[PROOF STATE]
proof (state)
this:
r = (Ps',  \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em)

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
with r1
[PROOF STATE]
proof (chain)
picking this:
r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<or> r = ([],  \<LM> At i  \<RM> \<Rightarrow>* At i)
r = (Ps',  \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em)
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
r = ([],  \<LM> ff  \<RM> \<Rightarrow>* Em) \<or> r = ([],  \<LM> At i  \<RM> \<Rightarrow>* At i)
r = (Ps',  \<LM> Compound F Fs  \<RM> \<Rightarrow>* Em)

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
leftPrincipal r A \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
leftPrincipal r A \<Longrightarrow> False
[PROOF STEP]
have "\<not> leftPrincipal r A"
[PROOF STATE]
proof (prove)
using this:
leftPrincipal r A \<Longrightarrow> False

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

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> rightPrincipal r A
\<not> leftPrincipal r A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> rightPrincipal r A
\<not> leftPrincipal r A

goal (1 subgoal):
 1. \<not> rightPrincipal r A \<and> \<not> leftPrincipal r A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> rightPrincipal r A \<and> \<not> leftPrincipal r A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extended_Ax_prems_empty:
assumes "r \<in> Ax"
shows "fst (extendRule S r) = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (extendRule S r) = []
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
r \<in> Ax

goal (1 subgoal):
 1. fst (extendRule S 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 (extendRule S r) = []
[PROOF STEP]
by (rule Ax.cases) (auto simp add:extendRule_def)


[STATEMENT]
lemma ruleSet:
assumes "R' \<subseteq> upRules"
    and "R = Ax \<union> R'"
    and "(Ps,C) \<in> R*"
shows "\<exists> S r. extendRule S r = (Ps,C) \<and> (r \<in> R' \<or> r \<in> Ax)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)
[PROOF STEP]
from \<open>(Ps,C) \<in> R*\<close>
[PROOF STATE]
proof (chain)
picking this:
(Ps, C) \<in> R*
[PROOF STEP]
have "\<exists> S r. extendRule S r = (Ps,C) \<and> r \<in> R"
[PROOF STATE]
proof (prove)
using this:
(Ps, C) \<in> R*

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

goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>S r. extendRule S r = (Ps, C) \<and> r \<in> R
[PROOF STEP]
obtain S r where "(Ps,C) = extendRule S r" and "r \<in> R"
[PROOF STATE]
proof (prove)
using this:
\<exists>S r. extendRule S r = (Ps, C) \<and> r \<in> R

goal (1 subgoal):
 1. (\<And>S r. \<lbrakk>(Ps, C) = extendRule S r; r \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S a b. \<lbrakk>\<And>S a b. \<lbrakk>(Ps, C) = extendRule S (a, b); (a, b) \<in> R\<rbrakk> \<Longrightarrow> thesis; extendRule S (a, b) = (Ps, C); (a, b) \<in> R\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (drule_tac x=S in meta_spec,drule_tac x=a in meta_spec, drule_tac x=b in meta_spec) auto
[PROOF STATE]
proof (state)
this:
(Ps, C) = extendRule S r
r \<in> R

goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Ps, C) = extendRule S r
r \<in> R

goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)
[PROOF STEP]
from \<open>r \<in> R\<close> and \<open>R = Ax \<union> R'\<close>
[PROOF STATE]
proof (chain)
picking this:
r \<in> R
R = Ax \<union> R'
[PROOF STEP]
have "r \<in> Ax \<or> r \<in> R'"
[PROOF STATE]
proof (prove)
using this:
r \<in> R
R = Ax \<union> R'

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

goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(Ps, C) = extendRule S r
r \<in> R
r \<in> Ax \<or> r \<in> R'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(Ps, C) = extendRule S r
r \<in> R
r \<in> Ax \<or> r \<in> R'

goal (1 subgoal):
 1. \<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)
[PROOF STEP]
by (rule_tac x=S in exI,rule_tac x=r in exI) (auto)
[PROOF STATE]
proof (state)
this:
\<exists>S r. extendRule S r = (Ps, C) \<and> (r \<in> R' \<or> r \<in> Ax)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dpWeak:
assumes a:"(\<Gamma> \<Rightarrow>* E,n) \<in> derivable R*"
   and  b: "R' \<subseteq> upRules"
   and  c: "R = Ax \<union> R'"
shows "(\<Gamma> + \<Gamma>' \<Rightarrow>* E,n) \<in> derivable R*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> \<Rightarrow>* E, n) \<in> derivable R*

goal (1 subgoal):
 1. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
[PROOF STEP]
proof (induct n arbitrary: \<Gamma> E rule:nat_less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n \<Gamma> E. \<lbrakk>\<forall>m<n. \<forall>x xa. ( x \<Rightarrow>* xa, m) \<in> derivable R* \<longrightarrow> ( x + \<Gamma>' \<Rightarrow>* xa, m) \<in> derivable R*; ( \<Gamma> \<Rightarrow>* E, n) \<in> derivable R*\<rbrakk> \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
[PROOF STEP]
case (1 n \<Gamma> E)
[PROOF STATE]
proof (state)
this:
\<forall>m<n. \<forall>x xa. ( x \<Rightarrow>* xa, m) \<in> derivable R* \<longrightarrow> ( x + \<Gamma>' \<Rightarrow>* xa, m) \<in> derivable R*
( \<Gamma> \<Rightarrow>* E, n) \<in> derivable R*

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. (\<And>r S. \<lbrakk>r \<in> R; extendRule S r = ([],  \<Gamma> \<Rightarrow>* E)\<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>* E)

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

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> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 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> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 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> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 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> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 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> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 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> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 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> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i)
[PROOF STEP]
have "extend S (\<LM>At i\<RM> \<Rightarrow>* At i) = (\<Gamma> \<Rightarrow>* At i)" and "At i = E"
[PROOF STATE]
proof (prove)
using this:
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i)

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

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

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

goal (1 subgoal):
 1. At i \<in># \<Gamma>
[PROOF STEP]
using extendID
[PROOF STATE]
proof (prove)
using this:
extend S ( \<LM> At i  \<RM> \<Rightarrow>* At i) = ( \<Gamma> \<Rightarrow>* At i)
At i = E
extend ?S ( \<LM> At ?i  \<RM> \<Rightarrow>* At ?i) = ( ?\<Gamma> \<Rightarrow>* ?\<Delta>) \<Longrightarrow> At ?i \<in># ?\<Gamma>

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

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

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

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

goal (1 subgoal):
 1. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
[PROOF STEP]
using c and containID[where \<Gamma>="\<Gamma>+\<Gamma>'" and R=R and i=i] and \<open>At i = E\<close>
[PROOF STATE]
proof (prove)
using this:
At i \<in># \<Gamma> + \<Gamma>'
R = Ax \<union> R'
\<lbrakk>At i \<in># \<Gamma> + \<Gamma>'; Ax \<subseteq> R\<rbrakk> \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* At i, 0) \<in> derivable R*
At i = E

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> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c = ( \<LM> At i  \<RM> \<Rightarrow>* At i) \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*

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

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

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 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> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 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>* E)"
[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>* E)
[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>* E)
r = ([], c)

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

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

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>* E)
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> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<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> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<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 c and containFalsum[where \<Gamma>="\<Gamma>+\<Gamma>'" and R=R]
[PROOF STATE]
proof (prove)
using this:
ff \<in># \<Gamma> + \<Gamma>'
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> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
c = ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
 2. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 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> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
c = ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
[PROOF STEP]
show "(\<Gamma> + \<Gamma>' \<Rightarrow>* E,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> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
c = ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*

goal (1 subgoal):
 1. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 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> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
c = ( \<LM> ff  \<RM> \<Rightarrow>* Em) \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 0) \<in> derivable R*
n = 0

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

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

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

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
( \<Gamma> \<Rightarrow>* E, n' + 1) \<in> derivable R*
[PROOF STEP]
obtain Ps where f:"Ps \<noteq> []"
                  and g:"(Ps, \<Gamma> \<Rightarrow>* E) \<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>* E, n' + 1) \<in> derivable R*

goal (1 subgoal):
 1. (\<And>Ps. \<lbrakk>Ps \<noteq> []; (Ps,  \<Gamma> \<Rightarrow>* E) \<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>* E" and m=n' and R="R*"]
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> \<Rightarrow>* E, n' + 1) \<in> derivable R*
( \<Gamma> \<Rightarrow>* E, n' + 1) \<in> derivable R* \<Longrightarrow> \<exists>Ps. Ps \<noteq> [] \<and> (Ps,  \<Gamma> \<Rightarrow>* E) \<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>* E) \<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>* E) \<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> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
[PROOF STEP]
from g c
[PROOF STATE]
proof (chain)
picking this:
(Ps,  \<Gamma> \<Rightarrow>* E) \<in> R*
R = Ax \<union> R'
[PROOF STEP]
obtain S r where "r \<in> R" and "(r \<in> Ax \<or> r \<in> R') \<and> extendRule S r = (Ps, \<Gamma> \<Rightarrow>* E)"
[PROOF STATE]
proof (prove)
using this:
(Ps,  \<Gamma> \<Rightarrow>* E) \<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>* E)\<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>* E)

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 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>* E)
[PROOF STEP]
have as: "(r \<in> Ax \<or> r \<in> upRules) \<and> extendRule S r = (Ps, \<Gamma> \<Rightarrow>* E)"
[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>* E)

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 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>* E)
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>* E)
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> + \<Gamma>' \<Rightarrow>* E, 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>* E)
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>* E)
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>* E); (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> + \<Gamma>' \<Rightarrow>* E, 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> + \<Gamma>' \<Rightarrow>* E, 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> + \<Gamma>' \<Rightarrow>* E, 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> + \<Gamma>' \<Rightarrow>* E, 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> + \<Gamma>' \<Rightarrow>* E, 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>* E)
r = (ps, c)
S = ( \<Gamma>1 \<Rightarrow>* \<delta>)
[PROOF STEP]
have pms: "\<forall> p \<in> set ps. \<exists> m\<le>n'. (extend (\<Gamma>1 \<Rightarrow>* \<delta>) 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>* E)
r = (ps, c)
S = ( \<Gamma>1 \<Rightarrow>* \<delta>)

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

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

goal (1 subgoal):
 1. (\<And>m. \<lbrakk>m \<le> n'; (extend ( \<Gamma>1 \<Rightarrow>* \<delta>) 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>* \<delta>) p, m) \<in> derivable R*

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

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

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

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

goal (1 subgoal):
 1. ( \<Gamma>1 + \<Gamma>2 + \<Gamma>' \<Rightarrow>* \<delta>, 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>* \<delta>, m) \<in> derivable R*
\<forall>m<n. \<forall>\<Gamma> E. ( \<Gamma> \<Rightarrow>* E, m) \<in> derivable R* \<longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
n = Suc n'
m \<le> n'

goal (1 subgoal):
 1. ( \<Gamma>1 + \<Gamma>2 + \<Gamma>' \<Rightarrow>* \<delta>, m) \<in> derivable R*
[PROOF STEP]
apply-
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>( \<Gamma>1 + \<Gamma>2 \<Rightarrow>* \<delta>, m) \<in> derivable R*; \<forall>m<n. \<forall>\<Gamma> E. ( \<Gamma> \<Rightarrow>* E, m) \<in> derivable R* \<longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*; n = Suc n'; m \<le> n'\<rbrakk> \<Longrightarrow> ( \<Gamma>1 + \<Gamma>2 + \<Gamma>' \<Rightarrow>* \<delta>, 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>* \<delta>, m) \<in> derivable R*; n = Suc n'; m \<le> n'; m < n \<longrightarrow> (\<forall>\<Gamma> E. ( \<Gamma> \<Rightarrow>* E, m) \<in> derivable R* \<longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*)\<rbrakk> \<Longrightarrow> ( \<Gamma>1 + \<Gamma>2 + \<Gamma>' \<Rightarrow>* \<delta>, m) \<in> derivable R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
( \<Gamma>1 + \<Gamma>2 + \<Gamma>' \<Rightarrow>* \<delta>, m) \<in> derivable R*

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. ( \<Gamma>1 + \<Gamma>2 + \<Gamma>' \<Rightarrow>* \<delta>', 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>* \<delta>', m) \<in> derivable R*
\<forall>m<n. \<forall>\<Gamma> E. ( \<Gamma> \<Rightarrow>* E, m) \<in> derivable R* \<longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*
n = Suc n'
m \<le> n'

goal (1 subgoal):
 1. ( \<Gamma>1 + \<Gamma>2 + \<Gamma>' \<Rightarrow>* \<delta>', m) \<in> derivable R*
[PROOF STEP]
apply-
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>( \<Gamma>1 + \<Gamma>2 \<Rightarrow>* \<delta>', m) \<in> derivable R*; \<forall>m<n. \<forall>\<Gamma> E. ( \<Gamma> \<Rightarrow>* E, m) \<in> derivable R* \<longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*; n = Suc n'; m \<le> n'\<rbrakk> \<Longrightarrow> ( \<Gamma>1 + \<Gamma>2 + \<Gamma>' \<Rightarrow>* \<delta>', 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>* \<delta>', m) \<in> derivable R*; n = Suc n'; m \<le> n'; m < n \<longrightarrow> (\<forall>\<Gamma> E. ( \<Gamma> \<Rightarrow>* E, m) \<in> derivable R* \<longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, m) \<in> derivable R*)\<rbrakk> \<Longrightarrow> ( \<Gamma>1 + \<Gamma>2 + \<Gamma>' \<Rightarrow>* \<delta>', m) \<in> derivable R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
( \<Gamma>1 + \<Gamma>2 + \<Gamma>' \<Rightarrow>* \<delta>', m) \<in> derivable R*

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, 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 + \<Gamma>' \<Rightarrow>* \<delta>) p, m) \<in> derivable R*
[PROOF STEP]
have "\<forall> p \<in> set (fst (extendRule (\<Gamma>1 + \<Gamma>' \<Rightarrow>* \<delta>) 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>* \<delta>) p, m) \<in> derivable R*

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

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

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
[PROOF STEP]
have "extendRule (\<Gamma>1 + \<Gamma>' \<Rightarrow>* \<delta>) r \<in> R*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* \<delta>) 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 + \<Gamma>' \<Rightarrow>* \<delta>) r \<in> R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* \<delta>) r \<in> R*

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

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

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

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

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>* \<delta>) 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 + \<Gamma>' \<Rightarrow>* \<delta>) r)). \<exists>m\<le>n'. (p, m) \<in> derivable R*
extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* \<delta>) r \<in> R*
extend ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* \<delta>) (snd r) = ( \<Gamma> + \<Gamma>' \<Rightarrow>* E)
\<lbrakk>extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* \<delta>) r \<in> R*; fst (extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* \<delta>) r) \<noteq> []; \<forall>p\<in>set (fst (extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* \<delta>) r)). \<exists>n\<le>n'. (p, n) \<in> derivable R*\<rbrakk> \<Longrightarrow> (snd (extendRule ( \<Gamma>1 + \<Gamma>' \<Rightarrow>* \<delta>) r), n' + 1) \<in> derivable R*
fst r \<noteq> []

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> ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n' + 1) \<in> derivable R*
[PROOF STEP]
show "( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*"
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n' + 1) \<in> derivable R*

goal (1 subgoal):
 1. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<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. ( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
( \<Gamma> + \<Gamma>' \<Rightarrow>* E, n) \<in> derivable R*

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

goal:
No subgoals!
[PROOF STEP]
qed