Theory NominalSequents

(*<*)
(* Author : Peter Chapman *)
(* License: LGPL *)
section "First Order Sequents" 
theory NominalSequents
imports "HOL-Library.Multiset" "HOL-Nominal.Nominal"
begin

atom_decl var

(*>*)
text‹
\section{First-Order Calculi \label{isafirstorder}}
To formalise first-order results we use the package \textit{Nominal Isabelle}.  The details, for the most part, are the same as in \S\ref{isadefs}.  However, we lose one important feature: that of polymorphism.

Recall we defined formulae as being indexed by a type of connectives.  We could then give abbreviations for these indexed formulae.  Unfortunately this feature (indexing by types) is not yet supported in \textit{Nominal Isabelle}.  Nested datatypes are also not supported.  Thus, strings are used for the connectives (both propositional and first-order) and lists of formulae are simulated to nest via a mutually recursive definition:

›

nominal_datatype form = At "nat" "var list" 
                                  | Cpd0 "string" "form_list"
                                  | Cpd1 "string" "«var»form" ("_ (∇ [_]._)" (*<*)[100,100,100]100(*>*))
                                  | ff
and form_list = FNil
                   | FCons "form" "form_list"

(*<*)
abbreviation multiset_abbrev ("\<LM> _  \<RM>" [75]75) where
   "\<LM> A \<RM> ≡ {# A #}"

abbreviation multiset_empty ("\<Empt>" 75) where
  "\<Empt> ≡ {#}"

datatype sequent = Sequent "form multiset" "form multiset" (" (_) ⇒* (_)" [6,6] 5)


(* We have that any step in a rule, be it a primitive rule or an instance of a rule in a derivation
   can be represented as a list of premisses and a conclusion.  We need a list since a list is finite
   by definition *)
type_synonym rule = "sequent list * sequent"

type_synonym deriv = "sequent * nat"

abbreviation
multiset_plus (infixl "⊕" 80) where
   "(Γ :: form multiset) ⊕ (A :: form) ≡ Γ + \<LM>A\<RM>"
abbreviation
multiset_minus (infixl "⊖" 80) where
   "(Γ :: form multiset) ⊖  (A :: form) ≡ Γ - \<LM>A\<RM>" 

consts
  (* extend a sequent by adding another one.  A form of weakening.  Is this overkill by adding a sequent? *)
  extend :: "sequent ⇒ sequent ⇒ sequent"
  extendRule :: "sequent ⇒ rule ⇒ rule"

  (* Unique conclusion Property *)
  uniqueConclusion :: "rule set ⇒ bool"

  (* functions to get at components of sequents *)
primrec antec :: "sequent ⇒ form multiset" where "antec (Sequent ant suc) = ant"
primrec succ :: "sequent ⇒ form multiset" where "succ (Sequent ant suc) = suc"
primrec mset :: "sequent ⇒ form multiset" where "mset (Sequent ant suc) = ant + suc"
primrec seq_size :: "sequent ⇒ nat" where "seq_size (Sequent ant suc) = size ant + size suc"
primrec set_of_seq :: "sequent ⇒ form set" where "set_of_seq (Sequent ant suc) = set_mset (mset (Sequent ant suc))"
primrec set_of_prem :: "sequent list ⇒ form set" where
  "set_of_prem Nil = {}"
| "set_of_prem (p # ps) = set_of_seq p ∪ set_of_prem ps"

(* Extend a sequent, and then a rule by adding seq to all premisses and the conclusion *)
overloading
  extend ≡ extend
  extendRule ≡ extendRule
  uniqueConclusion ≡ uniqueConclusion
begin

definition extend
  where "extend forms seq ≡ (antec forms + antec seq) ⇒* (succ forms + succ seq)"

definition extendRule
  where "extendRule forms R ≡ (map (extend forms) (fst R), extend forms (snd R))"

(* The unique conclusion property.  A set of rules has unique conclusion property if for any pair of rules,
   the conclusions being the same means the rules are the same*)
definition uniqueConclusion :: "rule set ⇒ bool"
  where "uniqueConclusion R ≡ ∀ r1 ∈ R. ∀ r2 ∈ R. (snd r1 = snd r2) ⟶ (r1 =r2)"

end

primrec sequentMinus :: "sequent ⇒ form ⇒ sequent" ("_ - _" [100,100]100) where
  "(Γ ⇒* Δ) - A = (Γ ⊖ A ⇒* Δ ⊖ A)"

primrec listMinus :: "sequent list ⇒ form ⇒ sequent list" (" _ - _ " [100,100]100) where
  "[] - A = []"
| "(P # Ps) - A = (P - A) # (Ps - A)"


(* The formulation of various rule sets *)

(* idRules is the set containing all identity RULES *)
inductive_set "Ax" where
   id[intro]: "([], \<LM> At i xs \<RM> ⇒* \<LM> At i xs \<RM>) ∈ Ax"
|  LBot[intro]: "([], \<LM>ff\<RM> ⇒* \<Empt>) ∈ Ax"

(* upRules is the set of all rules which have a single conclusion.  This is akin to each rule having a 
   single principal formula.  We don't want rules to have no premisses, hence the restriction
   that ps ≠ [] *)
inductive_set "upRules" where
   I[intro]: "⟦ mset c ≡ \<LM> Cpd0 R Fs \<RM> ; ps ≠ [] ⟧ ⟹ (ps,c) ∈ upRules"
(*>*)

text‹
\noindent Formulae are quantified over a single variable at a time.  This is a restriction imposed by \textit{Nominal Isabelle}.  

There are two new \SC rule sets in addition to the propositional rule set: first-order rules without a freshness proviso and first-order rules with a freshness proviso.  Freshness provisos are particularly easy to encode in \textit{Nominal Isabelle}.  We also show that the rules with a freshness proviso form a subset of the first-order rules.  The function \texttt{set-of-prem} takes a list of premisses, and returns all the formulae in that list:
›

(* provRules is the set of rules where we have a freshness proviso *)
inductive_set "provRules" where
  (*<*) I[intro]:(*>*) "⟦ mset c = \<LM> F ∇ [x].A \<RM> ; ps ≠ [] ; x ♯ set_of_prem (ps - A)⟧
                      ⟹ (ps,c) ∈ provRules"

(* nprovRules is the set of rules where we do not have a freshness proviso, but we have
   a first order formula *)
inductive_set "nprovRules" where
   (*<*)I[intro]:(*>*) "⟦ mset c = \<LM> F ∇ [x].A \<RM> ; ps ≠ [] ⟧
                   ⟹ (ps,c) ∈ nprovRules"

(* provRules are a subset of nprovRules *)
lemma nprovContain:
shows "provRules ⊆ nprovRules"
proof-
{fix ps c
 assume "(ps,c) ∈ provRules"
 then have "(ps,c) ∈ nprovRules" by (cases) auto
}
then show ?thesis by auto
qed
(*<*)
primrec subst :: "var ⇒ var ⇒ var list ⇒ var list" ("[_;_]_" [100,100,100] 100) where
  Empt:"[z;y][] = []"
| NEmpt:"[z;y](x#ys) = (if x=y then (z#([z;y]ys)) else (x#([z;y]ys)))"

lemma subst_var_list_eqvt[eqvt]:
  fixes pi::"var prm"
  and   y::"var list"
  shows "pi∙([z;x]y) = [(pi∙z);(pi∙x)](pi∙y)"
by (induct y) (auto simp add: eqvts)
(*>*)

text‹
\noindent Substitution is defined in the usual way:›

nominal_primrec 
    subst_form  :: "var ⇒ var ⇒ form ⇒ form" ("[_,_]_"(*<*) [100,100,100] 100(*>*))
and subst_forms :: "var ⇒ var ⇒ form_list ⇒ form_list" ("[_,_]_"(*<*) [100,100,100] 100(*>*))
where
   "[z,y](At P xs) = At P ([z;y]xs)"
|  "x♯(z,y) ⟹ [z,y](F ∇ [x].A) = F ∇ [x].([z,y]A)"
|  "[z,y](Cpd0 F Fs) = Cpd0 F ([z,y]Fs)"
|  "[z,y]ff = ff"
|  "[z,y]FNil = FNil"
|  "[z,y](FCons f Fs) = FCons ([z,y]f) ([z,y]Fs)"
(*<*)
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)+
apply(fresh_guess add: fresh_string)+
done
(*>*)

text‹\noindent Substitution is extended to multisets in the obvious way.

To formalise the condition ``no specific substitutions'', an inductive predicate is introduced.  If some formula in the multiset $\Gamma$ is a non-trivial substitution, then \texttt{multSubst} $\Gamma$:
›

definition multSubst :: "form multiset ⇒ bool" where
multSubst_def: "multSubst Γ ≡ (∃ A ∈ (set_mset Γ). ∃ x y B. [y,x]B = A ∧ y≠x)"

text‹
\noindent The notation $[z;y]xs$ stands for substitution of a variable in a variable list.  The details are simple, and so are not shown.

Extending the rule sets with passive parts depends upon which kind of active part is being extended.  The active parts with freshness contexts have additional constraints upon the multisets which are added:
›

(* We need to be careful now about how to extend a rule, since we have binding *)
inductive_set extRules :: "rule set ⇒ rule set"   (" _*" )
   for R :: "rule set"
   where
  id(*<*)[intro](*>*):   "⟦ r ∈ R ; r ∈ Ax ⟧ ⟹ extendRule S r ∈ R*"
| sc(*<*)[intro](*>*):   "⟦ r ∈ R ; r ∈ upRules ⟧ ⟹ extendRule S r ∈ R*"
| np(*<*)[intro](*>*):   "⟦ r ∈ R ; r ∈ nprovRules ⟧ ⟹ extendRule S r ∈ R*"
| p(*<*)[intro](*>*):     "⟦ (ps,c) ∈ R ; (ps,c) ∈ provRules ; mset c = \<LM> F ∇ [x].A \<RM> ; x ♯ set_of_seq S ⟧
                          ⟹ extendRule S (ps,c) ∈ R*"

(*<*)
(* A formulation of what it means to be a principal formula for a rule.  Note that we have to build up from
   single conclusion rules.   *)

inductive leftPrincipal :: "rule ⇒ form ⇒ bool"
  where
  sc[intro]: "⟦ C = (\<LM>A\<RM> ⇒* \<Empt>) ; A ≠ ff ⟧  ⟹ 
                   leftPrincipal (Ps,C) A"


inductive rightPrincipal :: "rule ⇒ form ⇒ bool"
  where
  sc[intro]: "C = (\<Empt> ⇒* \<LM>A\<RM>) ⟹ rightPrincipal (Ps,C) A"


(* What it means to be a derivable sequent.  Can have this as a predicate or as a set.
   The two formation rules say that the supplied premisses are derivable, and the second says
   that if all the premisses of some rule are derivable, then so is the conclusion. *)

inductive_set derivable :: "rule set ⇒ deriv set"
  for R :: "rule set"
  where
   base[intro]: "⟦([],C) ∈ R⟧ ⟹ (C,0) ∈ derivable R"
|  step[intro]: "⟦ r ∈ R ; (fst r)≠[] ; ∀ p ∈ set (fst r). ∃ n ≤ m. (p,n) ∈ derivable R ⟧ 
                       ⟹ (snd r,m + 1) ∈ derivable R"


(* Characterisation of a sequent *)
lemma characteriseSeq:
shows "∃ A B. (C :: sequent) = (A ⇒* B)"
apply (rule_tac x="antec C" in exI, rule_tac x="succ C" in exI) by (cases C) (auto)


(* Helper function for later *)
lemma nonEmptySet:
shows "A ≠ [] ⟶ (∃ a. a ∈ set A)"
by (auto simp add:neq_Nil_conv)


(* Lemma which says that if we have extended an identity rule, then the propositional variable is
   contained in the extended multisets *)
lemma extendID:
assumes "extend S (\<LM> At i xs \<RM> ⇒* \<LM> At i xs \<RM>) = (Γ ⇒* Δ)"
shows "At i xs ∈# Γ ∧ At i xs ∈# Δ"
using assms
proof-
  from assms have "∃ Γ' Δ'. Γ = Γ' ⊕ At i xs ∧ Δ = Δ' ⊕ At i xs" 
     using extend_def[where forms=S and seq="\<LM> At i xs \<RM> ⇒* \<LM> At i xs \<RM>"]
     by (rule_tac x="antec S" in exI,rule_tac x="succ S" in exI) auto
  then show ?thesis by auto
qed


lemma extendFalsum:
assumes "extend S (\<LM> ff \<RM> ⇒* \<Empt>) = (Γ ⇒* Δ)"
shows "ff ∈# Γ"
proof-
  from assms have "∃ Γ'. Γ = Γ' ⊕ ff" 
     using extend_def[where forms=S and seq="\<LM> ff \<RM> ⇒* \<Empt>"]
     by (rule_tac x="antec S" in exI) auto
  then show ?thesis by auto
qed



(* Lemma that says if a propositional variable is in both the antecedent and succedent of a sequent,
   then it is derivable from idscRules *)
lemma containID:
assumes a:"At i xs ∈# Γ ∧ At i xs ∈# Δ"
    and b:"Ax ⊆ R"
shows "(Γ ⇒* Δ,0) ∈ derivable R*"
proof-
from a have "Γ = Γ ⊖ At i xs ⊕ At i xs ∧ Δ = Δ ⊖ At i xs ⊕ At i xs" by auto
then have "extend ((Γ ⊖ At i xs) ⇒* (Δ ⊖ At i xs)) (\<LM> At i xs \<RM> ⇒* \<LM> At i xs \<RM>) = (Γ ⇒* Δ)" 
     using extend_def[where forms="Γ ⊖ At i xs ⇒* Δ ⊖ At i xs" and seq="\<LM>At i xs\<RM> ⇒* \<LM>At i xs\<RM>"] by auto
moreover
have "([],\<LM> At i xs \<RM> ⇒* \<LM> At i xs \<RM>) ∈ R" using b by auto
ultimately
have "([],Γ ⇒* Δ) ∈ extRules R" 
     using extRules.id[where R=R and r="([],  \<LM>At i xs\<RM> ⇒* \<LM>At i xs\<RM>)" and S="Γ ⊖ At i xs ⇒* Δ ⊖ At i xs"] 
       and extendRule_def[where forms="Γ ⊖ At i xs ⇒* Δ ⊖ At i xs" and R="([],  \<LM>At i xs\<RM> ⇒* \<LM>At i xs\<RM>)"] by auto
then show ?thesis using derivable.base[where R="R*" and C="Γ ⇒* Δ"] by auto
qed

lemma containFalsum:
assumes a: "ff ∈# Γ"
   and  b: "Ax ⊆ R"
shows "(Γ ⇒* Δ,0) ∈ derivable R*"
proof-
from a have "Γ = Γ ⊖ ff ⊕ ff" by auto
then have "extend (Γ ⊖ ff ⇒* Δ) (\<LM>ff\<RM> ⇒* \<Empt>) = (Γ ⇒* Δ)"
     using extend_def[where forms="Γ ⊖ ff ⇒* Δ" and seq="\<LM>ff\<RM> ⇒* \<Empt>"] by auto 
moreover
have "([],\<LM>ff\<RM> ⇒* \<Empt>) ∈ R" using b by auto
ultimately have "([],Γ ⇒* Δ) ∈ R*"
     using extRules.id[where R=R and r="([],  \<LM>ff\<RM> ⇒* \<Empt>)" and S="Γ ⊖ ff ⇒* Δ"]
       and extendRule_def[where forms="Γ ⊖ ff ⇒* Δ" and R="([],  \<LM>ff\<RM> ⇒* \<Empt>)"] by auto
then show ?thesis using derivable.base[where R="R*" and C="Γ ⇒* Δ"] by auto
qed 


(* Lemma which says that if r is an identity rule, then r is of the form
   ([], P ⇒* P) *)
lemma characteriseAx:
shows "r ∈ Ax ⟹ r = ([],\<LM>ff\<RM> ⇒* \<Empt>) ∨ (∃ i xs. r = ([], \<LM> At i xs\<RM> ⇒* \<LM> At i xs\<RM>))"
apply (cases r) by (rule Ax.cases) auto


(* A lemma about the last rule used in a derivation, i.e. that one exists *)
lemma characteriseLast:
assumes "(C,m+1) ∈ derivable R"
shows "∃ Ps. Ps ≠ [] ∧
             (Ps,C) ∈ R ∧ 
             (∀ p ∈ set Ps. ∃ n≤m. (p,n) ∈ derivable R)"
using assms
proof (cases)
  case base
  then show "∃ Ps. Ps ≠ [] ∧
    (Ps,C) ∈ R ∧ 
    (∀ p ∈ set Ps. ∃ n≤m. (p,n) ∈ derivable R)" using assms by simp
next
  case (step r n)
  then obtain Ps where "r = (Ps,C)" and "m=n" by (cases r) (auto)
  then have "fst r = Ps" and "snd r = C" by auto
  then show "∃ Ps. Ps ≠ [] ∧
    (Ps,C) ∈ R ∧ 
    (∀ p ∈ set Ps. ∃ n≤m. (p,n) ∈ derivable R)" 
    using ‹r ∈ R› and ‹m=n› and step(4,5)
    by (rule_tac x=Ps in exI) (auto)
qed



lemma propRuleCharacterise:
assumes "(Ps,C) ∈ upRules"
shows "∃ F Fs. C = (\<Empt> ⇒* \<LM>Cpd0 F Fs\<RM>) ∨ C = (\<LM>Cpd0 F Fs\<RM> ⇒* \<Empt>)"
using assms
proof (cases)
  case (I F Fs)
  then obtain Γ Δ where "C = (Γ ⇒* Δ)" using characteriseSeq[where C=C] by auto
  then have "(Ps,Γ ⇒* Δ) ∈ upRules" using assms by simp
  then show "∃ F Fs. C = (\<Empt> ⇒* \<LM>Cpd0 F Fs\<RM>) ∨ C = (\<LM>Cpd0 F Fs\<RM> ⇒* \<Empt>)" 
    using ‹mset C ≡ \<LM>Cpd0 F Fs\<RM>› and ‹C = (Γ ⇒* Δ)›
      and mset.simps[where ant=Γ and suc=Δ] and union_is_single[where M=Γ and N=Δ and a="Cpd0 F Fs"]
    by auto
qed

lemma provRuleCharacterise:
assumes "(Ps,C) ∈ provRules"
shows "∃ F x A. (C = (\<Empt> ⇒* \<LM> F ∇ [x].A \<RM>) ∨ C = (\<LM> F ∇ [x].A \<RM> ⇒* \<Empt>)) ∧ x ♯ set_of_prem (Ps - A)"
using assms
proof (cases)
  case (I F x A)
  then obtain Γ Δ where "C = (Γ ⇒* Δ)" using characteriseSeq[where C=C] by auto
  then have "(Ps,Γ ⇒* Δ) ∈ provRules" using assms by simp
  then show "∃ F x A. (C = (\<Empt> ⇒* \<LM> F ∇ [x].A \<RM>) ∨ C = (\<LM> F ∇ [x].A \<RM> ⇒* \<Empt>)) ∧ x ♯ set_of_prem (Ps - A)" 
    using ‹mset C = \<LM> F ∇ [x].A \<RM>› and ‹C = (Γ ⇒* Δ)› and ‹x ♯ set_of_prem (Ps - A)›
      and mset.simps[where ant=Γ and suc=Δ] and union_is_single[where M=Γ and N=Δ and a="F ∇ [x].A"]
    by auto
qed

lemma nprovRuleCharacterise:
assumes "(Ps,C) ∈ nprovRules"
shows "∃ F x A. C = (\<Empt> ⇒* \<LM> F ∇ [x].A \<RM>) ∨ C = (\<LM> F ∇ [x].A \<RM> ⇒* \<Empt>)"
using assms
proof (cases)
  case (I F x A)
  then obtain Γ Δ where "C = (Γ ⇒* Δ)" using characteriseSeq[where C=C] by auto
  then have "(Ps,Γ ⇒* Δ) ∈ nprovRules" using assms by simp
  then show "∃ F x A. C = (\<Empt> ⇒* \<LM> F ∇ [x].A \<RM>) ∨ C = (\<LM> F ∇ [x].A \<RM> ⇒* \<Empt>)" 
    using ‹mset C = \<LM> F ∇ [x].A \<RM>› and ‹C = (Γ ⇒* Δ)›
      and mset.simps[where ant=Γ and suc=Δ] and union_is_single[where M=Γ and N=Δ and a="F ∇ [x].A"]
    by auto
qed


lemma extendEmpty:
shows "extend (\<Empt> ⇒* \<Empt>) C = C"
apply (auto simp add:extend_def) by (cases C) auto



lemma extendContain:
assumes "r = (ps,c)"
    and "(Ps,C) = extendRule S r"
    and "p ∈ set ps"
shows "extend S p ∈ set Ps"
proof-
from ‹p ∈ set ps› have "extend S p ∈ set (map (extend S) ps)" by auto
moreover from ‹(Ps,C) = extendRule S r› and ‹r = (ps,c)› have "map (extend S) ps = Ps" by (simp add:extendRule_def) 
ultimately show ?thesis by auto
qed

lemma finSeqSet:
fixes S :: "sequent"
shows "finite (set_of_seq S)"
proof-
obtain Γ Δ where "S = (Γ ⇒* Δ)" by (cases S) auto
then show ?thesis by (auto simp add:finite_set_mset)
qed

lemma finPremSet:
fixes Ps :: "sequent list"
shows "finite (set_of_prem Ps)"
by (induct Ps) (auto simp add:finSeqSet)


lemma finSupp:
fixes A :: "form" and As :: "form_list"
shows "finite ((supp A) :: var set)" and "finite ((supp As) :: var set)"
proof (nominal_induct A and As rule:form_form_list.strong_inducts)
print_cases
case (At n xs)   
   have "finite (set xs :: var set)" by (induct xs) auto
   moreover have "set xs = (supp xs :: var set)" by (induct xs) (auto simp add:supp_list_nil supp_set_empty supp_list_cons supp_atm)
   ultimately have "finite (supp xs :: var set)" by auto
   moreover have "supp (At n xs) = supp n ∪ (supp xs :: var set)" using form.supp(1)[where ?x2.0=n and ?x1.0=xs] by auto
   then have "supp (At n xs) = (supp xs :: var set)" using supp_nat[where n=n] by force
   ultimately show ?case by auto
next
case FNil
   have "supp FNil = ({} :: var set)" using form_list.supp by auto
   then show ?case by auto
next
case (FCons F Fs)
   then show ?case using form_list.supp by auto
next
case (Cpd0 Str Fs)
   then show ?case using form.supp(2)[where ?x2.0="Str" and ?x1.0=Fs] and supp_string[where s=Str] by auto
next
case (Cpd1 F x B)
   from ‹finite (supp B)› have "supp ([x].B) = supp B - {x}" using abs_fun_supp[OF pt_var_inst, OF at_var_inst] by auto
   then show ?case using form.supp(3)[where ?x3.0=F and ?x1.0=x and ?x2.0=B] and supp_string[where s=F]
                   and ‹finite (supp B)› by force
next
case ff
   then show ?case using form.supp by auto
qed

lemma getFresh:
fixes x :: "var" and A :: "form" and S :: "sequent" and Ps :: "sequent list"
shows "∃ (y :: var). y ♯ x ∧ y ♯ A ∧ y ♯ set_of_seq S ∧ y ♯ set_of_prem Ps"
proof-
have "finite ({A} ∪ set_of_seq S ∪ set_of_prem Ps)" using finSeqSet and finPremSet by auto
then have "finite (supp ({A} ∪ set_of_seq S ∪ set_of_prem Ps) :: var set)"
     using finSupp(1) and supp_of_fin_sets[OF pt_var_inst, OF at_var_inst, OF fs_var_inst,
                                           where X="({A} ∪ set_of_seq S ∪ set_of_prem Ps)"] 
     by auto
then have "finite (supp ({A} ∪ set_of_seq S ∪ set_of_prem Ps) ∪ supp x :: var set)" using supp_atm by auto
then obtain y where "y ∉ (supp ({A} ∪ set_of_seq S ∪ set_of_prem Ps) ∪ supp x :: var set)" 
     using ex_in_inf[OF at_var_inst,where A="supp ({A} ∪ set_of_seq S ∪ set_of_prem Ps) ∪ supp x"] by auto
then have "y ∉ supp x ∧ y ∉ supp ({A} ∪ set_of_seq S ∪ set_of_prem Ps)" by auto
then have "y ♯ ({A} ∪ set_of_seq S ∪ set_of_prem Ps) ∧ y ♯ x" using fresh_def[where a=y and x=x]
     and fresh_def[where a=y and x="{A} ∪ set_of_seq S ∪ set_of_prem Ps"] by auto
then have "y ♯ A ∧ y ♯ (set_of_seq S ∪ set_of_prem Ps) ∧ y ♯ x" 
     using fresh_fin_insert[OF pt_var_inst, OF at_var_inst, OF fs_var_inst,where X="set_of_seq S ∪ set_of_prem Ps" and x=A]
       and finSeqSet and finPremSet by auto
then have "y ♯ A ∧ y ♯ set_of_seq S ∧ y ♯ set_of_prem Ps ∧ y ♯ x"
     using fresh_fin_union[OF pt_var_inst,OF at_var_inst, OF fs_var_inst, where X="set_of_seq S" and Y="set_of_prem Ps"]
       and finSeqSet and finPremSet by auto
then show ?thesis by auto
qed

lemma switchAux:
fixes Xs :: "var list"
assumes "y ♯ Xs"
shows "[y;x]Xs = [(y,x)]∙Xs"
using assms
proof (induct Xs)
print_cases
case Nil
   then show ?case using nil_eqvt by auto
next
case (Cons a As)
   then have "y ♯ a ∧ y ♯ As" and "[y;x]As = [(y,x)]∙As" 
        using fresh_list_cons[where a=y and x=a and xs=As] by auto
   then show ?case using NEmpt[where z=y and y=x and x=a and ys= As] 
                 and cons_eqvt[where pi="[(y,x)]" and x=a and xs=As] by (perm_simp add:fresh_atm)
qed

lemma switch:
fixes A :: "form" and As :: "form_list"
shows "y ♯ A ⟹ [y,x]A = [(y,x)]∙A" and "y ♯ As ⟹ [y,x]As = [(y,x)]∙As"
proof (nominal_induct A and As avoiding: x y rule:form_form_list.strong_inducts)
  case (At n xs s t)
  then have "t ♯ xs" using form.fresh by auto
  then show ?case using perm_nat_def[where pi="[(t,s)]" and i=n] and switchAux[where y=t and Xs=xs]
    by auto
next
  case FNil
  then show ?case by auto
next
  case (FCons B Bs s t)
  then show ?case by auto
next
  case (Cpd0 Str Bs s t)
  then show ?case using Cpd0.hyps[where ba=t and b=s] and form.fresh
    and perm_string[where s="Str" and pi="[(t,s)]"] by auto
next
  case (Cpd1 F a B s t)
  then have "t ♯ B" using form.fresh(3)[where ?x3.0=F and ?x1.0=a and ?x2.0=B and a=t] 
    and fresh_atm[where a=a and b=t] and fresh_string[where a=t and s=F] 
    and fresh_abs_funE[OF pt_var_inst, OF at_var_inst,where x=B and b=t and a=a]
    and finSupp(1)[where A=B] by auto
  then show ?case using Cpd1(4)[where ba=t and b=s] and form.fresh and Cpd1(1,2)
    and perm_string[where pi="[(t,s)]" and s=F] and fresh_atm by perm_simp
next
  case ff
  then show ?case by auto
qed
(*>*)
    

text‹
\noindent The final clause says we can only use an $S$ which is suitable fresh.

The only lemma which is unique to first-order calculi is the Substitution Lemma.  We show the crucial step in the proof; namely that one can substitute a fresh variable into a formula and the resultant formula is unchanged.  The proof is not particularly edifying and is omitted:
›

lemma formSubst:
shows "y ♯ x ∧ y ♯ A ⟹ F ∇ [x].A = F ∇ [y].([y,x]A)"
(*<*)
proof-
assume "y ♯ x ∧ y ♯ A" then have "[x].A = [y].([y,x]A)" 
  using abs_fun_eq3[OF pt_var_inst, OF at_var_inst,where x="[y,x]A" and y=A and a=y and b=x]
  and switch(1)[where y=y and A=A and x=x] and fresh_atm[where a=y and b=x] by (perm_simp)
then show ?thesis using form.inject(3) by auto
qed
(*>*)

text‹
\noindent  Using the above lemma, we can change any sequent to an equivalent new sequent which does not contain certain variables.  Therefore, we can extend with any sequent:
›

lemma extend_for_any_seq:
fixes S :: "sequent"
assumes rules: "R1 ⊆ upRules ∧ R2 ⊆ nprovRules ∧ R3 ⊆ provRules"
    and rules2: "R = Ax ∪ R1 ∪ R2 ∪ R3"
    and rin: "r ∈ R"
shows "extendRule S r ∈ R*"
 (*<*)
proof-
from rin and rules2 have "r ∈ Ax ∨ r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3" by auto
moreover
    {assume "r ∈ Ax"
     then have "extendRule S r ∈ R*" using extRules.id[where r=r and R=R and S=S] and rin by auto
    }
moreover
    {assume "r ∈ R1"
     then have "r ∈ upRules" using rules by auto
     then have "extendRule S r ∈ R*" using extRules.sc[where r=r and R=R and S=S] and rin by auto
    }
moreover
    {assume "r ∈ R2"
     then have "r ∈ nprovRules" using rules by auto
     then have "extendRule S r ∈ R*" using extRules.np[where r=r and R=R and S=S] and rin by auto
    }
moreover

 {(*>*)
txt‹\noindent  We only show the interesting case: where the last inference had a freshness proviso:›
  
  assume "r ∈ R3" 
  then have "r ∈ provRules" using rules by auto
  obtain ps c where "r = (ps,c)" by (cases r) auto
  then have r1: "(ps,c) ∈ R" 
          and r2: "(ps,c) ∈ provRules" using ‹r ∈ provRules› and rin by auto
  with ‹r = (ps,c)› obtain F x A 
       where "(c = ( \<Empt> ⇒* \<LM>F ∇ [x].A\<RM>) ∨ 
                 c = ( \<LM>F ∇ [x].A\<RM> ⇒* \<Empt>)) ∧ x ♯ set_of_prem ( ps - A )"
         using provRuleCharacterise(*<*)[where Ps=ps and C=c](*>*) and ‹r ∈ provRules› by auto
  then have "mset c = \<LM> F ∇ [x].A \<RM> ∧ x ♯ set_of_prem (ps - A)" (*<*)using mset.simps(*>*) by auto
  moreover obtain y where fr:  "y ♯ x ∧ 
                                  y ♯ A ∧ 
                                  y ♯ set_of_seq S ∧ 
                                 (y :: var) ♯ set_of_prem (ps-A)"
         using getFresh(*<*)[where x=x and A=A and S=S and Ps="ps-A"](*>*) by auto
  then have fr2: "y ♯ set_of_seq S" by auto 
  ultimately have "mset c = \<LM> F ∇ [y].([y,x]A) \<RM> ∧ y ♯ set_of_prem (ps - A)" 
         using formSubst and fr by auto
  then have "mset c = \<LM> F ∇ [y].([y,x]A) \<RM>" by auto
  then have "extendRule S (ps,c) ∈ R*" using r1 and r2 and fr2
         and extRules.p(*<*)[where ps=ps and c=c and R=R and F=F and x=y and A="[y,x]A" and S=S](*>*) by auto
  then have "extendRule S r ∈ R*" using ‹r = (ps,c)› by simp
   (*<*) }

ultimately show ?thesis by blast
qed


(* Constructing the rule set we will use.  It contains all axioms, but only a subset
   of the possible logical rules. *)
lemma ruleSet:
assumes "R1 ⊆ upRules" and "R2 ⊆ nprovRules" and "R3 ⊆ provRules"
    and "R = Ax ∪ R1 ∪ R2 ∪ R3"
    and "(Ps,C) ∈ R*"
shows "∃ S r. extendRule S r = (Ps,C) ∧ (r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3 ∨ r ∈ Ax)"
proof-
from ‹(Ps,C) ∈ R*› have "∃ S r. extendRule S r = (Ps,C) ∧ r ∈ R" by (cases) auto
then obtain S r where "(Ps,C) = extendRule S r" and "r ∈ R" apply auto 
                by (drule_tac x=S in meta_spec,drule_tac x=a in meta_spec, drule_tac x=b in meta_spec) auto
moreover from ‹r ∈ R› and ‹R = Ax ∪ R1 ∪ R2 ∪ R3› have "r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3 ∨ r ∈ Ax" by blast
ultimately show ?thesis by (rule_tac x=S in exI,rule_tac x=r in exI) (auto)
qed

(* Non-principal rule lemma *)
lemma nonPrincipalInvertRight:
assumes "R1 ⊆ upRules" and "R2 ⊆ nprovRules" and "R3 ⊆ provRules"
    and "R = Ax ∪ R1 ∪ R2 ∪ R3" and "r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3" and "r = (ps,c)"
    and IH: "∀m<n. ∀Γ Δ. ( Γ ⇒* Δ ⊕ F ∇ [x].A, m) ∈ derivable R* ⟶
              (∀r' ∈ R. rightPrincipal r' (F ∇ [x].A) ⟶ ( Γ' ⇒* Δ') ∈ set (fst r')) ⟶
              (¬ multSubst Γ' ∧ ¬ multSubst Δ') ⟶
              (∃m'≤m. ( Γ + Γ' ⇒* Δ + Δ', m') ∈ derivable R*)"
    and a': "(Γ ⇒* Δ ⊕ F ∇ [x].A,n) ∈ derivable R*" 
    and b': "∀ r' ∈ R. rightPrincipal r' (F ∇ [x].A) ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
    and c': "¬ multSubst Γ' ∧ ¬ multSubst Δ'"
    and np: "¬ rightPrincipal r (F ∇ [x].A)"
    and ext: "extendRule S r = (Ps,Γ ⇒* Δ ⊕ F ∇ [x].A)"
    and num: "n = n' + 1"
    and all: "∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*"
    and nonempty: "Ps ≠ []"
shows "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
proof-
from ext obtain Φ Ψ where "S = (Φ ⇒* Ψ)" by (cases S) (auto)
from ‹r = (ps,c)› obtain G H where "c = (G ⇒* H)" by (cases c) (auto)
then have "\<LM> F ∇ [x].A  \<RM> ≠ H" using ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3›
     proof-
     {assume "r ∈ R1" then have "r ∈ upRules" using ‹R1 ⊆ upRules› by auto
      with ‹r = (ps,c)› obtain T Ts where "c = (\<Empt> ⇒* \<LM>Cpd0 T Ts\<RM>) ∨ c = (\<LM>Cpd0 T Ts\<RM> ⇒* \<Empt>)"
            using propRuleCharacterise[where Ps=ps and C=c] by auto
      moreover
        {assume "c = (\<Empt> ⇒* \<LM>Cpd0 T Ts\<RM>)"
         with ‹c = (G ⇒* H)› have "\<LM> F ∇ [x].A \<RM> ≠ H" by auto
        }
      moreover
        {assume "c = (\<LM>Cpd0 T Ts\<RM> ⇒* \<Empt>)"
         then have "\<LM>F ∇ [x].A \<RM> ≠ H" using ‹c = (G ⇒* H)› by auto
        }
      ultimately have "\<LM> F ∇ [x].A \<RM> ≠ H" by blast
     }
     moreover
     {assume "r ∈ R2 ∨ r ∈ R3" 
      then have "r ∈ provRules ∨ r ∈ nprovRules" using ‹R2 ⊆ nprovRules› and ‹R3 ⊆ provRules› by auto
      with ‹r = (ps,c)› obtain T y B where "c = (\<Empt> ⇒* \<LM> T ∇ [y].B \<RM>) ∨ c = (\<LM> T ∇ [y].B\<RM> ⇒* \<Empt>)"
            using provRuleCharacterise[where Ps=ps and C=c]
            and nprovRuleCharacterise[where Ps=ps and C=c] by auto
      moreover
        {assume "c = (\<Empt> ⇒* \<LM> T ∇ [y].B\<RM>)"
         then have "rightPrincipal r (T ∇ [y].B)" using ‹r = (ps,c)› by auto
         with ‹¬ rightPrincipal r (F ∇ [x].A)› have "T ∇ [y].B ≠ F ∇ [x].A" by auto
         with ‹c = (G ⇒* H)› have "\<LM> F ∇ [x].A \<RM> ≠ H" using ‹c = (\<Empt> ⇒* \<LM> T ∇ [y].B \<RM>)› by auto
        }
      moreover
        {assume "c = (\<LM>T ∇ [y].B \<RM> ⇒* \<Empt>)"
         then have "\<LM>F ∇ [x].A \<RM> ≠ H" using ‹c = (G ⇒* H)› by auto
        }
      ultimately have "\<LM> F ∇ [x].A \<RM> ≠ H" by blast
     }
     ultimately show ?thesis using ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3› by blast
     qed
moreover have "succ S + succ (snd r) = (Δ ⊕ F ∇ [x].A)" 
         using ext and extendRule_def[where forms=S and R=r]
                   and extend_def[where forms=S and seq="snd r"] by auto
then have "Ψ + H = Δ ⊕ F ∇ [x].A" using ‹S = (Φ ⇒* Ψ)› and ‹r = (ps,c)› and ‹c = (G ⇒* H)› by auto
moreover from ‹r = (ps,c)› and ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3› and ‹R1 ⊆ upRules› and ‹R2 ⊆ nprovRules›
              and ‹R3 ⊆ provRules› have "(ps,c) ∈ upRules ∨ (ps,c) ∈ nprovRules ∨ (ps,c) ∈ provRules" by auto
then have "∃ A. c = (\<Empt> ⇒* \<LM>A\<RM>) ∨ c = (\<LM>A\<RM> ⇒* \<Empt>)"
     using propRuleCharacterise[where Ps=ps and C=c]
       and nprovRuleCharacterise[where Ps=ps and C=c]
       and provRuleCharacterise[where Ps=ps and C=c] by auto
then have "H = \<Empt> ∨ (∃ A. H = \<LM>A\<RM>)" using ‹c = (G ⇒* H)› by auto
ultimately have "F ∇ [x].A ∈# Ψ"
    proof-
    have "H = \<Empt> ∨ (∃ A. H = \<LM>A\<RM>)" by fact
    moreover
    {assume "H = \<Empt>"
     then have "Ψ = Δ ⊕ F ∇ [x].A" using ‹Ψ + H = Δ ⊕ F ∇ [x].A› by auto
     then have "F ∇ [x].A ∈# Ψ" by auto
    }
    moreover
    {assume "∃ A. H = \<LM>A\<RM>"
     then obtain T where "H = \<LM>T\<RM>" by auto
     then have "Ψ ⊕ T = Δ ⊕ F ∇ [x].A" using ‹Ψ + H = Δ ⊕ F ∇ [x].A› by auto
     then have "set_mset (Ψ ⊕ T) = set_mset (Δ ⊕ F ∇ [x].A)" by auto
     then have "set_mset Ψ ∪ {T} = set_mset Δ ∪ {F ∇ [x].A}" by auto
     moreover from ‹H = \<LM>T\<RM>› and ‹\<LM>F ∇ [x].A\<RM> ≠ H› have "F ∇ [x].A ≠ T" by auto
     ultimately have "F ∇ [x].A ∈ set_mset Ψ" by auto
     then have "F ∇ [x].A ∈# Ψ" by auto
    }
    ultimately show "F ∇ [x].A ∈# Ψ" by blast
    qed
then have "∃ Ψ1. Ψ = Ψ1 ⊕ F ∇ [x].A" 
     by (rule_tac x="Ψ ⊖ F ∇ [x].A" in exI) (auto simp add:multiset_eq_iff)
then obtain Ψ1 where "S = (Φ ⇒* Ψ1 ⊕ F ∇ [x].A)" using ‹S = (Φ ⇒* Ψ)› by auto
have "Ps = map (extend S) ps" 
     using ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ F ∇ [x].A)› and extendRule_def and ‹r = (ps,c)› by auto
then have "∀ p ∈ set Ps. (∃ p'. p = extend S p')" using ex_map_conv[where ys=Ps and f="extend S"] by auto
then have "∀ p ∈ set Ps. (F ∇ [x].A ∈# succ p)" 
     using ‹F ∇ [x].A ∈# Ψ› and ‹S = (Φ ⇒* Ψ)› apply (auto simp add:Ball_def) 
     by (drule_tac x=xa in spec) (auto simp add:extend_def)
then have a1:"∀ p ∈ set Ps. ∃ Φ' Ψ'. p = (Φ' ⇒* Ψ' ⊕ F ∇ [x].A)" using characteriseSeq
     apply (auto simp add:Ball_def) apply (drule_tac x=xa in spec,simp) 
     apply (rule_tac x="antec xa" in exI,rule_tac x="succ xa ⊖ F ∇ [x].A" in exI) 
     by (drule_tac x=xa in meta_spec) (auto simp add:multiset_eq_iff)
with all have "∀ p ∈ set Ps. ∃ Φ' Ψ' n. n≤n' ∧ (Φ' ⇒* Ψ' ⊕ F ∇ [x].A,n) ∈ derivable R* ∧ p = (Φ' ⇒* Ψ' ⊕ F ∇ [x].A)"
                 by (auto simp add:Ball_def)
then have a2: "∀ p ∈ set Ps. ∃ Φ' Ψ' m. m≤n' ∧ (Φ' + Γ' ⇒* Ψ' + Δ',m) ∈ derivable R* ∧ p = (Φ' ⇒* Ψ' ⊕ F ∇ [x].A)"
                 using num and b' and IH and c'
                 apply (auto simp add:Ball_def) apply (drule_tac x=xa in spec) apply simp
                 apply hypsubst_thin
                 apply (elim exE conjE) apply (drule_tac x=n in spec) apply simp
                 apply (drule_tac x=Φ' in spec,drule_tac x=Ψ' in spec)
                 apply (simp) apply (elim exE conjE) by (rule_tac x=m' in exI) (arith)
obtain Ps' where eq: "Ps' = map (extend (Φ + Γ' ⇒* Ψ1 + Δ')) ps" by auto
have "length Ps = length Ps'" using ‹Ps' = map (extend (Φ + Γ' ⇒* Ψ1 + Δ')) ps›
                              and ‹Ps = map (extend S) ps› by auto
then have "Ps' ≠ []" using nonempty by auto
from ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3› have "r ∈ R" using ‹R = Ax ∪ R1 ∪ R2 ∪ R3› by auto
then have "extendRule (Φ + Γ' ⇒* Ψ1 + Δ') r ∈ R*" using ‹R = Ax ∪ R1 ∪ R2 ∪ R3›
     and extend_for_any_seq[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and r=r and S="Φ + Γ' ⇒* Ψ1 + Δ'"]
     and ‹R1 ⊆ upRules› and ‹R2 ⊆ nprovRules› and ‹R3 ⊆ provRules› by auto
moreover have "extendRule (Φ + Γ' ⇒* Ψ1 + Δ') r = (Ps',Γ + Γ' ⇒* Δ + Δ')"
         using ‹S = (Φ ⇒* Ψ1 ⊕ F ∇ [x].A)› and ‹extendRule S r = (Ps, Γ ⇒* Δ ⊕ F ∇ [x].A)›
         and ‹r = (ps,c)› and eq
         by (auto simp add:extendRule_def extend_def union_ac)
ultimately have "(Ps',Γ + Γ' ⇒* Δ + Δ') ∈ R*" by simp
have c1:"∀ p ∈ set ps. extend S p ∈ set Ps" using ‹Ps = map (extend S) ps› by (simp add:Ball_def)           
have c2:"∀ p ∈ set ps. extend (Φ + Γ' ⇒* Ψ1 + Δ') p ∈ set Ps'" using eq by (simp add:Ball_def)
then have eq2:"∀ p ∈ set Ps'. ∃ Φ' Ψ'. p = (Φ' + Γ' ⇒* Ψ' + Δ')" using eq
          by (auto simp add: extend_def) 
have d1:"∀ p ∈ set Ps. ∃ p' ∈ set ps. p = extend S p'" using ‹Ps = map (extend S) ps› by (auto simp add:Ball_def Bex_def)
then have "∀ p ∈ set Ps. ∃ p'. p' ∈ set Ps'" using c2 by (auto simp add:Ball_def Bex_def)
moreover have d2: "∀ p ∈ set Ps'. ∃ p' ∈ set ps. p = extend (Φ + Γ' ⇒* Ψ1 + Δ') p'" using eq
            by (auto simp add:Ball_def Bex_def)
then have "∀ p ∈ set Ps'. ∃ p'. p' ∈ set Ps" using c1 by (auto simp add:Ball_def Bex_def)
have "∀ Φ' Ψ'. (Φ' ⇒* Ψ' ⊕ F ∇ [x].A) ∈ set Ps ⟶ (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'"
               proof-
                 {fix Φ' Ψ'
                 assume "(Φ' ⇒* Ψ' ⊕ F ∇ [x].A) ∈ set Ps"  
                 then have "∃ p ∈ set ps. extend (Φ ⇒* Ψ1 ⊕ F ∇ [x].A) p = (Φ' ⇒* Ψ' ⊕ F ∇ [x].A)"
                      using ‹Ps = map (extend S) ps› and ‹S = (Φ ⇒* Ψ1 ⊕ F ∇ [x].A)› and a1 and d1
                           apply (simp only:Ball_def Bex_def) apply (drule_tac x=" Φ' ⇒* Ψ' ⊕ F ∇ [x].A" in spec)
                           by (drule_tac x="Φ' ⇒* Ψ' ⊕ F ∇ [x].A" in spec) (auto)
                 then obtain p where t:"p ∈ set ps ∧ (Φ' ⇒* Ψ' ⊕ F ∇ [x].A) = extend (Φ ⇒* Ψ1 ⊕ F ∇ [x].A) p"
                      apply auto by (drule_tac x=p in meta_spec) (simp)
                 then obtain D B where "p = (D ⇒* B)" by (cases p) 
                 then have "(D ⇒* B) ∈ set ps ∧ (Φ' ⇒* Ψ' ⊕ F ∇ [x].A) = extend (Φ ⇒* Ψ1 ⊕ F ∇ [x].A) (D ⇒* B)"
                      using t by auto
                 then have ant: "Φ' = Φ + D" and suc: "Ψ' ⊕ F ∇ [x].A = Ψ1 ⊕ F ∇ [x].A + B" using extend_def by auto
                 from ant have "Φ' + Γ' = (Φ + Γ') + D" by (auto simp add:union_ac)
                 moreover
                 from suc have "Ψ' = Ψ1 + B" by auto
                 then have "Ψ' + Δ' = (Ψ1 + Δ') + B" by (auto simp add:union_ac)
                 ultimately have "(Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ + Γ' ⇒* Ψ1 + Δ') (D ⇒* B)" using extend_def by auto
                 moreover have "extend (Φ + Γ' ⇒* Ψ1 + Δ') (D ⇒* B) ∈ set Ps'" using ‹p = (D ⇒* B)› and t and c2 by auto
                 ultimately have "(Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'" by simp
                 }
                 thus ?thesis by blast
               qed
            moreover
            have "∀ Φ' Ψ'. (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps' ⟶ (Φ' ⇒* Ψ' ⊕ F ∇ [x].A) ∈ set Ps"
               proof-
                 {fix Φ' Ψ'
                 assume "(Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'"  
                 then have "∃ p ∈ set ps. extend (Φ + Γ' ⇒* Ψ1 + Δ') p = (Φ' + Γ' ⇒* Ψ' + Δ')"
                      using eq and eq2 and d2
                           apply (simp only:Ball_def Bex_def) apply (drule_tac x="Φ' + Γ' ⇒* Ψ' + Δ'" in spec)
                           by (drule_tac x="Φ' + Γ' ⇒* Ψ' + Δ'" in spec) (auto)
                 then obtain p where t:"p ∈ set ps ∧ (Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ + Γ' ⇒* Ψ1 + Δ') p"
                      apply auto by (drule_tac x=p in meta_spec) (simp)
                 then obtain D B where "p = (D ⇒* B)" by (cases p) 
                 then have "(D ⇒* B) ∈ set ps ∧ (Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ + Γ' ⇒* Ψ1 + Δ') (D ⇒* B)"
                      using t by auto
                 then have ant: "Φ' + Γ' = Φ + Γ' + D" and suc: "Ψ' + Δ' = Ψ1 + Δ' + B" using extend_def by auto
                 from ant have "Φ' + Γ' = (Φ + D) + Γ'" by (auto simp add:union_ac)
                 then have "Φ' = Φ + D" by simp
                 moreover
                 from suc have "Ψ' + Δ' = (Ψ1 + B) + Δ'" by (auto simp add:union_ac)
                 then have "Ψ' = Ψ1 + B" by simp
                 then have "Ψ' ⊕ F ∇ [x].A = (Ψ1 ⊕ F ∇ [x].A) + B" by (auto simp add:union_ac)
                 ultimately have "(Φ' ⇒* Ψ' ⊕ F ∇ [x].A) = extend (Φ ⇒* Ψ1 ⊕ F ∇ [x].A) (D ⇒* B)" 
                      using extend_def by auto
                 moreover have "extend (Φ  ⇒* Ψ1 ⊕ F ∇ [x].A) (D ⇒* B) ∈ set Ps" using ‹p = (D ⇒* B)› and t and c1
                      and ‹S = (Φ ⇒* Ψ1 ⊕ F ∇ [x].A)› by auto
                 ultimately have "(Φ' ⇒* Ψ' ⊕ F ∇ [x].A) ∈ set Ps" by simp
                 }
                 thus ?thesis by blast
               qed
ultimately
have "∀ Φ' Ψ'. ((Φ' ⇒* Ψ' ⊕ F ∇ [x].A) ∈ set Ps) = ((Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps')" by auto
then have "∀ p ∈ set Ps'. ∃ Φ' Ψ' n. n≤n' ∧ (Φ' + Γ' ⇒* Ψ' + Δ',n) ∈ derivable R*
                ∧ p = (Φ' + Γ' ⇒* Ψ' + Δ')" using eq2 and a2
     apply (simp add:Ball_def) apply (intro allI impI) apply (drule_tac x=xa in spec) apply simp
     apply (elim exE) apply (drule_tac x=Φ' in spec,drule_tac x=Ψ' in spec)  
     by (drule_tac x="Φ' ⇒* Ψ' ⊕ F ∇ [x].A" in spec) (simp)
then have all:"∀ p ∈ set Ps'. ∃ n≤n'. (p,n) ∈ derivable R*" by auto
then show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" using num
     and ‹(Ps',Γ + Γ' ⇒* Δ + Δ') ∈ R*› and ‹Ps' ≠ []›
     and derivable.step[where r="(Ps',Γ + Γ' ⇒* Δ + Δ')" and R="R*"]
     by (auto simp add:Ball_def Bex_def)
qed


(* Non-principal Left *)
lemma nonPrincipalInvertLeft:
assumes "R1 ⊆ upRules" and "R2 ⊆ nprovRules" and "R3 ⊆ provRules"
    and "R = Ax ∪ R1 ∪ R2 ∪ R3" and "r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3" and "r = (ps,c)"
    and IH: "∀m<n. ∀Γ Δ. ( Γ ⊕ F ∇ [x].A ⇒* Δ, m) ∈ derivable R* ⟶
              (∀r' ∈ R. leftPrincipal r' (F ∇ [x].A) ⟶ ( Γ' ⇒* Δ') ∈ set (fst r')) ⟶
              (¬ multSubst Γ' ∧ ¬ multSubst Δ') ⟶
              (∃m'≤m. ( Γ + Γ' ⇒* Δ + Δ', m') ∈ derivable R*)"
    and a': "(Γ ⊕ F ∇ [x].A ⇒* Δ,n) ∈ derivable R*" 
    and b': "∀ r' ∈ R. leftPrincipal r' (F ∇ [x].A) ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
    and c': "¬ multSubst Γ' ∧ ¬ multSubst Δ'"
    and np: "¬ leftPrincipal r (F ∇ [x].A)"
    and ext: "extendRule S r = (Ps,Γ ⊕ F ∇ [x].A ⇒* Δ)"
    and num: "n = n' + 1"
    and all: "∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*"
    and nonempty: "Ps ≠ []"
shows "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
proof-
from ext obtain Φ Ψ where "S = (Φ ⇒* Ψ)" by (cases S) (auto)
from ‹r = (ps,c)› obtain G H where "c = (G ⇒* H)" by (cases c) (auto)
then have "\<LM> F ∇ [x].A  \<RM> ≠ G" using ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3›
     proof-
     {assume "r ∈ R1" then have "r ∈ upRules" using ‹R1 ⊆ upRules› by auto
      with ‹r = (ps,c)› obtain T Ts where "c = (\<Empt> ⇒* \<LM>Cpd0 T Ts\<RM>) ∨ c = (\<LM>Cpd0 T Ts\<RM> ⇒* \<Empt>)"
            using propRuleCharacterise[where Ps=ps and C=c] by auto
      moreover
        {assume "c = (\<Empt> ⇒* \<LM>Cpd0 T Ts\<RM>)"
         with ‹c = (G ⇒* H)› have "\<LM> F ∇ [x].A \<RM> ≠ G" by auto
        }
      moreover
        {assume "c = (\<LM>Cpd0 T Ts\<RM> ⇒* \<Empt>)"
         then have "\<LM>F ∇ [x].A \<RM> ≠ G" using ‹c = (G ⇒* H)› by auto
        }
      ultimately have "\<LM> F ∇ [x].A \<RM> ≠ G" by blast
     }
     moreover
     {assume "r ∈ R2 ∨ r ∈ R3" 
      then have "r ∈ provRules ∨ r ∈ nprovRules" using ‹R2 ⊆ nprovRules› and ‹R3 ⊆ provRules› by auto
      with ‹r = (ps,c)› obtain T y B where "c = (\<Empt> ⇒* \<LM> T ∇ [y].B \<RM>) ∨ c = (\<LM> T ∇ [y].B\<RM> ⇒* \<Empt>)"
            using provRuleCharacterise[where Ps=ps and C=c]
            and nprovRuleCharacterise[where Ps=ps and C=c] by auto
      moreover
        {assume "c = (\<Empt> ⇒* \<LM> T ∇ [y].B\<RM>)"
         then have "\<LM>F ∇ [x].A \<RM> ≠ G" using ‹c = (G ⇒* H)› by auto         
        }
      moreover
        {assume "c = (\<LM>T ∇ [y].B \<RM> ⇒* \<Empt>)"
         then have "leftPrincipal r (T ∇ [y].B)" using ‹r = (ps,c)› by auto
         with ‹¬ leftPrincipal r (F ∇ [x].A)› have "T ∇ [y].B ≠ F ∇ [x].A" by auto
         with ‹c = (G ⇒* H)› have "\<LM> F ∇ [x].A \<RM> ≠ G" using ‹c = (\<LM> T ∇ [y].B \<RM> ⇒* \<Empt>)› by auto
        }
      ultimately have "\<LM> F ∇ [x].A \<RM> ≠ G" by blast
     }
     ultimately show ?thesis using ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3› by blast
     qed
moreover have "antec S + antec (snd r) = (Γ ⊕ F ∇ [x].A)" 
         using ext and extendRule_def[where forms=S and R=r]
                   and extend_def[where forms=S and seq="snd r"] by auto
then have "Φ + G = Γ ⊕ F ∇ [x].A" using ‹S = (Φ ⇒* Ψ)› and ‹r = (ps,c)› and ‹c = (G ⇒* H)› by auto
moreover from ‹r = (ps,c)› and ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3› and ‹R1 ⊆ upRules› and ‹R2 ⊆ nprovRules›
              and ‹R3 ⊆ provRules› have "(ps,c) ∈ upRules ∨ (ps,c) ∈ nprovRules ∨ (ps,c) ∈ provRules" by auto
then have "∃ A. c = (\<Empt> ⇒* \<LM>A\<RM>) ∨ c = (\<LM>A\<RM> ⇒* \<Empt>)"
     using propRuleCharacterise[where Ps=ps and C=c]
       and nprovRuleCharacterise[where Ps=ps and C=c]
       and provRuleCharacterise[where Ps=ps and C=c] by auto
then have "G = \<Empt> ∨ (∃ A. G = \<LM>A\<RM>)" using ‹c = (G ⇒* H)› by auto
ultimately have "F ∇ [x].A ∈# Φ"
    proof-
    have "G = \<Empt> ∨ (∃ A. G = \<LM>A\<RM>)" by fact
    moreover
    {assume "G = \<Empt>"
     then have "Φ = Γ ⊕ F ∇ [x].A" using ‹Φ + G = Γ ⊕ F ∇ [x].A› by auto
     then have "F ∇ [x].A ∈# Φ" by auto
    }
    moreover
    {assume "∃ A. G = \<LM>A\<RM>"
     then obtain T where "G = \<LM>T\<RM>" by auto
     then have "Φ ⊕ T = Γ ⊕ F ∇ [x].A" using ‹Φ + G = Γ ⊕ F ∇ [x].A› by auto
     then have "set_mset (Φ ⊕ T) = set_mset (Γ ⊕ F ∇ [x].A)" by auto
     then have "set_mset Φ ∪ {T} = set_mset Γ ∪ {F ∇ [x].A}" by auto
     moreover from ‹G = \<LM>T\<RM>› and ‹\<LM>F ∇ [x].A\<RM> ≠ G› have "F ∇ [x].A ≠ T" by auto
     ultimately have "F ∇ [x].A ∈ set_mset Φ" by auto
     then have "F ∇ [x].A ∈# Φ" by auto
    }
    ultimately show "F ∇ [x].A ∈# Φ" by blast
    qed
then have "∃ Φ1. Φ = Φ1 ⊕ F ∇ [x].A" 
     by (rule_tac x="Φ ⊖ F ∇ [x].A" in exI) (auto simp add:multiset_eq_iff)
then obtain Φ1 where "S = (Φ1 ⊕ F ∇ [x].A ⇒* Ψ)" using ‹S = (Φ ⇒* Ψ)› by auto
have "Ps = map (extend S) ps" 
     using ‹extendRule S r = (Ps,Γ ⊕ F ∇ [x].A ⇒* Δ)› and extendRule_def and ‹r = (ps,c)› by auto
then have "∀ p ∈ set Ps. (∃ p'. p = extend S p')" using ex_map_conv[where ys=Ps and f="extend S"] by auto
then have "∀ p ∈ set Ps. (F ∇ [x].A ∈# antec p)" 
     using ‹F ∇ [x].A ∈# Φ› and ‹S = (Φ ⇒* Ψ)› apply (auto simp add:Ball_def) 
     by (drule_tac x=xa in spec) (auto simp add:extend_def)
then have a1:"∀ p ∈ set Ps. ∃ Φ' Ψ'. p = (Φ' ⊕ F ∇ [x].A ⇒* Ψ')" using characteriseSeq
     apply (auto simp add:Ball_def) apply (drule_tac x=xa in spec,simp) 
     apply (rule_tac x="antec xa ⊖ F ∇ [x].A" in exI,rule_tac x="succ xa" in exI) 
     by (drule_tac x=xa in meta_spec) (auto simp add:multiset_eq_iff)
with all have "∀ p ∈ set Ps. ∃ Φ' Ψ' n. n≤n' ∧ (Φ' ⊕ F ∇ [x].A ⇒* Ψ',n) ∈ derivable R* ∧ p = (Φ' ⊕ F ∇ [x].A ⇒* Ψ')"
                 by (auto simp add:Ball_def)
then have a2: "∀ p ∈ set Ps. ∃ Φ' Ψ' m. m≤n' ∧ (Φ' + Γ' ⇒* Ψ' + Δ',m) ∈ derivable R* ∧ p = (Φ' ⊕ F ∇ [x].A ⇒* Ψ')"
                 using num and b' and IH and c'
                 apply (auto simp add:Ball_def) apply (drule_tac x=xa in spec) apply simp
                 apply hypsubst_thin
                 apply (elim exE conjE) apply (drule_tac x=n in spec) apply simp
                 apply (drule_tac x=Φ' in spec,drule_tac x=Ψ' in spec)
                 apply (simp) apply (elim exE conjE) by (rule_tac x=m' in exI) (arith)
obtain Ps' where eq: "Ps' = map (extend (Φ1 + Γ' ⇒* Ψ + Δ')) ps" by auto
have "length Ps = length Ps'" using ‹Ps' = map (extend (Φ1 + Γ' ⇒* Ψ + Δ')) ps›
                              and ‹Ps = map (extend S) ps› by auto
then have "Ps' ≠ []" using nonempty by auto
from ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3› have "r ∈ R" using ‹R = Ax ∪ R1 ∪ R2 ∪ R3› by auto
then have "extendRule (Φ1 + Γ' ⇒* Ψ + Δ') r ∈ R*" using ‹R = Ax ∪ R1 ∪ R2 ∪ R3›
     and extend_for_any_seq[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and r=r and S="Φ1 + Γ' ⇒* Ψ + Δ'"]
     and ‹R1 ⊆ upRules› and ‹R2 ⊆ nprovRules› and ‹R3 ⊆ provRules› by auto
moreover have "extendRule (Φ1 + Γ' ⇒* Ψ + Δ') r = (Ps',Γ + Γ' ⇒* Δ + Δ')"
         using ‹S = (Φ1 ⊕ F ∇ [x].A ⇒* Ψ)› and ‹extendRule S r = (Ps, Γ ⊕ F ∇ [x].A ⇒* Δ)›
         and ‹r = (ps,c)› and eq
         by (auto simp add:extendRule_def extend_def)
ultimately have "(Ps',Γ + Γ' ⇒* Δ + Δ') ∈ R*" by simp
have c1:"∀ p ∈ set ps. extend S p ∈ set Ps" using ‹Ps = map (extend S) ps› by (simp add:Ball_def)           
have c2:"∀ p ∈ set ps. extend (Φ1 + Γ' ⇒* Ψ + Δ') p ∈ set Ps'" using eq by (simp add:Ball_def)
then have eq2:"∀ p ∈ set Ps'. ∃ Φ' Ψ'. p = (Φ' + Γ' ⇒* Ψ' + Δ')" using eq
          by (auto simp add:Ball_def extend_def) 
have d1:"∀ p ∈ set Ps. ∃ p' ∈ set ps. p = extend S p'" using ‹Ps = map (extend S) ps› by (auto simp add:Ball_def Bex_def)
then have "∀ p ∈ set Ps. ∃ p'. p' ∈ set Ps'" using c2 by (auto simp add:Ball_def Bex_def)
moreover have d2: "∀ p ∈ set Ps'. ∃ p' ∈ set ps. p = extend (Φ1 + Γ' ⇒* Ψ + Δ') p'" using eq
            by (auto simp add:Ball_def Bex_def)
then have "∀ p ∈ set Ps'. ∃ p'. p' ∈ set Ps" using c1 by (auto simp add:Ball_def Bex_def)
have "∀ Φ' Ψ'. (Φ' ⊕ F ∇ [x].A ⇒* Ψ') ∈ set Ps ⟶ (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'"
               proof-
                 {fix Φ' Ψ'
                 assume "(Φ' ⊕ F ∇ [x].A ⇒* Ψ') ∈ set Ps"  
                 then have "∃ p ∈ set ps. extend (Φ1 ⊕ F ∇ [x].A ⇒* Ψ) p = (Φ' ⊕ F ∇ [x].A ⇒* Ψ')"
                      using ‹Ps = map (extend S) ps› and ‹S = (Φ1 ⊕ F ∇ [x].A ⇒* Ψ)› and a1 and d1
                           apply (simp only:Ball_def Bex_def) apply (drule_tac x=" Φ' ⊕ F ∇ [x].A ⇒* Ψ'" in spec)
                           by (drule_tac x="Φ' ⊕ F ∇ [x].A ⇒* Ψ'" in spec) (auto)
                 then obtain p where t:"p ∈ set ps ∧ (Φ' ⊕ F ∇ [x].A ⇒* Ψ') = extend (Φ1 ⊕ F ∇ [x].A ⇒* Ψ) p"
                      apply auto by (drule_tac x=p in meta_spec) (simp)
                 then obtain D B where "p = (D ⇒* B)" by (cases p) 
                 then have "(D ⇒* B) ∈ set ps ∧ (Φ' ⊕ F ∇ [x].A ⇒* Ψ') = extend (Φ1 ⊕ F ∇ [x].A ⇒* Ψ) (D ⇒* B)"
                      using t by auto
                 then have ant: "Φ' ⊕ F ∇ [x].A = Φ1 ⊕ F ∇ [x].A + D" and suc: "Ψ' = Ψ + B" using extend_def by auto
                 from suc have "Ψ' + Δ' = (Ψ + Δ') + B" by (auto simp add:union_ac)
                 moreover
                 from ant have "Φ' = Φ1 + D" by auto
                 then have "Φ' + Γ' = (Φ1 + Γ') + D" by (auto simp add:union_ac)
                 ultimately have "(Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ1 + Γ' ⇒* Ψ + Δ') (D ⇒* B)" using extend_def by auto
                 moreover have "extend (Φ1 + Γ' ⇒* Ψ + Δ') (D ⇒* B) ∈ set Ps'" using ‹p = (D ⇒* B)› and t and c2 by auto
                 ultimately have "(Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'" by simp
                 }
                 thus ?thesis by blast
               qed
            moreover
            have "∀ Φ' Ψ'. (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps' ⟶ (Φ' ⊕ F ∇ [x].A ⇒* Ψ') ∈ set Ps"
               proof-
                 {fix Φ' Ψ'
                 assume "(Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'"  
                 then have "∃ p ∈ set ps. extend (Φ1 + Γ' ⇒* Ψ + Δ') p = (Φ' + Γ' ⇒* Ψ' + Δ')"
                      using eq and eq2 and d2
                           apply (simp only:Ball_def Bex_def) apply (drule_tac x="Φ' + Γ' ⇒* Ψ' + Δ'" in spec)
                           by (drule_tac x="Φ' + Γ' ⇒* Ψ' + Δ'" in spec) (auto)
                 then obtain p where t:"p ∈ set ps ∧ (Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ1 + Γ' ⇒* Ψ + Δ') p"
                      apply auto by (drule_tac x=p in meta_spec) (simp)
                 then obtain D B where "p = (D ⇒* B)" by (cases p) 
                 then have "(D ⇒* B) ∈ set ps ∧ (Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ1 + Γ' ⇒* Ψ + Δ') (D ⇒* B)"
                      using t by auto
                 then have ant: "Φ' + Γ' = Φ1 + Γ' + D" and suc: "Ψ' + Δ' = Ψ + Δ' + B" using extend_def by auto
                 from ant have "Φ' + Γ' = (Φ1 + D) + Γ'" by (auto simp add:union_ac)
                 then have "Φ' = Φ1 + D" by simp
                 then have "Φ' ⊕ F ∇ [x].A = (Φ1 ⊕ F ∇ [x].A) + D" by (auto simp add:union_ac)
                 moreover
                 from suc have "Ψ' + Δ' = (Ψ + B) + Δ'" by (auto simp add:union_ac)
                 then have "Ψ' = Ψ + B" by simp
                 ultimately have "(Φ' ⊕ F ∇ [x].A ⇒* Ψ') = extend (Φ1 ⊕ F ∇ [x].A ⇒* Ψ) (D ⇒* B)" 
                      using extend_def by auto
                 moreover have "extend (Φ1 ⊕ F ∇ [x].A  ⇒* Ψ) (D ⇒* B) ∈ set Ps" using ‹p = (D ⇒* B)› and t and c1
                      and ‹S = (Φ1 ⊕ F ∇ [x].A ⇒* Ψ)› by auto
                 ultimately have "(Φ' ⊕ F ∇ [x].A ⇒* Ψ') ∈ set Ps" by simp
                 }
                 thus ?thesis by blast
               qed
ultimately
have "∀ Φ' Ψ'. ((Φ' ⊕ F ∇ [x].A ⇒* Ψ') ∈ set Ps) = ((Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps')" by auto
then have "∀ p ∈ set Ps'. ∃ Φ' Ψ' n. n≤n' ∧ (Φ' + Γ' ⇒* Ψ' + Δ',n) ∈ derivable R*
                ∧ p = (Φ' + Γ' ⇒* Ψ' + Δ')" using eq2 and a2
     apply (simp add:Ball_def) apply (intro allI impI) apply (drule_tac x=xa in spec) apply simp
     apply (elim exE) apply (drule_tac x=Φ' in spec,drule_tac x=Ψ' in spec)  
     by (drule_tac x="Φ' ⊕ F ∇ [x].A ⇒* Ψ'" in spec) (simp)
then have all:"∀ p ∈ set Ps'. ∃ n≤n'. (p,n) ∈ derivable R*" by auto
then show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" using num
     and ‹(Ps',Γ + Γ' ⇒* Δ + Δ') ∈ R*› and ‹Ps' ≠ []›
     and derivable.step[where r="(Ps',Γ + Γ' ⇒* Δ + Δ')" and R="R*"]
     by (auto simp add:Ball_def Bex_def)
qed
(*>*)

text‹
\noindent We can then give the two inversion lemmata.  The principal case (where the last inference had a freshness proviso) for the right inversion lemma is shown:
›
lemma rightInvert:
fixes Γ Δ :: "form multiset"
assumes rules: "R1 ⊆ upRules ∧ R2 ⊆ nprovRules ∧ R3 ⊆ provRules ∧ R = Ax ∪ R1 ∪ R2 ∪ R3"
    and   a: "(Γ ⇒* Δ ⊕ F ∇ [x].A,n) ∈ derivable R*"
    and   b: "∀ r' ∈ R. rightPrincipal r' (F ∇ [x].A) ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
    and   c: "¬ multSubst Γ' ∧ ¬ multSubst Δ'"
shows "∃ m≤n. (Γ +Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
(*<*)
using assms
proof (induct n arbitrary: Γ Δ rule:nat_less_induct)
 case (1 n Γ Δ)
 then have IH:"∀m<n. ∀Γ Δ. ( Γ ⇒* Δ ⊕ F ∇ [x].A, m) ∈ derivable R* ⟶
              (∀r' ∈ R. rightPrincipal r' (F ∇ [x].A) ⟶ ( Γ' ⇒* Δ') ∈ set (fst r')) ⟶
              (¬ multSubst Γ' ∧ ¬ multSubst Δ') ⟶
              (∃m'≤m. ( Γ + Γ' ⇒* Δ + Δ', m') ∈ derivable R*)" 
     and a': "(Γ ⇒* Δ ⊕ F ∇ [x].A,n) ∈ derivable R*" 
     and b': "∀ r' ∈ R. rightPrincipal r' (F ∇ [x].A) ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
     and c': "¬ multSubst Γ' ∧ ¬ multSubst Δ'"
       by auto
 show ?case
 proof (cases n)
     case 0
     then have "(Γ ⇒* Δ ⊕ F ∇ [x].A,0) ∈ derivable R*" using a' by simp
     then have "([],Γ ⇒* Δ ⊕ F ∇ [x].A) ∈ R*" by (cases) (auto)
     then have "∃ r S. extendRule S r = ([],Γ ⇒* Δ ⊕ F ∇ [x].A) ∧ (r ∈ Ax ∨ r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3)"
          using rules and ruleSet[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and Ps="[]" and C="Γ ⇒* Δ ⊕ F ∇ [x].A"]
           by auto
     then obtain r S where "extendRule S r = ([],Γ ⇒* Δ ⊕ F ∇ [x].A)" and "r ∈ Ax ∨ r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3" by auto
      moreover
      {assume "r ∈ Ax"
       then obtain i xs where "([], \<LM> At i xs \<RM> ⇒* \<LM> At i xs \<RM>) = r ∨ r = ([],\<LM>ff\<RM> ⇒* \<Empt>)" 
            using characteriseAx[where r=r] by auto
       moreover 
           {assume "r = ([],\<LM>At i xs\<RM> ⇒* \<LM>At i xs\<RM>)"
            with ‹extendRule S r = ([],Γ ⇒* Δ ⊕ F ∇ [x].A)›
               have "extend S (\<LM> At i xs \<RM> ⇒* \<LM> At i xs \<RM>) = (Γ ⇒* Δ ⊕ F ∇ [x].A)"
               using extendRule_def[where R="([],\<LM>At i xs\<RM> ⇒* \<LM>At i xs\<RM>)" and forms=S] by auto
            then have "At i xs ∈# Γ ∧ At i xs ∈# Δ" 
                 using extendID[where S=S and i=i and xs=xs and Γ=Γ and Δ="Δ ⊕ F ∇ [x].A"] by auto
            then have "At i xs ∈# Γ + Γ' ∧ At i xs ∈# Δ + Δ'" by auto
            then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" using rules
                 and containID[where Γ="Γ + Γ'" and i=i and Δ="Δ + Δ'" and R=R] by auto
           }
       moreover
           {assume "r = ([],\<LM>ff\<RM> ⇒* \<Empt>)"
            with ‹extendRule S r = ([],Γ ⇒* Δ ⊕ F ∇ [x].A)›
               have "extend S (\<LM> ff \<RM> ⇒* \<Empt>) = (Γ ⇒* Δ ⊕ F ∇ [x].A)"
               using extendRule_def[where R="([],\<LM>ff\<RM> ⇒* \<Empt>)" and forms=S] by auto
            then have "ff ∈# Γ" 
                 using extendFalsum[where S=S and Γ=Γ and Δ="Δ ⊕ F ∇ [x].A"] by auto
            then have "ff ∈# Γ + Γ'" by auto
            then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" using rules
                 and containFalsum[where Γ="Γ + Γ'" and Δ="Δ + Δ'" and R=R] by auto
           }
       ultimately have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" by blast      
      }
      moreover
      {assume "r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3"
       then have "∃ Ps C. Ps ≠ [] ∧ r = (Ps,C)"
            proof-
            obtain y z where "r = (y,z)" by (cases r)
            with ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3› have "(y,z) ∈ R1 ∨ (y,z) ∈ R2 ∨ (y,z) ∈ R3" by simp
            then have "y ≠ []"
                 proof-
                 {assume "(y,z) ∈ R1"
                  then have "(y,z) ∈ upRules" using rules by auto
                  then have "y≠[]" by (cases) auto
                 }
                 moreover
                 {assume "(y,z) ∈ R2"
                  then have "(y,z) ∈ nprovRules" using rules by auto
                  then have "y≠[]" by (cases) auto
                 }
                 moreover
                 {assume "(y,z) ∈ R3"
                  then have "(y,z) ∈ provRules" using rules by auto
                  then have "y≠[]" by (cases) auto
                 }
                 ultimately show "y ≠ []" using ‹(y,z) ∈ R1 ∨ (y,z) ∈ R2 ∨ (y,z) ∈ R3› by blast
                 qed
            then show "∃ Ps C. Ps ≠ [] ∧ r = (Ps,C)" using ‹r = (y,z)›  by blast
            qed
       then obtain Ps C where "Ps ≠ []" and "r = (Ps,C)" by auto
       moreover from ‹extendRule S r = ([], Γ ⇒* Δ ⊕ F ∇ [x].A)› have "∃ S. r = ([],S)"
            using extendRule_def[where forms=S and R=r] by (cases r) (auto)
       then obtain S where "r = ([],S)" by blast
       ultimately have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" using rules by simp
       }
       ultimately show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" using ‹n=0› by blast
 next
     case (Suc n')
     then have "(Γ ⇒* Δ ⊕ F ∇ [x].A,n'+1) ∈ derivable R*" using a' by simp
     then obtain Ps where "(Ps, Γ ⇒* Δ ⊕ F ∇ [x].A) ∈ R*" and 
                          "Ps ≠ []" and 
                       d':"∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*"
          using characteriseLast[where C="Γ ⇒* Δ ⊕ F ∇ [x].A" and m=n' and R="R*"] by auto
     then have "∃ r S. (r ∈ Ax ∨ r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3) ∧ extendRule S r = (Ps, Γ ⇒* Δ ⊕ F ∇ [x].A)"
          using rules 
            and ruleSet[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and Ps=Ps and C="Γ ⇒* Δ ⊕ F ∇ [x].A"] by auto
     then obtain r S where "r ∈ Ax ∨ r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3" 
                    and e':"extendRule S r = (Ps, Γ ⇒* Δ ⊕ F ∇ [x].A)" by auto
     moreover
        {assume "r ∈ Ax"
         then have "fst r = []" apply (cases r) by (rule Ax.cases) auto
         moreover have "fst r ≠ []" using ‹Ps ≠ []› and ‹extendRule S r = (Ps, Γ ⇒* Δ ⊕ F ∇ [x].A)›
                            and extendRule_def[where forms=S and R=r]
                            and extend_def[where forms=S and seq="snd r"] by auto
         ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by simp
        }
     moreover
        {assume "r ∈ R1"
         obtain ps c where "r = (ps,c)" by (cases r) auto
         then have "r ∈ upRules" using rules and ‹r ∈ R1› by auto
         then obtain T Ts where sw:"c = (\<Empt> ⇒* \<LM> Cpd0 T Ts \<RM>) ∨ c = (\<LM> Cpd0 T Ts \<RM> ⇒* \<Empt>)"
              using propRuleCharacterise[where Ps=ps and C=c] and ‹r = (ps,c)› by auto
         have "(rightPrincipal r (F ∇ [x].A)) ∨ ¬(rightPrincipal r (F ∇ [x].A))" by blast
         moreover
            {assume "rightPrincipal r (F ∇ [x].A)"
             then have "c = (\<Empt> ⇒* \<LM> F ∇ [x].A \<RM>)" using ‹r=  (ps,c)› by (cases) auto
             with sw have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by auto
            }
         moreover
            {assume "¬ rightPrincipal r (F ∇ [x].A)"
             then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
                  using nonPrincipalInvertRight[where r=r and F=F and x=x and A=A and ps=ps and c=c and R=R
                                                and Γ'=Γ' and Δ'=Δ' and ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3
                                                and S=S and Ps=Ps and Γ=Γ and Δ=Δ and n=n and n'=n']
                  and ‹n = Suc n'› and ‹Ps ≠ []› and a' and b' and e'
                  and c' and rules and IH and ‹r ∈ R1› and d' and ‹r = (ps,c)› by auto
            }
         ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by blast         
        }
     moreover
        {assume "r ∈ R2"
         obtain ps c where "r = (ps,c)" by (cases r) auto
         then have "r ∈ nprovRules" using rules and ‹r ∈ R2› by auto
         have "rightPrincipal r (F ∇ [x].A) ∨ ¬ rightPrincipal r (F ∇ [x].A)" by blast
         moreover
            {assume "rightPrincipal r (F ∇ [x].A)"
             then have "(Γ' ⇒* Δ') ∈ set ps" using b' and ‹r = (ps,c)› and ‹r ∈ R2› and rules
                  by auto
             then have "extend S (Γ' ⇒* Δ') ∈ set Ps" using ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ F ∇ [x].A)›
                  and ‹r = (ps,c)› by (simp add:extendContain)
             moreover from ‹rightPrincipal r (F ∇ [x].A)› have "c = (\<Empt> ⇒* \<LM>F ∇ [x].A\<RM>)" 
                  using ‹r = (ps,c)› by (cases) auto
             with ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ F ∇ [x].A)› have "S = (Γ ⇒* Δ)"
                  using ‹r = (ps,c)› apply (auto simp add:extendRule_def extend_def) by (cases S) auto
             ultimately have "(Γ + Γ' ⇒* Δ + Δ') ∈ set Ps" by (simp add:extend_def)
             then have "∃ m≤n'. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
                  using ‹∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*› by auto
             then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" using ‹n = Suc n'›
                  by (auto,rule_tac x=m in exI) (simp)
            }
         moreover
            {assume "¬ rightPrincipal r (F ∇ [x].A)"
             then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
                  using nonPrincipalInvertRight[where r=r and F=F and x=x and A=A and ps=ps and c=c and R=R
                                                and Γ'=Γ' and Δ'=Δ' and ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3
                                                and S=S and Ps=Ps and Γ=Γ and Δ=Δ and n=n and n'=n']
                  and ‹n = Suc n'› and ‹Ps ≠ []› and a' and b' and e'
                  and c' and rules and IH and ‹r ∈ R2› and d' and ‹r = (ps,c)› by auto
            }
         ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by blast
        }
     moreover


  {(*>*)
   
   
   assume "r ∈ R3"
   obtain ps c where "r = (ps,c)" by (cases r) auto
   then have "r ∈ provRules" using rules and ‹r ∈ R3› by auto
   have "rightPrincipal r (F ∇ [x].A) ∨ ¬ rightPrincipal r (F ∇ [x].A)" by blast
   moreover
      {assume "rightPrincipal r (F ∇ [x].A)"
       then have "(Γ' ⇒* Δ') ∈ set ps" using(*<*) b' and(*>*) ‹r = (ps,c)› and ‹r ∈ R3› and rules
            by auto
       then have "extend S (Γ' ⇒* Δ') ∈ set Ps" using 
           ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ F ∇ [x].A)›
            and ‹r = (ps,c)› by (simp add:extendContain)
       moreover from ‹rightPrincipal r (F ∇ [x].A)› have 
            "c = (\<Empt> ⇒* \<LM>F ∇ [x].A\<RM>)" 
            using ‹r = (ps,c)› by (cases) auto
       with ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ F ∇ [x].A)› have "S = (Γ ⇒* Δ)"
            using ‹r = (ps,c)› (*<*)apply (auto simp add:extendRule_def extend_def)(*>*) by (cases S) auto
       ultimately have "(Γ + Γ' ⇒* Δ + Δ') ∈ set Ps" by (simp add:extend_def)
       then have "∃ m≤n'. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
            using ‹∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*› by auto
       then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" 
            using ‹n = Suc n'› by (*<*)(auto,rule_tac x=m in exI)(*>*) (simp)
      }
(*<*)
         moreover
            {assume "¬ rightPrincipal r (F ∇ [x].A)"
             then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
                  using nonPrincipalInvertRight[where r=r and F=F and x=x and A=A and ps=ps and c=c and R=R
                                                and Γ'=Γ' and Δ'=Δ' and ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3
                                                and S=S and Ps=Ps and Γ=Γ and Δ=Δ and n=n and n'=n']
                  and ‹n = Suc n'› and ‹Ps ≠ []› and a' and b' and e'
                  and c' and rules and IH and ‹r ∈ R3› and d' and ‹r = (ps,c)› by auto
            }
         ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by blast
        }
     ultimately show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by blast
   qed
qed
(*>*)


lemma leftInvert:
fixes Γ Δ :: "form multiset"
assumes rules: "R1 ⊆ upRules ∧ R2 ⊆ nprovRules ∧ R3 ⊆ provRules ∧ R = Ax ∪ R1 ∪ R2 ∪ R3"
    and   a: "(Γ ⊕ F ∇ [x].A ⇒* Δ,n) ∈ derivable R*"
    and   b: "∀ r' ∈ R. leftPrincipal r' (F ∇ [x].A) ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
    and   c: "¬ multSubst Γ' ∧ ¬ multSubst Δ'"
shows "∃ m≤n. (Γ +Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
(*<*)
using assms
proof (induct n arbitrary: Γ Δ rule:nat_less_induct)
 case (1 n Γ Δ)
 then have IH:"∀m<n. ∀Γ Δ. ( Γ ⊕ F ∇ [x].A ⇒* Δ, m) ∈ derivable R* ⟶
              (∀r' ∈ R. leftPrincipal r' (F ∇ [x].A) ⟶ ( Γ' ⇒* Δ') ∈ set (fst r')) ⟶
              (¬ multSubst Γ' ∧ ¬ multSubst Δ') ⟶
              (∃m'≤m. ( Γ + Γ' ⇒* Δ + Δ', m') ∈ derivable R*)" 
     and a': "(Γ ⊕ F ∇ [x].A ⇒* Δ,n) ∈ derivable R*" 
     and b': "∀ r' ∈ R. leftPrincipal r' (F ∇ [x].A) ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
     and c': "¬ multSubst Γ' ∧ ¬ multSubst Δ'"
       by auto
 show ?case
 proof (cases n)
     case 0
     then have "(Γ ⊕ F ∇ [x].A ⇒* Δ,0) ∈ derivable R*" using a' by simp
     then have "([],Γ ⊕ F ∇ [x].A ⇒* Δ) ∈ R*" by (cases) (auto)
     then have "∃ r S. extendRule S r = ([],Γ ⊕ F ∇ [x].A ⇒* Δ) ∧ (r ∈ Ax ∨ r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3)"
          using rules and ruleSet[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and Ps="[]" and C="Γ ⊕ F ∇ [x].A ⇒*Δ"]
           by auto
     then obtain r S where "extendRule S r = ([],Γ ⊕ F ∇ [x].A ⇒* Δ)" and "r ∈ Ax ∨ r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3" by auto
      moreover
      {assume "r ∈ Ax"
       then obtain i xs where "r = ([],\<LM>At i xs\<RM> ⇒* \<LM>At i xs\<RM>) ∨ r = ([], \<LM>ff\<RM> ⇒* \<Empt>)"
            using characteriseAx[where r=r] by auto
       moreover 
           {assume "r = ([],\<LM>At i xs\<RM> ⇒* \<LM>At i xs\<RM>)"
            with ‹extendRule S r = ([],Γ ⊕ F ∇ [x].A ⇒* Δ)›
               have "extend S (\<LM> At i xs \<RM> ⇒* \<LM> At i xs \<RM>) = (Γ ⊕ F ∇ [x].A ⇒* Δ)"
               using extendRule_def[where R="([],\<LM>At i xs\<RM> ⇒* \<LM>At i xs\<RM>)" and forms=S] by auto
            then have "At i xs ∈# Γ ∧ At i xs ∈# Δ" 
                 using extendID[where S=S and i=i and xs=xs and Γ="Γ⊕ F ∇ [x].A" and Δ=Δ] by auto
            then have "At i xs ∈# Γ + Γ' ∧ At i xs ∈# Δ + Δ'" by auto
            then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" using rules
                 and containID[where Γ="Γ + Γ'" and i=i and Δ="Δ + Δ'" and R=R] by auto
           }
       moreover
           {assume "r = ([],\<LM>ff\<RM> ⇒* \<Empt>)"
            with ‹extendRule S r = ([],Γ ⊕ F ∇ [x].A ⇒* Δ)›
               have "extend S (\<LM> ff \<RM> ⇒* \<Empt>) = (Γ ⊕ F ∇ [x].A ⇒* Δ)"
               using extendRule_def[where R="([],\<LM>ff\<RM> ⇒* \<Empt>)" and forms=S] by auto
            then have "ff ∈# Γ" 
                 using extendFalsum[where S=S and Γ="Γ⊕F ∇ [x].A" and Δ=Δ] by auto
            then have "ff ∈# Γ + Γ'" by auto
            then have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" using rules
                 and containFalsum[where Γ="Γ + Γ'" and Δ="Δ + Δ'" and R=R] by auto
           }
       ultimately have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" by blast      
      }
      moreover
      {assume "r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3"
       then have "∃ Ps C. Ps ≠ [] ∧ r = (Ps,C)"
            proof-
            obtain y z where "r = (y,z)" by (cases r)
            with ‹r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3› have "(y,z) ∈ R1 ∨ (y,z) ∈ R2 ∨ (y,z) ∈ R3" by simp
            then have "y ≠ []"
                 proof-
                 {assume "(y,z) ∈ R1"
                  then have "(y,z) ∈ upRules" using rules by auto
                  then have "y≠[]" by (cases) auto
                 }
                 moreover
                 {assume "(y,z) ∈ R2"
                  then have "(y,z) ∈ nprovRules" using rules by auto
                  then have "y≠[]" by (cases) auto
                 }
                 moreover
                 {assume "(y,z) ∈ R3"
                  then have "(y,z) ∈ provRules" using rules by auto
                  then have "y≠[]" by (cases) auto
                 }
                 ultimately show "y ≠ []" using ‹(y,z) ∈ R1 ∨ (y,z) ∈ R2 ∨ (y,z) ∈ R3› by blast
                 qed
            then show "∃ Ps C. Ps ≠ [] ∧ r = (Ps,C)" using ‹r = (y,z)›  by blast
            qed
       then obtain Ps C where "Ps ≠ []" and "r = (Ps,C)" by auto
       moreover from ‹extendRule S r = ([], Γ ⊕ F ∇ [x].A ⇒* Δ)› have "∃ S. r = ([],S)"
            using extendRule_def[where forms=S and R=r] by (cases r) (auto)
       then obtain S where "r = ([],S)" by blast
       ultimately have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" using rules by simp
       }
       ultimately show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" using ‹n=0› by blast
 next
     case (Suc n')
     then have "(Γ ⊕ F ∇ [x].A ⇒* Δ,n'+1) ∈ derivable R*" using a' by simp
     then obtain Ps where "(Ps, Γ ⊕ F ∇ [x].A ⇒* Δ) ∈ R*" and 
                          "Ps ≠ []" and 
                       d':"∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*"
          using characteriseLast[where C="Γ ⊕ F ∇ [x].A ⇒* Δ" and m=n' and R="R*"] by auto
     then have "∃ r S. (r ∈ Ax ∨ r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3) ∧ extendRule S r = (Ps, Γ ⊕ F ∇ [x].A ⇒* Δ)"
          using rules 
            and ruleSet[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and Ps=Ps and C="Γ ⊕ F ∇ [x].A ⇒* Δ"] by auto
     then obtain r S where "r ∈ Ax ∨ r ∈ R1 ∨ r ∈ R2 ∨ r ∈ R3" 
                    and e':"extendRule S r = (Ps, Γ ⊕ F ∇ [x].A ⇒* Δ)" by auto
     moreover
        {assume "r ∈ Ax"
         then have "fst r = []" apply (cases r) by (rule Ax.cases) auto
         moreover have "fst r ≠ []" using ‹Ps ≠ []› and ‹extendRule S r = (Ps, Γ ⊕ F ∇ [x].A ⇒* Δ)›
                            and extendRule_def[where forms=S and R=r]
                            and extend_def[where forms=S and seq="snd r"] by auto
         ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by auto
        }
     moreover
        {assume "r ∈ R1"
         obtain ps c where "r = (ps,c)" by (cases r) auto
         then have "r ∈ upRules" using rules and ‹r ∈ R1› by auto
         then obtain T Ts where sw:"c = (\<Empt> ⇒* \<LM> Cpd0 T Ts \<RM>) ∨ c = (\<LM> Cpd0 T Ts \<RM> ⇒* \<Empt>)"
              using propRuleCharacterise[where Ps=ps and C=c] and ‹r = (ps,c)› by auto
         have "(leftPrincipal r (F ∇ [x].A)) ∨ ¬(leftPrincipal r (F ∇ [x].A))" by blast
         moreover
            {assume "leftPrincipal r (F ∇ [x].A)"
             then have "c = (\<LM> F ∇ [x].A \<RM> ⇒* \<Empt>)" using ‹r=  (ps,c)› by (cases) auto
             with sw have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by auto
            }
         moreover
            {assume "¬ leftPrincipal r (F ∇ [x].A)"
             then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
                  using nonPrincipalInvertLeft[where r=r and F=F and x=x and A=A and ps=ps and c=c and R=R
                                                and Γ'=Γ' and Δ'=Δ' and ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3
                                                and S=S and Ps=Ps and Γ=Γ and Δ=Δ and n=n and n'=n']
                  and ‹n = Suc n'› and ‹Ps ≠ []› and a' and b' and e'
                  and c' and rules and IH and ‹r ∈ R1› and d' and ‹r = (ps,c)› by auto
            }
         ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by blast         
        }
     moreover
        {assume "r ∈ R2"
         obtain ps c where "r = (ps,c)" by (cases r) auto
         then have "r ∈ nprovRules" using rules and ‹r ∈ R2› by auto
         have "leftPrincipal r (F ∇ [x].A) ∨ ¬ leftPrincipal r (F ∇ [x].A)" by blast
         moreover
            {assume "leftPrincipal r (F ∇ [x].A)"
             then have "(Γ' ⇒* Δ') ∈ set ps" using b' and ‹r = (ps,c)› and ‹r ∈ R2› and rules
                  by auto
             then have "extend S (Γ' ⇒* Δ') ∈ set Ps" using ‹extendRule S r = (Ps,Γ ⊕ F ∇ [x].A ⇒* Δ)›
                  and ‹r = (ps,c)› by (simp add:extendContain)
             moreover from ‹leftPrincipal r (F ∇ [x].A)› have "c = (\<LM>F ∇ [x].A\<RM> ⇒* \<Empt>)" 
                  using ‹r = (ps,c)› by (cases) auto
             with ‹extendRule S r = (Ps,Γ ⊕ F ∇ [x].A ⇒* Δ)› have "S = (Γ ⇒* Δ)"
                  using ‹r = (ps,c)› apply (auto simp add:extendRule_def extend_def) by (cases S) auto
             ultimately have "(Γ + Γ' ⇒* Δ + Δ') ∈ set Ps" by (simp add:extend_def)
             then have "∃ m≤n'. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
                  using ‹∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*› by auto
             then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" using ‹n = Suc n'›
                  by (auto,rule_tac x=m in exI) (simp)
            }
         moreover
            {assume "¬ leftPrincipal r (F ∇ [x].A)"
             then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
                  using nonPrincipalInvertLeft[where r=r and F=F and x=x and A=A and ps=ps and c=c and R=R
                                                and Γ'=Γ' and Δ'=Δ' and ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3
                                                and S=S and Ps=Ps and Γ=Γ and Δ=Δ and n=n and n'=n']
                  and ‹n = Suc n'› and ‹Ps ≠ []› and a' and b' and e'
                  and c' and rules and IH and ‹r ∈ R2› and d' and ‹r = (ps,c)› by auto
            }
         ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by blast
        }
     moreover
        {assume "r ∈ R3"
         obtain ps c where "r = (ps,c)" by (cases r) auto
         then have "r ∈ provRules" using rules and ‹r ∈ R3› by auto
         have "leftPrincipal r (F ∇ [x].A) ∨ ¬ leftPrincipal r (F ∇ [x].A)" by blast
         moreover
            {assume "leftPrincipal r (F ∇ [x].A)"
             then have "(Γ' ⇒* Δ') ∈ set ps" using b' and ‹r = (ps,c)› and ‹r ∈ R3› and rules
                  by auto
             then have "extend S (Γ' ⇒* Δ') ∈ set Ps" using ‹extendRule S r = (Ps,Γ ⊕ F ∇ [x].A ⇒* Δ)›
                  and ‹r = (ps,c)› by (simp add:extendContain)
             moreover from ‹leftPrincipal r (F ∇ [x].A)› have "c = (\<LM>F ∇ [x].A\<RM> ⇒* \<Empt>)" 
                  using ‹r = (ps,c)› by (cases) auto
             with ‹extendRule S r = (Ps,Γ ⊕ F ∇ [x].A⇒* Δ)› have "S = (Γ ⇒* Δ)"
                  using ‹r = (ps,c)› apply (auto simp add:extendRule_def extend_def) by (cases S) auto
             ultimately have "(Γ + Γ' ⇒* Δ + Δ') ∈ set Ps" by (simp add:extend_def)
             then have "∃ m≤n'. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
                  using ‹∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*› by auto
             then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" using ‹n = Suc n'›
                  by (auto,rule_tac x=m in exI) (simp)
            }
         moreover
            {assume "¬ leftPrincipal r (F ∇ [x].A)"
             then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
                  using nonPrincipalInvertLeft[where r=r and F=F and x=x and A=A and ps=ps and c=c and R=R
                                                and Γ'=Γ' and Δ'=Δ' and ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3
                                                and S=S and Ps=Ps and Γ=Γ and Δ=Δ and n=n and n'=n']
                  and ‹n = Suc n'› and ‹Ps ≠ []› and a' and b' and e'
                  and c' and rules and IH and ‹r ∈ R3› and d' and ‹r = (ps,c)› by auto
            }
         ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by blast
        }
     ultimately show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by blast
   qed
qed
(*>*)

text‹
\noindent In both cases, the assumption labelled $c$ captures the ``no specific substitution'' condition.  Interestingly, it is never used throughout the proof.  This highlights the difference between the object- and meta-level existential quantifiers.

Owing to the lack of indexing within datatypes, it is difficult to give an example demonstrating these results.  It would be little effort to change the theory file to accommodate type variables when they are supported in \textit{Nominal Isabelle}, at which time an example would be simple to write.  
›
(*<*)
end
(*>*)