Theory MultiSequents

(* Author : Peter Chapman *)
(* License: LGPL *)
(*<*)
section "Multisuccedent Sequents"

theory MultiSequents
imports "HOL-Library.Multiset"
begin
(*>*)

text‹
\section{Introduction}
In this paper, we give an overview of some results about invertibility in sequent calculi.  The framework is outlined in \S\ref{isadefs}.  The results are mainly concerned with multisuccedent calculi that have a single principal formula.  We will use, as our running example throughout, the calculus \textbf{G3cp}.  In \S\ref{isasingle}, we look at the formalisation of single-succedent calculi; in \S\ref{isafirstorder}, the formalisation in \textit{Nominal Isabelle} for first-order calculi is shown; in \S\ref{isamodal} the results for modal logic are examined.  We return to multisuccedent calculi in \S\ref{isaSRC} to look at manipulating rule sets.


\section{Formalising the Framework \label{isadefs}}

\subsection{Formulae and Sequents \label{isaformulae}}
A \textit{formula} is either a propositional variable, the constant $\bot$, or a connective applied to a list of formulae.  We thus have a type variable indexing formulae, where the type variable will be a set of connectives.  In the usual way, we index propositional variables by use of natural numbers.  So, formulae are given by the datatype:
›

datatype 'a form = At "nat"
                        | Compound "'a" "'a form list"
                        | ff

text‹
\noindent For \textbf{G3cp}, we define the datatype $Gp$, and give the following abbreviations:
›


(* --------------------------------------------
   --------------------------------------------
               G3cp EXAMPLE
   --------------------------------------------
   -------------------------------------------- *)
(* Try a small example with conjunction and disjunction *)
datatype Gp = con | dis | imp
type_synonym Gp_form = "Gp form"

abbreviation con_form (infixl ‹∧*› 80) where
   "p ∧* q ≡ Compound con [p,q]"

abbreviation dis_form (infixl ‹∨*› 80) where
   "p ∨* q ≡ Compound dis [p,q]"

abbreviation imp_form (infixl ‹⊃› 80) where
   "p ⊃ q  ≡ Compound imp [p,q]"
(* --------------------------------------------
   --------------------------------------------
               G3cp EXAMPLE ENDS
   --------------------------------------------
   -------------------------------------------- *)
(*<*)
abbreviation multiset_abbrev (‹\<LM> _  \<RM>› [75]75) where
   "\<LM> A \<RM> ≡ {# A #}"

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

datatype 'a sequent = Sequent "('a form) multiset" "('a 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 'a rule = "'a sequent list * 'a sequent"

type_synonym 'a deriv = "'a sequent * nat"

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

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

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

  (* Invertible definitions *)
  invertible :: "'a rule ⇒ 'a rule set ⇒ bool"
  invertible_set :: "'a rule set ⇒ bool"

  (* functions to get at components of sequents *)
primrec antec :: "'a sequent ⇒ 'a form multiset" where "antec (Sequent ant suc) = ant"
primrec succ :: "'a sequent ⇒ 'a form multiset" where "succ (Sequent ant suc) = suc"
primrec mset :: "'a sequent ⇒ 'a form multiset" where "mset (Sequent ant suc) = ant + suc"
primrec seq_size :: "'a sequent ⇒ nat" where "seq_size (Sequent ant suc) = size ant + size suc"

primrec max_list :: "nat list ⇒ nat" where
  "max_list [] = 0"
| "max_list (n # ns) = max n (max_list ns)"

(* The depth of a formula.  Will be useful in later files. *)
fun depth :: "'a form ⇒ nat"
where
   "depth (At i) = 0"
|  "depth (Compound f fs) = (max_list (map depth fs)) + 1"
|  "depth (ff) = 0"

(* The formulation of various rule sets *)
(*>*)

text‹
\noindent A \textit{sequent} is a pair of multisets of formulae.  Sequents are indexed by the connectives used to index the formulae.  To add a single formula to a multiset of formulae, we use the symbol $\oplus$, whereas to join two multisets, we use the symbol $+$.

\subsection{Rules and Rule Sets \label{isarules}}
A \textit{rule} is a list of sequents (called the premisses) paired with a sequent (called the conclusion).  The two \textit{rule sets} used for multisuccedent calculi are the axioms, and the \SC rules (i.e. rules having one principal formula).  Both are defined as inductive sets.  There are two clauses for axioms, corresponding to $L\bot$ and normal axioms:

›
inductive_set "Ax" where
   id(*<*)[intro](*>*): "([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>) ∈ Ax"
|  Lbot(*<*)[intro](*>*): "([], \<LM> ff \<RM> ⇒* \<Empt>) ∈ Ax"

text‹
\noindent The set of \SC rules, on the other hand, must not have empty premisses, and must have a single, compound formula in its conclusion.  The function \texttt{mset} takes a sequent, and returns the multiset obtained by adding the antecedent and the succedent together:
›

(* 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> Compound R Fs \<RM> ; ps ≠ [] ⟧ ⟹ (ps,c) ∈ upRules"

text‹
\noindent For \textbf{G3cp}, we have the following six rules, which we then show are a subset of the set of \SC rules:
›

(* --------------------------------------------
   --------------------------------------------
               G3cp EXAMPLE
   --------------------------------------------
   -------------------------------------------- *)

inductive_set "g3cp"
where
    conL(*<*)[intro](*>*): "([\<LM> A \<RM> + \<LM> B \<RM> ⇒* \<Empt>], \<LM> A ∧* B \<RM> ⇒* \<Empt>) ∈ g3cp"
|   conR(*<*)[intro](*>*): "([\<Empt> ⇒* \<LM> A \<RM>, \<Empt> ⇒* \<LM> B \<RM>], \<Empt> ⇒* \<LM> A ∧* B \<RM>) ∈ g3cp"
|   disL(*<*)[intro](*>*): "([\<LM> A \<RM> ⇒* \<Empt>, \<LM> B \<RM> ⇒* \<Empt>], \<LM> A ∨* B\<RM> ⇒* \<Empt>) ∈ g3cp"
|   disR(*<*)[intro](*>*): "([\<Empt> ⇒* \<LM> A \<RM> + \<LM> B \<RM>], \<Empt> ⇒* \<LM> A ∨* B \<RM>) ∈ g3cp"
|   impL(*<*)[intro](*>*): "([\<Empt> ⇒* \<LM> A \<RM>, \<LM> B \<RM> ⇒* \<Empt>], \<LM> A ⊃ B \<RM> ⇒* \<Empt>) ∈ g3cp"
|   impR(*<*)[intro](*>*): "([\<LM> A \<RM> ⇒* \<LM> B \<RM>], \<Empt> ⇒* \<LM> A ⊃ B \<RM>) ∈ g3cp"

lemma g3cp_upRules:
shows "g3cp ⊆ upRules"
proof-
 {
  fix ps c
  assume "(ps,c) ∈ g3cp"
  then have "(ps,c) ∈ upRules" by (induct) auto
 }
thus "g3cp ⊆ upRules" by auto
qed


(* --------------------------------------------
   --------------------------------------------
               G3cp EXAMPLE ENDS
   --------------------------------------------
   -------------------------------------------- *)

text‹
\noindent We have thus given the \textit{active} parts of the \textbf{G3cp} calculus.  We now need to extend these active parts with \textit{passive} parts.

Given a sequent $C$, we extend it with another sequent $S$ by adding the two antecedents and the two succedents.  To extend an active part $(Ps,C)$ with a sequent $S$, we extend every $P \in Ps$ and $C$ with $S$:
›

(* Extend a sequent, and then a rule by adding seq to all premisses and the conclusion *)
overloading
  extend ≡ extend
  extendRule ≡ extendRule
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))"

end

text‹
\noindent Given a rule set $\mathcal{R}$, the \textit{extension} of $\mathcal{R}$, called $\mathcal{R}^{\star}$, is then defined as another inductive set:
›

inductive_set extRules :: "'a rule set ⇒ 'a rule set"  (‹_*›)
  for R :: "'a rule set" 
  where I(*<*)[intro](*>*): "r ∈ R ⟹ extendRule seq r ∈ R*"

text‹
\noindent The rules of \textbf{G3cp} all have unique conclusions.  This is easily formalised:
›


(* 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*)
overloading uniqueConclusion ≡ uniqueConclusion
begin

definition uniqueConclusion :: "'a rule set ⇒ bool"
  where "uniqueConclusion R ≡ ∀ r1 ∈ R. ∀ r2 ∈ R. (snd r1 = snd r2) ⟶ (r1 = r2)"

end

(* --------------------------------------------
   --------------------------------------------
               G3cp EXAMPLE
   --------------------------------------------
   -------------------------------------------- *)
lemma g3cp_uc:
shows "uniqueConclusion g3cp"
apply (auto simp add:uniqueConclusion_def Ball_def)
apply (rule g3cp.cases) apply auto by (rotate_tac 1,rule g3cp.cases,auto)+
(* --------------------------------------------
   --------------------------------------------
               G3cp EXAMPLE ENDS
   --------------------------------------------
   -------------------------------------------- *)
(*<*)
(* 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 :: "'a rule ⇒ 'a form ⇒ bool"
  where
  up[intro]: "C = (\<LM>Compound F Fs\<RM> ⇒* \<Empt>)  ⟹ 
                   leftPrincipal (Ps,C) (Compound F Fs)"

(*>*)

text‹
\subsection{Principal Rules and Derivations \label{isaderv}}
A formula $A$ is \textit{left principal} for an active part $R$ iff the conclusion of $R$ is of the form $A \Rightarrow \emptyset$.  The definition of \textit{right principal} is then obvious.  We have an inductive predicate to check these things:
›

inductive rightPrincipal :: "'a rule ⇒ 'a form ⇒ bool"
  where
  up(*<*)[intro](*>*): "C = (\<Empt> ⇒* \<LM>Compound F Fs\<RM>) ⟹ 
                        rightPrincipal (Ps,C) (Compound F Fs)"

text‹
\noindent As an example, we show that if $A\wedge B$ is principal for an active part in \textbf{G3cp}, then $\emptyset \Rightarrow A$ is a premiss of that active part:
›

(* --------------------------------------------
   --------------------------------------------
               G3cp EXAMPLE
   --------------------------------------------
   -------------------------------------------- *)

lemma principal_means_premiss:
assumes a: "rightPrincipal r (A ∧* B)"
and     b: "r ∈ g3cp"
shows      "(\<Empt> ⇒* \<LM> A \<RM>) ∈ set (fst r)"
proof-
    from a and b obtain Ps where req: "r = (Ps, \<Empt> ⇒* \<LM> A∧*B \<RM>)" 
         by (cases r) auto
    with b have "Ps = [\<Empt> ⇒* \<LM> A \<RM>, \<Empt> ⇒* \<LM> B \<RM>]"
         apply (cases r) by (rule g3cp.cases) auto
    with req show "(\<Empt> ⇒* \<LM> A \<RM>) ∈ set (fst r)" by auto
qed



(* --------------------------------------------
   --------------------------------------------
               G3cp EXAMPLE ENDS
   --------------------------------------------
   -------------------------------------------- *)



(* 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.  *)

text‹
\noindent A sequent is \textit{derivable} at height $0$ if it is the conclusion of a rule with no premisses.  If a rule has $m$ premisses, and the maximum height of the derivation of any of the premisses is $n$, then the conclusion will be derivable at height $n+1$.  We encode this as pairs of sequents and natural numbers.  A sequent $S$ is derivable at a height $n$ in a rule system $\mathcal{R}$ iff $(S,n)$ belongs to the inductive set \texttt{derivable} $\mathcal{R}$:
›

inductive_set derivable :: "'a rule set ⇒ 'a deriv set"
  for R :: "'a 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"

text‹
\noindent In some instances, we do not care about the height of a derivation, rather that the root is derivable.  For this, we have the additional definition of \texttt{derivable'}, which is a set of sequents:
›

(* When we don't care about height! *)
inductive_set derivable' :: "'a rule set ⇒ 'a sequent set"
   for R :: "'a rule set"
   where
    base(*<*)[intro](*>*): "⟦ ([],C) ∈ R ⟧ ⟹ C ∈ derivable' R"
|   step(*<*)[intro](*>*):  "⟦ r ∈ R ; (fst r) ≠ [] ; ∀ p ∈ set (fst r). p ∈ derivable' R ⟧
                       ⟹ (snd r) ∈ derivable' R"

text‹
\noindent It is desirable to switch between the two notions.  Shifting from derivable at a height to derivable is simple: we delete the information about height.  The converse is more complicated and involves an induction on the length of the premiss list:
›

lemma deriv_to_deriv(*<*)[simp](*>*):
assumes "(C,n) ∈ derivable R"
shows "C ∈ derivable' R"
using assms by (induct) auto

lemma deriv_to_deriv2:
assumes "C ∈ derivable' R"
shows "∃ n. (C,n) ∈ derivable R"
using assms
  proof (induct)
  case (base C)
  then have "(C,0) ∈ derivable R" by auto
  then show ?case by blast
next
  case (step r)
  then obtain ps c where "r = (ps,c)" and "ps ≠ []" by (cases r) auto
  with step(3) have aa: "∀ p ∈ set ps. ∃ n. (p,n) ∈ derivable R" by auto
  then have "∃ m. ∀ p ∈ set ps. ∃ n≤m. (p,n) ∈ derivable R"
  proof (induct ps) ― ‹induction on the list›
    case Nil
    then show ?case by auto
  next
    case (Cons a as)
    then have "∃ m. ∀ p ∈ set as. ∃ n≤m. (p,n) ∈ derivable R" by auto
    then obtain m where "∀ p ∈ set as. ∃ n≤m. (p,n) ∈ derivable R" by auto
    moreover from ‹∀ p ∈ set (a # as). ∃ n. (p,n) ∈ derivable R› have
      "∃ n. (a,n) ∈ derivable R" by auto
    then obtain m' where "(a,m') ∈ derivable R" by blast
    ultimately have "∀ p ∈ set (a # as). ∃ n≤(max m m'). (p,n) ∈ derivable R" 

(*<*)
      apply (auto simp add:Ball_def)
      apply (rule_tac x=m' in exI) apply simp
      apply (drule_tac x=x in spec) apply auto(*>*) by (*<*)(rule_tac x=n in exI)(*>*) auto ― ‹max returns the maximum of two integers›
    then show ?case by blast
  qed
  then obtain m where "∀ p ∈ set ps. ∃ n≤m. (p,n) ∈ derivable R" by blast
  with ‹r = (ps,c)› and ‹r ∈ R› have "(c,m+1) ∈ derivable R" using ‹ps ≠ []› and
    derivable.step[where r="(ps,c)" and R=R and m=m] by auto
  then show ?case using ‹r = (ps,c)› by auto
qed
(*<*)
(* definition of invertible rule and invertible set of rules.  It's a bit nasty, but all it really says is
   If a rule is in the given set, and if any extension of that rule is derivable at n, then the
   premisses of the extended rule are derivable at height at most n.  *)





(* Characterisation of a sequent *)
lemma characteriseSeq:
shows "∃ A B. (C :: 'a 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 comes in helpful ALL THE TIME *)
lemma midMultiset:
  assumes "Γ ⊕ A = Γ' ⊕ B" and "A ≠ B"
  shows "∃ Γ''. Γ = Γ'' ⊕ B ∧ Γ' = Γ'' ⊕ A"
proof-
  from assms have "A ∈# Γ'"
      proof-
      from assms have "set_mset (Γ ⊕ A) = set_mset (Γ' ⊕ B)" by auto
      then have "set_mset Γ ∪ {A} = set_mset Γ' ∪ {B}" by auto
      then have "set_mset Γ ∪ {A} ⊆ set_mset Γ' ∪ {B}" by simp
      then have "A ∈ set_mset Γ'" using assms by auto
      thus "A ∈# Γ'" by simp
      qed
  then have "Γ' ⊖ A ⊕ A = Γ'" by (auto simp add:multiset_eq_iff)
  then have "∃ Γ''. Γ' = Γ'' ⊕ A" apply (rule_tac x="Γ' ⊖ A" in exI) by auto
  then obtain Γ'' where eq1:"Γ' = Γ'' ⊕ A" by blast
  from ‹Γ ⊕ A = Γ' ⊕ B› eq1 have "Γ ⊕ A = Γ'' ⊕ A ⊕ B" by auto
  then have "Γ = Γ'' ⊕ B" by auto
  thus ?thesis using eq1 by blast
qed

(* 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 \<RM> ⇒* \<LM> At i \<RM>) = (Γ ⇒* Δ)"
shows "At i ∈# Γ ∧ At i ∈# Δ"
using assms
proof-
  from assms have "∃ Γ' Δ'. Γ = Γ' ⊕ At i ∧ Δ = Δ' ⊕ At i" 
     using extend_def[where forms=S and seq="\<LM> At i \<RM> ⇒* \<LM> At i \<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 idupRules *)
lemma containID:
assumes a:"At i ∈# Γ ∧ At i ∈# Δ"
    and b:"Ax ⊆ R"
shows "(Γ ⇒* Δ,0) ∈ derivable R*"
proof-
from a have "Γ = Γ ⊖ At i ⊕ At i ∧ Δ = Δ ⊖ At i ⊕ At i" by auto
then have "extend ((Γ ⊖ At i) ⇒* (Δ ⊖ At i)) (\<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = (Γ ⇒* Δ)" 
     using extend_def[where forms="Γ ⊖ At i ⇒* Δ ⊖ At i" and seq="\<LM>At i\<RM> ⇒* \<LM>At i\<RM>"] by auto
moreover
have "([],\<LM> At i \<RM> ⇒* \<LM> At i \<RM>) ∈ R" using b by auto
ultimately
have "([],Γ ⇒* Δ) ∈ R*" 
     using extRules.I[where R=R and r="([],  \<LM>At i\<RM> ⇒* \<LM>At i\<RM>)" and seq="Γ ⊖ At i ⇒* Δ ⊖ At i"] 
       and extendRule_def[where forms="Γ ⊖ At i ⇒* Δ ⊖ At i" and R="([],  \<LM>At i\<RM> ⇒* \<LM>At i\<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.I[where R=R and r="([],  \<LM>ff\<RM> ⇒* \<Empt>)" and seq="Γ ⊖ 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. r = ([], \<LM> At i \<RM> ⇒* \<LM> At i \<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
by (cases) auto


(* Lemma which says that if rule is an upRule, then the succedent is either empty, or a single formula *)
lemma succ_upRule:
assumes "(Ps,Φ ⇒* Ψ) ∈ upRules"
shows "Ψ = \<Empt> ∨ (∃ A. Ψ = \<LM>A\<RM>)"
using assms 
proof (cases)
    case (I R Rs)
    then show "Ψ = \<Empt> ∨ (∃ A. Ψ = \<LM>A\<RM>)" using mset.simps[where ant=Φ and suc=Ψ] 
         and union_is_single[where M=Φ and N=Ψ and a="Compound R Rs"] by (simp,elim disjE) (auto)
qed

(* Equivalent, but the antecedent *)
lemma antec_upRule:
assumes "(Ps,Φ ⇒* Ψ) ∈ upRules"
shows "Φ = \<Empt> ∨ (∃ A. Φ = \<LM>A\<RM>)"
using assms 
proof (cases)
    case (I R Rs)
    then show "Φ = \<Empt> ∨ (∃ A. Φ = \<LM>A\<RM>)" using mset.simps[where ant=Φ and suc=Ψ] 
         and union_is_single[where M=Φ and N=Ψ and a="Compound R Rs"] by (simp,elim disjE) (auto)
qed

lemma upRule_Size:
assumes "r ∈ upRules"
shows "seq_size (snd r) = 1"
using assms
proof-
    obtain Ps C where "r = (Ps,C)" by (cases r)
    then have "(Ps,C) ∈ upRules" using assms by simp
    then show ?thesis
       proof (cases)
          case (I R Rs)
          obtain G H where "C = (G ⇒* H)" by (cases C) (auto)
          then have "G + H = \<LM>Compound R Rs\<RM>" using mset.simps and ‹mset C ≡ \<LM>Compound R Rs\<RM>› by auto
          then have "size (G+H) = 1" by auto 
          then have "size G + size H = 1" by auto
          then have "seq_size C = 1" using seq_size.simps[where ant=G and suc=H] and ‹C = (G ⇒* H)› by auto
          moreover have "snd r = C" using ‹r = (Ps,C)› by simp
          ultimately show "seq_size (snd r) = 1" by simp
       qed
qed

lemma upRuleCharacterise:
assumes "(Ps,C) ∈ upRules"
shows "∃ F Fs. C = (\<Empt> ⇒* \<LM>Compound F Fs\<RM>) ∨ C = (\<LM>Compound 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>Compound F Fs\<RM>) ∨ C = (\<LM>Compound F Fs\<RM> ⇒* \<Empt>)" 
    using ‹mset C ≡ \<LM>Compound F Fs\<RM>› and ‹C = (Γ ⇒* Δ)›
      and mset.simps[where ant=Γ and suc=Δ] and union_is_single[where M=Γ and N=Δ and a="Compound F Fs"]
    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 nonPrincipalID:
fixes A :: "'a form"
assumes "r ∈ Ax"
shows "¬ rightPrincipal r A ∧ ¬ leftPrincipal r A"
proof-
from assms obtain i where r1:"r = ([], \<LM> ff \<RM> ⇒* \<Empt>) ∨ r = ([], \<LM> At i \<RM> ⇒* \<LM> At i\<RM>)" 
     using characteriseAx[where r=r] by auto
{ assume "rightPrincipal r A" then obtain Ps where r2:"r = (Ps, \<Empt> ⇒* \<LM> A \<RM>)" by (cases r) auto
  with r1 have "False" by simp
}
then have "¬ rightPrincipal r A" by auto
moreover
{ assume "leftPrincipal r A" then obtain Ps' F Fs where r3:"r = (Ps', \<LM>Compound F Fs\<RM> ⇒* \<Empt>)" by (cases r) auto
  with r1 have "False" by auto
}
then have "¬ leftPrincipal r A" by auto
ultimately show ?thesis by simp
qed

lemma extendCommute:
shows "(extend S) (extend R c) = (extend R) (extend S c)"
by (auto simp add:extend_def union_ac)

lemma mapCommute:
shows "map (extend S) (map (extend R) c) = map (extend R) (map (extend S) c)"
by (induct_tac c) (auto simp add:extendCommute)

lemma extendAssoc:
shows "(extend S) (extend R c) = extend (extend S R) c" 
by (auto simp add:extend_def union_ac)

lemma mapAssoc:
shows "map (extend S) (map (extend R) c) = map (extend (extend S R)) c"
by (induct_tac c) (auto simp add:extendAssoc)

lemma extended_Ax_prems_empty:
assumes "r ∈ Ax"
shows "fst (extendRule S r) = []"
using assms apply (cases r) by (rule Ax.cases) (auto simp add:extendRule_def)

inductive lastRule :: "'a deriv ⇒ 'a rule ⇒ 'a rule set ⇒ bool"
  where
  base[intro]: "⟦ r ∈ Ax; Ax ⊆ R ; snd (extendRule S r) = (Γ ⇒* Δ)⟧
                 ⟹ lastRule (Γ ⇒* Δ,0) r R"
|    I[intro]:  "⟦ r∈R ; r ∉ Ax ; snd (extendRule S r) = (Γ ⇒* Δ) ; 
                ∀ p ∈ set (fst (extendRule S r)). ∃ m≤n. (p,m) ∈ derivable R* ⟧ 
                 ⟹ lastRule (Γ ⇒* Δ,n+1) r R" 

lemma obv:
fixes a :: "('a * 'b)"
shows "a = (fst a, snd a)" by auto

lemma getLast:
assumes "lastRule (Γ ⇒* Δ,n+1) r R"
shows "∃ S Ps. extendRule S r = (Ps, Γ ⇒* Δ) ∧ (∀ p ∈ set Ps. ∃ m≤n. (p,m) ∈ derivable R*) ∧ r ∈ R ∧ r ∉ Ax"
proof-
  from assms show ?thesis apply (rule lastRule.cases) apply simp apply simp
  apply (rule_tac x=S in exI) apply (rule_tac x="fst (extendRule S r)" in exI) apply simp
  apply auto
  apply (subgoal_tac "extendRule S (a,b) = (fst (extendRule S (a,b)),snd (extendRule S (a,b)))")
  apply simp by (rule obv)
qed

lemma getAx:
assumes "lastRule (Γ ⇒* Δ,0) r R"
shows "r ∈ Ax ∧ (∃ S. extendRule S r = ([],Γ ⇒* Δ))"
proof-
  from assms have "r ∈ Ax ∧ (∃ S. snd (extendRule S r) = (Γ ⇒* Δ))"
       by (rule lastRule.cases) auto
  then obtain S where "r ∈ Ax" and "snd (extendRule S r) = (Γ ⇒* Δ)" by auto
  from ‹r ∈ Ax› have "fst r = []" apply (cases r) by (rule Ax.cases) auto
  then have "fst (extendRule S r) = []" by (auto simp add:extendRule_def)
  with ‹snd (extendRule S r) = (Γ ⇒* Δ)› and ‹r ∈ Ax› show ?thesis apply auto
       apply (rule_tac x=S in exI) 
       apply (subgoal_tac "extendRule S r = (fst (extendRule S r),snd (extendRule S r))") apply simp
       by (rule obv)
qed


(* -------------------------------------------
   -------------------------------------------
       THIS IS NOW INVERTIBLERULESPOLY.THY
   -------------------------------------------
   ------------------------------------------- *)

(* Constructing the rule set we will use.  It contains all axioms, but only a subset
   of the possible logical rules. *)
lemma ruleSet:
assumes "R' ⊆ upRules"
    and "R = Ax ∪ R'"
    and "(Ps,C) ∈ R*"
shows "∃ S r. extendRule S r = (Ps,C) ∧ (r ∈ R' ∨ 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 ∪ R'› have "r ∈ Ax ∨ r ∈ R'" by blast
ultimately show ?thesis by (rule_tac x=S in exI,rule_tac x=r in exI) (auto)
qed
(*>*)

text‹
\section{Formalising the Results \label{isaproofs}}
A variety of ``helper'' lemmata are used in the proofs, but they are not shown.  The proof tactics themselves are hidden in the following proof, except where they are interesting.  Indeed, only the interesting parts of the proof are shown at all.  The main result of this section is that a rule is invertible if the premisses appear as premisses of \textit{every} rule with the same principal formula.  The proof is interspersed with comments.
›

lemma rightInvertible:
fixes Γ Δ :: "'a form multiset"
assumes rules: "R' ⊆ upRules ∧ R = Ax ∪ R'"
  and   a: "(Γ ⇒* Δ ⊕ Compound F Fs,n) ∈ derivable R*"
  and   b: "∀ r' ∈ R. rightPrincipal r' (Compound F Fs) ⟶ 
            (Γ' ⇒* Δ') ∈ set (fst r')"
shows "∃ m≤n. (Γ +Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
using assms
txt‹
\noindent The height of derivations is decided by the length of the longest branch.  Thus, we need to use
strong induction: i.e. $\forall m\leq n.\ \textrm{If } P(m) \textrm{ then } P(n+1)$.
›
proof (induct n arbitrary:Γ Δ rule:nat_less_induct)
 case (1 n Γ Δ)
 then have IH:"∀m<n. ∀Γ Δ. ( Γ ⇒* Δ ⊕ Compound F Fs, m) ∈ derivable R* ⟶
                   (∀r' ∈ R. rightPrincipal r' (Compound F Fs) ⟶ 
                   ( Γ' ⇒* Δ') ∈ set (fst r')) ⟶
                   (∃m'≤m. ( Γ + Γ' ⇒* Δ + Δ', m') ∈ derivable R*)" 
     and a': "(Γ ⇒* Δ ⊕ Compound F Fs,n) ∈ derivable R*" 
     and b': "∀ r' ∈ R. rightPrincipal r' (Compound F Fs) ⟶ 
                        (Γ' ⇒* Δ') ∈ set (fst r')"
       by auto
 show ?case
 proof (cases n)   ― ‹Case analysis on $n$›
     case 0
 (*<*)    then have "(Γ ⇒* Δ ⊕ Compound F Fs,0) ∈ derivable R*" using a' by simp
     then have "([],Γ ⇒* Δ ⊕ Compound F Fs) ∈ R*" by (cases) (auto)
     then have "∃ r S. extendRule S r = ([],Γ ⇒* Δ ⊕ Compound F Fs) ∧ (r ∈ Ax ∨ r ∈ R')"
          using rules and ruleSet[where R'=R' and R=R and Ps="[]" and C="Γ ⇒* Δ ⊕ Compound F Fs"] by auto(*>*)
     then obtain r S where "extendRule S r = ([],Γ ⇒* Δ ⊕ Compound F Fs)" 
                   and "r ∈ Ax ∨ r ∈ R'" by auto  ― ‹At height 0, the premisses are empty›
      moreover
      {assume "r ∈ Ax"
       then obtain i where "([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = r ∨ 
                             r = ([], \<LM> ff \<RM> ⇒* \<Empt>)" 
            using characteriseAx[where r=r] by auto
          moreover ― ‹Case split on the kind of axiom used›
          {assume "r = ([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>)"
 (*<*)         with ‹extendRule S r = ([],Γ ⇒* Δ ⊕ Compound F Fs)›
                have "extend S (\<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = (Γ ⇒* Δ ⊕ Compound F Fs)"
                using extendRule_def[where R="([],\<LM>At i\<RM>⇒*\<LM>At i\<RM>)" and forms=S] by auto (*>*)
          then have "At i ∈# Γ ∧ At i ∈# Δ" (*<*)using extendID[where S=S and i=i and Γ=Γ and Δ="Δ ⊕ Compound F Fs"](*>*) by auto
           then have "At i ∈# Γ + Γ' ∧ At i ∈# Δ + Δ'" 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 = ([],Γ ⇒* Δ ⊕ Compound F Fs)›
                have "extend S (\<LM> ff \<RM> ⇒* \<Empt>) = (Γ ⇒* Δ ⊕ Compound F Fs)"
                using extendRule_def[where R="([],\<LM>ff\<RM>⇒*\<Empt>)" and forms=S] by auto (*>*)
          then have "ff ∈# Γ" (*<*)using extendFalsum[where S=S and Γ=Γ and Δ="Δ ⊕ Compound F Fs"](*>*)  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 ∈ R'" ― ‹This leads to a contradiction›
 (*<*)      then have "r ∈ upRules" using rules by auto
       then have "∃ Ps C. Ps ≠ [] ∧ r = (Ps,C)"
            proof-
            obtain x y where "r = (x,y)" by (cases r)
            with ‹r ∈ upRules› have "(x,y) ∈ upRules" by simp
            then obtain Ps where "(Ps :: 'a sequent list) ≠ []" and "x=Ps" by (cases) (auto)
            with ‹r = (x,y)› have "r = (Ps, y)" by simp
            then show "∃ Ps C. Ps ≠ [] ∧ r = (Ps,C)" using ‹Ps ≠ []› by blast
            qed (*>*)
      then obtain Ps C where "Ps ≠ []" and "r = (Ps,C)" by auto
       moreover (*<*) from ‹extendRule S r = ([], Γ ⇒* Δ ⊕ Compound F Fs)› 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   ― ‹Contradiction›
       ultimately have "(Γ + Γ' ⇒* Δ + Δ',0) ∈ derivable R*" using rules by simp
       }
       ultimately show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" (*<*)using ‹n=0› (*>*) by blast
(*<*)next (*>*)
txt‹\noindent In the case where $n = n' + 1$ for some $n'$, we know the premisses are empty,
and every premiss is derivable at a height lower than $n'$:›
  case (Suc n')
  then have "(Γ ⇒* Δ ⊕ Compound F Fs,n'+1) ∈ derivable R*" using a' by simp
  then obtain Ps where "(Ps, Γ ⇒* Δ ⊕ Compound F Fs) ∈ R*" and 
                       "Ps ≠ []" and 
                       "∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*" (*<*)
       using characteriseLast[where C="Γ ⇒* Δ ⊕ Compound F Fs" and m=n' and R="R*"](*>*) by auto
 (*<*)    then have "∃ r S. (r ∈ Ax ∨ r ∈ R') ∧ extendRule S r = (Ps, Γ ⇒* Δ ⊕ Compound F Fs)"
          using rules and ruleSet[where R'=R' and R=R and Ps=Ps and C="Γ ⇒* Δ ⊕ Compound F Fs"] by auto (*>*)
  then obtain r S where "r ∈ Ax ∨ r ∈ R'"  
                  and "extendRule S r = (Ps, Γ ⇒* Δ ⊕ Compound F Fs)" by auto
  moreover
     {assume "r ∈ Ax"   ― ‹Gives a contradiction›
      then have "fst r = []" apply (cases r) by (rule Ax.cases) auto
      moreover obtain x y where "r = (x,y)" by (cases r)
      then have "x ≠ []" using ‹Ps ≠ []›
                    and ‹extendRule S r = (Ps, Γ ⇒* Δ ⊕ Compound F Fs)› (*<*)
                          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*" (*<*)
              using ‹r=(x,y)›(*>*)  by auto
     }
  moreover
     {assume "r ∈ R'"
      obtain ps c where "r = (ps,c)" by (cases r) auto
  (*<*)       then have "r ∈ upRules" using rules and ‹r ∈ R'› by auto (*>*)
      have "(rightPrincipal r (Compound F Fs)) ∨ 
                ¬(rightPrincipal r (Compound F Fs))" 
      by blast  ― ‹The formula is principal, or not›
    (*<*)  moreover (*>*)
txt‹\noindent If the formula is principal, then $\Gamma' \Rightarrow \Delta'$ is amongst the premisses of $r$:›
  {assume "rightPrincipal r (Compound F Fs)"
   then have "(Γ' ⇒* Δ') ∈ set ps" using b' (*<*)and ‹r = (ps,c)› and ‹r ∈ R'› and rules(*>*)
        by auto
   then have "extend S (Γ' ⇒* Δ') ∈ set Ps" 
        using ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ Compound F Fs)›
      (*<*)  and ‹r = (ps,c)›(*>*) by (simp(*<*) add:extendContain(*>*))
   moreover (*<*)from ‹rightPrincipal r (Compound F Fs)› have "c = (\<Empt> ⇒* \<LM>Compound F Fs\<RM>)" 
        using ‹r = (ps,c)› by (cases) auto
   with ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ Compound F Fs)›(*>*) 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 (*>*)
txt‹\noindent If the formula is not principal, then it must appear in the premisses.  The first two lines give a characterisation of the extension and conclusion, respectively.  Then, we apply the induction hypothesis
at the lower height of the premisses:›
  {assume "¬ rightPrincipal r (Compound F Fs)"
   obtain Φ Ψ where "S = (Φ ⇒* Ψ)" by (cases S) (auto)   
   then obtain G H where "c = (G ⇒* H)" by (cases c) (auto)  
   then have "\<LM> Compound F Fs \<RM> ≠ H"   ― ‹Proof omitted›
 (*<*)                 proof-
                  from ‹r = (ps,c)› and ‹r ∈ upRules›
                     obtain T Ts where  "c = (\<Empt> ⇒* \<LM>Compound T Ts\<RM>) ∨ c = (\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
                     using upRuleCharacterise[where Ps=ps and C=c] by auto
                  moreover
                     {assume "c = (\<Empt> ⇒* \<LM>Compound T Ts\<RM>)"
                      then have "rightPrincipal r (Compound T Ts)" using ‹r = (ps,c)› by auto
                      with ‹¬ rightPrincipal r (Compound F Fs)› have "Compound T Ts ≠ Compound F Fs" by auto
                      then have "\<LM>Compound F Fs\<RM> ≠ H" using ‹c = (G ⇒* H)› and ‹c = (\<Empt> ⇒* \<LM>Compound T Ts\<RM>)› by auto
                     }
                  moreover
                     {assume "c = (\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
                      then have "\<LM>Compound F Fs\<RM> ≠ H" using ‹c = (G ⇒* H)› by auto
                     }
                  ultimately show "\<LM>Compound F Fs\<RM> ≠ H" by blast
                  qed 
             moreover have "succ S + succ (snd r) = (Δ ⊕ Compound F Fs)" 
                         using ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ Compound F Fs)›
                         and extendRule_def[where forms=S and R=r]
                         and extend_def[where forms=S and seq="snd r"] by auto
   then (*>*) have "Ψ + H = Δ ⊕ Compound F Fs" 
        using ‹S = (Φ ⇒* Ψ)› and ‹r = (ps,c)› and ‹c = (G ⇒* H)› by auto
   moreover from ‹r = (ps,c)› and ‹c = (G ⇒* H)› (*<*)and ‹r ∈ upRules› (*>*)
   
   have "H = \<Empt> ∨ (∃ A. H = \<LM>A\<RM>)"(*<*)
            using succ_upRule[where Ps=ps and Φ=G and Ψ=H](*>*) by auto
   ultimately have "Compound F Fs ∈# Ψ"   ― ‹Proof omitted›
 (*<*)                proof-
                 have "H = \<Empt> ∨ (∃ A. H = \<LM>A\<RM>)" by fact
                 moreover
                    {assume "H = \<Empt>"
                     then have "Ψ = Δ ⊕ Compound F Fs" using ‹Ψ + H = Δ ⊕ Compound F Fs› by auto
                     then have "Compound F Fs ∈# Ψ" by auto
                    }
                 moreover
                    {assume "∃ A. H = \<LM>A\<RM>"
                     then obtain A where "H = \<LM>A\<RM>" by auto
                     then have "Ψ ⊕ A = Δ ⊕ Compound F Fs" using ‹Ψ + H = Δ ⊕ Compound F Fs› by auto
                     then have "set_mset (Ψ ⊕ A) = set_mset (Δ ⊕ Compound F Fs)" by auto
                     then have "set_mset Ψ ∪ {A} = set_mset Δ ∪ {Compound F Fs}" by auto
                     moreover from ‹H = \<LM>A\<RM>› and ‹\<LM>Compound F Fs\<RM> ≠ H› have "Compound F Fs ≠ A" by auto
                     ultimately have "Compound F Fs ∈ set_mset Ψ" by auto
                     then have "Compound F Fs ∈# Ψ" by auto
                    }
                 ultimately show "Compound F Fs ∈# Ψ" by blast
                 qed (*>*)
  then have "∃ Ψ1. Ψ = Ψ1 ⊕ Compound F Fs" by (*<*)(rule_tac x="Ψ ⊖ Compound F Fs" in exI)(*>*) (auto(*<*) simp add:multiset_eq_iff(*>*))
  then obtain Ψ1 where "S = (Φ ⇒* Ψ1 ⊕ Compound F Fs)"(*<*) using ‹S = (Φ ⇒* Ψ)›(*>*) by auto
 (*<*)           have "Ps = map (extend S) ps" 
                 using ‹extendRule S r = (Ps,Γ ⇒* Δ ⊕ Compound F Fs)› 
                 and extendRule_def[where forms=S and R=r] 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. (Compound F Fs ∈# succ p)"  ― ‹Appears in every premiss›
                 (*<*)     using ‹Compound F Fs ∈# Ψ› and ‹S = (Φ ⇒* Ψ)› apply (auto simp add:Ball_def) (*>*)
         by (*<*)(drule_tac x=x in spec)(*>*) (auto(*<*) simp add:extend_def(*>*))
  (*<*)          then have a1:"∀ p ∈ set Ps. ∃ Φ' Ψ'. p = (Φ' ⇒* Ψ' ⊕ Compound F Fs)" using characteriseSeq
                      apply (auto simp add:Ball_def) apply (drule_tac x=x in spec,simp) 
                      apply (rule_tac x="antec x" in exI,rule_tac x="succ x ⊖ Compound F Fs" in exI) 
                      by (drule_tac x=x in meta_spec) (auto simp add:multiset_eq_iff)
            moreover have "∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*" by fact
            ultimately have "∀ p ∈ set Ps. ∃ Φ' Ψ' n. n≤n' ∧ (Φ' ⇒* Ψ' ⊕ Compound F Fs,n) ∈ derivable R*
                                                     ∧ p = (Φ' ⇒* Ψ' ⊕ Compound F Fs)"
                 by (auto simp add:Ball_def) (*>*)
 then have (*<*)a2:(*>*) "∀ p ∈ set Ps. ∃ Φ' Ψ' m. m≤n' ∧ 
                                   (Φ' + Γ' ⇒* Ψ' + Δ',m) ∈ derivable R* ∧
                                   p = (Φ' ⇒* Ψ' ⊕ Compound F Fs)" using (*<*)‹n = Suc n'› and b' and (*>*)IH(*<*)
                 apply (auto simp add:Ball_def) apply (drule_tac x=x in spec) apply simp
                 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)(*>*) by(*<*) (rule_tac x=m' in exI)(*>*) (arith) 
txt‹\noindent  To this set of new premisses, we apply a new instance of $r$, with a different extension:›           
  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 ‹Ps ≠ []› by auto
            from ‹r ∈ R'› have "extendRule (Φ + Γ' ⇒* Ψ1 + Δ') r ∈ R*" using rules by auto
            moreover have "extendRule (Φ + Γ' ⇒* Ψ1 + Δ') r = (Ps',Γ + Γ' ⇒* Δ + Δ')"
                 using ‹S = (Φ ⇒* Ψ1 ⊕ Compound F Fs)› and ‹extendRule S r = (Ps, Γ ⇒* Δ ⊕ Compound F Fs)› 
                 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: 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 "∀ Φ' Ψ'. (Φ' ⇒* Ψ' ⊕ Compound F Fs) ∈ set Ps ⟶ 
                            (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'"
               proof-
                 {fix Φ' Ψ'
                 assume "(Φ' ⇒* Ψ' ⊕ Compound F Fs) ∈ set Ps"  
                 then have "∃ p ∈ set ps. extend (Φ ⇒* Ψ1 ⊕ Compound F Fs) p = (Φ' ⇒* Ψ' ⊕ Compound F Fs)"
                      using ‹Ps = map (extend S) ps› and ‹S = (Φ ⇒* Ψ1 ⊕ Compound F Fs)› and a1 and d1
                           apply (simp only:Ball_def Bex_def) apply (drule_tac x=" Φ' ⇒* Ψ' ⊕ Compound F Fs" in spec)
                           by (drule_tac x="Φ' ⇒* Ψ' ⊕ Compound F Fs" in spec) (auto)
                 then obtain p where t:"p ∈ set ps ∧ (Φ' ⇒* Ψ' ⊕ Compound F Fs) = extend (Φ ⇒* Ψ1 ⊕ Compound F Fs) p"
                      apply auto by (drule_tac x=p in meta_spec) (simp)
                 then obtain A B where "p = (A ⇒* B)" by (cases p) 
                 then have "(A ⇒* B) ∈ set ps ∧ (Φ' ⇒* Ψ' ⊕ Compound F Fs) = extend (Φ ⇒* Ψ1 ⊕ Compound F Fs) (A ⇒* B)"
                      using t by auto
                 then have ant: "Φ' = Φ + A" and suc: "Ψ' ⊕ Compound F Fs = Ψ1 ⊕ Compound F Fs + B" 
                      using extend_def[where forms="Φ ⇒* Ψ1 ⊕ Compound F Fs" and seq="A ⇒* B"] by auto
                 from ant have "Φ' + Γ' = (Φ + Γ') + A" 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 + Δ') (A ⇒* B)" 
                      using extend_def[where forms="Φ + Γ' ⇒* Ψ1 + Δ'" and seq="A ⇒* B"] by auto
                 moreover have "extend (Φ + Γ' ⇒* Ψ1 + Δ') (A ⇒* B) ∈ set Ps'" using ‹p = (A ⇒* B)› and t and c2 by auto
                 ultimately have "(Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'" by simp
                 }
                 thus ?thesis by blast
               qed
            moreover
            have "∀ Φ' Ψ'. (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps' ⟶ (Φ' ⇒* Ψ' ⊕ Compound F Fs) ∈ 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 A B where "p = (A ⇒* B)" by (cases p) 
                 then have "(A ⇒* B) ∈ set ps ∧ (Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ + Γ' ⇒* Ψ1 + Δ') (A ⇒* B)"
                      using t by auto
                 then have ant: "Φ' + Γ' = Φ + Γ' + A" and suc: "Ψ' + Δ' = Ψ1 + Δ' + B" 
                      using extend_def[where forms="Φ + Γ' ⇒* Ψ1 + Δ'" and seq="A ⇒* B"] by auto
                 from ant have "Φ' + Γ' = (Φ + A) + Γ'" by (auto simp add:union_ac)
                 then have "Φ' = Φ + A" by simp
                 moreover
                 from suc have "Ψ' + Δ' = (Ψ1 + B) + Δ'" by (auto simp add:union_ac)
                 then have "Ψ' = Ψ1 + B" by simp
                 then have "Ψ' ⊕ Compound F Fs = (Ψ1 ⊕ Compound F Fs) + B" by (auto simp add:union_ac)
                 ultimately have "(Φ' ⇒* Ψ' ⊕ Compound F Fs) = extend (Φ ⇒* Ψ1 ⊕ Compound F Fs) (A ⇒* B)" 
                      using extend_def[where forms="Φ ⇒* Ψ1 ⊕ Compound F Fs" and seq="A⇒*B"] by auto
                 moreover have "extend (Φ  ⇒* Ψ1 ⊕ Compound F Fs) (A ⇒* B) ∈ set Ps" using ‹p = (A ⇒* B)› and t and c1
                      and ‹S = (Φ ⇒* Ψ1 ⊕ Compound F Fs)› by auto
                 ultimately have "(Φ' ⇒* Ψ' ⊕ Compound F Fs) ∈ set Ps" by simp
                 }
                 thus ?thesis by blast
               qed
            ultimately
            have "∀ Φ' Ψ'. ((Φ' ⇒* Ψ' ⊕ Compound F Fs) ∈ 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=x in spec) apply simp
                 apply (elim exE) apply (drule_tac x=Φ' in spec,drule_tac x=Ψ' in spec)  
                 by (drule_tac x="Φ' ⇒* Ψ' ⊕ Compound F Fs" in spec) (simp) (*>*)
  then have "∀ p ∈ set Ps'. ∃ n≤n'. (p,n) ∈ derivable R*" by auto
  then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" 
    using (*<*)‹n = Suc n'› and ‹Ps' ≠ []›
    and(*>*) ‹(Ps',Γ + Γ' ⇒* Δ + Δ') ∈ R*› (*<*)
       and derivable.step[where r="(Ps',Γ + Γ' ⇒* Δ + Δ')" and R="R*"](*>*)
 by (auto(*<*) simp add:Ball_def Bex_def(*>*))
  (*<*)          }
         ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by blast         
        }(*>*)
 txt‹\noindent All of the cases are now complete.›
 ultimately show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by blast
 (*<*)  qed (*>*)
qed
(* --------------------------------------------
   --------------------------------------------
               G3cp EXAMPLE
   --------------------------------------------
   -------------------------------------------- *)
text‹
As an example, we show the left premiss of $R\wedge$ in \textbf{G3cp} is derivable at a height not greater than that of the conclusion.  The two results used in the proof (\texttt{principal-means-premiss} and \texttt{rightInvertible}) are those we have previously shown:
›

lemma conRInvert:
assumes "(Γ ⇒* Δ ⊕ (A ∧* B),n) ∈ derivable (g3cp ∪ Ax)*"
shows "∃ m≤n. (Γ ⇒* Δ ⊕ A,m) ∈ derivable (g3cp ∪ Ax)*"
proof-
have "∀ r ∈ g3cp. rightPrincipal r (A ∧* B) ⟶ (\<Empt> ⇒* \<LM> A \<RM>) ∈ set (fst r)"
     using principal_means_premiss by auto
with assms show ?thesis using rightInvertible(*<*)[where R'="g3cp" and Γ'="\<Empt>" and Δ'="\<LM> A \<RM>" 
                           and R="g3cp ∪ Ax"](*>*) by (auto(*<*) simp add:Un_commute Ball_def nonPrincipalID g3cp_upRules(*>*))
qed
(* --------------------------------------------
   --------------------------------------------
             G3cp EXAMPLE ENDS
   --------------------------------------------
   -------------------------------------------- *)

text‹
\noindent  We can obviously show the equivalent proof for left rules, too:
›

lemma leftInvertible:
fixes Γ Δ :: "'a form multiset"
assumes rules: "R' ⊆ upRules ∧ R = Ax ∪ R'"
  and   a: "(Γ ⊕ Compound F Fs ⇒* Δ,n) ∈ derivable R*"
  and   b: "∀ r' ∈ R. leftPrincipal r' (Compound F Fs) ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
shows "∃ m≤n. (Γ +Γ' ⇒* Δ + Δ',m) ∈ derivable R*"
(*<*)
using assms
proof (induct n arbitrary:Γ Δ rule:nat_less_induct)
 case (1 n Γ Δ)
 then have IH:"∀m<n. ∀Γ Δ. ( Γ ⊕ Compound F Fs ⇒* Δ, m) ∈ derivable R* ⟶
              (∀r' ∈ R. leftPrincipal r' (Compound F Fs) ⟶ ( Γ' ⇒* Δ') ∈ set (fst r')) ⟶
              (∃m'≤m. ( Γ + Γ' ⇒* Δ + Δ', m') ∈ derivable R*)" 
     and a': "(Γ ⊕ Compound F Fs ⇒* Δ,n) ∈ derivable R*" 
     and b': "∀ r' ∈ R. leftPrincipal r' (Compound F Fs) ⟶ (Γ' ⇒* Δ') ∈ set (fst r')"
       by auto
 show ?case
 proof (cases n)
     case 0
     then have "(Γ ⊕ Compound F Fs ⇒* Δ,0) ∈ derivable R*" using a' by simp
     then have "([],Γ ⊕ Compound F Fs ⇒* Δ) ∈ R*" by (cases) (auto)
     then have "∃ r S. extendRule S r = ([],Γ ⊕ Compound F Fs ⇒* Δ) ∧ (r ∈ Ax ∨ r ∈ R')"
          using rules and ruleSet[where Ps="[]" and C="Γ ⊕ Compound F Fs ⇒* Δ" and R'=R' and R=R] by (auto)
     then obtain r S where "extendRule S r = ([],Γ ⊕ Compound F Fs ⇒* Δ)" and "r ∈ Ax ∨ r ∈ R'" by auto
      moreover
      {assume "r ∈ Ax"
       then obtain i where "([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = r ∨ r = ([],\<LM>ff\<RM> ⇒* \<Empt>)" 
            using characteriseAx[where r=r] by auto
          moreover
          {assume "r = ([], \<LM> At i \<RM> ⇒* \<LM> At i \<RM>)"
           with ‹extendRule S r = ([],Γ ⊕ Compound F Fs ⇒* Δ)›
                have "extend S (\<LM> At i \<RM> ⇒* \<LM> At i \<RM>) = (Γ ⊕ Compound F Fs ⇒* Δ)"
                using extendRule_def[where R="([],\<LM>At i\<RM>⇒*\<LM>At i\<RM>)" and forms=S] by auto
           then have "At i ∈# Γ ∧ At i ∈# Δ" using extendID[where S=S and i=i and Γ="Γ ⊕ Compound F Fs" and Δ=Δ] by auto
           then have "At i ∈# Γ + Γ' ∧ At i ∈# Δ + Δ'" 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 = ([],Γ ⊕ Compound F Fs ⇒* Δ)›
                have "extend S (\<LM> ff \<RM> ⇒* \<Empt>) = (Γ ⊕ Compound F Fs ⇒* Δ)"
                using extendRule_def[where R="([],\<LM>ff\<RM>⇒*\<Empt>)" and forms=S] by auto
           then have "ff ∈# Γ" using extendFalsum[where S=S and Γ="Γ⊕Compound F Fs" 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 ∈ R'"
       then have "r ∈ upRules" using rules by auto
       then have "∃ Ps C. Ps ≠ [] ∧ r = (Ps,C)"
            proof-
            obtain x y where "r = (x,y)" by (cases r)
            with ‹r ∈ upRules› have "(x,y) ∈ upRules" by simp
            then obtain Ps where "(Ps :: 'a sequent list) ≠ []" and "x=Ps" by (cases) (auto)
            with ‹r = (x,y)› have "r = (Ps, y)" by simp
            then show "∃ Ps C. Ps ≠ [] ∧ r = (Ps,C)" using ‹Ps ≠ []› by blast
            qed
       then obtain Ps C where "Ps ≠ []" and "r = (Ps,C)" by auto
       moreover from ‹extendRule S r = ([], Γ ⊕ Compound F Fs ⇒* Δ)› 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*" by simp
       }
       ultimately show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" using ‹n=0› by blast
 next
     case (Suc n')
     then have "(Γ ⊕ Compound F Fs ⇒* Δ,n'+1) ∈ derivable R*" using a' by simp
     then obtain Ps where "(Ps, Γ ⊕ Compound F Fs ⇒* Δ) ∈ R*" and 
                          "Ps ≠ []" and 
                          "∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*"
          using characteriseLast[where C="Γ ⊕ Compound F Fs ⇒* Δ" and m=n' and R="R*"] by auto
     then have "∃ r S. (r ∈ Ax ∨ r ∈ R') ∧ extendRule S r = (Ps, Γ ⊕ Compound F Fs ⇒* Δ)"
          using rules ruleSet[where R'=R' and R=R and Ps=Ps and C="Γ⊕ Compound F Fs ⇒* Δ"] by auto
     then obtain r S where "r ∈ Ax ∨ r ∈ R'" and "extendRule S r = (Ps, Γ ⊕ Compound F Fs ⇒* Δ)" by auto
     moreover
        {assume "r ∈ Ax"
         then have "fst r = []" apply (cases r) by (rule Ax.cases) auto
         moreover obtain x y where "r = (x,y)" by (cases r)
         then have "x ≠ []" using ‹Ps ≠ []› and ‹extendRule S r = (Ps, Γ ⊕ Compound F Fs ⇒* Δ)›
                            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*"
              using ‹r=(x,y)› by auto
        }
     moreover
        {assume "r ∈ R'"
         obtain ps c where "r = (ps,c)" by (cases r) auto
         then have "r ∈ upRules" using rules and ‹r ∈ R'› by auto
         have "(leftPrincipal r (Compound F Fs)) ∨ ¬(leftPrincipal r (Compound F Fs))" by blast
         moreover
            {assume "leftPrincipal r (Compound F Fs)"
             then have "(Γ' ⇒* Δ') ∈ set ps" using b' and ‹r = (ps,c)› and ‹r ∈ R'› and rules
                  by auto
             then have "extend S (Γ' ⇒* Δ') ∈ set Ps" using ‹extendRule S r = (Ps,Γ ⊕ Compound F Fs ⇒* Δ)›
                  and ‹r = (ps,c)› by (simp add:extendContain)
             moreover from ‹leftPrincipal r (Compound F Fs)› have "c = (\<LM>Compound F Fs\<RM> ⇒* \<Empt>)"
                  using  ‹r = (ps,c)› by (cases) auto
             with ‹extendRule S r = (Ps,Γ ⊕ Compound F Fs ⇒* Δ)› 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 (Compound F Fs)"
             obtain Φ Ψ where "S = (Φ ⇒* Ψ)" by (cases S) (auto)
             then obtain G H where "c = (G ⇒* H)" by (cases c) (auto)
             then have "\<LM> Compound F Fs \<RM> ≠ G" 
                  proof-
                  from ‹r = (ps,c)› and ‹r ∈ upRules›
                     obtain T Ts where  "c = (\<Empt> ⇒* \<LM>Compound T Ts\<RM>) ∨ c = (\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
                     using upRuleCharacterise[where Ps=ps and C=c] by auto
                  moreover
                     {assume "c = (\<Empt> ⇒* \<LM>Compound T Ts\<RM>)"
                      then have "\<LM>Compound F Fs\<RM> ≠ G" using ‹c = (G ⇒* H)› by auto   
                     }
                  moreover
                     {assume "c = (\<LM>Compound T Ts\<RM> ⇒* \<Empt>)"
                      then have "leftPrincipal r (Compound T Ts)" using ‹r = (ps,c)› by auto
                      with ‹¬ leftPrincipal r (Compound F Fs)› have "Compound T Ts ≠ Compound F Fs" by auto
                      then have "\<LM>Compound F Fs\<RM> ≠ G" using ‹c = (G ⇒* H)› and ‹c = (\<LM>Compound T Ts\<RM> ⇒* \<Empt>)› by auto
                     }
                  ultimately show "\<LM>Compound F Fs\<RM> ≠ G" by blast
                  qed
             moreover have "antec S + antec (snd r) = (Γ ⊕ Compound F Fs)" 
                         using ‹extendRule S r = (Ps,Γ ⊕ Compound F Fs ⇒* Δ)›
                         and extendRule_def[where forms=S and R=r]
                         and extend_def[where forms=S and seq="snd r"] by auto
             then have "Φ + G = Γ ⊕ Compound F Fs" using ‹S = (Φ ⇒* Ψ)› and ‹r = (ps,c)› and ‹c = (G ⇒* H)› by auto
             moreover from ‹r = (ps,c)› and ‹c = (G⇒* H)› and ‹r ∈ upRules› have "G = \<Empt> ∨ (∃ A. G = \<LM>A\<RM>)"
                      using antec_upRule[where Ps=ps and Φ=G and Ψ=H] by auto
             ultimately have "Compound F Fs ∈# Φ"
                 proof-
                 have "G = \<Empt> ∨ (∃ A. G = \<LM>A\<RM>)" by fact
                 moreover
                    {assume "G = \<Empt>"
                     then have "Φ = Γ ⊕ Compound F Fs" using ‹Φ + G = Γ ⊕ Compound F Fs› by auto
                     then have "Compound F Fs ∈# Φ" by auto
                    }
                 moreover
                    {assume "∃ A. G = \<LM>A\<RM>"
                     then obtain A where "G = \<LM>A\<RM>" by auto
                     then have "Φ ⊕ A = Γ ⊕ Compound F Fs" using ‹Φ + G = Γ ⊕ Compound F Fs› by auto
                     then have "set_mset (Φ ⊕ A) = set_mset (Γ ⊕ Compound F Fs)" by auto
                     then have "set_mset Φ ∪ {A} = set_mset Γ ∪ {Compound F Fs}" by auto
                     moreover from ‹G = \<LM>A\<RM>› and ‹\<LM>Compound F Fs\<RM> ≠ G› have "Compound F Fs ≠ A" by auto
                     ultimately have "Compound F Fs ∈ set_mset Φ" by auto
                     then have "Compound F Fs ∈# Φ" by auto
                    }
                 ultimately show "Compound F Fs ∈# Φ" by blast
                 qed
            then have "∃ Φ1. Φ = Φ1 ⊕ Compound F Fs" 
                 by (rule_tac x="Φ ⊖ Compound F Fs" in exI) (auto simp add:multiset_eq_iff)
            then obtain Φ1 where "S = (Φ1 ⊕ Compound F Fs ⇒* Ψ)" using ‹S = (Φ ⇒* Ψ)› by auto
            have "Ps = map (extend S) ps" 
                 using ‹extendRule S r = (Ps,Γ ⊕ Compound F Fs ⇒* Δ)› 
                 and extendRule_def[where forms=S and R=r] 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. (Compound F Fs ∈# antec p)" 
                      using ‹Compound F Fs ∈# Φ› and ‹S = (Φ ⇒* Ψ)› apply (auto simp add:Ball_def) 
                      by (drule_tac x=x in spec) (auto simp add:extend_def)
            then have a1:"∀ p ∈ set Ps. ∃ Φ' Ψ'. p = (Φ' ⊕ Compound F Fs ⇒* Ψ')" using characteriseSeq
                      apply (auto simp add:Ball_def) apply (drule_tac x=x in spec,simp) 
                      apply (rule_tac x="antec x ⊖ Compound F Fs" in exI,rule_tac x="succ x" in exI) 
                      by (drule_tac x=x in meta_spec) (auto simp add:multiset_eq_iff)
            moreover have "∀ p ∈ set Ps. ∃ n≤n'. (p,n) ∈ derivable R*" by fact
            ultimately have "∀ p ∈ set Ps. ∃ Φ' Ψ' n. n≤n' ∧ (Φ' ⊕ Compound F Fs ⇒* Ψ',n) ∈ derivable R*
                                                     ∧ p = (Φ' ⊕ Compound F Fs ⇒* Ψ')"
                 by (auto simp add:Ball_def)
            then have a2: "∀ p ∈ set Ps. ∃ Φ' Ψ' m. m≤n' ∧ (Φ' + Γ' ⇒* Ψ' + Δ',m) ∈ derivable R*
                                                   ∧ p = (Φ' ⊕ Compound F Fs ⇒* Ψ')"
                 using ‹n = Suc n'› and b' and IH
                 apply (auto simp add:Ball_def) apply (drule_tac x=x in spec) apply simp
                 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) 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 ‹Ps ≠ []› by auto
            from ‹r ∈ R'› have "extendRule (Φ1 + Γ' ⇒* Ψ + Δ') r ∈ R*" using rules by auto
            moreover have "extendRule (Φ1 + Γ' ⇒* Ψ + Δ') r = (Ps',Γ + Γ' ⇒* Δ + Δ')"
                 using ‹S = (Φ1 ⊕ Compound F Fs ⇒* Ψ)› and ‹extendRule S r = (Ps, Γ ⊕ Compound F Fs ⇒* Δ)› 
                 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: 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 "∀ Φ' Ψ'. (Φ' ⊕ Compound F Fs ⇒* Ψ') ∈ set Ps ⟶ (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'"
               proof-
                 {fix Φ' Ψ'
                 assume "(Φ' ⊕ Compound F Fs ⇒* Ψ') ∈ set Ps"  
                 then have "∃ p ∈ set ps. extend (Φ1 ⊕ Compound F Fs ⇒* Ψ) p = (Φ' ⊕ Compound F Fs ⇒* Ψ')"
                      using ‹Ps = map (extend S) ps› and ‹S = (Φ1 ⊕ Compound F Fs ⇒* Ψ)› and a1 and d1
                           apply (simp only:Ball_def Bex_def) apply (drule_tac x="Φ' ⊕ Compound F Fs ⇒* Ψ'" in spec)
                           by (drule_tac x="Φ' ⊕ Compound F Fs ⇒* Ψ'" in spec) (auto)
                 then obtain p where t:"p ∈ set ps ∧ (Φ' ⊕ Compound F Fs ⇒* Ψ') = extend (Φ1 ⊕ Compound F Fs ⇒* Ψ) p"
                      apply auto by (drule_tac x=p in meta_spec) (simp)
                 then obtain A B where "p = (A ⇒* B)" by (cases p) 
                 then have "(A ⇒* B) ∈ set ps ∧ (Φ' ⊕ Compound F Fs ⇒* Ψ') = extend (Φ1 ⊕ Compound F Fs ⇒* Ψ) (A ⇒* B)"
                      using t by auto
                 then have ant: "Φ' ⊕ Compound F Fs = Φ1 ⊕ Compound F Fs + A" and suc: "Ψ' = Ψ + B"
                      using extend_def[where forms="Φ1 ⊕ Compound F Fs ⇒* Ψ" and seq="A⇒*B"] by auto
                 from ant have "Φ' = Φ1 + A" by auto
                 then have "Φ' + Γ' = (Φ1 + Γ') + A" by (auto simp add:union_ac)
                 moreover
                 from suc have "Ψ' + Δ' = (Ψ + Δ') + B" by (auto simp add:union_ac)
                 ultimately have "(Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ1 + Γ' ⇒* Ψ + Δ') (A ⇒* B)" 
                      using extend_def[where forms="Φ1 + Γ' ⇒* Ψ + Δ'" and seq="A ⇒* B"] by auto
                 moreover have "extend (Φ1 + Γ' ⇒* Ψ + Δ') (A ⇒* B) ∈ set Ps'" using ‹p = (A ⇒* B)› and t and c2 by auto
                 ultimately have "(Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps'" by simp
                 }
                 thus ?thesis by blast
               qed
            moreover
            have "∀ Φ' Ψ'. (Φ' + Γ' ⇒* Ψ' + Δ') ∈ set Ps' ⟶ (Φ' ⊕ Compound F Fs ⇒* Ψ') ∈ 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 A B where "p = (A ⇒* B)" by (cases p) 
                 then have "(A ⇒* B) ∈ set ps ∧ (Φ' + Γ' ⇒* Ψ' + Δ') = extend (Φ1 + Γ' ⇒* Ψ + Δ') (A ⇒* B)"
                      using t by auto
                 then have ant: "Φ' + Γ' = Φ1 + Γ' + A" and suc: "Ψ' + Δ' = Ψ + Δ' + B" 
                      using extend_def[where forms="Φ1 + Γ' ⇒* Ψ + Δ'" and seq="A ⇒* B"] by auto
                 from ant have "Φ' + Γ' = (Φ1 + A) + Γ'" by (auto simp add:union_ac)
                 then have "Φ' = Φ1 + A" by simp
                 then have "Φ' ⊕ Compound F Fs = (Φ1 ⊕ Compound F Fs) + A" by (auto simp add:union_ac)
                 moreover
                 from suc have "Ψ' + Δ' = (Ψ + B) + Δ'" by (auto simp add:union_ac)
                 then have "Ψ' = Ψ + B" by simp
                 ultimately have "(Φ' ⊕ Compound F Fs ⇒* Ψ') = extend (Φ1 ⊕ Compound F Fs ⇒* Ψ) (A ⇒* B)" 
                      using extend_def[where forms="Φ1 ⊕ Compound F Fs ⇒* Ψ" and seq="A⇒*B"] by auto
                 moreover have "extend (Φ1 ⊕ Compound F Fs ⇒* Ψ) (A ⇒* B) ∈ set Ps" using ‹p = (A ⇒* B)› and t and c1
                      and ‹S = (Φ1 ⊕ Compound F Fs ⇒* Ψ)› by auto
                 ultimately have "(Φ' ⊕ Compound F Fs ⇒* Ψ') ∈ set Ps" by simp
                 }
                 thus ?thesis by blast
               qed
            ultimately
            have "∀ Φ' Ψ'. ((Φ' ⊕ Compound F Fs ⇒* Ψ') ∈ 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=x in spec) apply simp
                 apply (elim exE) apply (drule_tac x=Φ' in spec,drule_tac x=Ψ' in spec)  
                 by (drule_tac x="Φ' ⊕ Compound F Fs ⇒* Ψ'" in spec) (simp)
            then have all:"∀ p ∈ set Ps'. ∃ n≤n'. (p,n) ∈ derivable R*" by auto
            then have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" using ‹n = Suc n'›
                 and ‹(Ps',Γ + Γ' ⇒* Δ + Δ') ∈ R*› and ‹Ps' ≠ []›
                 and derivable.step[where r="(Ps',Γ + Γ' ⇒* Δ + Δ')" and R="R*"]
                 by (auto simp add:Ball_def Bex_def)
            }
         ultimately have "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by blast         
        }
      ultimately show "∃ m≤n. (Γ + Γ' ⇒* Δ + Δ',m) ∈ derivable R*" by blast
  qed
qed



lemma invertibleRule:
assumes rules: "R' ⊆ upRules ∧ R = Ax ∪ R'"
   and UC:     "uniqueConclusion R'"
   and IN:     "(Ps,C) ∈ R*"
   and der:    "(C,n) ∈ derivable R*"
shows "∀ p ∈ set Ps. ∃ m≤n. (p,m) ∈ derivable R*"
proof-
  from IN have "∃ r' S. (r' ∈ Ax ∨ r' ∈  R') ∧ (Ps,C) = extendRule S r'" 
    using rules and ruleSet[where R'=R' and R=R and Ps=Ps and C=C]
    apply (auto) apply (rule_tac x=a in exI,rule_tac x=b in exI) apply simp apply (rule_tac x=S in exI) apply (simp)
    apply (rule_tac x=a in exI,rule_tac x=b in exI) apply simp by (rule_tac x=S in exI) simp
  then obtain r' S where "r' ∈ Ax ∨ r' ∈ R'" and "(Ps,C) = extendRule S r'" by blast
  then obtain Γ Δ where gam1:"S = (Γ ⇒* Δ)" by (cases S) auto
  have "r' ∈ Ax ∨ r' ∈ R'" by fact
  moreover
  {assume "r' ∈ Ax"
    then have "Ps = []" using characteriseAx[where r=r'] and ‹(Ps,C) = extendRule S r'› 
      and extendRule_def[where forms=S and R=r'] by auto
    then have "∀ p ∈ set Ps. ∃ m≤n. (p,m) ∈ derivable R*" by (auto simp add:Ball_def)
  }
  moreover
  {assume "r' ∈ R'"
    {fix P
      assume "P ∈ set Ps"
      from ‹r' ∈ R'› have "r' ∈ upRules" using rules by auto
      then obtain ps c where "r' = (ps,c)" by (cases r') (auto)
      then have "∃ p ∈ set ps. P = extend S p" using ‹P ∈ set Ps› and ‹(Ps,C) = extendRule S r'›
        by (auto simp add:extendRule_def extend_def)
      then obtain p where "p ∈ set ps" and "P = extend S p" by auto
      then obtain Γ' Δ' where "p = (Γ' ⇒* Δ')" using characteriseSeq[where C=p] by auto
      then have P: "P = (Γ + Γ' ⇒* Δ + Δ')" using gam1 and ‹P = extend S p› by (auto simp add:extend_def)    
      then have "(Γ' ⇒* Δ') ∈ set (fst r')" using ‹p ∈ set ps› and ‹r' = (ps,c)› and ‹p = (Γ' ⇒* Δ')› by auto
      from ‹r'=(ps,c)› have "∃ F Fs. c = (\<Empt> ⇒* \<LM>Compound F Fs\<RM>) ∨ c = (\<LM>Compound F Fs\<RM> ⇒* \<Empt>)" 
        using ‹r' ∈ upRules› and upRuleCharacterise[where Ps=ps and C=c] by auto
      then obtain F Fs where "c = (\<Empt> ⇒* \<LM>Compound F Fs\<RM>) ∨ c = (\<LM>Compound F Fs\<RM> ⇒* \<Empt>)" by auto
      moreover
      {assume "c = (\<Empt> ⇒* \<LM> Compound F Fs \<RM>)"          
        with ‹c= (\<Empt> ⇒* \<LM>Compound F Fs\<RM>)› and ‹(Ps,C) = extendRule S r'› and ‹r' = (ps,c)› and gam1
        have gam2:"C = (Γ ⇒* Δ ⊕ Compound F Fs)"
          using extendRule_def[where forms=S and R=r'] and extend_def[where forms=S and seq=c]
          by simp
        with ‹c = (\<Empt> ⇒* \<LM>Compound F Fs\<RM>)› have "rightPrincipal r' (Compound F Fs)"  
          using ‹r' = (ps,c)› by auto
        then have a1:"∀ r ∈ R'. rightPrincipal r (Compound F Fs) ⟶ r = r'" using ‹uniqueConclusion R'›
        proof-
          {fix r
            assume "r ∈ R'" then have "r ∈ upRules" using ‹R' ⊆ upRules ∧ R = Ax ∪ R'› by auto
            assume "rightPrincipal r (Compound F Fs)"
            obtain ps' c' where "r = (ps',c')" by (cases r) auto
            with ‹rightPrincipal r (Compound F Fs)› have "c' = (\<Empt> ⇒* \<LM>Compound F Fs\<RM>)"
              by (cases) auto
            then have "c' = c" using ‹c = (\<Empt> ⇒* \<LM>Compound F Fs\<RM>)› by simp
            then have "r = r'" using ‹uniqueConclusion R'› and ‹r ∈ R'› and ‹r' ∈ R'›
              and ‹r'=(ps,c)› and ‹r = (ps',c')›
              by (simp add:uniqueConclusion_def Ball_def)
          }
          thus ?thesis by (auto simp add:Ball_def)
        qed
        with ‹p ∈ set ps› and ‹r' = (ps,c)› and ‹(Γ' ⇒* Δ') ∈ set (fst r')›
        have b1:"∀ r ∈ R'. rightPrincipal r (Compound F Fs) ⟶ (Γ' ⇒* Δ') ∈ set (fst r)" by blast
        have "∀ r ∈ R. rightPrincipal r (Compound F Fs) ⟶ (Γ' ⇒* Δ') ∈ set (fst r)"
        proof-               
          {fix t
            assume "t ∈ R" and "rightPrincipal t (Compound F Fs)"
            then obtain pss d where "t = (pss,d)" by (cases t) auto
            with ‹rightPrincipal t (Compound F Fs)› have rP:"d = (\<Empt> ⇒* \<LM>Compound F Fs\<RM>)" by (cases) auto
            from ‹t ∈ R› have split:"t ∈ Ax ∨ t ∈ R'" using rules by auto
            moreover
            {assume "t ∈ Ax"
              then obtain i where "d = (\<LM>At i\<RM> ⇒* \<LM>At i\<RM>) ∨ d = (\<LM>ff\<RM> ⇒* \<Empt>)" 
                using characteriseAx[where r=t] and ‹t = (pss,d)› by auto
              then have "(Γ' ⇒* Δ') ∈ set (fst t)" using rP by auto
            }
            moreover
            {assume "t ∈ R'"
              with ‹rightPrincipal t (Compound F Fs)› have "(Γ' ⇒* Δ') ∈ set (fst t)" using b1 and ‹t ∈ R'› by auto
            }
            ultimately have "(Γ' ⇒* Δ') ∈ set (fst t)" by blast
          }
          then show ?thesis by auto
        qed
        then have "∃ m≤n. (P,m) ∈ derivable R*" using rules and gam1 and gam2 and P
          and rightInvertible[where R'=R' and R=R and F=F and Fs=Fs and n=n and Γ=Γ and Γ'=Γ' and Δ=Δ and Δ'=Δ']
          and IN and der by auto 
      }
      moreover
      {assume "c = (\<LM>Compound F Fs\<RM> ⇒* \<Empt>)"          
        with ‹c= (\<LM>Compound F Fs\<RM> ⇒* \<Empt>)› and ‹(Ps,C) = extendRule S r'› and ‹r' = (ps,c)› and gam1
        have gam3:"C = (Γ ⊕ Compound F Fs ⇒* Δ)"
          using extendRule_def[where forms=S and R=r'] and extend_def[where forms=S and seq=c]
          by simp
        with ‹c = (\<LM>Compound F Fs\<RM> ⇒* \<Empt>)› have "leftPrincipal r' (Compound F Fs)" 
          using ‹r' = (ps,c)› and ‹r' ∈ R'› by auto
        then have a1:"∀ r ∈ R'. leftPrincipal r (Compound F Fs) ⟶ r = r'" using ‹uniqueConclusion R'›
        proof-
          {fix r
            assume "r ∈ R'" then have "r ∈ upRules" using ‹R' ⊆ upRules ∧ R = Ax ∪ R'› by auto
            assume "leftPrincipal r (Compound F Fs)"
            obtain ps' c' where "r = (ps',c')" by (cases r) auto
            with ‹leftPrincipal r (Compound F Fs)› have "c' = (\<LM>Compound F Fs\<RM> ⇒* \<Empt>)" by (cases) auto
            then have "c' = c" using ‹c = (\<LM>Compound F Fs\<RM> ⇒* \<Empt>)› by simp
            then have "r = r'" using ‹uniqueConclusion R'› and ‹r ∈ R'› and ‹r' ∈ R'›
              and ‹r'=(ps,c)› and ‹r = (ps',c')›
              by (simp add:uniqueConclusion_def Ball_def)
          }
          thus ?thesis by (auto simp add:Ball_def)
        qed
        with ‹p ∈ set ps› and ‹r' = (ps,c)› and ‹(Γ' ⇒* Δ') ∈ set (fst r')›
        have b1:"∀ r ∈ R'. leftPrincipal r (Compound F Fs) ⟶ (Γ' ⇒* Δ') ∈ set (fst r)" by blast
        have "∀ r ∈ R. leftPrincipal r (Compound F Fs) ⟶ (Γ' ⇒* Δ') ∈ set (fst r)"
        proof-               
          {fix t
            assume "t ∈ R" and "leftPrincipal t (Compound F Fs)"
            then obtain pss d where "t = (pss,d)" by (cases t) auto
            with ‹leftPrincipal t (Compound F Fs)› have rP:"antec d = \<LM>Compound F Fs\<RM>" by (cases) auto
            from ‹t ∈ R› have split:"t ∈ Ax ∨ t ∈ R'" using rules by (cases) auto
            moreover
            {assume "t ∈ Ax"
              then obtain i where "d = (\<LM>At i\<RM> ⇒* \<LM>At i\<RM>) ∨ d = (\<LM>ff\<RM> ⇒* \<Empt>)" 
                using characteriseAx[where r=t] and ‹t = (pss,d)› by auto
              then have "(Γ' ⇒* Δ') ∈ set (fst t)" using rP by auto
            }
            moreover
            {assume "t ∈ R'"
              with ‹leftPrincipal t (Compound F Fs)› have "(Γ' ⇒* Δ') ∈ set (fst t)" using b1 and ‹t ∈ R'› by auto
            }
            ultimately have "(Γ' ⇒* Δ') ∈ set (fst t)" by blast
          }
          then show ?thesis by auto
        qed
        then have "∃ m≤n. (P,m) ∈ derivable R*" using rules and gam1 and gam3 and P
          and leftInvertible[where R'=R' and R=R and F=F and Fs=Fs and n=n and Γ=Γ and Γ'=Γ' and Δ=Δ and Δ'=Δ']
          and IN and der by auto
      }
      ultimately have "∃ m≤n. (P,m) ∈ derivable R*" by blast
    }
    then have "∀ p ∈ set Ps. ∃ m≤n. (p,m) ∈ derivable R*" by auto
  }
  ultimately show "∀ p ∈ set Ps. ∃ m≤n. (p,m) ∈ derivable R*" by blast
qed

(*>*)

text‹
A rule is invertible iff every premiss is derivable at a height lower than that of the conclusion.  A set of rules is invertible iff every rule is invertible.  These definitions are easily formalised:›

overloading
  invertible ≡ invertible
  invertible_set ≡ invertible_set
begin

definition invertible
  where "invertible r R ≡
       ∀ n S. (r ∈ R ∧ (snd (extendRule S r),n) ∈ derivable R*) ⟶
       (∀ p ∈ set (fst (extendRule S r)). ∃ m ≤ n. (p,m) ∈ derivable R*)"

definition invertible_set
  where "invertible_set R ≡ ∀ (ps,c) ∈ R. invertible (ps,c) R"

end

text‹
\noindent A set of multisuccedent \SC rules is invertible if each rule has a different conclusion.  \textbf{G3cp} has the unique conclusion property (as shown in \S\ref{isarules}).  Thus, \textbf{G3cp} is an invertible set of rules:
›

lemma unique_to_invertible:
assumes (*<*)a:(*>*) "R' ⊆ upRules ∧ R = Ax ∪ R'"
   and  "uniqueConclusion R'"
shows "invertible_set R"
(*<*)
using assms invertibleRule
  apply (auto simp add:invertible_set_def invertible_def)
  apply (drule_tac x=R' in meta_spec) apply (drule_tac x=R in meta_spec)
  apply (drule_tac x="fst (extendRule S (a,b))" in meta_spec)
  apply (drule_tac x="snd (extendRule S (a,b))" in meta_spec)
  apply (drule_tac x=n in meta_spec)
  apply (simp add:a extRules.intros)
  apply (drule_tac x=R' in meta_spec) apply (drule_tac x=R in meta_spec)
  apply (drule_tac x="fst (extendRule S (a,b))" in meta_spec)
  apply (drule_tac x="snd (extendRule S (a,b))" in meta_spec)
  apply (drule_tac x=n in meta_spec)
by (simp add:a extRules.intros)
(*>*)
(* --------------------------------------------
   --------------------------------------------
               G3cp EXAMPLE
   --------------------------------------------
   -------------------------------------------- *)

lemma g3cp_invertible:
shows "invertible_set (Ax ∪ g3cp)"
using g3cp_uc and g3cp_upRules
   and unique_to_invertible[where R'="g3cp" and R="Ax ∪ g3cp"] 
by auto

text‹
\subsection{Conclusions}
For \SC multisuccedent calculi, the theoretical results have been formalised.  Moreover, the running example demonstrates that it is straightforward to implement such calculi and reason about them.  Indeed, it will be this class of calculi for which we will prove more results in \S\ref{isaSRC}.
›
(*<*)
end
(*>*)