(* A Invertibility for sequents, First-Order *) 
theory InvertibleNominal
imports "SequentDepthNominal"
begin

(* Constructing the rule set we will use.  It contains all axioms, but only a subset
   of the possible logical rules. *)
lemma ruleSet:
assumes "R1 \<subseteq> propRules" and "R2 \<subseteq> nprovRules" and "R3 \<subseteq> provRules"
    and "R = idRules \<union> R1 \<union> R2 \<union> R3"
    and "(Ps,C) \<in> R*"
shows "\<exists> S r. extendRule S r = (Ps,C) \<and> (r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3 \<or> r \<in> idRules)"
proof-
from `(Ps,C) \<in> R*` have "\<exists> S r. extendRule S r = (Ps,C) \<and> r \<in> R" by (cases) auto
then obtain S r where "(Ps,C) = extendRule S r" and "r \<in> 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 \<in> R` and `R = idRules \<union> R1 \<union> R2 \<union> R3` have "r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3 \<or> r \<in> idRules" 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 \<subseteq> propRules" and "R2 \<subseteq> nprovRules" and "R3 \<subseteq> provRules"
    and "R = idRules \<union> R1 \<union> R2 \<union> R3" and "r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3" and "r = (ps,c)"
    and IH: "\<forall>m<n. \<forall>\<Gamma> \<Delta>. ( \<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A, m) \<in> derivable R* \<longrightarrow>
              (\<forall>r' \<in> R. rightPrincipal r' (F \<nabla> [x].A) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* \<Delta>') \<in> set (fst r')) \<longrightarrow>
              (\<not> multSubst \<Gamma>' \<and> \<not> multSubst \<Delta>') \<longrightarrow>
              (\<exists>m'\<le>m. ( \<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>', m') \<in> derivable R*)"
    and a': "(\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A,n) \<in> derivable R*" 
    and b': "\<forall> r' \<in> R. rightPrincipal r' (F \<nabla> [x].A) \<longrightarrow> (\<Gamma>' \<Rightarrow>* \<Delta>') \<in> set (fst r')"
    and c': "\<not> multSubst \<Gamma>' \<and> \<not> multSubst \<Delta>'"
    and np: "\<not> rightPrincipal r (F \<nabla> [x].A)"
    and ext: "extendRule S r = (Ps,\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A)"
    and num: "n = n' + 1"
    and all: "\<forall> p \<in> set Ps. \<exists> n\<le>n'. (p,n) \<in> derivable R*"
    and nonempty: "Ps \<noteq> []"
shows "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*"
proof-
from ext obtain \<Phi> \<Psi> where "S = (\<Phi> \<Rightarrow>* \<Psi>)" by (cases S) (auto)
from `r = (ps,c)` obtain G H where "c = (G \<Rightarrow>* H)" by (cases c) (auto)
then have "{# F \<nabla> [x].A  #} \<noteq> H" using `r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3`
     proof-
     {assume "r \<in> R1" then have "r \<in> propRules" using `R1 \<subseteq> propRules` by auto
      with `r = (ps,c)` obtain T Ts where "c = ({#} \<Rightarrow>* {#Cpd0 T Ts#}) \<or> c = ({#Cpd0 T Ts#} \<Rightarrow>* {#})"
            using propRuleCharacterise[where Ps=ps and C=c] by auto
      moreover
        {assume "c = ({#} \<Rightarrow>* {#Cpd0 T Ts#})"
         with `c = (G \<Rightarrow>* H)` have "{# F \<nabla> [x].A #} \<noteq> H" by auto
        }
      moreover
        {assume "c = ({#Cpd0 T Ts#} \<Rightarrow>* {#})"
         then have "{#F \<nabla> [x].A #} \<noteq> H" using `c = (G \<Rightarrow>* H)` by auto
        }
      ultimately have "{# F \<nabla> [x].A #} \<noteq> H" by blast
     }
     moreover
     {assume "r \<in> R2 \<or> r \<in> R3" 
      then have "r \<in> provRules \<or> r \<in> nprovRules" using `R2 \<subseteq> nprovRules` and `R3 \<subseteq> provRules` by auto
      with `r = (ps,c)` obtain T y B where "c = ({#} \<Rightarrow>* {# T \<nabla> [y].B #}) \<or> c = ({# T \<nabla> [y].B#} \<Rightarrow>* {#})"
            using provRuleCharacterise[where Ps=ps and C=c]
            and nprovRuleCharacterise[where Ps=ps and C=c] by auto
      moreover
        {assume "c = ({#} \<Rightarrow>* {# T \<nabla> [y].B#})"
         then have "rightPrincipal r (T \<nabla> [y].B)" using `r = (ps,c)` by auto
         with `\<not> rightPrincipal r (F \<nabla> [x].A)` have "T \<nabla> [y].B \<noteq> F \<nabla> [x].A" by auto
         with `c = (G \<Rightarrow>* H)` have "{# F \<nabla> [x].A #} \<noteq> H" using `c = ({#} \<Rightarrow>* {# T \<nabla> [y].B #})` by auto
        }
      moreover
        {assume "c = ({#T \<nabla> [y].B #} \<Rightarrow>* {#})"
         then have "{#F \<nabla> [x].A #} \<noteq> H" using `c = (G \<Rightarrow>* H)` by auto
        }
      ultimately have "{# F \<nabla> [x].A #} \<noteq> H" by blast
     }
     ultimately show ?thesis using `r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3` by blast
     qed
moreover have "succ S + succ (snd r) = (\<Delta> \<oplus> F \<nabla> [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 "\<Psi> + H = \<Delta> \<oplus> F \<nabla> [x].A" using `S = (\<Phi> \<Rightarrow>* \<Psi>)` and `r = (ps,c)` and `c = (G \<Rightarrow>* H)` by auto
moreover from `r = (ps,c)` and `r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3` and `R1 \<subseteq> propRules` and `R2 \<subseteq> nprovRules`
              and `R3 \<subseteq> provRules` have "(ps,c) \<in> propRules \<or> (ps,c) \<in> nprovRules \<or> (ps,c) \<in> provRules" by auto
then have "\<exists> A. c = ({#} \<Rightarrow>* {#A#}) \<or> c = ({#A#} \<Rightarrow>* {#})"
     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 = {#} \<or> (\<exists> A. H = {#A#})" using `c = (G \<Rightarrow>* H)` by auto
ultimately have "F \<nabla> [x].A :# \<Psi>"
    proof-
    have "H = {#} \<or> (\<exists> A. H = {#A#})" by fact
    moreover
    {assume "H = {#}"
     then have "\<Psi> = \<Delta> \<oplus> F \<nabla> [x].A" using `\<Psi> + H = \<Delta> \<oplus> F \<nabla> [x].A` by auto
     then have "F \<nabla> [x].A :# \<Psi>" by auto
    }
    moreover
    {assume "\<exists> A. H = {#A#}"
     then obtain T where "H = {#T#}" by auto
     then have "\<Psi> \<oplus> T = \<Delta> \<oplus> F \<nabla> [x].A" using `\<Psi> + H = \<Delta> \<oplus> F \<nabla> [x].A` by auto
     then have "set_of (\<Psi> \<oplus> T) = set_of (\<Delta> \<oplus> F \<nabla> [x].A)" by auto
     then have "set_of \<Psi> \<union> {T} = set_of \<Delta> \<union> {F \<nabla> [x].A}" by auto
     moreover from `H = {#T#}` and `{#F \<nabla> [x].A#} \<noteq> H` have "F \<nabla> [x].A \<noteq> T" by auto
     ultimately have "F \<nabla> [x].A \<in> set_of \<Psi>" by auto
     then have "F \<nabla> [x].A :# \<Psi>" by auto
    }
    ultimately show "F \<nabla> [x].A :# \<Psi>" by blast
    qed
then have "\<exists> \<Psi>1. \<Psi> = \<Psi>1 \<oplus> F \<nabla> [x].A" 
     by (rule_tac x="\<Psi> \<ominus> F \<nabla> [x].A" in exI) (auto simp add:multiset_eq_conv_count_eq)
then obtain \<Psi>1 where "S = (\<Phi> \<Rightarrow>* \<Psi>1 \<oplus> F \<nabla> [x].A)" using `S = (\<Phi> \<Rightarrow>* \<Psi>)` by auto
have "Ps = map (extend S) ps" 
     using `extendRule S r = (Ps,\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A)` and extendRule_def and `r = (ps,c)` by auto
then have "\<forall> p \<in> set Ps. (\<exists> p'. p = extend S p')" using ex_map_conv[where ys=Ps and f="extend S"] by auto
then have "\<forall> p \<in> set Ps. (F \<nabla> [x].A :# succ p)" 
     using `F \<nabla> [x].A :# \<Psi>` and `S = (\<Phi> \<Rightarrow>* \<Psi>)` apply (auto simp add:Ball_def) 
     by (drule_tac x=xa in spec) (auto simp add:extend_def)
then have a1:"\<forall> p \<in> set Ps. \<exists> \<Phi>' \<Psi>'. p = (\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [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 \<ominus> F \<nabla> [x].A" in exI) 
     by (drule_tac x=xa in meta_spec) (auto simp add:multiset_eq_conv_count_eq)
with all have "\<forall> p \<in> set Ps. \<exists> \<Phi>' \<Psi>' n. n\<le>n' \<and> (\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [x].A,n) \<in> derivable R* \<and> p = (\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [x].A)"
                 by (auto simp add:Ball_def)
then have a2: "\<forall> p \<in> set Ps. \<exists> \<Phi>' \<Psi>' m. m\<le>n' \<and> (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>',m) \<in> derivable R* \<and> p = (\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [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 (elim exE conjE) apply (drule_tac x=n in spec) apply simp
                 apply (drule_tac x=\<Phi>' in spec,drule_tac x=\<Psi>' in spec)
                 apply (simp) apply (elim exE conjE) by (rule_tac x=m' in exI) (arith)
obtain Ps' where eq: "Ps' = map (extend (\<Phi> + \<Gamma>' \<Rightarrow>* \<Psi>1 + \<Delta>')) ps" by auto
have "length Ps = length Ps'" using `Ps' = map (extend (\<Phi> + \<Gamma>' \<Rightarrow>* \<Psi>1 + \<Delta>')) ps`
                              and `Ps = map (extend S) ps` by auto
then have "Ps' \<noteq> []" using nonempty by auto
from `r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3` have "r \<in> R" using `R = idRules \<union> R1 \<union> R2 \<union> R3` by auto
then have "extendRule (\<Phi> + \<Gamma>' \<Rightarrow>* \<Psi>1 + \<Delta>') r \<in> R*" using `R = idRules \<union> R1 \<union> R2 \<union> 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="\<Phi> + \<Gamma>' \<Rightarrow>* \<Psi>1 + \<Delta>'"]
     and `R1 \<subseteq> propRules` and `R2 \<subseteq> nprovRules` and `R3 \<subseteq> provRules` by auto
moreover have "extendRule (\<Phi> + \<Gamma>' \<Rightarrow>* \<Psi>1 + \<Delta>') r = (Ps',\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>')"
         using `S = (\<Phi> \<Rightarrow>* \<Psi>1 \<oplus> F \<nabla> [x].A)` and `extendRule S r = (Ps, \<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A)`
         and `r = (ps,c)` and eq
         by (auto simp add:extendRule_def extend_def union_ac multiset_eq_conv_count_eq)
ultimately have "(Ps',\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>') \<in> R*" by simp
have c1:"\<forall> p \<in> set ps. extend S p \<in> set Ps" using `Ps = map (extend S) ps` by (simp add:Ball_def)           
have c2:"\<forall> p \<in> set ps. extend (\<Phi> + \<Gamma>' \<Rightarrow>* \<Psi>1 + \<Delta>') p \<in> set Ps'" using eq by (simp add:Ball_def)
then have eq2:"\<forall> p \<in> set Ps'. \<exists> \<Phi>' \<Psi>'. p = (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>')" using eq
          apply (auto simp add:Ball_def extend_def) 
          apply (drule_tac x=xa in spec,simp) apply (rule_tac x="\<Phi> + antec xa" in exI) apply (simp add:union_ac) 
          apply (drule_tac x=xa in spec,simp) by (rule_tac x="\<Psi>1 + succ xa" in exI) (simp add: union_ac)
have d1:"\<forall> p \<in> set Ps. \<exists> p' \<in> set ps. p = extend S p'" using `Ps = map (extend S) ps` by (auto simp add:Ball_def Bex_def)
then have "\<forall> p \<in> set Ps. \<exists> p'. p' \<in> set Ps'" using c2 by (auto simp add:Ball_def Bex_def)
moreover have d2: "\<forall> p \<in> set Ps'. \<exists> p' \<in> set ps. p = extend (\<Phi> + \<Gamma>' \<Rightarrow>* \<Psi>1 + \<Delta>') p'" using eq
            by (auto simp add:Ball_def Bex_def)
then have "\<forall> p \<in> set Ps'. \<exists> p'. p' \<in> set Ps" using c1 by (auto simp add:Ball_def Bex_def)
have "\<forall> \<Phi>' \<Psi>'. (\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [x].A) \<in> set Ps \<longrightarrow> (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') \<in> set Ps'"
               proof-
                 {fix \<Phi>' \<Psi>'
                 assume "(\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [x].A) \<in> set Ps"  
                 then have "\<exists> p \<in> set ps. extend (\<Phi> \<Rightarrow>* \<Psi>1 \<oplus> F \<nabla> [x].A) p = (\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [x].A)"
                      using `Ps = map (extend S) ps` and `S = (\<Phi> \<Rightarrow>* \<Psi>1 \<oplus> F \<nabla> [x].A)` and a1 and d1
                           apply (simp only:Ball_def Bex_def) apply (drule_tac x=" \<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [x].A" in spec)
                           by (drule_tac x="\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [x].A" in spec) (auto)
                 then obtain p where t:"p \<in> set ps \<and> (\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [x].A) = extend (\<Phi> \<Rightarrow>* \<Psi>1 \<oplus> F \<nabla> [x].A) p"
                      apply auto by (drule_tac x=p in meta_spec) (simp)
                 then obtain D B where "p = (D \<Rightarrow>* B)" by (cases p) 
                 then have "(D \<Rightarrow>* B) \<in> set ps \<and> (\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [x].A) = extend (\<Phi> \<Rightarrow>* \<Psi>1 \<oplus> F \<nabla> [x].A) (D \<Rightarrow>* B)"
                      using t by auto
                 then have ant: "\<Phi>' = \<Phi> + D" and suc: "\<Psi>' \<oplus> F \<nabla> [x].A = \<Psi>1 \<oplus> F \<nabla> [x].A + B" using extend_def by auto
                 from ant have "\<Phi>' + \<Gamma>' = (\<Phi> + \<Gamma>') + D" by (auto simp add:union_ac)
                 moreover
                 from suc have "\<Psi>' = \<Psi>1 + B" by (auto simp add:union_ac multiset_eq_conv_count_eq)
                 then have "\<Psi>' + \<Delta>' = (\<Psi>1 + \<Delta>') + B" by (auto simp add:union_ac)
                 ultimately have "(\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') = extend (\<Phi> + \<Gamma>' \<Rightarrow>* \<Psi>1 + \<Delta>') (D \<Rightarrow>* B)" using extend_def by auto
                 moreover have "extend (\<Phi> + \<Gamma>' \<Rightarrow>* \<Psi>1 + \<Delta>') (D \<Rightarrow>* B) \<in> set Ps'" using `p = (D \<Rightarrow>* B)` and t and c2 by auto
                 ultimately have "(\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') \<in> set Ps'" by simp
                 }
                 thus ?thesis by blast
               qed
            moreover
            have "\<forall> \<Phi>' \<Psi>'. (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') \<in> set Ps' \<longrightarrow> (\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [x].A) \<in> set Ps"
               proof-
                 {fix \<Phi>' \<Psi>'
                 assume "(\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') \<in> set Ps'"  
                 then have "\<exists> p \<in> set ps. extend (\<Phi> + \<Gamma>' \<Rightarrow>* \<Psi>1 + \<Delta>') p = (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>')"
                      using eq and eq2 and d2
                           apply (simp only:Ball_def Bex_def) apply (drule_tac x="\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>'" in spec)
                           by (drule_tac x="\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>'" in spec) (auto)
                 then obtain p where t:"p \<in> set ps \<and> (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') = extend (\<Phi> + \<Gamma>' \<Rightarrow>* \<Psi>1 + \<Delta>') p"
                      apply auto by (drule_tac x=p in meta_spec) (simp)
                 then obtain D B where "p = (D \<Rightarrow>* B)" by (cases p) 
                 then have "(D \<Rightarrow>* B) \<in> set ps \<and> (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') = extend (\<Phi> + \<Gamma>' \<Rightarrow>* \<Psi>1 + \<Delta>') (D \<Rightarrow>* B)"
                      using t by auto
                 then have ant: "\<Phi>' + \<Gamma>' = \<Phi> + \<Gamma>' + D" and suc: "\<Psi>' + \<Delta>' = \<Psi>1 + \<Delta>' + B" using extend_def by auto
                 from ant have "\<Phi>' + \<Gamma>' = (\<Phi> + D) + \<Gamma>'" by (auto simp add:union_ac)
                 then have "\<Phi>' = \<Phi> + D" by simp
                 moreover
                 from suc have "\<Psi>' + \<Delta>' = (\<Psi>1 + B) + \<Delta>'" by (auto simp add:union_ac)
                 then have "\<Psi>' = \<Psi>1 + B" by simp
                 then have "\<Psi>' \<oplus> F \<nabla> [x].A = (\<Psi>1 \<oplus> F \<nabla> [x].A) + B" by (auto simp add:union_ac)
                 ultimately have "(\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [x].A) = extend (\<Phi> \<Rightarrow>* \<Psi>1 \<oplus> F \<nabla> [x].A) (D \<Rightarrow>* B)" 
                      using extend_def by auto
                 moreover have "extend (\<Phi>  \<Rightarrow>* \<Psi>1 \<oplus> F \<nabla> [x].A) (D \<Rightarrow>* B) \<in> set Ps" using `p = (D \<Rightarrow>* B)` and t and c1
                      and `S = (\<Phi> \<Rightarrow>* \<Psi>1 \<oplus> F \<nabla> [x].A)` by auto
                 ultimately have "(\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [x].A) \<in> set Ps" by simp
                 }
                 thus ?thesis by blast
               qed
ultimately
have "\<forall> \<Phi>' \<Psi>'. ((\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [x].A) \<in> set Ps) = ((\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') \<in> set Ps')" by auto
then have "\<forall> p \<in> set Ps'. \<exists> \<Phi>' \<Psi>' n. n\<le>n' \<and> (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>',n) \<in> derivable R*
                \<and> p = (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>')" 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=\<Phi>' in spec,drule_tac x=\<Psi>' in spec)  
     by (drule_tac x="\<Phi>' \<Rightarrow>* \<Psi>' \<oplus> F \<nabla> [x].A" in spec) (simp)
then have all:"\<forall> p \<in> set Ps'. \<exists> n\<le>n'. (p,n) \<in> derivable R*" by auto
then show "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" using num
     and `(Ps',\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>') \<in> R*` and `Ps' \<noteq> []`
     and derivable.step[where r="(Ps',\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>')" and R="R*"]
     by (auto simp add:Ball_def Bex_def)
qed


(* Non-principal Left *)
lemma nonPrincipalInvertLeft:
assumes "R1 \<subseteq> propRules" and "R2 \<subseteq> nprovRules" and "R3 \<subseteq> provRules"
    and "R = idRules \<union> R1 \<union> R2 \<union> R3" and "r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3" and "r = (ps,c)"
    and IH: "\<forall>m<n. \<forall>\<Gamma> \<Delta>. ( \<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>, m) \<in> derivable R* \<longrightarrow>
              (\<forall>r' \<in> R. leftPrincipal r' (F \<nabla> [x].A) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* \<Delta>') \<in> set (fst r')) \<longrightarrow>
              (\<not> multSubst \<Gamma>' \<and> \<not> multSubst \<Delta>') \<longrightarrow>
              (\<exists>m'\<le>m. ( \<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>', m') \<in> derivable R*)"
    and a': "(\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>,n) \<in> derivable R*" 
    and b': "\<forall> r' \<in> R. leftPrincipal r' (F \<nabla> [x].A) \<longrightarrow> (\<Gamma>' \<Rightarrow>* \<Delta>') \<in> set (fst r')"
    and c': "\<not> multSubst \<Gamma>' \<and> \<not> multSubst \<Delta>'"
    and np: "\<not> leftPrincipal r (F \<nabla> [x].A)"
    and ext: "extendRule S r = (Ps,\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>)"
    and num: "n = n' + 1"
    and all: "\<forall> p \<in> set Ps. \<exists> n\<le>n'. (p,n) \<in> derivable R*"
    and nonempty: "Ps \<noteq> []"
shows "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*"
proof-
from ext obtain \<Phi> \<Psi> where "S = (\<Phi> \<Rightarrow>* \<Psi>)" by (cases S) (auto)
from `r = (ps,c)` obtain G H where "c = (G \<Rightarrow>* H)" by (cases c) (auto)
then have "{# F \<nabla> [x].A  #} \<noteq> G" using `r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3`
     proof-
     {assume "r \<in> R1" then have "r \<in> propRules" using `R1 \<subseteq> propRules` by auto
      with `r = (ps,c)` obtain T Ts where "c = ({#} \<Rightarrow>* {#Cpd0 T Ts#}) \<or> c = ({#Cpd0 T Ts#} \<Rightarrow>* {#})"
            using propRuleCharacterise[where Ps=ps and C=c] by auto
      moreover
        {assume "c = ({#} \<Rightarrow>* {#Cpd0 T Ts#})"
         with `c = (G \<Rightarrow>* H)` have "{# F \<nabla> [x].A #} \<noteq> G" by auto
        }
      moreover
        {assume "c = ({#Cpd0 T Ts#} \<Rightarrow>* {#})"
         then have "{#F \<nabla> [x].A #} \<noteq> G" using `c = (G \<Rightarrow>* H)` by auto
        }
      ultimately have "{# F \<nabla> [x].A #} \<noteq> G" by blast
     }
     moreover
     {assume "r \<in> R2 \<or> r \<in> R3" 
      then have "r \<in> provRules \<or> r \<in> nprovRules" using `R2 \<subseteq> nprovRules` and `R3 \<subseteq> provRules` by auto
      with `r = (ps,c)` obtain T y B where "c = ({#} \<Rightarrow>* {# T \<nabla> [y].B #}) \<or> c = ({# T \<nabla> [y].B#} \<Rightarrow>* {#})"
            using provRuleCharacterise[where Ps=ps and C=c]
            and nprovRuleCharacterise[where Ps=ps and C=c] by auto
      moreover
        {assume "c = ({#} \<Rightarrow>* {# T \<nabla> [y].B#})"
         then have "{#F \<nabla> [x].A #} \<noteq> G" using `c = (G \<Rightarrow>* H)` by auto         
        }
      moreover
        {assume "c = ({#T \<nabla> [y].B #} \<Rightarrow>* {#})"
         then have "leftPrincipal r (T \<nabla> [y].B)" using `r = (ps,c)` by auto
         with `\<not> leftPrincipal r (F \<nabla> [x].A)` have "T \<nabla> [y].B \<noteq> F \<nabla> [x].A" by auto
         with `c = (G \<Rightarrow>* H)` have "{# F \<nabla> [x].A #} \<noteq> G" using `c = ({# T \<nabla> [y].B #} \<Rightarrow>* {#})` by auto
        }
      ultimately have "{# F \<nabla> [x].A #} \<noteq> G" by blast
     }
     ultimately show ?thesis using `r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3` by blast
     qed
moreover have "antec S + antec (snd r) = (\<Gamma> \<oplus> F \<nabla> [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 "\<Phi> + G = \<Gamma> \<oplus> F \<nabla> [x].A" using `S = (\<Phi> \<Rightarrow>* \<Psi>)` and `r = (ps,c)` and `c = (G \<Rightarrow>* H)` by auto
moreover from `r = (ps,c)` and `r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3` and `R1 \<subseteq> propRules` and `R2 \<subseteq> nprovRules`
              and `R3 \<subseteq> provRules` have "(ps,c) \<in> propRules \<or> (ps,c) \<in> nprovRules \<or> (ps,c) \<in> provRules" by auto
then have "\<exists> A. c = ({#} \<Rightarrow>* {#A#}) \<or> c = ({#A#} \<Rightarrow>* {#})"
     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 = {#} \<or> (\<exists> A. G = {#A#})" using `c = (G \<Rightarrow>* H)` by auto
ultimately have "F \<nabla> [x].A :# \<Phi>"
    proof-
    have "G = {#} \<or> (\<exists> A. G = {#A#})" by fact
    moreover
    {assume "G = {#}"
     then have "\<Phi> = \<Gamma> \<oplus> F \<nabla> [x].A" using `\<Phi> + G = \<Gamma> \<oplus> F \<nabla> [x].A` by auto
     then have "F \<nabla> [x].A :# \<Phi>" by auto
    }
    moreover
    {assume "\<exists> A. G = {#A#}"
     then obtain T where "G = {#T#}" by auto
     then have "\<Phi> \<oplus> T = \<Gamma> \<oplus> F \<nabla> [x].A" using `\<Phi> + G = \<Gamma> \<oplus> F \<nabla> [x].A` by auto
     then have "set_of (\<Phi> \<oplus> T) = set_of (\<Gamma> \<oplus> F \<nabla> [x].A)" by auto
     then have "set_of \<Phi> \<union> {T} = set_of \<Gamma> \<union> {F \<nabla> [x].A}" by auto
     moreover from `G = {#T#}` and `{#F \<nabla> [x].A#} \<noteq> G` have "F \<nabla> [x].A \<noteq> T" by auto
     ultimately have "F \<nabla> [x].A \<in> set_of \<Phi>" by auto
     then have "F \<nabla> [x].A :# \<Phi>" by auto
    }
    ultimately show "F \<nabla> [x].A :# \<Phi>" by blast
    qed
then have "\<exists> \<Phi>1. \<Phi> = \<Phi>1 \<oplus> F \<nabla> [x].A" 
     by (rule_tac x="\<Phi> \<ominus> F \<nabla> [x].A" in exI) (auto simp add:multiset_eq_conv_count_eq)
then obtain \<Phi>1 where "S = (\<Phi>1 \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>)" using `S = (\<Phi> \<Rightarrow>* \<Psi>)` by auto
have "Ps = map (extend S) ps" 
     using `extendRule S r = (Ps,\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>)` and extendRule_def and `r = (ps,c)` by auto
then have "\<forall> p \<in> set Ps. (\<exists> p'. p = extend S p')" using ex_map_conv[where ys=Ps and f="extend S"] by auto
then have "\<forall> p \<in> set Ps. (F \<nabla> [x].A :# antec p)" 
     using `F \<nabla> [x].A :# \<Phi>` and `S = (\<Phi> \<Rightarrow>* \<Psi>)` apply (auto simp add:Ball_def) 
     by (drule_tac x=xa in spec) (auto simp add:extend_def)
then have a1:"\<forall> p \<in> set Ps. \<exists> \<Phi>' \<Psi>'. p = (\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>')" using characteriseSeq
     apply (auto simp add:Ball_def) apply (drule_tac x=xa in spec,simp) 
     apply (rule_tac x="antec xa \<ominus> F \<nabla> [x].A" in exI,rule_tac x="succ xa" in exI) 
     by (drule_tac x=xa in meta_spec) (auto simp add:multiset_eq_conv_count_eq)
with all have "\<forall> p \<in> set Ps. \<exists> \<Phi>' \<Psi>' n. n\<le>n' \<and> (\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>',n) \<in> derivable R* \<and> p = (\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>')"
                 by (auto simp add:Ball_def)
then have a2: "\<forall> p \<in> set Ps. \<exists> \<Phi>' \<Psi>' m. m\<le>n' \<and> (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>',m) \<in> derivable R* \<and> p = (\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>')"
                 using num and b' and IH and c'
                 apply (auto simp add:Ball_def) apply (drule_tac x=xa in spec) apply simp
                 apply (elim exE conjE) apply (drule_tac x=n in spec) apply simp
                 apply (drule_tac x=\<Phi>' in spec,drule_tac x=\<Psi>' in spec)
                 apply (simp) apply (elim exE conjE) by (rule_tac x=m' in exI) (arith)
obtain Ps' where eq: "Ps' = map (extend (\<Phi>1 + \<Gamma>' \<Rightarrow>* \<Psi> + \<Delta>')) ps" by auto
have "length Ps = length Ps'" using `Ps' = map (extend (\<Phi>1 + \<Gamma>' \<Rightarrow>* \<Psi> + \<Delta>')) ps`
                              and `Ps = map (extend S) ps` by auto
then have "Ps' \<noteq> []" using nonempty by auto
from `r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3` have "r \<in> R" using `R = idRules \<union> R1 \<union> R2 \<union> R3` by auto
then have "extendRule (\<Phi>1 + \<Gamma>' \<Rightarrow>* \<Psi> + \<Delta>') r \<in> R*" using `R = idRules \<union> R1 \<union> R2 \<union> 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="\<Phi>1 + \<Gamma>' \<Rightarrow>* \<Psi> + \<Delta>'"]
     and `R1 \<subseteq> propRules` and `R2 \<subseteq> nprovRules` and `R3 \<subseteq> provRules` by auto
moreover have "extendRule (\<Phi>1 + \<Gamma>' \<Rightarrow>* \<Psi> + \<Delta>') r = (Ps',\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>')"
         using `S = (\<Phi>1 \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>)` and `extendRule S r = (Ps, \<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>)`
         and `r = (ps,c)` and eq
         by (auto simp add:extendRule_def extend_def union_ac multiset_eq_conv_count_eq)
ultimately have "(Ps',\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>') \<in> R*" by simp
have c1:"\<forall> p \<in> set ps. extend S p \<in> set Ps" using `Ps = map (extend S) ps` by (simp add:Ball_def)           
have c2:"\<forall> p \<in> set ps. extend (\<Phi>1 + \<Gamma>' \<Rightarrow>* \<Psi> + \<Delta>') p \<in> set Ps'" using eq by (simp add:Ball_def)
then have eq2:"\<forall> p \<in> set Ps'. \<exists> \<Phi>' \<Psi>'. p = (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>')" using eq
          apply (auto simp add:Ball_def extend_def) 
          apply (drule_tac x=xa in spec,simp) apply (rule_tac x="\<Phi>1 + antec xa" in exI) apply (simp add:union_ac) 
          apply (drule_tac x=xa in spec,simp) by (rule_tac x="\<Psi> + succ xa" in exI) (simp add: union_ac)
have d1:"\<forall> p \<in> set Ps. \<exists> p' \<in> set ps. p = extend S p'" using `Ps = map (extend S) ps` by (auto simp add:Ball_def Bex_def)
then have "\<forall> p \<in> set Ps. \<exists> p'. p' \<in> set Ps'" using c2 by (auto simp add:Ball_def Bex_def)
moreover have d2: "\<forall> p \<in> set Ps'. \<exists> p' \<in> set ps. p = extend (\<Phi>1 + \<Gamma>' \<Rightarrow>* \<Psi> + \<Delta>') p'" using eq
            by (auto simp add:Ball_def Bex_def)
then have "\<forall> p \<in> set Ps'. \<exists> p'. p' \<in> set Ps" using c1 by (auto simp add:Ball_def Bex_def)
have "\<forall> \<Phi>' \<Psi>'. (\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>') \<in> set Ps \<longrightarrow> (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') \<in> set Ps'"
               proof-
                 {fix \<Phi>' \<Psi>'
                 assume "(\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>') \<in> set Ps"  
                 then have "\<exists> p \<in> set ps. extend (\<Phi>1 \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>) p = (\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>')"
                      using `Ps = map (extend S) ps` and `S = (\<Phi>1 \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>)` and a1 and d1
                           apply (simp only:Ball_def Bex_def) apply (drule_tac x=" \<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>'" in spec)
                           by (drule_tac x="\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>'" in spec) (auto)
                 then obtain p where t:"p \<in> set ps \<and> (\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>') = extend (\<Phi>1 \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>) p"
                      apply auto by (drule_tac x=p in meta_spec) (simp)
                 then obtain D B where "p = (D \<Rightarrow>* B)" by (cases p) 
                 then have "(D \<Rightarrow>* B) \<in> set ps \<and> (\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>') = extend (\<Phi>1 \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>) (D \<Rightarrow>* B)"
                      using t by auto
                 then have ant: "\<Phi>' \<oplus> F \<nabla> [x].A = \<Phi>1 \<oplus> F \<nabla> [x].A + D" and suc: "\<Psi>' = \<Psi> + B" using extend_def by auto
                 from suc have "\<Psi>' + \<Delta>' = (\<Psi> + \<Delta>') + B" by (auto simp add:union_ac)
                 moreover
                 from ant have "\<Phi>' = \<Phi>1 + D" by (auto simp add:union_ac multiset_eq_conv_count_eq)
                 then have "\<Phi>' + \<Gamma>' = (\<Phi>1 + \<Gamma>') + D" by (auto simp add:union_ac)
                 ultimately have "(\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') = extend (\<Phi>1 + \<Gamma>' \<Rightarrow>* \<Psi> + \<Delta>') (D \<Rightarrow>* B)" using extend_def by auto
                 moreover have "extend (\<Phi>1 + \<Gamma>' \<Rightarrow>* \<Psi> + \<Delta>') (D \<Rightarrow>* B) \<in> set Ps'" using `p = (D \<Rightarrow>* B)` and t and c2 by auto
                 ultimately have "(\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') \<in> set Ps'" by simp
                 }
                 thus ?thesis by blast
               qed
            moreover
            have "\<forall> \<Phi>' \<Psi>'. (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') \<in> set Ps' \<longrightarrow> (\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>') \<in> set Ps"
               proof-
                 {fix \<Phi>' \<Psi>'
                 assume "(\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') \<in> set Ps'"  
                 then have "\<exists> p \<in> set ps. extend (\<Phi>1 + \<Gamma>' \<Rightarrow>* \<Psi> + \<Delta>') p = (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>')"
                      using eq and eq2 and d2
                           apply (simp only:Ball_def Bex_def) apply (drule_tac x="\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>'" in spec)
                           by (drule_tac x="\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>'" in spec) (auto)
                 then obtain p where t:"p \<in> set ps \<and> (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') = extend (\<Phi>1 + \<Gamma>' \<Rightarrow>* \<Psi> + \<Delta>') p"
                      apply auto by (drule_tac x=p in meta_spec) (simp)
                 then obtain D B where "p = (D \<Rightarrow>* B)" by (cases p) 
                 then have "(D \<Rightarrow>* B) \<in> set ps \<and> (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') = extend (\<Phi>1 + \<Gamma>' \<Rightarrow>* \<Psi> + \<Delta>') (D \<Rightarrow>* B)"
                      using t by auto
                 then have ant: "\<Phi>' + \<Gamma>' = \<Phi>1 + \<Gamma>' + D" and suc: "\<Psi>' + \<Delta>' = \<Psi> + \<Delta>' + B" using extend_def by auto
                 from ant have "\<Phi>' + \<Gamma>' = (\<Phi>1 + D) + \<Gamma>'" by (auto simp add:union_ac)
                 then have "\<Phi>' = \<Phi>1 + D" by simp
                 then have "\<Phi>' \<oplus> F \<nabla> [x].A = (\<Phi>1 \<oplus> F \<nabla> [x].A) + D" by (auto simp add:union_ac)
                 moreover
                 from suc have "\<Psi>' + \<Delta>' = (\<Psi> + B) + \<Delta>'" by (auto simp add:union_ac)
                 then have "\<Psi>' = \<Psi> + B" by simp
                 ultimately have "(\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>') = extend (\<Phi>1 \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>) (D \<Rightarrow>* B)" 
                      using extend_def by auto
                 moreover have "extend (\<Phi>1 \<oplus> F \<nabla> [x].A  \<Rightarrow>* \<Psi>) (D \<Rightarrow>* B) \<in> set Ps" using `p = (D \<Rightarrow>* B)` and t and c1
                      and `S = (\<Phi>1 \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>)` by auto
                 ultimately have "(\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>') \<in> set Ps" by simp
                 }
                 thus ?thesis by blast
               qed
ultimately
have "\<forall> \<Phi>' \<Psi>'. ((\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>') \<in> set Ps) = ((\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>') \<in> set Ps')" by auto
then have "\<forall> p \<in> set Ps'. \<exists> \<Phi>' \<Psi>' n. n\<le>n' \<and> (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>',n) \<in> derivable R*
                \<and> p = (\<Phi>' + \<Gamma>' \<Rightarrow>* \<Psi>' + \<Delta>')" 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=\<Phi>' in spec,drule_tac x=\<Psi>' in spec)  
     by (drule_tac x="\<Phi>' \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Psi>'" in spec) (simp)
then have all:"\<forall> p \<in> set Ps'. \<exists> n\<le>n'. (p,n) \<in> derivable R*" by auto
then show "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" using num
     and `(Ps',\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>') \<in> R*` and `Ps' \<noteq> []`
     and derivable.step[where r="(Ps',\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>')" and R="R*"]
     by (auto simp add:Ball_def Bex_def)
qed

lemma rightInvert:
fixes \<Gamma> \<Delta> :: "form multiset"
assumes rules: "R1 \<subseteq> propRules \<and> R2 \<subseteq> nprovRules \<and> R3 \<subseteq> provRules \<and> R = idRules \<union> R1 \<union> R2 \<union> R3"
    and   a: "(\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A,n) \<in> derivable R*"
    and   b: "\<forall> r' \<in> R. rightPrincipal r' (F \<nabla> [x].A) \<longrightarrow> (\<Gamma>' \<Rightarrow>* \<Delta>') \<in> set (fst r')"
    and   c: "\<not> multSubst \<Gamma>' \<and> \<not> multSubst \<Delta>'"
shows "\<exists> m\<le>n. (\<Gamma> +\<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*"
using assms
proof (induct n arbitrary: \<Gamma> \<Delta> rule:nat_less_induct)
 case (1 n \<Gamma> \<Delta>)
 then have IH:"\<forall>m<n. \<forall>\<Gamma> \<Delta>. ( \<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A, m) \<in> derivable R* \<longrightarrow>
              (\<forall>r' \<in> R. rightPrincipal r' (F \<nabla> [x].A) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* \<Delta>') \<in> set (fst r')) \<longrightarrow>
              (\<not> multSubst \<Gamma>' \<and> \<not> multSubst \<Delta>') \<longrightarrow>
              (\<exists>m'\<le>m. ( \<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>', m') \<in> derivable R*)" 
     and a': "(\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A,n) \<in> derivable R*" 
     and b': "\<forall> r' \<in> R. rightPrincipal r' (F \<nabla> [x].A) \<longrightarrow> (\<Gamma>' \<Rightarrow>* \<Delta>') \<in> set (fst r')"
     and c': "\<not> multSubst \<Gamma>' \<and> \<not> multSubst \<Delta>'"
       by auto
 show ?case
 proof (cases n)
     case 0
     then have "(\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A,0) \<in> derivable R*" using a' by simp
     then have "([],\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A) \<in> R*" by (cases) (auto)
     then have "\<exists> r S. extendRule S r = ([],\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A) \<and> (r \<in> idRules \<or> r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3)"
          using rules and ruleSet[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and Ps="[]" and C="\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A"]
           by auto
     then obtain r S where "extendRule S r = ([],\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A)" and "r \<in> idRules \<or> r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3" by auto
      moreover
      {assume "r \<in> idRules"
       then have "\<exists> i xs. r = ([],{# At i xs #} \<Rightarrow>* {# At i xs #})" using characteriseID[where r=r] by auto
       then obtain i xs where "([], {# At i xs #} \<Rightarrow>* {# At i xs #}) = r" by blast
       from `extendRule S r = ([],\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A)` and `([], {# At i xs #} \<Rightarrow>* {# At i xs #}) = r`
       have "extend S ({# At i xs #} \<Rightarrow>* {# At i xs #}) = (\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A)"
          using extendRule_def[where R=r and forms=S] 
                extend_def[where forms=S and seq="{#At i xs#} \<Rightarrow>* {#At i xs#}"] by auto
       then have "At i xs :# \<Gamma> \<and> At i xs :# \<Delta>" 
            using extendID[where S=S and i=i and xs=xs and \<Gamma>=\<Gamma> and \<Delta>="\<Delta> \<oplus> F \<nabla> [x].A"] by auto
       then have "At i xs :# \<Gamma> + \<Gamma>' \<and> At i xs :# \<Delta> + \<Delta>'" by auto
       then have "(\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',0) \<in> derivable R*" using rules
            and containID[where \<Gamma>="\<Gamma> + \<Gamma>'" and i=i and \<Delta>="\<Delta> + \<Delta>'" and R=R] by auto
      }
      moreover
      {assume "r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3"
       then have "\<exists> Ps C. Ps \<noteq> [] \<and> r = (Ps,C)"
            proof-
            obtain y z where "r = (y,z)" by (cases r)
            with `r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3` have "(y,z) \<in> R1 \<or> (y,z) \<in> R2 \<or> (y,z) \<in> R3" by simp
            then have "y \<noteq> []"
                 proof-
                 {assume "(y,z) \<in> R1"
                  then have "(y,z) \<in> propRules" using rules by auto
                  then have "y\<noteq>[]" by (cases) auto
                 }
                 moreover
                 {assume "(y,z) \<in> R2"
                  then have "(y,z) \<in> nprovRules" using rules by auto
                  then have "y\<noteq>[]" by (cases) auto
                 }
                 moreover
                 {assume "(y,z) \<in> R3"
                  then have "(y,z) \<in> provRules" using rules by auto
                  then have "y\<noteq>[]" by (cases) auto
                 }
                 ultimately show "y \<noteq> []" using `(y,z) \<in> R1 \<or> (y,z) \<in> R2 \<or> (y,z) \<in> R3` by blast
                 qed
            then show "\<exists> Ps C. Ps \<noteq> [] \<and> r = (Ps,C)" using `r = (y,z)`  by blast
            qed
       then obtain Ps C where "Ps \<noteq> []" and "r = (Ps,C)" by auto
       moreover from `extendRule S r = ([], \<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A)` have "\<exists> 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 "(\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',0) \<in> derivable R*" using rules by simp
       }
       ultimately show "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" using `n=0` by blast
 next
     case (Suc n')
     then have "(\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A,n'+1) \<in> derivable R*" using a' by simp
     then obtain Ps where "(Ps, \<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A) \<in> R*" and 
                          "Ps \<noteq> []" and 
                       d':"\<forall> p \<in> set Ps. \<exists> n\<le>n'. (p,n) \<in> derivable R*"
          using characteriseLast[where C="\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A" and m=n' and R="R*"] by auto
     then have "\<exists> r S. (r \<in> idRules \<or> r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3) \<and> extendRule S r = (Ps, \<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [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="\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A"] by auto
     then obtain r S where "r \<in> idRules \<or> r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3" 
                    and e':"extendRule S r = (Ps, \<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A)" by auto
     moreover
        {assume "r \<in> idRules"
         then have "\<exists> i xs. r = ([],{# At i xs #} \<Rightarrow>* {# At i xs #})" using characteriseID[where r=r] by auto
         moreover obtain z y where "r = (z,y)" by (cases r)
         then have "z \<noteq> []" using `Ps \<noteq> []` and `extendRule S r = (Ps, \<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [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 "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*"
              using `r=(z,y)` by auto
        }
     moreover
        {assume "r \<in> R1"
         obtain ps c where "r = (ps,c)" by (cases r) auto
         then have "r \<in> propRules" using rules and `r \<in> R1` by auto
         then obtain T Ts where sw:"c = ({#} \<Rightarrow>* {# Cpd0 T Ts #}) \<or> c = ({# Cpd0 T Ts #} \<Rightarrow>* {#})"
              using propRuleCharacterise[where Ps=ps and C=c] and `r = (ps,c)` by auto
         have "(rightPrincipal r (F \<nabla> [x].A)) \<or> \<not>(rightPrincipal r (F \<nabla> [x].A))" by blast
         moreover
            {assume "rightPrincipal r (F \<nabla> [x].A)"
             then have "c = ({#} \<Rightarrow>* {# F \<nabla> [x].A #})" using `r=  (ps,c)` by (cases) auto
             with sw have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" by auto
            }
         moreover
            {assume "\<not> rightPrincipal r (F \<nabla> [x].A)"
             then have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> 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 \<Gamma>'=\<Gamma>' and \<Delta>'=\<Delta>' and ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3
                                                and S=S and Ps=Ps and \<Gamma>=\<Gamma> and \<Delta>=\<Delta> and n=n and n'=n']
                  and `n = Suc n'` and `Ps \<noteq> []` and a' and b' and e'
                  and c' and rules and IH and `r \<in> R1` and d' and `r = (ps,c)` by auto
            }
         ultimately have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" by blast         
        }
     moreover
        {assume "r \<in> R2"
         obtain ps c where "r = (ps,c)" by (cases r) auto
         then have "r \<in> nprovRules" using rules and `r \<in> R2` by auto
         have "rightPrincipal r (F \<nabla> [x].A) \<or> \<not> rightPrincipal r (F \<nabla> [x].A)" by blast
         moreover
            {assume "rightPrincipal r (F \<nabla> [x].A)"
             then have "(\<Gamma>' \<Rightarrow>* \<Delta>') \<in> set ps" using b' and `r = (ps,c)` and `r \<in> R2` and rules
                  by auto
             then have "extend S (\<Gamma>' \<Rightarrow>* \<Delta>') \<in> set Ps" using `extendRule S r = (Ps,\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A)`
                  and `r = (ps,c)` by (simp add:extendContain)
             moreover from `rightPrincipal r (F \<nabla> [x].A)` have "c = ({#} \<Rightarrow>* {#F \<nabla> [x].A#})" 
                  using `r = (ps,c)` by (cases) auto
             with `extendRule S r = (Ps,\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A)` have "S = (\<Gamma> \<Rightarrow>* \<Delta>)"
                  using `r = (ps,c)` apply (auto simp add:extendRule_def extend_def) by (cases S) auto
             ultimately have "(\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>') \<in> set Ps" by (simp add:extend_def)
             then have "\<exists> m\<le>n'. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*"
                  using `\<forall> p \<in> set Ps. \<exists> n\<le>n'. (p,n) \<in> derivable R*` by auto
             then have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" using `n = Suc n'`
                  by (auto,rule_tac x=m in exI) (simp)
            }
         moreover
            {assume "\<not> rightPrincipal r (F \<nabla> [x].A)"
             then have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> 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 \<Gamma>'=\<Gamma>' and \<Delta>'=\<Delta>' and ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3
                                                and S=S and Ps=Ps and \<Gamma>=\<Gamma> and \<Delta>=\<Delta> and n=n and n'=n']
                  and `n = Suc n'` and `Ps \<noteq> []` and a' and b' and e'
                  and c' and rules and IH and `r \<in> R2` and d' and `r = (ps,c)` by auto
            }
         ultimately have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" by blast
        }
     moreover
        {assume "r \<in> R3"
         obtain ps c where "r = (ps,c)" by (cases r) auto
         then have "r \<in> provRules" using rules and `r \<in> R3` by auto
         have "rightPrincipal r (F \<nabla> [x].A) \<or> \<not> rightPrincipal r (F \<nabla> [x].A)" by blast
         moreover
            {assume "rightPrincipal r (F \<nabla> [x].A)"
             then have "(\<Gamma>' \<Rightarrow>* \<Delta>') \<in> set ps" using b' and `r = (ps,c)` and `r \<in> R3` and rules
                  by auto
             then have "extend S (\<Gamma>' \<Rightarrow>* \<Delta>') \<in> set Ps" using `extendRule S r = (Ps,\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A)`
                  and `r = (ps,c)` by (simp add:extendContain)
             moreover from `rightPrincipal r (F \<nabla> [x].A)` have "c = ({#} \<Rightarrow>* {#F \<nabla> [x].A#})" 
                  using `r = (ps,c)` by (cases) auto
             with `extendRule S r = (Ps,\<Gamma> \<Rightarrow>* \<Delta> \<oplus> F \<nabla> [x].A)` have "S = (\<Gamma> \<Rightarrow>* \<Delta>)"
                  using `r = (ps,c)` apply (auto simp add:extendRule_def extend_def) by (cases S) auto
             ultimately have "(\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>') \<in> set Ps" by (simp add:extend_def)
             then have "\<exists> m\<le>n'. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*"
                  using `\<forall> p \<in> set Ps. \<exists> n\<le>n'. (p,n) \<in> derivable R*` by auto
             then have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" using `n = Suc n'`
                  by (auto,rule_tac x=m in exI) (simp)
            }
         moreover
            {assume "\<not> rightPrincipal r (F \<nabla> [x].A)"
             then have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> 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 \<Gamma>'=\<Gamma>' and \<Delta>'=\<Delta>' and ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3
                                                and S=S and Ps=Ps and \<Gamma>=\<Gamma> and \<Delta>=\<Delta> and n=n and n'=n']
                  and `n = Suc n'` and `Ps \<noteq> []` and a' and b' and e'
                  and c' and rules and IH and `r \<in> R3` and d' and `r = (ps,c)` by auto
            }
         ultimately have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" by blast
        }
     ultimately show "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" by blast
   qed
qed

lemma leftInvert:
fixes \<Gamma> \<Delta> :: "form multiset"
assumes rules: "R1 \<subseteq> propRules \<and> R2 \<subseteq> nprovRules \<and> R3 \<subseteq> provRules \<and> R = idRules \<union> R1 \<union> R2 \<union> R3"
    and   a: "(\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>,n) \<in> derivable R*"
    and   b: "\<forall> r' \<in> R. leftPrincipal r' (F \<nabla> [x].A) \<longrightarrow> (\<Gamma>' \<Rightarrow>* \<Delta>') \<in> set (fst r')"
    and   c: "\<not> multSubst \<Gamma>' \<and> \<not> multSubst \<Delta>'"
shows "\<exists> m\<le>n. (\<Gamma> +\<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*"
using assms
proof (induct n arbitrary: \<Gamma> \<Delta> rule:nat_less_induct)
 case (1 n \<Gamma> \<Delta>)
 then have IH:"\<forall>m<n. \<forall>\<Gamma> \<Delta>. ( \<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>, m) \<in> derivable R* \<longrightarrow>
              (\<forall>r' \<in> R. leftPrincipal r' (F \<nabla> [x].A) \<longrightarrow> ( \<Gamma>' \<Rightarrow>* \<Delta>') \<in> set (fst r')) \<longrightarrow>
              (\<not> multSubst \<Gamma>' \<and> \<not> multSubst \<Delta>') \<longrightarrow>
              (\<exists>m'\<le>m. ( \<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>', m') \<in> derivable R*)" 
     and a': "(\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>,n) \<in> derivable R*" 
     and b': "\<forall> r' \<in> R. leftPrincipal r' (F \<nabla> [x].A) \<longrightarrow> (\<Gamma>' \<Rightarrow>* \<Delta>') \<in> set (fst r')"
     and c': "\<not> multSubst \<Gamma>' \<and> \<not> multSubst \<Delta>'"
       by auto
 show ?case
 proof (cases n)
     case 0
     then have "(\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>,0) \<in> derivable R*" using a' by simp
     then have "([],\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>) \<in> R*" by (cases) (auto)
     then have "\<exists> r S. extendRule S r = ([],\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>) \<and> (r \<in> idRules \<or> r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3)"
          using rules and ruleSet[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and Ps="[]" and C="\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>*\<Delta>"]
           by auto
     then obtain r S where "extendRule S r = ([],\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>)" and "r \<in> idRules \<or> r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3" by auto
      moreover
      {assume "r \<in> idRules"
       then have "\<exists> i xs. r = ([],{# At i xs #} \<Rightarrow>* {# At i xs #})" using characteriseID[where r=r] by auto
       then obtain i xs where "([], {# At i xs #} \<Rightarrow>* {# At i xs #}) = r" by blast
       from `extendRule S r = ([],\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>)` and `([], {# At i xs #} \<Rightarrow>* {# At i xs #}) = r`
       have "extend S ({# At i xs #} \<Rightarrow>* {# At i xs #}) = (\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>)"
          using extendRule_def[where R=r and forms=S] 
                extend_def[where forms=S and seq="{#At i xs#} \<Rightarrow>* {#At i xs#}"] by auto
       then have "At i xs :# \<Gamma> \<and> At i xs :# \<Delta>" 
            using extendID[where S=S and i=i and xs=xs and \<Gamma>="\<Gamma>\<oplus> F \<nabla> [x].A" and \<Delta>=\<Delta>] by auto
       then have "At i xs :# \<Gamma> + \<Gamma>' \<and> At i xs :# \<Delta> + \<Delta>'" by auto
       then have "(\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',0) \<in> derivable R*" using rules
            and containID[where \<Gamma>="\<Gamma> + \<Gamma>'" and i=i and \<Delta>="\<Delta> + \<Delta>'" and R=R] by auto
      }
      moreover
      {assume "r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3"
       then have "\<exists> Ps C. Ps \<noteq> [] \<and> r = (Ps,C)"
            proof-
            obtain y z where "r = (y,z)" by (cases r)
            with `r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3` have "(y,z) \<in> R1 \<or> (y,z) \<in> R2 \<or> (y,z) \<in> R3" by simp
            then have "y \<noteq> []"
                 proof-
                 {assume "(y,z) \<in> R1"
                  then have "(y,z) \<in> propRules" using rules by auto
                  then have "y\<noteq>[]" by (cases) auto
                 }
                 moreover
                 {assume "(y,z) \<in> R2"
                  then have "(y,z) \<in> nprovRules" using rules by auto
                  then have "y\<noteq>[]" by (cases) auto
                 }
                 moreover
                 {assume "(y,z) \<in> R3"
                  then have "(y,z) \<in> provRules" using rules by auto
                  then have "y\<noteq>[]" by (cases) auto
                 }
                 ultimately show "y \<noteq> []" using `(y,z) \<in> R1 \<or> (y,z) \<in> R2 \<or> (y,z) \<in> R3` by blast
                 qed
            then show "\<exists> Ps C. Ps \<noteq> [] \<and> r = (Ps,C)" using `r = (y,z)`  by blast
            qed
       then obtain Ps C where "Ps \<noteq> []" and "r = (Ps,C)" by auto
       moreover from `extendRule S r = ([], \<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>)` have "\<exists> 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 "(\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',0) \<in> derivable R*" using rules by simp
       }
       ultimately show "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" using `n=0` by blast
 next
     case (Suc n')
     then have "(\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>,n'+1) \<in> derivable R*" using a' by simp
     then obtain Ps where "(Ps, \<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>) \<in> R*" and 
                          "Ps \<noteq> []" and 
                       d':"\<forall> p \<in> set Ps. \<exists> n\<le>n'. (p,n) \<in> derivable R*"
          using characteriseLast[where C="\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>" and m=n' and R="R*"] by auto
     then have "\<exists> r S. (r \<in> idRules \<or> r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3) \<and> extendRule S r = (Ps, \<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>)"
          using rules 
            and ruleSet[where ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3 and R=R and Ps=Ps and C="\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>"] by auto
     then obtain r S where "r \<in> idRules \<or> r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3" 
                    and e':"extendRule S r = (Ps, \<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>)" by auto
     moreover
        {assume "r \<in> idRules"
         then have "\<exists> i xs. r = ([],{# At i xs #} \<Rightarrow>* {# At i xs #})" using characteriseID[where r=r] by auto
         moreover obtain z y where "r = (z,y)" by (cases r)
         then have "z \<noteq> []" using `Ps \<noteq> []` and `extendRule S r = (Ps, \<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>)`
                            and extendRule_def[where forms=S and R=r]
                            and extend_def[where forms=S and seq="snd r"] by auto
         ultimately have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*"
              using `r=(z,y)` by auto
        }
     moreover
        {assume "r \<in> R1"
         obtain ps c where "r = (ps,c)" by (cases r) auto
         then have "r \<in> propRules" using rules and `r \<in> R1` by auto
         then obtain T Ts where sw:"c = ({#} \<Rightarrow>* {# Cpd0 T Ts #}) \<or> c = ({# Cpd0 T Ts #} \<Rightarrow>* {#})"
              using propRuleCharacterise[where Ps=ps and C=c] and `r = (ps,c)` by auto
         have "(leftPrincipal r (F \<nabla> [x].A)) \<or> \<not>(leftPrincipal r (F \<nabla> [x].A))" by blast
         moreover
            {assume "leftPrincipal r (F \<nabla> [x].A)"
             then have "c = ({# F \<nabla> [x].A #} \<Rightarrow>* {#})" using `r=  (ps,c)` by (cases) auto
             with sw have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" by auto
            }
         moreover
            {assume "\<not> leftPrincipal r (F \<nabla> [x].A)"
             then have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> 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 \<Gamma>'=\<Gamma>' and \<Delta>'=\<Delta>' and ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3
                                                and S=S and Ps=Ps and \<Gamma>=\<Gamma> and \<Delta>=\<Delta> and n=n and n'=n']
                  and `n = Suc n'` and `Ps \<noteq> []` and a' and b' and e'
                  and c' and rules and IH and `r \<in> R1` and d' and `r = (ps,c)` by auto
            }
         ultimately have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" by blast         
        }
     moreover
        {assume "r \<in> R2"
         obtain ps c where "r = (ps,c)" by (cases r) auto
         then have "r \<in> nprovRules" using rules and `r \<in> R2` by auto
         have "leftPrincipal r (F \<nabla> [x].A) \<or> \<not> leftPrincipal r (F \<nabla> [x].A)" by blast
         moreover
            {assume "leftPrincipal r (F \<nabla> [x].A)"
             then have "(\<Gamma>' \<Rightarrow>* \<Delta>') \<in> set ps" using b' and `r = (ps,c)` and `r \<in> R2` and rules
                  by auto
             then have "extend S (\<Gamma>' \<Rightarrow>* \<Delta>') \<in> set Ps" using `extendRule S r = (Ps,\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>)`
                  and `r = (ps,c)` by (simp add:extendContain)
             moreover from `leftPrincipal r (F \<nabla> [x].A)` have "c = ({#F \<nabla> [x].A#} \<Rightarrow>* {#})" 
                  using `r = (ps,c)` by (cases) auto
             with `extendRule S r = (Ps,\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>)` have "S = (\<Gamma> \<Rightarrow>* \<Delta>)"
                  using `r = (ps,c)` apply (auto simp add:extendRule_def extend_def) by (cases S) auto
             ultimately have "(\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>') \<in> set Ps" by (simp add:extend_def)
             then have "\<exists> m\<le>n'. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*"
                  using `\<forall> p \<in> set Ps. \<exists> n\<le>n'. (p,n) \<in> derivable R*` by auto
             then have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" using `n = Suc n'`
                  by (auto,rule_tac x=m in exI) (simp)
            }
         moreover
            {assume "\<not> leftPrincipal r (F \<nabla> [x].A)"
             then have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> 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 \<Gamma>'=\<Gamma>' and \<Delta>'=\<Delta>' and ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3
                                                and S=S and Ps=Ps and \<Gamma>=\<Gamma> and \<Delta>=\<Delta> and n=n and n'=n']
                  and `n = Suc n'` and `Ps \<noteq> []` and a' and b' and e'
                  and c' and rules and IH and `r \<in> R2` and d' and `r = (ps,c)` by auto
            }
         ultimately have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" by blast
        }
     moreover
        {assume "r \<in> R3"
         obtain ps c where "r = (ps,c)" by (cases r) auto
         then have "r \<in> provRules" using rules and `r \<in> R3` by auto
         have "leftPrincipal r (F \<nabla> [x].A) \<or> \<not> leftPrincipal r (F \<nabla> [x].A)" by blast
         moreover
            {assume "leftPrincipal r (F \<nabla> [x].A)"
             then have "(\<Gamma>' \<Rightarrow>* \<Delta>') \<in> set ps" using b' and `r = (ps,c)` and `r \<in> R3` and rules
                  by auto
             then have "extend S (\<Gamma>' \<Rightarrow>* \<Delta>') \<in> set Ps" using `extendRule S r = (Ps,\<Gamma> \<oplus> F \<nabla> [x].A \<Rightarrow>* \<Delta>)`
                  and `r = (ps,c)` by (simp add:extendContain)
             moreover from `leftPrincipal r (F \<nabla> [x].A)` have "c = ({#F \<nabla> [x].A#} \<Rightarrow>* {#})" 
                  using `r = (ps,c)` by (cases) auto
             with `extendRule S r = (Ps,\<Gamma> \<oplus> F \<nabla> [x].A\<Rightarrow>* \<Delta>)` have "S = (\<Gamma> \<Rightarrow>* \<Delta>)"
                  using `r = (ps,c)` apply (auto simp add:extendRule_def extend_def) by (cases S) auto
             ultimately have "(\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>') \<in> set Ps" by (simp add:extend_def)
             then have "\<exists> m\<le>n'. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*"
                  using `\<forall> p \<in> set Ps. \<exists> n\<le>n'. (p,n) \<in> derivable R*` by auto
             then have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" using `n = Suc n'`
                  by (auto,rule_tac x=m in exI) (simp)
            }
         moreover
            {assume "\<not> leftPrincipal r (F \<nabla> [x].A)"
             then have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> 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 \<Gamma>'=\<Gamma>' and \<Delta>'=\<Delta>' and ?R1.0=R1 and ?R2.0=R2 and ?R3.0=R3
                                                and S=S and Ps=Ps and \<Gamma>=\<Gamma> and \<Delta>=\<Delta> and n=n and n'=n']
                  and `n = Suc n'` and `Ps \<noteq> []` and a' and b' and e'
                  and c' and rules and IH and `r \<in> R3` and d' and `r = (ps,c)` by auto
            }
         ultimately have "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" by blast
        }
     ultimately show "\<exists> m\<le>n. (\<Gamma> + \<Gamma>' \<Rightarrow>* \<Delta> + \<Delta>',m) \<in> derivable R*" by blast
   qed
qed


end