Theory Strong_Late_Axiomatisation

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Strong_Late_Axiomatisation
  imports Strong_Late_Expansion_Law
begin

lemma inputSuppPres:
  fixes P :: pi
  and   Q :: pi
  and   x :: name
  and   Rel  :: "(pi × pi) set"

  assumes PRelQ: "⋀y. y ∈ supp(P, Q, x) ⟹ (P[x::=y], Q[x::=y]) ∈ Rel"
  and     Eqvt: "eqvt Rel"

  shows "a<x>.P ↝[Rel] a<x>.Q"
proof -
  from Eqvt show ?thesis
  proof(induct rule: simCasesCont[where C="(x, a, Q, P)"])
    case(Bound b y Q')
    have "x ∈ supp(P, Q, x)" by(simp add: supp_prod supp_atm)
    with PRelQ have "(P, Q) ∈ Rel" by fastforce
    have QTrans: "a<x>.Q ⟼ b«y» ≺ Q'" by fact
    have "y ♯ (x, a, Q, P)" by fact
    hence "y ≠ a" and yineqx: "y ≠ x" and "y ♯ Q" and "y ♯ P" by(simp add: fresh_prod)+
    with QTrans show ?case
    proof(induct rule: inputCases)
      have "a<y>.([(x, y)] ∙ P) ⟼a<y> ≺ ([(x, y)] ∙ P)" by(rule Input)
      hence "a<x>.P ⟼a<y> ≺ ([(x, y)] ∙ P)" using ‹y ♯ P› by(simp add: alphaInput)
      moreover have "derivative ([(x, y)] ∙ P) ([(x, y)] ∙ Q) (InputS a) y Rel"
      proof(auto simp add: derivative_def)
        fix u
        have "x ∈ supp(P, Q, x)" by(simp add: supp_prod supp_atm)
        have "(P[x::=u], Q[x::=u]) ∈ Rel"
        proof(cases "u ∈ supp(P, Q, x)")
          case True
          with PRelQ show ?thesis by auto
        next
          case False
          hence "u ♯ P" and "u ♯ Q" by(auto simp add: fresh_def supp_prod)
          moreover from ‹eqvt Rel› ‹(P, Q) ∈ Rel› have "([(x, u)] ∙ P, [(x, u)] ∙ Q) ∈ Rel"
            by(rule eqvtRelI)
          ultimately show ?thesis by(simp only: injPermSubst)
        qed
        with ‹y ♯ P› ‹y ♯ Q› show "(([(x, y)] ∙ P)[y::=u], ([(x, y)] ∙ Q)[y::=u]) ∈ Rel"
          by(simp add: renaming)
      qed
      ultimately show "∃P'. a<x>.P ⟼ a<y> ≺ P' ∧ derivative P' ([(x, y)] ∙ Q) (InputS a) y Rel"
        by blast
    qed
  next
    case(Free α Q')
    have "a<x>.Q ⟼ α ≺ Q'" by fact
    hence False by auto
    thus ?case by blast
  qed
qed

lemma inputSuppPresBisim:
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  assumes PSimQ: "⋀y. y ∈ supp(P, Q, x) ⟹ P[x::=y] ∼ Q[x::=y]"

  shows "a<x>.P ∼ a<x>.Q"
proof -
  let ?X = "{(a<x>.P, a<x>.Q) | a x P Q. ∀y ∈ supp(P, Q, x). P[x::=y] ∼ Q[x::=y]}"
  have "eqvt ?X"
    apply(auto simp add: eqvt_def)
    apply(rule_tac x="perm ∙ aa" in exI)
    apply(rule_tac x="perm ∙ x" in exI)
    apply(rule_tac x="perm ∙ P" in exI)
    apply auto
    apply(rule_tac x="perm ∙ Q" in exI)
    apply auto
    apply(drule_tac pi="rev perm" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
    apply(simp add: eqvts pt_rev_pi[OF pt_name_inst, OF at_name_inst])
    apply(erule_tac x="rev perm ∙ y" in ballE)
    apply auto
    apply(drule_tac p=perm in bisimClosed)
    by(simp add: eqvts pt_pi_rev[OF pt_name_inst, OF at_name_inst])
  from assms have "(a<x>.P, a<x>.Q) ∈ ?X" by fastforce
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cSim P Q)
    thus ?case using ‹eqvt ?X›
      by(fastforce intro: inputSuppPres)
  next
    case(cSym P Q)
    thus ?case by(fastforce simp add: supp_prod dest: symmetric)
  qed
qed

inductive equiv :: "pi ⇒ pi ⇒ bool" (infixr ‹≡⇩e› 80)
where
  Refl:              "P ≡⇩e P"
| Sym:               "P ≡⇩e Q ⟹ Q ≡⇩e P"
| Trans:             "⟦P ≡⇩e Q; Q ≡⇩e R⟧ ⟹ P ≡⇩e R"

| Match:             "[a⌢a]P ≡⇩e P"
| Match':            "a ≠ b ⟹ [a⌢b]P ≡⇩e 𝟬"

| Mismatch:         "a ≠ b ⟹ [a≠b]P ≡⇩e P"
| Mismatch':        "[a≠a]P ≡⇩e 𝟬"
 
| SumSym:            "P ⊕ Q ≡⇩e Q ⊕ P"
| SumAssoc:          "(P ⊕ Q) ⊕ R ≡⇩e P ⊕ (Q ⊕ R)"
| SumZero:           "P ⊕ 𝟬 ≡⇩e P"
| SumIdemp:          "P ⊕ P ≡⇩e P"
| SumRes:            "<νx>(P ⊕ Q) ≡⇩e (<νx>P) ⊕ (<νx>Q)"

| ResNil:            "<νx>𝟬 ≡⇩e 𝟬"
| ResInput:          "⟦x ≠ a; x ≠ y⟧ ⟹ <νx>a<y>.P ≡⇩e a<y>.(<νx>P)"
| ResInput':         "<νx>x<y>.P ≡⇩e 𝟬"
| ResOutput:         "⟦x ≠ a; x ≠ b⟧ ⟹ <νx>a{b}.P ≡⇩e a{b}.(<νx>P)"
| ResOutput':        "<νx>x{b}.P ≡⇩e 𝟬"
| ResTau:            "<νx>τ.(P) ≡⇩e τ.(<νx>P)"
| ResComm:           "<νx><νy>P ≡⇩e <νy><νx>P"
| ResFresh:          "x ♯ P ⟹ <νx>P ≡⇩e P"

| Expand:            "⟦(R, expandSet P Q) ∈ sumComposeSet; hnf P; hnf Q⟧ ⟹ P ∥ Q ≡⇩e R"

| SumPres:           "P ≡⇩e Q ⟹ P ⊕ R ≡⇩e Q ⊕ R" 
| ParPres:           "⟦P ≡⇩e P'; Q ≡⇩e Q'⟧ ⟹ P ∥ Q ≡⇩e P' ∥ Q'"
| ResPres:           "P ≡⇩e Q ⟹ <νx>P ≡⇩e <νx>Q"
| TauPres:           "P ≡⇩e Q ⟹ τ.(P) ≡⇩e τ.(Q)"
| OutputPres:        "P ≡⇩e Q ⟹ a{b}.P ≡⇩e a{b}.Q"
| InputPres:         "⟦∀y ∈ supp(P, Q, x). P[x::=y] ≡⇩e Q[x::=y]⟧ ⟹ a<x>.P ≡⇩e a<x>.Q"

lemma SumIdemp':
  fixes P  :: pi
  and   P' :: pi

  assumes "P ≡⇩e P'"

  shows "P ⊕ P' ≡⇩e P"
proof -
  have "P ≡⇩e P ⊕ P" by(blast intro: Sym SumIdemp)
  moreover from assms have "P ⊕ P ≡⇩e P' ⊕ P" by(rule SumPres)
  moreover have "P' ⊕ P ≡⇩e P ⊕ P'" by(rule SumSym)
  ultimately have "P ≡⇩e P ⊕ P'" by(blast intro: Trans)
  thus ?thesis by(rule Sym)
qed

lemma SumPres':
  fixes P  :: pi
  and   P' :: pi
  and   Q  :: pi
  and   Q' :: pi

  assumes PeqP': "P ≡⇩e P'"
  and     QeqQ': "Q ≡⇩e Q'"

  shows "P ⊕ Q ≡⇩e P' ⊕ Q'"
proof -
  from PeqP' have "P ⊕ Q ≡⇩e P' ⊕ Q" by(rule SumPres)
  moreover have "P' ⊕ Q ≡⇩e Q ⊕ P'" by(rule SumSym)
  moreover from QeqQ' have "Q ⊕ P' ≡⇩e Q' ⊕ P'" by(rule SumPres)
  moreover have "Q' ⊕ P' ≡⇩e P' ⊕ Q'" by(rule SumSym)
  ultimately show ?thesis by(blast intro: Trans)
qed
(*
lemma ParComm:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  assumes "(R, expandSet P Q) ∈ sumComposeSet"

  obtains R' where "(R, expandSet Q P) ∈ sumComposeSet" and "R ≡⇩e R'"
using assms
apply(induct S=="expandSet P Q" rule: sumComposeSet.induct)
apply auto
apply(simp add: expandSet_def)
apply fastforce
apply auto
apply(clarify)
*)
lemma sound:
  fixes P :: pi
  and   Q :: pi

  assumes "P ≡⇩e Q"

  shows "P ∼ Q"
using assms
proof(induct)
  case(Refl P)
  show ?case by(rule reflexive)
next
  case(Sym P Q)
  have "P ∼ Q" by fact
  thus ?case by(rule symmetric)
next
  case(Trans P Q R)
  have "P ∼ Q" and "Q ∼ R" by fact+
  thus ?case by(rule transitive)
next
  case(Match a P)
  show ?case by(rule matchId)
next
  case(Match' a b P)
  have "a ≠ b" by fact
  thus ?case by(rule matchNil)
next
  case(Mismatch a b P)
  have "a ≠ b" by fact
  thus ?case by(rule mismatchId)
next
  case(Mismatch' a P)
  show ?case by(rule mismatchNil)
next
  case(SumSym P Q)
  show ?case by(rule sumSym)
next
  case(SumAssoc P Q R)
  show ?case by(rule sumAssoc)
next
  case(SumZero P)
  show ?case by(rule sumZero)
next
  case(SumIdemp P)
  show ?case by(rule sumIdemp)
next
  case(SumRes x P Q)
  show ?case by(rule sumRes)
next
  case(ResNil x)
  show ?case by(rule nilRes)
next
  case(ResInput x a y P)
  have "x ≠ a" and "x ≠ y" by fact+
  thus ?case by(rule resInput)
next
  case(ResInput' x y P)
  show ?case by(rule resNil)
next
  case(ResOutput x a b P)
  have "x ≠ a" and "x ≠ b" by fact+
  thus ?case by(rule resOutput)
next
  case(ResOutput' x b P)
  show ?case by(rule resNil)
next
  case(ResTau x P)
  show ?case by(rule resTau)
next
  case(ResComm x P)
  show ?case by(rule resComm)
next
  case(ResFresh x P)
  have "x ♯ P" by fact
  thus ?case by(rule scopeFresh)
next
  case(Expand R P Q)
  have "(R, expandSet P Q) ∈ sumComposeSet" and "hnf P" and "hnf Q" by fact+
  thus ?case by(rule expandSC)
next
  case(SumPres P Q R)
  from ‹P ∼ Q› show ?case by(rule sumPres)
next
  case(ParPres P P' Q Q')
  have "P ∼ P'" and "Q ∼ Q'" by fact+
  thus ?case by(metis transitive symmetric parPres parSym)
next
  case(ResPres P Q x)
  from ‹P ∼ Q› show ?case by(rule resPres)
next
  case(TauPres P Q)
  from ‹P ∼ Q› show ?case by(rule tauPres)
next
  case(OutputPres P Q a b)
  from ‹P ∼ Q› show ?case by(rule outputPres)
next
  case(InputPres P Q x a)
  have "∀y ∈ supp(P, Q, x). P[x::=y] ≡⇩e Q[x::=y] ∧ P[x::=y] ∼ Q[x::=y]" by fact
  hence "∀y ∈ supp(P, Q, x). P[x::=y] ∼ Q[x::=y]" by blast
  thus ?case by(rule_tac inputSuppPresBisim) auto
qed

lemma zeroDest[dest]:
  fixes a :: name
  and   b :: name
  and   x :: name
  and   P :: pi

  shows "(a{b}.P) ≡⇩e 𝟬 ⟹ False"
  and   "(a<x>.P) ≡⇩e 𝟬 ⟹ False"
  and   "(τ.(P)) ≡⇩e 𝟬 ⟹ False"

  and   "𝟬 ≡⇩e a{b}.P ⟹ False"
  and   "𝟬 ≡⇩e a<x>.P ⟹ False"
  and   "𝟬 ≡⇩e τ.(P) ⟹ False"
by(auto dest: sound)

lemma eq_eqvt:
  fixes pi::"name prm"
  and   x::"'a::pt_name"
  shows "pi∙(x=y) = ((pi∙x)=(pi∙y))"
by(simp add: perm_bool perm_bij)
    
nominal_primrec "depth" :: "pi ⇒ nat" where
  "depth 𝟬 = 0"
| "depth (τ.(P)) = 1 + (depth P)"
| "a ♯ x ⟹ depth (a<x>.P) = 1 + (depth P)"
| "depth (a{b}.P) = 1 + (depth P)"
| "depth ([a⌢b]P) = (depth P)"
| "depth ([a≠b]P) = (depth P)"
| "depth (P ⊕ Q) = max (depth P) (depth Q)"
| "depth (P ∥ Q) = ((depth P) + (depth Q))"
| "depth (<νx>P) = (depth P)"
| "depth (!P) = (depth P)"
apply(auto simp add: fresh_nat)
apply(finite_guess)+
by(fresh_guess)+

lemma depthEqvt[simp]:
  fixes P :: pi
  and   p :: "name prm"
  
  shows "depth(p ∙ P) = depth P"
by(nominal_induct P rule: pi.strong_induct, auto simp add: name_bij)

lemma depthInput[simp]:
  fixes a :: name
  and   x :: name
  and   P :: pi

  shows "depth (a<x>.P) = 1 + (depth P)"
proof -
  obtain y where yineqa: "y ≠ a" and yFreshP: "y ♯ P"
    by(force intro: name_exists_fresh[of "(a, P)"] simp add: fresh_prod)
  from yFreshP have "a<x>.P = a<y>.([(x, y)] ∙ P)" by(simp add: alphaInput)
  with yineqa show ?thesis by simp
qed

nominal_primrec "valid" :: "pi ⇒ bool" where
  "valid 𝟬 = True"
| "valid (τ.(P)) = valid P"
| "x ♯ a ⟹ valid (a<x>.P) = valid P"
| "valid (a{b}.P) = valid P"
| "valid ([a⌢b]P) = valid P"
| "valid ([a≠b]P) = valid P"
| "valid (P ⊕ Q) = ((valid P) ∧ (valid Q))"
| "valid (P ∥ Q) = ((valid P) ∧ (valid Q))"
| "valid (<νx>P) = valid P"
| "valid (!P) = False"
apply(auto simp add: fresh_bool)
apply(finite_guess)+
by(fresh_guess)+

lemma validEqvt[simp]:
  fixes P :: pi
  and   p :: "name prm"
  
  shows "valid(p ∙ P) = valid P"
by(nominal_induct P rule: pi.strong_induct, auto simp add: name_bij)

lemma validInput[simp]:
  fixes a :: name
  and   x :: name
  and   P :: pi

  shows "valid (a<x>.P) = valid P"
proof -
  obtain y where yineqa: "y ≠ a" and yFreshP: "y ♯ P"
    by(force intro: name_exists_fresh[of "(a, P)"] simp add: fresh_prod)
  from yFreshP have "a<x>.P = a<y>.([(x, y)] ∙ P)" by(simp add: alphaInput)
  with yineqa show ?thesis by simp
qed

lemma depthMin[intro]:
  fixes P

  shows "0 ≤ depth P"
by(induct P rule: pi.induct, auto)

lemma hnfTransition:
  fixes P :: pi

  assumes "hnf P"
  and     "P ≠ 𝟬"

  shows "∃Rs. P ⟼ Rs"
using assms
by(induct rule: pi.induct, auto intro: Output Tau Input Sum1 Open)

definition "uhnf" :: "pi ⇒ bool" where
  "uhnf P ≡ hnf P ∧ (∀R ∈ summands P. ∀R' ∈ summands P. R ≠ R' ⟶ ¬(R ≡⇩e R'))"

lemma summandsIdemp:
  fixes P :: pi
  and   Q :: pi

  assumes "Q ∈ summands P"
  and     "Q ≡⇩e Q'"
  
  shows "P ⊕ Q' ≡⇩e P"
using assms
proof(nominal_induct P arbitrary: Q rule: pi.strong_inducts)
  case(PiNil Q)
  have "Q ∈ summands 𝟬" by fact
  hence False by simp
  thus ?case by simp
next
  case(Output a b P Q)
  have "Q ≡⇩e Q'" by fact
  hence "a{b}.P ⊕ Q' ≡⇩e a{b}.P ⊕ Q" by(blast intro: SumPres' Refl Sym)
  moreover have "Q = a{b}.P"
  proof  -
    have "Q ∈ summands (a{b}.P)" by fact
    thus ?thesis by simp
  qed
  ultimately show ?case by(blast intro: SumIdemp Trans)
next
  case(Tau P Q)
  have "Q ≡⇩e Q'" by fact
  hence "τ.(P) ⊕ Q' ≡⇩e τ.(P) ⊕ Q" by(blast intro: SumPres' Refl Sym)
  moreover have "Q = τ.(P)"
  proof  -
    have "Q ∈ summands (τ.(P))" by fact
    thus ?thesis by simp
  qed
  ultimately show ?case by(blast intro: SumIdemp Trans)
next
  case(Input a x P Q)
  have "Q ≡⇩e Q'" by fact
  hence "a<x>.P ⊕ Q' ≡⇩e a<x>.P ⊕ Q" by(blast intro: SumPres' Refl Sym)
  moreover have "Q = a<x>.P"
  proof  -
    have "Q ∈ summands (a<x>.P)" by fact
    thus ?thesis by simp
  qed
  ultimately show ?case by(blast intro: SumIdemp Trans)
next
  case(Match a b P Q)
  have "Q ∈ summands ([a⌢b]P)" by fact
  hence False by simp
  thus ?case by simp
next
  case(Mismatch a b P Q)
  have "Q ∈ summands ([a≠b]P)" by fact
  hence False by simp
  thus ?case by simp
next
  case(Sum P Q R)
  have IHP: "⋀P'. ⟦P' ∈ summands P; P' ≡⇩e Q'⟧ ⟹ P ⊕ Q' ≡⇩e P" by fact
  have IHQ: "⋀Q''. ⟦Q'' ∈ summands Q; Q'' ≡⇩e Q'⟧ ⟹ Q ⊕ Q' ≡⇩e Q" by fact
  have ReqQ': "R ≡⇩e Q'" by fact
  have "R ∈ summands(P ⊕ Q)" by fact
  hence "R ∈ summands P ∨ R ∈ summands Q" by simp
  thus ?case
  proof(rule disjE)
    assume "R ∈ summands P"
    hence PQ'eqP: "P ⊕ Q' ≡⇩e P" using ReqQ' by(rule IHP)
    
    have "(P ⊕ Q) ⊕ Q' ≡⇩e P ⊕ (Q ⊕ Q')" by(rule SumAssoc)
    moreover have "P ⊕ (Q ⊕ Q') ≡⇩e P ⊕ (Q' ⊕ Q)" by(blast intro: Refl SumSym SumPres')
    moreover have "P ⊕ (Q' ⊕ Q) ≡⇩e (P ⊕ Q') ⊕ Q" by(blast intro: SumAssoc Sym)
    moreover from PQ'eqP have "(P ⊕ Q') ⊕ Q ≡⇩e P ⊕ Q" by(blast intro: SumPres' Refl)
    ultimately show ?case by(blast intro: Trans)
  next
    assume "R ∈ summands Q"
    hence QQ'eqQ: "Q ⊕ Q' ≡⇩e Q" using ReqQ' by(rule IHQ)
    
    have "(P ⊕ Q) ⊕ Q' ≡⇩e P ⊕ (Q ⊕ Q')" by(rule SumAssoc)
    moreover from QQ'eqQ have "P ⊕ (Q ⊕ Q') ≡⇩e P ⊕ Q" by(blast intro: Refl SumPres')
    ultimately show ?case by(rule Trans)
  qed
next
  case(Par P Q R)
  have "R ∈ summands (P ∥ Q)" by fact
  hence False by simp
  thus ?case by simp
next
  case(Res x P Q)
  have "Q ≡⇩e Q'" by fact
  hence "(<νx>P) ⊕ Q' ≡⇩e (<νx>P) ⊕ Q" by(blast intro: SumPres' Refl Sym)
  moreover have "Q = <νx>P"
  proof  -
    have "Q ∈ summands (<νx>P)" by fact
    thus ?thesis by(auto simp add: if_split)
  qed
  ultimately show ?case by(blast intro: SumIdemp Trans)
next
  case(Bang P Q)
  have "Q ∈ summands(!P)" by fact
  hence False by simp
  thus ?case by simp
qed

lemma uhnfSum:
  fixes P :: pi
  and   Q :: pi

  assumes Phnf: "uhnf P"
  and     Qhnf: "uhnf Q"
  and     validP: "valid P"
  and     validQ: "valid Q"

  shows "∃R. uhnf R ∧ valid R ∧ P ⊕ Q ≡⇩e R ∧ (depth R) ≤ (depth (P ⊕ Q))"
using assms
proof(nominal_induct P arbitrary: Q rule: pi.strong_inducts)
  case(PiNil Q)
  have "uhnf Q" by fact
  moreover have "valid Q" by fact
  moreover have "𝟬 ⊕ Q ≡⇩e Q" by(blast intro: SumZero SumSym Trans)
  moreover have "depth Q ≤ depth(𝟬 ⊕ Q)" by auto
  ultimately show ?case by blast
next
  case(Output a b P Q)
  show ?case
  proof(case_tac "Q = 𝟬")
    assume "Q = 𝟬"
    moreover have "uhnf (a{b}.P)" by(simp add: uhnf_def)
    moreover have "valid (a{b}.P)" by fact
    moreover have "a{b}.P ⊕ 𝟬 ≡⇩e a{b}.P" by(rule SumZero)
    moreover have "depth(a{b}.P) ≤ depth(a{b}.P ⊕ 𝟬)" by simp
    ultimately show ?case by blast
  next
    assume QineqNil: "Q ≠ 𝟬" 
    have Qhnf: "uhnf Q" by fact
    have validQ: "valid Q" by fact
    have validP: "valid(a{b}.P)" by fact
    show ?case
    proof(case_tac "∃Q' ∈ summands Q. Q' ≡⇩e a{b}.P")
      assume "∃Q' ∈ summands Q. Q' ≡⇩e a{b}.P"
      then obtain Q' where "Q' ∈ summands Q" and "Q' ≡⇩e a{b}.P" by blast
      hence "Q ⊕ a{b}.P ≡⇩e Q" by(rule summandsIdemp)
      moreover have "depth Q ≤ depth(Q ⊕ a{b}.P)" by simp
      ultimately show ?case using Qhnf validQ by(force intro: SumSym Trans)
    next
      assume "¬(∃Q' ∈ summands Q. Q' ≡⇩e a{b}.P)"
      hence "∀Q' ∈ summands Q. ¬(Q' ≡⇩e a{b}.P)" by simp
      with Qhnf QineqNil have "uhnf (a{b}.P ⊕ Q)"
        by(force dest: Sym simp add: uhnf_def)
      moreover from validQ validP have "valid(a{b}.P ⊕ Q)"  by simp
      moreover have "a{b}.P ⊕ Q ≡⇩e a{b}.P ⊕ Q" by(rule Refl)
      moreover have "depth(a{b}.P ⊕ Q) ≤ depth(a{b}.P ⊕ Q)" by simp
      ultimately show ?case by blast
    qed
  qed
next
  case(Tau P Q)
  show ?case
  proof(case_tac "Q = 𝟬")
    assume "Q = 𝟬"
    moreover have "uhnf (τ.(P))" by(simp add: uhnf_def)
    moreover have "valid (τ.(P))" by fact
    moreover have "τ.(P) ⊕ 𝟬 ≡⇩e τ.(P)" by(rule SumZero)
    moreover have "depth(τ.(P)) ≤ depth(τ.(P) ⊕ 𝟬)" by simp
    ultimately show ?case by blast
  next
    assume QineqNil: "Q ≠ 𝟬" 
    have Qhnf: "uhnf Q" by fact
    have validP: "valid(τ.(P))" and validQ: "valid Q" by fact+
    show ?case
    proof(case_tac "∃Q' ∈ summands Q. Q' ≡⇩e τ.(P)")
      assume "∃Q' ∈ summands Q. Q' ≡⇩e τ.(P)"
      then obtain Q' where "Q' ∈ summands Q" and "Q' ≡⇩e τ.(P)" by blast
      hence "Q ⊕ τ.(P) ≡⇩e Q" by(rule summandsIdemp)
      moreover have "depth Q ≤ depth(Q ⊕ τ.(P))" by simp
      ultimately show ?case using Qhnf validQ by(force intro: SumSym Trans)
    next
      assume "¬(∃Q' ∈ summands Q. Q' ≡⇩e τ.(P))"
      hence "∀Q' ∈ summands Q. ¬(Q' ≡⇩e τ.(P))" by simp
      with Qhnf QineqNil have "uhnf (τ.(P) ⊕ Q)"
        by(force dest: Sym simp add: uhnf_def)
      moreover from validP validQ have "valid(τ.(P) ⊕ Q)" by simp
      moreover have "τ.(P) ⊕ Q ≡⇩e τ.(P) ⊕ Q" by(rule Refl)
      moreover have "depth(τ.(P) ⊕ Q) ≤ depth(τ.(P) ⊕ Q)" by simp
      ultimately show ?case by blast
    qed
  qed
next
  case(Input a x P Q)
  show ?case
  proof(case_tac "Q = 𝟬")
    assume "Q = 𝟬"
    moreover have "uhnf (a<x>.P)" by(simp add: uhnf_def)
    moreover have "valid (a<x>.P)" by fact
    moreover have "a<x>.P ⊕ 𝟬 ≡⇩e a<x>.P" by(rule SumZero)
    moreover have "depth(a<x>.P) ≤ depth(a<x>.P ⊕ 𝟬)" by simp
    ultimately show ?case by blast
  next
    assume QineqNil: "Q ≠ 𝟬" 
    have validP: "valid(a<x>.P)" and validQ: "valid Q" by fact+
    have Qhnf: "uhnf Q" by fact
    show ?case
    proof(case_tac "∃Q' ∈ summands Q. Q' ≡⇩e a<x>.P")
      assume "∃Q' ∈ summands Q. Q' ≡⇩e a<x>.P"
      then obtain Q' where "Q' ∈ summands Q" and "Q' ≡⇩e a<x>.P" by blast
      hence "Q ⊕ a<x>.P ≡⇩e Q" by(rule summandsIdemp)
      moreover have "depth Q ≤ depth(Q ⊕ a<x>.P)" by simp
      ultimately show ?case using Qhnf validQ by(force intro: SumSym Trans)
    next
      assume "¬(∃Q' ∈ summands Q. Q' ≡⇩e a<x>.P)"
      hence "∀Q' ∈ summands Q. ¬(Q' ≡⇩e a<x>.P)" by simp
      with Qhnf QineqNil have "uhnf (a<x>.P ⊕ Q)"
        by(force dest: Sym simp add: uhnf_def)
      moreover from validP validQ have "valid(a<x>.P ⊕ Q)" by simp
      moreover have "a<x>.P ⊕ Q ≡⇩e a<x>.P ⊕ Q" by(rule Refl)
      moreover have "depth(a<x>.P ⊕ Q) ≤ depth(a<x>.P ⊕ Q)" by simp
      ultimately show ?case by blast
    qed
  qed
next
  case(Match a b P Q)
  have "uhnf ([a⌢b]P)" by fact
  hence False by(simp add: uhnf_def)
  thus ?case by simp
next
  case(Mismatch a b P Q)
  have "uhnf ([a≠b]P)" by fact
  hence False by(simp add: uhnf_def)
  thus ?case by simp
next
  case(Sum P Q R)
  have Rhnf: "uhnf R" by fact
  have validR: "valid R" by fact
  have PQhnf: "uhnf (P ⊕ Q)" by fact
  have validPQ: "valid(P ⊕ Q)" by fact
  have "∃T. uhnf T ∧ valid T ∧ Q ⊕ R ≡⇩e T ∧ depth T ≤ depth (Q ⊕ R)"
  proof -
    from PQhnf have "uhnf Q" by(simp add: uhnf_def)
    moreover from validPQ have "valid Q" by simp+
    moreover have "⋀R. ⟦uhnf Q; uhnf R; valid Q; valid R⟧ ⟹ ∃T. uhnf T ∧ valid T ∧ Q ⊕ R ≡⇩e T ∧ depth T ≤ depth(Q ⊕ R)" by fact
    ultimately show ?thesis using Rhnf validR by blast
  qed
  then obtain T where Thnf: "uhnf T" and QReqT: "Q ⊕ R ≡⇩e T" and validT: "valid T"
                  and Tdepth: "depth T ≤ depth(Q ⊕ R)" by blast
  
  have "∃S. uhnf S ∧ valid S ∧ P ⊕ T ≡⇩e S ∧ depth S ≤ depth(P ⊕ T)"
  proof -
    from PQhnf have "uhnf P" by(simp add: uhnf_def)
    moreover from validPQ have "valid P" by simp
    moreover have "⋀T. ⟦uhnf P; uhnf T; valid P; valid T⟧ ⟹ ∃S. uhnf S ∧ valid S ∧ P ⊕ T ≡⇩e S ∧ depth S ≤ depth(P ⊕ T)" by fact
    ultimately show ?thesis using Thnf validT by blast
  qed
  then obtain S where Shnf: "uhnf S" and PTeqS: "P ⊕ T ≡⇩e S" and validS: "valid S"
                  and Sdepth: "depth S ≤ depth(P ⊕ T)" by blast
    
  have "(P ⊕ Q) ⊕ R ≡⇩e S"
  proof -
    have "(P ⊕ Q) ⊕ R ≡⇩e P ⊕ (Q ⊕ R)" by(rule SumAssoc)
    moreover from QReqT have "P ⊕ (Q ⊕ R) ≡⇩e P ⊕ T"
      by(blast intro: Refl SumPres')
    ultimately show ?thesis using PTeqS by(blast intro: Trans)
  qed
  moreover from Tdepth Sdepth have "depth S ≤ depth((P ⊕ Q) ⊕ R)" by auto
  
  ultimately show ?case using Shnf validS by blast
next
  case(Par P Q R)
  have "uhnf (P ∥ Q)" by fact
  hence False by(simp add: uhnf_def)
  thus ?case by simp
next
  case(Res x P Q)
  show ?case
  proof(case_tac "Q = 𝟬")
    assume "Q = 𝟬"
    moreover have "uhnf (<νx>P)" by fact
    moreover have "valid (<νx>P)" by fact
    moreover have "<νx>P ⊕ 𝟬 ≡⇩e <νx>P" by(rule SumZero)
    moreover have "depth(<νx>P) ≤ depth((<νx>P) ⊕ 𝟬)" by simp
    ultimately show ?case by blast
  next
    assume QineqNil: "Q ≠ 𝟬" 
    have Qhnf: "uhnf Q" by fact
    have validP: "valid(<νx>P)" and validQ: "valid Q" by fact+
    show ?case
    proof(case_tac "∃Q' ∈ summands Q. Q' ≡⇩e <νx>P")
      assume "∃Q' ∈ summands Q. Q' ≡⇩e <νx>P"
      then obtain Q' where "Q' ∈ summands Q" and "Q' ≡⇩e <νx>P" by blast
      hence "Q ⊕ <νx>P ≡⇩e Q" by(rule summandsIdemp)
      moreover have "depth Q ≤ depth(Q ⊕ <νx>P)" by simp
      ultimately show ?case using Qhnf validQ by(force intro: SumSym Trans)
    next
      assume "¬(∃Q' ∈ summands Q. Q' ≡⇩e <νx>P)"
      hence "∀Q' ∈ summands Q. ¬(Q' ≡⇩e <νx>P)" by simp
      moreover have "uhnf (<νx>P)" by fact
      ultimately have "uhnf (<νx>P ⊕ Q)" using Qhnf QineqNil 
        by(force dest: Sym simp add: uhnf_def)
      moreover from validP validQ have "valid(<νx>P ⊕ Q)" by simp
      moreover have "(<νx>P) ⊕ Q ≡⇩e (<νx>P) ⊕ Q" by(rule Refl)
      moreover have "depth((<νx>P) ⊕ Q) ≤ depth((<νx>P) ⊕ Q)" by simp
      ultimately show ?case by blast
    qed
  qed
next
  case(Bang P Q)
  have "uhnf (!P)" by fact
  hence False by(simp add: uhnf_def)
  thus ?case by simp
qed

lemma uhnfRes:
  fixes x :: name
  and   P :: pi

  assumes Phnf: "uhnf P"
  and     validP: "valid P"

  shows "∃P'. uhnf P' ∧ valid P' ∧ <νx>P ≡⇩e P' ∧ depth P' ≤ depth(<νx>P)"
using assms
proof(nominal_induct P avoiding: x rule: pi.strong_inducts)
  case(PiNil x)
  have "uhnf 𝟬" by(simp add: uhnf_def)
  moreover have "valid 𝟬" by simp
  moreover have "<νx>𝟬 ≡⇩e 𝟬" by(rule ResNil)
  moreover have "depth 𝟬 ≤ depth(<νx>𝟬)" by simp
  ultimately show ?case by blast
next
  case(Output a b P)
  have "valid(a{b}.P)" by fact
  hence validP: "valid P" by simp
  show ?case
  proof(case_tac "x=a")
    assume "x = a"
    moreover have "uhnf 𝟬" by(simp add: uhnf_def)
    moreover have "valid 𝟬" by simp
    moreover have "𝟬 ≡⇩e <νx>x{b}.P" by(blast intro: ResOutput' Sym)
    moreover have "depth 𝟬 ≤ depth(<νx>x{b}.P)" by simp
    ultimately show ?case by(blast intro: Sym)
  next
    assume xineqa: "x ≠ a"
    show ?case
    proof(case_tac "x=b")
      assume "x=b"
      moreover from xineqa have "uhnf(<νx>a{x}.P)" by(force simp add: uhnf_def)
      moreover from validP have "valid(<νx>a{x}.P)" by simp
      moreover have "<νx>a{x}.P ≡⇩e <νx>a{x}.P" by(rule Refl)
      moreover have "depth(<νx>a{x}.P) ≤ depth(<νx>a{x}.P)" by simp
      ultimately show ?case by blast
    next
      assume xineqb: "x ≠ b"
      have "uhnf(a{b}.(<νx>P))" by(simp add: uhnf_def)
      moreover from validP have "valid(a{b}.(<νx>P))" by simp
      moreover from xineqa xineqb have "a{b}.(<νx>P) ≡⇩e <νx>a{b}.P" by(blast intro: ResOutput Sym)
      moreover have "depth(a{b}.(<νx>P)) ≤ depth(<νx>a{b}.P)" by simp
      ultimately show ?case by(blast intro: Sym)
    qed
  qed
next
  case(Tau P)
  have "valid(τ.(P))" by fact
  hence validP: "valid P" by simp
  
  have "uhnf(τ.(<νx>P))" by(simp add: uhnf_def)
  moreover from validP have "valid(τ.(<νx>P))" by simp
  moreover have "τ.(<νx>P) ≡⇩e <νx>τ.(P)" by(blast intro: ResTau Sym)
  moreover have "depth(τ.(<νx>P)) ≤ depth(<νx>τ.(P))" by simp
  ultimately show ?case by(blast intro: Sym)
next
  case(Input a y P x)
  have "valid(a<y>.P)" by fact
  hence validP: "valid P" by simp
  have "y ♯ x" by fact hence yineqx: "y ≠ x" by simp
  show ?case
  proof(case_tac "x=a")
    assume "x = a"
    moreover have "uhnf 𝟬" by(simp add: uhnf_def)
    moreover have "valid 𝟬" by simp
    moreover have "𝟬 ≡⇩e <νx>x<y>.P" by(blast intro: ResInput' Sym)
    moreover have "depth 𝟬 ≤ depth(<νx>x<y>.P)" by simp
    ultimately show ?case by(blast intro: Sym)
  next
    assume xineqa: "x ≠ a"
    have "uhnf(a<y>.(<νx>P))" by(simp add: uhnf_def)
    moreover from validP have "valid(a<y>.(<νx>P))" by simp
    moreover from xineqa yineqx have "a<y>.(<νx>P) ≡⇩e <νx>a<y>.P" by(blast intro: ResInput Sym)
    moreover have "depth(a<y>.(<νx>P)) ≤ depth(<νx>a<y>.P)" by simp
    ultimately show ?case by(blast intro: Sym)
  qed
next
  case(Match a b P x)
  have "uhnf([a⌢b]P)" by fact
  hence False by(simp add: uhnf_def)
  thus ?case by simp
next
  case(Mismatch a b P x)
  have "uhnf([a≠b]P)" by fact
  hence False by(simp add: uhnf_def)
  thus ?case by simp
next
  case(Sum P Q x)
  have "valid(P ⊕ Q)" by fact
  hence validP: "valid P" and validQ: "valid Q" by simp+
  have "uhnf(P ⊕ Q)" by fact
  hence Phnf: "uhnf P" and Qhnf: "uhnf Q" by(auto simp add: uhnf_def)
  
  have "∃P'. uhnf P' ∧ valid P' ∧ P' ≡⇩e <νx>P ∧ (depth P') ≤ (depth(<νx>P))"
  proof -
    have "⟦uhnf P; valid P⟧ ⟹ ∃P'. uhnf P' ∧ valid P' ∧ <νx>P ≡⇩e P' ∧ (depth P') ≤ (depth (<νx>P))" by fact
    with validP Phnf show ?thesis by(blast intro: Sym)
  qed
  then obtain P' where P'hnf: "uhnf P'" and P'eqP: "P' ≡⇩e <νx>P" and validP': "valid P'"
                   and P'depth: "(depth P') ≤ (depth(<νx>P))" by blast

  have "∃Q'. uhnf Q' ∧ valid Q' ∧ Q' ≡⇩e <νx>Q ∧ (depth Q') ≤ (depth(<νx>Q))"
  proof -
    have "⟦uhnf Q; valid Q⟧ ⟹ ∃Q'. uhnf Q' ∧ valid Q' ∧ <νx>Q ≡⇩e Q' ∧ (depth Q') ≤ (depth(<νx>Q))" by fact
    with validQ Qhnf show ?thesis by(blast intro: Sym)
  qed
  
  then obtain Q' where Q'hnf: "uhnf Q'" and Q'eqQ: "Q' ≡⇩e <νx>Q" and validQ': "valid Q'"
                   and Q'depth: "(depth Q') ≤ (depth(<νx>Q))" by blast    
      
  from P'hnf Q'hnf validP' validQ' obtain R where Rhnf: "uhnf R" and validR: "valid R"
                                              and P'Q'eqR: "P' ⊕ Q' ≡⇩e R"
                                              and Rdepth: "depth R ≤ depth(P' ⊕ Q')"
    apply(drule_tac uhnfSum) apply assumption+ by blast
    
  from P'eqP Q'eqQ P'Q'eqR have "<νx>(P ⊕ Q) ≡⇩e R" by(blast intro: Sym SumPres' SumRes Trans)
  moreover from Rdepth P'depth Q'depth have "depth R ≤ depth(<νx>(P ⊕ Q))" by auto
  ultimately show ?case using validR Rhnf by(blast intro: Sym)
next
  case(Par P Q)
  have "uhnf(P ∥ Q)" by fact
  hence False by(simp add: uhnf_def)
  thus ?case by simp
next
  case(Res y P x)
  have "valid(<νy>P)" by fact hence validP: "valid P" by simp
  have "uhnf(<νy>P)" by fact
  then obtain a P' where aineqy: "a ≠ y" and PeqP': "P = a{y}.P'"
    by(force simp add: uhnf_def)
    
  show ?case
  proof(case_tac "x=y")
    assume "x=y"
    moreover from aineqy have "uhnf(<νy>a{y}.P')" by(force simp add: uhnf_def)
    moreover from validP PeqP' have "valid(<νy>a{y}.P')" by simp
    moreover have "<νy><νy>a{y}.P' ≡⇩e <νy>a{y}.P'"
    proof -
      have "y ♯ <νy>a{y}.P'" by(simp add: name_fresh_abs)
      hence "<νy><νy>a{y}.P' ≡⇩e <νy>a{y}.P'" by(rule ResFresh)
      thus ?thesis by(blast intro: Trans)
    qed
    moreover have "depth(<νy>a{y}.P') ≤ depth(<νy><νy>a{y}.P')" by simp
    ultimately show ?case using PeqP' by blast
  next
    assume xineqy: "x≠y"
    show ?case
    proof(case_tac "x=a")
      assume "x=a"
      moreover have "uhnf 𝟬" by(simp add: uhnf_def)
      moreover have "valid 𝟬" by simp
      moreover have "<νa><νy>a{y}.P' ≡⇩e 𝟬"
      proof -
        have "<νa><νy>a{y}.P' ≡⇩e <νy><νa>a{y}.P'" by(rule ResComm)
        moreover have "<νy><νa>a{y}.P' ≡⇩e 𝟬"
          by(blast intro: ResOutput' ResNil ResPres Trans)
        ultimately show ?thesis by(blast intro: Trans)
      qed
      moreover have "depth 𝟬 ≤ depth(<νa><νy>a{y}.P')" by simp
      ultimately show ?case using PeqP' by blast
    next
      assume xineqa: "x ≠ a"
      from aineqy have "uhnf(<νy>a{y}.(<νx>P'))" by(force simp add: uhnf_def)
      moreover from validP PeqP' have "valid(<νy>a{y}.(<νx>P'))" by simp
      moreover have "<νx><νy>a{y}.P' ≡⇩e <νy>a{y}.(<νx>P')"
      proof -
        have "<νx><νy>a{y}.P' ≡⇩e <νy><νx>a{y}.P'" by(rule ResComm)
        moreover from xineqa xineqy have "<νy><νx>a{y}.P' ≡⇩e <νy>a{y}.(<νx>P')"
          by(blast intro: ResOutput ResPres Trans)
        ultimately show ?thesis by(blast intro: Trans)
      qed
      moreover have "depth(<νy>a{y}.(<νx>P')) ≤ depth(<νx><νy>a{y}.P')"
        by simp
      ultimately show ?case using PeqP' by blast
    qed
  qed
next
  case(Bang P x)
  have "valid(!P)" by fact
  hence False by simp
  thus ?case by simp
qed

lemma expandHnf:
  fixes P :: pi
  and   S :: "pi set"

  assumes "(P, S) ∈ sumComposeSet"
  and     "∀P ∈ S. uhnf P ∧ valid P"

  shows "∃P'. uhnf P' ∧ valid P' ∧ P ≡⇩e P' ∧ depth P' ≤ depth P"
using assms
proof(induct rule: sumComposeSet.induct)
  case empty
  have "uhnf 𝟬" by(simp add: uhnf_def)
  moreover have "valid 𝟬" by simp
  moreover have "𝟬 ≡⇩e 𝟬" by(rule Refl)
  moreover have "depth 𝟬 ≤ depth 𝟬" by simp
  ultimately show ?case by blast
next
  case(insert Q S P)
  have Shnf: "∀P ∈ S. uhnf P ∧ valid P" by fact
  hence "∀P ∈ (S - {(Q)}). uhnf P ∧ valid P" by simp
  moreover have "∀P ∈ (S - {(Q)}). uhnf P ∧ valid P ⟹ ∃P'. uhnf P' ∧ valid P' ∧ P ≡⇩e P' ∧ depth P' ≤ depth P" by fact
  ultimately obtain P' where P'hnf: "uhnf P'" and validP': "valid P'"
                         and PeqP': "P ≡⇩e P'" and PP'depth: "depth P' ≤ depth P"
    by blast
  
  have "Q ∈ S" by fact
  with Shnf have "uhnf Q" and "valid Q" by simp+
  with P'hnf validP' obtain R where Rhnf: "uhnf R" and validR: "valid R"
                                and P'QeqR: "P' ⊕ Q ≡⇩e R" and P'QRdepth: "depth R ≤ depth (P' ⊕ Q)"
    by(auto dest: uhnfSum)
  
  from PeqP' P'QeqR have "P ⊕ Q ≡⇩e R" by(blast intro: SumPres Trans)
  moreover from PP'depth P'QRdepth have "depth R ≤ depth(P ⊕ Q)" by simp
  ultimately show ?case using Rhnf validR by blast
qed

lemma hnfSummandsRemove:
  fixes P :: pi
  and   Q :: pi

  assumes "P ∈ summands Q"
  and     "uhnf Q"

  shows "(summands Q) - {P' | P'. P' ∈ summands Q ∧ P' ≡⇩e P} = (summands Q) - {P}"
using assms
by(auto intro: Refl simp add: uhnf_def)

lemma pullSummand:
  fixes P  :: pi
  and   Q  :: pi

  assumes PsummQ: "P ∈ summands Q"
  and     Qhnf:   "uhnf Q"

  shows "∃Q'. P ⊕ Q' ≡⇩e Q ∧ (summands Q') = ((summands Q)  - {x. ∃P'. x = P' ∧ P' ∈ (summands Q) ∧ P' ≡⇩e P}) ∧ uhnf Q'"
proof -
  have SumGoal: "⋀P Q R. ⟦P ∈ summands Q; uhnf(Q ⊕ R);
                           ⋀P. ⟦P ∈ summands Q⟧ ⟹ ∃Q'. P ⊕ Q' ≡⇩e Q ∧ 
                                   (summands Q') = ((summands Q) - {P' |P'. P' ∈ summands Q ∧ P' ≡⇩e P}) ∧ uhnf Q';
                           ⋀P. ⟦P ∈ summands R⟧ ⟹ ∃R'. P ⊕ R' ≡⇩e R ∧ 
                                   (summands R') = ((summands R) - {P' |P'. P' ∈ summands R ∧ P' ≡⇩e P}) ∧ uhnf R'⟧
    ⟹ ∃Q'. P ⊕ Q' ≡⇩e Q ⊕ R ∧
             summands Q' = summands (pi.Sum Q R) - {P' |P'. P' ∈ summands (Q ⊕ R) ∧ P' ≡⇩e P} ∧ uhnf Q'"
  proof -
    fix P Q R
    assume IHR: "⋀P. P ∈ summands R ⟹ ∃R'. P ⊕ R' ≡⇩e R ∧ 
                                         (summands R') = ((summands R) - {P' |P'. P' ∈ summands R ∧ P' ≡⇩e P}) ∧ uhnf R'"
    assume PsummQ: "P ∈ summands Q"
    moreover assume "⋀P. P ∈ summands Q ⟹ ∃Q'. P ⊕ Q' ≡⇩e Q ∧ 
                                   (summands Q') = ((summands Q) - {P' |P'. P' ∈ summands Q ∧ P' ≡⇩e P}) ∧ uhnf Q'" 

    ultimately obtain Q' where PQ'eqQ: "P ⊕ Q' ≡⇩e Q"
                           and Q'summQ: "(summands Q') = ((summands Q) - {P' |P'. P' ∈ summands Q ∧ P' ≡⇩e P})"
                           and Q'hnf: "uhnf Q'"
      by blast
    assume QRhnf: "uhnf(Q ⊕ R)"

    show "∃Q'. P ⊕ Q' ≡⇩e Q ⊕ R ∧
             summands Q' = summands (pi.Sum Q R) - {P' |P'. P' ∈ summands (Q ⊕ R) ∧ P' ≡⇩e P} ∧ uhnf Q'"
    proof(cases "∃P' ∈ summands R. P' ≡⇩e P")
      assume "∃P' ∈ summands R. P' ≡⇩e P"
      then obtain P' where P'summR: "P' ∈ summands R" and P'eqP: "P' ≡⇩e P" by blast
      with IHR obtain R' where PR'eqR: "P' ⊕ R' ≡⇩e R"
        and R'summR: "(summands R') = ((summands R) - {P'' |P''. P'' ∈ summands R ∧ P'' ≡⇩e P'})"
        and R'hnf: "uhnf R'"
        by blast
      
      have L1: "P ⊕ (Q' ⊕ R') ≡⇩e Q ⊕ R"
      proof -
        from P'eqP have "P ⊕ (Q' ⊕ R') ≡⇩e (P ⊕ P') ⊕ (Q' ⊕ R')"
          by(blast intro: SumIdemp' SumPres Sym)
        moreover have "(P ⊕ P') ⊕ (Q' ⊕ R') ≡⇩e P ⊕ (P' ⊕ (Q' ⊕ R'))" by(rule SumAssoc)
        moreover have "P ⊕ (P' ⊕ (Q' ⊕ R')) ≡⇩e P ⊕ (P' ⊕ (R' ⊕ Q'))"
          by(blast intro: Refl SumPres' SumSym)
        moreover have "P ⊕ (P' ⊕ (R' ⊕ Q')) ≡⇩e P ⊕ (P' ⊕ R') ⊕ Q'"
          by(blast intro: Refl SumPres' Sym SumAssoc)
        moreover have "P ⊕ (P' ⊕ R') ⊕ Q' ≡⇩e (P ⊕ Q') ⊕ (P' ⊕ R')"
        proof -
          have "P ⊕ (P' ⊕ R') ⊕ Q' ≡⇩e P ⊕ Q' ⊕ (P' ⊕ R')"
            by(blast intro: Refl SumPres' SumSym)
          thus ?thesis by(blast intro: Sym SumAssoc Trans)
        qed
        moreover from PQ'eqQ PR'eqR have "(P ⊕ Q') ⊕ (P' ⊕ R') ≡⇩e Q ⊕ R" by(rule SumPres')
        ultimately show ?thesis by(blast intro!: Trans)
      qed
      
      show ?thesis
      proof(cases "Q' = 𝟬")
        assume Q'eqNil: "Q' = 𝟬"
        have "P ⊕ R' ≡⇩e Q ⊕ R"
        proof -
          have "P ⊕ R' ≡⇩e P ⊕ (R' ⊕ 𝟬)" by(blast intro: SumZero Refl Trans SumPres' Sym)
          moreover have "P ⊕ (R' ⊕ 𝟬) ≡⇩e P ⊕ (𝟬 ⊕ R')"
            by(blast intro: SumSym Trans SumPres' Refl)
          ultimately show ?thesis using L1 Q'eqNil by(blast intro: Trans)
        qed
        moreover from R'summR Q'summQ P'eqP Q'eqNil have "summands (R') = (summands (Q ⊕ R) - {P' |P'. P' ∈ summands(Q ⊕ R) ∧ P' ≡⇩e P})"
          by(auto intro: Sym Trans)
        ultimately show ?thesis using R'hnf by blast
      next
        assume Q'ineqNil: "Q' ≠ 𝟬"
        show ?thesis
        proof(case_tac "R' = 𝟬")
          assume R'eqNil: "R' = 𝟬"
          have "P ⊕ Q' ≡⇩e Q ⊕ R"
          proof -
            have "P ⊕ Q' ≡⇩e P ⊕ (Q' ⊕ 𝟬)" by(blast intro: SumZero Refl Trans SumPres' Sym)
            with L1 R'eqNil show ?thesis by(blast intro: Trans)
          qed
          moreover from R'summR Q'summQ P'eqP R'eqNil have "summands (Q') = (summands (Q ⊕ R) - {P' |P'. P' ∈ summands(Q ⊕ R) ∧ P' ≡⇩e P})"
            by(auto intro: Sym Trans)
          ultimately show ?thesis using Q'hnf by blast
        next
          assume R'ineqNil: "R' ≠ 𝟬"
          
          from R'summR Q'summQ P'eqP have "summands (Q' ⊕ R') = (summands (Q ⊕ R) - {P' |P'. P' ∈ summands(Q ⊕ R) ∧ P' ≡⇩e P})"
            by(auto intro: Sym Trans)
          moreover from QRhnf Q'hnf R'hnf R'summR Q'summQ Q'ineqNil R'ineqNil have "uhnf(Q' ⊕ R')"
            by(auto simp add: uhnf_def)
          
          ultimately show ?thesis using L1 by blast
        qed
      qed
    next
      assume "¬(∃P' ∈ summands R. P' ≡⇩e P)"
      hence Case: "∀P' ∈ summands R. ¬(P' ≡⇩e P)" by simp
      show ?thesis
      proof(case_tac "Q' = 𝟬")
        assume Q'eqNil: "Q' = 𝟬"
        have "P ⊕ R ≡⇩e Q ⊕ R" 
        proof -

          have "P ⊕ R ≡⇩e (P ⊕ 𝟬) ⊕ R" by(blast intro: SumZero Sym Trans SumPres)
          moreover from  PQ'eqQ have "P ⊕ (Q' ⊕ R) ≡⇩e Q ⊕ R"
             by(blast intro: SumAssoc Trans Sym SumPres) 
           ultimately show ?thesis using Q'eqNil by(blast intro: SumAssoc Trans)
         qed
         
         moreover from Q'summQ Q'eqNil Case have "summands (R) = (summands (Q ⊕ R) - {P' |P'. P' ∈ summands(Q ⊕ R) ∧ P' ≡⇩e P})"
           by auto
         moreover from QRhnf have "uhnf R" by(simp add: uhnf_def)

         ultimately show ?thesis by blast       
       next
         assume Q'ineqNil: "Q' ≠ 𝟬"
         from PQ'eqQ have "P ⊕ (Q' ⊕ R) ≡⇩e Q ⊕ R" 
           by(blast intro: SumAssoc Trans Sym SumPres) 
         
         moreover from Q'summQ Case have "summands (Q' ⊕ R) = (summands (Q ⊕ R) - {P' |P'. P' ∈ summands(Q ⊕ R) ∧ P' ≡⇩e P})"
           by auto
         moreover from QRhnf Q'hnf Q'summQ Q'ineqNil have "uhnf (Q' ⊕ R)"
           by(auto simp add: uhnf_def)
         ultimately show ?thesis by blast
       qed
     qed
   qed

   from assms show ?thesis
   proof(nominal_induct Q arbitrary: P rule: pi.strong_inducts)
     case PiNil
     have "P ∈ summands 𝟬" by fact
     hence False by auto
     thus ?case by simp
   next
     case(Output a b Q)
     have "P ∈ summands (a{b}.Q)" by fact
     hence PeqQ: "P = a{b}.Q" by simp
     have "P ⊕ 𝟬 ≡⇩e a{b}.Q"
     proof -
       have "P ⊕ 𝟬 ≡⇩e P" by(rule SumZero)
       with PeqQ show ?thesis by simp
     qed
     moreover have "(summands 𝟬) = (summands (a{b}.Q)) - {P' | P'. P' ∈ summands (a{b}.Q) ∧ P' ≡⇩e P}"
     proof -
       have "a{b}.Q ≡⇩e a{b}.Q" by(rule Refl)
       with PeqQ show ?thesis by simp
     qed
     moreover have "uhnf 𝟬" by(simp add: uhnf_def)
     ultimately show ?case by blast
   next
     case(Tau Q)
     have "P ∈ summands (τ.(Q))" by fact
     hence PeqQ: "P = τ.(Q)" by simp
     have "P ⊕ 𝟬 ≡⇩e τ.(Q)"
     proof -
       have "P ⊕ 𝟬 ≡⇩e P" by(rule SumZero)
       with PeqQ show ?thesis by simp
     qed
     moreover have "(summands 𝟬) = (summands (τ.(Q))) - {P' | P'. P' ∈ summands (τ.(Q)) ∧ P' ≡⇩e P}"
     proof -
       have "τ.(Q) ≡⇩e τ.(Q)" by(rule Refl)
       with PeqQ show ?thesis by simp
     qed
     moreover have "uhnf 𝟬" by(simp add: uhnf_def)
     ultimately show ?case by blast
   next
     case(Input a x Q)
     have "P ∈ summands (a<x>.Q)" by fact
     hence PeqQ: "P = a<x>.Q" by simp
     have "P ⊕ 𝟬 ≡⇩e a<x>.Q"
     proof -
       have "P ⊕ 𝟬 ≡⇩e P" by(rule SumZero)
       with PeqQ show ?thesis by simp
     qed
     moreover have "(summands 𝟬) = (summands (a<x>.Q)) - {P' | P'. P' ∈ summands (a<x>.Q) ∧ P' ≡⇩e P}"
     proof -
       have "a<x>.Q ≡⇩e a<x>.Q" by(rule Refl)
       with PeqQ show ?thesis by simp
     qed
     moreover have "uhnf 𝟬" by(simp add: uhnf_def)
     ultimately show ?case by blast
   next
     case(Match a b Q)
     have "P ∈ summands ([a⌢b]Q)" by fact
     hence False by simp
     thus ?case by simp
   next
     case(Mismatch a b Q)
     have "P ∈ summands ([a≠b]Q)" by fact
     hence False by simp
     thus ?case by simp
   next
     case(Sum Q R)
     have QRhnf: "uhnf (Q ⊕ R)" by fact
     hence Qhnf: "uhnf Q" and Rhnf: "uhnf R" by(simp add: uhnf_def)+
     have "⋀P. ⟦P ∈ summands Q; uhnf Q⟧ ⟹ ∃Q'. P ⊕ Q' ≡⇩e Q ∧ 
                                          (summands Q') = ((summands Q) - {P' |P'. P' ∈ summands Q ∧ P' ≡⇩e P}) ∧ uhnf Q'"
       by fact
     with Qhnf have IHQ: "⋀P. P ∈ summands Q ⟹ ∃Q'. P ⊕ Q' ≡⇩e Q ∧ 
                                  (summands Q') = ((summands Q) - {P' |P'. P' ∈ summands Q ∧ P' ≡⇩e P}) ∧ uhnf Q'"
       by simp
     have "⋀P. ⟦P ∈ summands R; uhnf R⟧ ⟹ ∃R'. P ⊕ R' ≡⇩e R ∧ 
                                          (summands R') = ((summands R) - {P' |P'. P' ∈ summands R ∧ P' ≡⇩e P}) ∧ uhnf R'"
       by fact
     with Rhnf have IHR: "⋀P. P ∈ summands R ⟹ ∃R'. P ⊕ R' ≡⇩e R ∧ 
                                  (summands R') = ((summands R) - {P' |P'. P' ∈ summands R ∧ P' ≡⇩e P}) ∧ uhnf R'"
       by simp
     have "P ∈ summands (Q ⊕ R)" by fact
     hence "P ∈ summands Q ∨ P ∈ summands R" by simp
     thus ?case
     proof(rule disjE)
       assume "P ∈ summands Q"
       thus ?case using QRhnf IHQ IHR by(rule SumGoal)
     next
       assume "P ∈ summands R"
       moreover from QRhnf have "uhnf (R ⊕ Q)" by(auto simp add: uhnf_def)
       ultimately have "∃Q'. (pi.Sum P Q') ≡⇩e (pi.Sum R Q) ∧
         summands Q' = summands (pi.Sum R Q) - {P' |P'. P' ∈ summands (pi.Sum R Q) ∧ P' ≡⇩e P} ∧ uhnf Q'" using IHR IHQ
         by(rule SumGoal)
       thus ?case 
         by(force intro: SumSym Trans)
     qed
   next
     case(Par Q R P)
     have "P ∈ summands (Q ∥ R)" by fact
     hence False by simp
     thus ?case by simp
   next
     case(Res x Q P)
     have "P ∈ summands (<νx>Q)" by fact
     hence PeqQ: "P = <νx>Q" by(simp add: if_split)
     have "P ⊕ 𝟬 ≡⇩e <νx>Q"
     proof -
       have "P ⊕ 𝟬 ≡⇩e P" by(rule SumZero)
       with PeqQ show ?thesis by simp
     qed
     moreover have "(summands 𝟬) = (summands (<νx>Q)) - {P' | P'. P' ∈ summands (<νx>Q) ∧ P' ≡⇩e P}"
     proof -
       have "<νx>Q ≡⇩e <νx>Q" by(rule Refl)
       with PeqQ show ?thesis by simp
     qed
     moreover have "uhnf 𝟬" by(simp add: uhnf_def)
     ultimately show ?case by blast
   next
     case(Bang Q P)
     have "P ∈ summands (!Q)" by fact
     hence False by simp
     thus ?case by simp
   qed
 qed
  
lemma nSym:
  fixes P :: pi
  and   Q :: pi

  assumes "¬(P ≡⇩e Q)"

  shows "¬(Q ≡⇩e P)"
using assms
by(blast dest: Sym)

lemma summandsZero:
  fixes P :: pi
  
  assumes "summands P = {}"
  and     "hnf P"

  shows "P = 𝟬"
using assms
by(nominal_induct P rule: pi.strong_inducts, auto intro: Refl SumIdemp SumPres' Trans)  

lemma summandsZero':
  fixes P :: pi
  
  assumes summP: "summands P = {}"
  and     Puhnf: "uhnf P"

  shows "P = 𝟬"
proof -
  from Puhnf have "hnf P" by(simp add: uhnf_def)
  with summP show ?thesis by(rule summandsZero)
qed

lemma summandEquiv:
  fixes P :: pi
  and   Q :: pi

  assumes Phnf: "uhnf P"
  and     Qhnf: "uhnf Q"
  and     PinQ: "∀P' ∈ summands P. ∃Q' ∈ summands Q. P' ≡⇩e Q'"
  and     QinP: "∀Q' ∈ summands Q. ∃P' ∈ summands P. Q' ≡⇩e P'"

  shows "P ≡⇩e Q"
proof -
  from finiteSummands assms show ?thesis
  proof(induct F=="summands P" arbitrary: P Q rule: finite_induct)
    case(empty P Q)
    have PEmpty: "{} = summands P" by fact
    moreover have "∀Q'∈summands Q. ∃P'∈summands P. Q' ≡⇩e P'" by fact
    ultimately have QEmpty: "summands Q = {}" by simp
    
    have "P = 𝟬"
    proof -
      have "uhnf P" by fact
      with PEmpty show ?thesis by(blast intro: summandsZero')
    qed
    moreover have "Q = 𝟬"
    proof -
      have "uhnf Q" by fact
      with QEmpty show ?thesis by(blast intro: summandsZero')
    qed
    ultimately show ?case by(blast intro: Refl)
  next
    case(insert P' F P Q)
    have Phnf: "uhnf P" by fact
    have Qhnf: "uhnf Q" by fact
    
    have IH: "⋀P Q. ⟦F = summands P; uhnf P; uhnf Q; ∀P' ∈ summands P. ∃Q' ∈ summands Q. P' ≡⇩e Q';
              ∀Q' ∈ summands Q. ∃P' ∈ summands P. Q' ≡⇩e P'⟧ ⟹ P ≡⇩e Q"
      by fact
    have PeqQ: "∀P' ∈ summands P. ∃Q' ∈ summands Q. P' ≡⇩e Q'" by fact
    have QeqP: "∀Q' ∈ summands Q. ∃P' ∈ summands P. Q' ≡⇩e P'" by fact
  
    have PSumm: "insert P' F = summands P" by fact
    hence P'SummP: "P' ∈ summands P" by auto
    
    with Phnf obtain P'' where P'P''eqP: "P' ⊕ P'' ≡⇩e P" 
                           and P''Summ: "summands P'' = summands P - {P'' |P''. P'' ∈ summands P ∧ P'' ≡⇩e P'}"
                           and P''hnf: "uhnf P''"
      by(blast dest: pullSummand)

    from PeqQ P'SummP obtain Q' where Q'SummQ: "Q' ∈ summands Q" and P'eqQ': "P' ≡⇩e Q'" by blast
    
    from Q'SummQ Qhnf obtain Q'' where Q'Q''eqQ: "Q' ⊕ Q'' ≡⇩e Q" 
                                   and Q''Summ: "summands Q'' = summands Q - {Q'' |Q''. Q'' ∈ summands Q ∧ Q'' ≡⇩e Q'}"
                                   and Q''hnf: "uhnf Q''"
      by(blast dest: pullSummand) 
    
    have FeqP'': "F = summands P''"
    proof -
      have "P' ∉ F" by fact
      with P''Summ PSumm hnfSummandsRemove[OF P'SummP Phnf] show ?thesis by blast
    qed

    moreover have "∀P' ∈ summands P''. ∃Q' ∈ summands Q''. P' ≡⇩e Q'"
    proof(rule ballI)
      fix P'''
      assume P'''Summ: "P''' ∈ summands P''"
      with P''Summ have "P''' ∈ summands P" by simp
      with PeqQ obtain Q''' where Q'''Summ: "Q''' ∈ summands Q" and P'''eqQ''': "P''' ≡⇩e Q'''" by blast
      have "Q''' ∈ summands Q''"
      proof -
        from P'''Summ P''Summ have "¬(P''' ≡⇩e P')" by simp
        with P'eqQ' P'''eqQ''' have "¬(Q''' ≡⇩e Q')"  by(blast intro: Trans Sym)
        with Q''Summ Q'''Summ show ?thesis by simp
      qed
    
      with P'''eqQ''' show "∃Q'∈summands Q''. P''' ≡⇩e Q'" by blast
    qed
    
    moreover have "∀Q' ∈ summands Q''. ∃P' ∈ summands P''. Q' ≡⇩e P'"
    proof(rule ballI)
      fix Q'''
      assume Q'''Summ: "Q''' ∈ summands Q''"
      with Q''Summ have "Q''' ∈ summands Q" by simp
      with QeqP obtain P''' where P'''Summ: "P''' ∈ summands P"
                              and Q'''eqP''': "Q''' ≡⇩e P'''" by blast
      have "P''' ∈ summands P''"
      proof -
        from Q'''Summ Q''Summ have "¬(Q''' ≡⇩e Q')" by simp
        with P'eqQ' Q'''eqP''' have "¬(P''' ≡⇩e P')"  by(blast intro: Trans)
        with P''Summ P'''Summ show ?thesis by simp
      qed
      with Q'''eqP''' show "∃P'∈summands P''. Q''' ≡⇩e P'" by blast
    qed
    
    ultimately have P''eqQ'': "P'' ≡⇩e Q''" using P''hnf Q''hnf by(rule_tac IH) 
    
    from P'P''eqP have "P ≡⇩e P' ⊕ P''" by(rule Sym)
    moreover from P'eqQ' P''eqQ'' have "P' ⊕ P'' ≡⇩e Q' ⊕ Q''" by(rule SumPres')
    ultimately show ?case using Q'Q''eqQ by(blast intro: Trans)
  qed
qed


lemma validSubst[simp]:
  fixes P :: pi
  and   a :: name
  and   b :: name
  and   p :: pi
  
  shows "valid(P[a::=b]) = valid P"
by(nominal_induct P avoiding: a b rule: pi.strong_inducts, auto)

lemma validOutputTransition:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi

  assumes "P ⟼a[b] ≺ P'" 
  and     "valid P"

  shows "valid P'"
using assms
by(nominal_induct rule: outputInduct, auto)

lemma validInputTransition:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi

  assumes PTrans: "P ⟼a<x> ≺ P'" 
  and     validP: "valid P"

  shows "valid P'"
proof -
  have Goal: "⋀P a x P'. ⟦P ⟼a<x> ≺ P'; x ♯ P; valid P⟧ ⟹ valid P'"
  proof -
    fix P a x P'
    assume "P ⟼a<x> ≺ P'" and "x ♯ P" and "valid P"
    thus "valid P'"
      by(nominal_induct rule: inputInduct, auto)
  qed
  obtain y::name where yFreshP: "y ♯ P" and yFreshP': "y ♯ P'"
    by(rule_tac name_exists_fresh[of "(P, P')"], auto simp add: fresh_prod)
  from yFreshP' PTrans have "P ⟼a<y> ≺ [(x, y)] ∙ P'" by(simp add: alphaBoundResidual)
  hence "valid ([(x, y)] ∙ P')" using yFreshP validP by(rule Goal)
  thus "valid P'" by simp
qed

lemma validBoundOutputTransition:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi

  assumes PTrans: "P ⟼a<νx> ≺ P'" 
  and     validP: "valid P"

  shows "valid P'"
proof -
  have Goal: "⋀P a x P'. ⟦P ⟼a<νx> ≺ P'; x ♯ P; valid P⟧ ⟹ valid P'"
  proof -
    fix P a x P'
    assume "P ⟼a<νx> ≺ P'" and "x ♯ P" and "valid P"
    thus "valid P'"
      apply(nominal_induct rule: boundOutputInduct, auto)
      proof -
        fix P a x P'
        assume "P ⟼(a::name)[x] ≺ P'" and "valid P"
        thus "valid P'"
          by(nominal_induct rule: outputInduct, auto)
      qed
  qed
  obtain y::name where yFreshP: "y ♯ P" and yFreshP': "y ♯ P'"
    by(rule_tac name_exists_fresh[of "(P, P')"], auto simp add: fresh_prod)
  from yFreshP' PTrans have "P ⟼a<νy> ≺ [(x, y)] ∙ P'" by(simp add: alphaBoundResidual)
  hence "valid ([(x, y)] ∙ P')" using yFreshP validP by(rule Goal)
  thus "valid P'" by simp
qed

lemma validTauTransition:
  fixes P  :: pi
  and   P' :: pi

  assumes PTrans: "P ⟼τ ≺ P'"
  and     validP: "valid P"

  shows "valid P'"
using assms
by(nominal_induct rule: tauInduct, auto dest: validOutputTransition validInputTransition validBoundOutputTransition)

lemmas validTransition = validInputTransition validOutputTransition validTauTransition validBoundOutputTransition

lemma validSummand:
  fixes P  :: pi
  and   P' :: pi
  and   a  :: name
  and   b  :: name
  and   x  :: name

  assumes "valid P"
  and     "hnf P"

  shows "τ.(P') ∈ summands P ⟹ valid P'"
  and   "a{b}.P' ∈ summands P ⟹ valid P'"
  and   "a<x>.P' ∈ summands P ⟹ valid P'"
  and   "⟦a ≠ x; <νx>a{x}.P' ∈ summands P⟧ ⟹ valid P'"
proof -
  assume "τ.(P') ∈ summands P"
  with assms show "valid P'" by(force intro: validTauTransition simp add: summandTransition)
next
  assume "a{b}.P' ∈ summands P"
  with assms show "valid P'" by(force intro: validOutputTransition simp add: summandTransition)
next
  assume "a<x>.P' ∈ summands P"
  with assms show "valid P'" by(force intro: validInputTransition simp add: summandTransition)
next
  assume "<νx>a{x}.P' ∈ summands P" and "a ≠ x"
  with assms show "valid P'" 
    by(force intro: validBoundOutputTransition simp add: summandTransition[THEN sym])
qed

lemma validExpand:
  fixes P :: pi
  and   Q :: pi

  assumes "valid P"
  and     "valid Q"
  and     "uhnf P"
  and     "uhnf Q"

  shows "∀R ∈ (expandSet P Q). uhnf R ∧ valid R"
proof -
  from assms have "hnf P" and "hnf Q" by(simp add: uhnf_def)+
  with assms show ?thesis
    apply(auto simp add: expandSet_def)
    apply(force dest: validSummand simp add: uhnf_def)
    apply(force dest: validSummand)
    apply(force dest: validSummand simp add: uhnf_def)
    apply(force dest: validSummand)
    apply(force dest: validSummand simp add: uhnf_def)
    apply(force dest: validSummand)
    apply(force dest: validSummand simp add: uhnf_def)
    apply(force dest: validSummand)
    apply(force dest: validSummand simp add: uhnf_def)
    apply(force dest: validSummand)
    apply(force dest: validSummand simp add: uhnf_def)
    apply(force dest: validSummand)
    apply(subgoal_tac "a≠x")
    apply(force dest: validSummand simp add: uhnf_def)
    apply blast
    apply(subgoal_tac "a≠x")
    apply(drule_tac validSummand(4)) apply assumption+
    apply blast
    apply(subgoal_tac "a≠x")
    apply(drule_tac validSummand(4)[where P=Q]) apply assumption+
    apply(force dest: validSummand simp add: uhnf_def)
    apply blast
    apply(subgoal_tac "a≠x")
    apply(drule_tac validSummand(4)[where P=Q]) apply assumption+
    apply blast
    apply(force dest: validSummand simp add: uhnf_def)
    apply(force dest: validSummand)
    apply(force dest: validSummand simp add: uhnf_def)
    apply(force simp add: uhnf_def)
    apply(force dest: validSummand)
    apply(force dest: validSummand)
    apply(force simp add: uhnf_def)
    apply(force dest: validSummand)
    apply(subgoal_tac "a≠y")
    apply(drule_tac validSummand(4)[where P=Q]) apply assumption+
    apply blast
    apply(force dest: validSummand simp add: uhnf_def)
    apply(subgoal_tac "a≠y")
    apply(drule_tac validSummand(4)) apply assumption+
    apply blast
    by(force dest: validSummand)
qed

lemma expandComplete:
  fixes F :: "pi set"

  assumes "finite F"

  shows "∃P. (P, F) ∈ sumComposeSet"
using assms
proof(induct F rule: finite_induct)
  case empty
  have "(𝟬, {}) ∈ sumComposeSet" by(rule sumComposeSet.empty)
  thus ?case by blast
next
  case(insert Q F)
  have "∃P. (P, F) ∈ sumComposeSet" by fact
  then obtain P where "(P, F) ∈ sumComposeSet" by blast
  moreover have "Q ∈ insert Q F" by simp
  moreover have "Q ∉ F" by fact
  ultimately have "(P ⊕ Q, insert Q F) ∈ sumComposeSet"
    by(force intro: sumComposeSet.insert)
  thus ?case by blast
qed

lemma expandDepth:
  fixes F :: "pi set"
  and   P :: pi
  and   Q :: pi

  assumes "(P, F) ∈ sumComposeSet"
  and     "F ≠ {}"

  shows "∃Q ∈ F. depth P ≤ depth Q ∧ (∀R ∈ F. depth R ≤ depth Q)"
using assms
proof(induct arbitrary: Q rule: sumComposeSet.induct)
  case empty
  have "({}::pi set) ≠ {}" by fact
  hence False by simp
  thus ?case by simp
next
  case(insert Q S P)
  have QinS: "Q ∈ S" by fact
  show ?case
  proof(case_tac "(S - {Q}) = {}")
    assume "(S - {Q}) = {}"
    with QinS have SeqQ: "S = {Q}" by auto
    have "(P, S - {Q}) ∈ sumComposeSet" by fact
    with SeqQ have "(P, {}) ∈ sumComposeSet" by simp
    hence "P = 𝟬" apply - by(ind_cases "(P, {}) ∈ sumComposeSet", auto)
    with QinS SeqQ show ?case by simp
  next
    assume "(S - {Q}) ≠ {}"
    moreover have "(S - {Q}) ≠ {} ⟹ ∃Q' ∈ (S - {Q}). depth P ≤ depth Q' ∧ (∀R ∈ (S - {Q}). depth R ≤ depth Q')" by fact
    ultimately obtain Q' where Q'inS: "Q' ∈ S - {Q}" and PQ'depth: "depth P ≤ depth Q'" and All: "∀R ∈ (S - {Q}). depth R ≤ depth Q'" by auto
    show ?case
    proof(case_tac "Q = Q'")
      assume "Q = Q'"
      with PQ'depth All QinS show ?case by auto
    next
      assume QineqQ': "Q ≠ Q'"
      show ?case
      proof(case_tac "depth Q ≤ depth Q'")
        assume "depth Q ≤ depth Q'"
        with QineqQ' PQ'depth All Q'inS show ?thesis by force
      next
        assume "¬ depth Q ≤ depth Q'"
        with QineqQ' PQ'depth All Q'inS QinS show ?thesis apply auto
          apply(rule_tac x=Q in bexI)
          apply auto
          apply(case_tac "R=Q")
          apply auto
          apply(erule_tac x=R in ballE)
          by auto
      qed
    qed
  qed
qed

lemma depthSubst[simp]:
  fixes P :: pi
  and   a :: name
  and   b :: name

  shows "depth(P[a::=b]) = depth P"
by(nominal_induct P avoiding: a b rule: pi.strong_inducts, auto)

lemma depthTransition:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi

  assumes Phnf: "hnf P"

  shows "P ⟼a[b] ≺ P' ⟹ depth P' < depth P"
  and   "P ⟼a<x> ≺ P' ⟹ depth P' < depth P"
  and   "P ⟼τ ≺ P' ⟹ depth P' < depth P"
  and   "P ⟼a<νx> ≺ P' ⟹ depth P' < depth P"
proof -
  assume "P ⟼a[b] ≺ P'"
  thus "depth P' < depth P" using assms
    by(nominal_induct rule: outputInduct, auto)
next
  assume Trans: "P ⟼a<x> ≺ P'"
  have Goal: "⋀P a x P'. ⟦P ⟼a<x> ≺ P'; x ♯ P; hnf P⟧ ⟹ depth P' < depth P"
  proof -
    fix P a x P'
    assume "P ⟼a<x> ≺ P'" and "x ♯ P" and "hnf P"
    thus "depth P' < depth P"
      by(nominal_induct rule: inputInduct, auto)
  qed
  obtain y::name where yFreshP: "y ♯ P" and yFreshP': "y ♯ P'"
    by(rule_tac name_exists_fresh[of "(P, P')"], auto simp add: fresh_prod)
  from yFreshP' Trans have "P ⟼a<y> ≺ [(x, y)] ∙ P'" by(simp add: alphaBoundResidual)
  hence "depth ([(x, y)] ∙ P') < depth P" using yFreshP Phnf by(rule Goal)
  thus "depth P' < depth P" by simp
next
  assume "P ⟼τ ≺ P'"
  thus "depth P' < depth P" using assms
    by(nominal_induct rule: tauInduct, auto simp add: uhnf_def)
next
  assume Trans: "P ⟼a<νx> ≺ P'"
  have Goal: "⋀P a x P'. ⟦P ⟼a<νx> ≺ P'; x ♯ P; hnf P⟧ ⟹ depth P' < depth P"
  proof -
    fix P a x P'
    assume "P ⟼a<νx> ≺ P'" and "x ♯ P" and "hnf P"
    thus "depth P' < depth P"
      by(nominal_induct rule: boundOutputInduct,
         auto elim: outputCases simp add: residual.inject)
  qed
  obtain y::name where yFreshP: "y ♯ P" and yFreshP': "y ♯ P'"
    by(rule_tac name_exists_fresh[of "(P, P')"], auto simp add: fresh_prod)
  from yFreshP' Trans have "P ⟼a<νy> ≺ [(x, y)] ∙ P'" by(simp add: alphaBoundResidual)
  hence "depth ([(x, y)] ∙ P') < depth P" using yFreshP Phnf by(rule Goal)
  thus "depth P' < depth P" by simp
qed

lemma maxExpandDepth:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi
  
  assumes "R ∈ expandSet P Q"
  and     "hnf P"
  and     "hnf Q"

  shows "depth R ≤ depth(P ∥ Q)"
using assms
apply(auto simp add: expandSet_def summandTransition[THEN sym] dest: depthTransition)
apply(subgoal_tac "a ≠ x")
apply(simp add: summandTransition[THEN sym])
apply(force dest: depthTransition)
apply blast
apply(subgoal_tac "a ≠ x")
apply(simp add: summandTransition[THEN sym])
apply(force dest: depthTransition)
apply blast
apply(force dest: depthTransition)
apply(force dest: depthTransition)
apply(subgoal_tac "a ≠ y")
apply(simp add: summandTransition[THEN sym])
apply(force dest: depthTransition)
apply blast
apply(subgoal_tac "a ≠ y")
apply(simp add: summandTransition[THEN sym])
apply(force dest: depthTransition)
by blast

lemma expandDepth':
  fixes P :: pi
  and   Q :: pi

  assumes Phnf: "hnf P"
  and     Qhnf: "hnf Q"

  shows "∃R. (R, expandSet P Q) ∈ sumComposeSet ∧ depth R ≤ depth(P ∥ Q)"
proof(case_tac "expandSet P Q = {}")
  assume "expandSet P Q = {}"
  with Phnf Qhnf show ?thesis by(auto intro: sumComposeSet.empty)
next
  assume "expandSet P Q ≠ {}"

  moreover from Phnf Qhnf finiteExpand obtain R where TSC: "(R, expandSet P Q) ∈ sumComposeSet"
    by(blast dest: expandComplete)
  ultimately obtain T where "T ∈ expandSet P Q"
                        and "depth R ≤ depth T"
    by(blast dest: expandDepth)
  with Phnf Qhnf have "depth R ≤ depth(P ∥ Q)"
    by(force dest: maxExpandDepth)
  with TSC show ?thesis by blast
qed

lemma validToHnf:
  fixes P :: pi

  assumes "valid P"

  shows "∃Q. uhnf Q ∧ valid Q ∧ Q ≡⇩e P ∧ (depth Q) ≤ (depth P)"
proof -
  have MatchGoal: "⋀a b P Q. ⟦uhnf Q; valid Q; Q ≡⇩e P; depth Q ≤ depth P⟧ ⟹
                               ∃Q. uhnf Q ∧ valid Q ∧ Q ≡⇩e [a⌢b]P ∧ depth Q ≤ depth ([a⌢b]P)"
  proof -
    fix a b P Q
    assume Qhnf: "uhnf Q" and validQ: "valid Q" and QeqP: "Q ≡⇩e P"
       and QPdepth: "depth Q ≤ depth P"
    show "∃Q. uhnf Q ∧ valid Q ∧ Q ≡⇩e [a⌢b]P ∧ depth Q ≤ depth ([a⌢b]P)"
    proof(case_tac "a = b")
      assume "a = b"
      with QeqP have "Q ≡⇩e [a⌢b]P" by(blast intro: Sym Trans equiv.Match)
      with Qhnf validQ QPdepth show ?thesis by force
    next
      assume "a ≠ b"
      hence "𝟬 ≡⇩e [a⌢b]P" by(blast intro: Sym Match')
      moreover have "uhnf 𝟬" by(simp add: uhnf_def)
      ultimately show ?thesis by force
    qed
  qed
  
  from assms show ?thesis
  proof(nominal_induct P rule: pi.strong_inducts)
    case PiNil
    have "uhnf 𝟬" by(simp add: uhnf_def)
    moreover have "valid 𝟬" by simp
    moreover have "𝟬 ≡⇩e 𝟬" by(rule Refl)
    moreover have "(depth 𝟬) ≤ (depth 𝟬)" by simp
    ultimately show ?case by blast
  next
    case(Output a b P)
    have "uhnf (a{b}.P)" by(simp add: uhnf_def)
    moreover have "valid(a{b}.P)" by fact
    moreover have "a{b}.P ≡⇩e a{b}.P" by(rule Refl)
    moreover have "(depth (a{b}.P)) ≤ (depth (a{b}.P))" by simp
    ultimately show ?case by blast
  next
    case(Tau P)
    have "uhnf (τ.(P))" by(simp add: uhnf_def)
    moreover have "valid (τ.(P))" by fact
    moreover have "τ.(P) ≡⇩e τ.(P)" by(rule Refl)
    moreover have "(depth (τ.(P))) ≤ (depth (τ.(P)))" by simp
    ultimately show ?case by blast
  next
    case(Input a x P)
    have "uhnf (a<x>.P)" by(simp add: uhnf_def)
    moreover have "valid (a<x>.P)" by fact
    moreover have "a<x>.P ≡⇩e a<x>.P" by(rule Refl)
    moreover have "(depth (a<x>.P)) ≤ (depth (a<x>.P))" by simp
    ultimately show ?case by blast
  next
    case(Match a b P)
    have "valid ([a⌢b]P)" by fact
    hence "valid P" by simp
    moreover have "valid P ⟹ ∃Q. uhnf Q ∧ valid Q ∧ Q ≡⇩e P ∧ depth Q ≤ depth P" by fact
    ultimately obtain Q where Qhnf: "uhnf Q" and validQ: "valid Q" and QeqP: "Q ≡⇩e P" 
                          and QPdepth: "depth Q ≤ depth P" by blast
    thus ?case by(rule MatchGoal)
  next
    case(Mismatch a b P)
    have "valid ([a≠b]P)" by fact
    hence "valid P" by simp
    moreover have "valid P ⟹ ∃Q. uhnf Q ∧ valid Q ∧ Q ≡⇩e P ∧ depth Q ≤ depth P" by fact
    ultimately obtain Q where Qhnf: "uhnf Q" and validQ: "valid Q" and QeqP: "Q ≡⇩e P" 
                          and QPdepth: "depth Q ≤ depth P" by blast
    show ?case
    proof(case_tac "a = b")
      assume "a = b"
      hence "𝟬 ≡⇩e [a≠b]P" by(blast intro: Sym Mismatch')
      moreover have "uhnf 𝟬" by(simp add: uhnf_def)
      ultimately show ?case by force
    next
      assume "a ≠ b"
      with QeqP have "Q ≡⇩e [a≠b]P" by(blast intro: Sym Trans equiv.Mismatch)
      with Qhnf validQ QPdepth show ?case by force
    qed
  next
    case(Sum P Q)
    have "valid(P ⊕ Q)" by fact
    hence validP: "valid P" and validQ: "valid Q" by simp+
    
    have "∃P'. uhnf P' ∧ valid P' ∧ P' ≡⇩e P ∧ (depth P') ≤ (depth P)"
    proof -
      have "valid P ⟹ ∃P'. uhnf P' ∧ valid P' ∧ P' ≡⇩e P ∧ (depth P') ≤ (depth P)" by fact
      with validP show ?thesis by simp
    qed
    then obtain P' where P'hnf: "uhnf P'" and P'eqP: "P' ≡⇩e P" and validP': "valid P'"
                     and P'depth: "(depth P') ≤ (depth P)" by blast

    have "∃Q'. uhnf Q' ∧ valid Q' ∧ Q' ≡⇩e Q ∧ (depth Q') ≤ (depth Q)"
    proof -
      have "valid Q ⟹ ∃Q'. uhnf Q' ∧ valid Q' ∧ Q' ≡⇩e Q ∧ (depth Q') ≤ (depth Q)" by fact
      with validQ show ?thesis by simp
    qed
    
    then obtain Q' where Q'hnf: "uhnf Q'" and Q'eqQ: "Q' ≡⇩e Q" and validQ': "valid Q'"
                     and Q'depth: "(depth Q') ≤ (depth Q)" by blast    
      
    from P'hnf Q'hnf validP' validQ' obtain R where Rhnf: "uhnf R" and validR: "valid R"
                                              and P'Q'eqR: "P' ⊕ Q' ≡⇩e R"
                                              and Rdepth: "depth R ≤ depth(P' ⊕ Q')"
      apply(drule_tac uhnfSum) apply assumption+ by blast
    
    from validP' validQ' have "valid(P' ⊕ Q')" by simp
    from P'eqP Q'eqQ P'Q'eqR have "P ⊕ Q ≡⇩e R" by(blast intro: Sym SumPres' Trans)
    moreover from Rdepth P'depth Q'depth have "depth R ≤ depth(P ⊕ Q)" by auto
    ultimately show ?case using validR Rhnf by(blast intro: Sym)
  next
    case(Par P Q)
    have "valid(P ∥ Q)" by fact
    
    hence validP: "valid P" and validQ: "valid Q" by simp+
    have "∃P'. uhnf P' ∧ valid P' ∧ P' ≡⇩e P ∧ (depth P') ≤ (depth P)"
    proof -
      have "valid P ⟹ ∃P'. uhnf P' ∧ valid P' ∧ P' ≡⇩e P ∧ (depth P') ≤ (depth P)" by fact
      with validP show ?thesis by simp
    qed
    then obtain P' where P'hnf: "uhnf P'" and P'eqP: "P' ≡⇩e P" and validP': "valid P'"
                     and P'depth: "(depth P') ≤ (depth P)" by blast

    have "∃Q'. uhnf Q' ∧ valid Q' ∧ Q' ≡⇩e Q ∧ (depth Q') ≤ (depth Q)"
    proof -
      have "valid Q ⟹ ∃Q'. uhnf Q' ∧ valid Q' ∧ Q' ≡⇩e Q ∧ (depth Q') ≤ (depth Q)" by fact
      with validQ show ?thesis by simp
    qed
    
    then obtain Q' where Q'hnf: "uhnf Q'" and Q'eqQ: "Q' ≡⇩e Q" and validQ': "valid Q'"
                     and Q'depth: "(depth Q') ≤ (depth Q)" by blast

    from P'hnf Q'hnf obtain R where Exp: "(R, expandSet P' Q') ∈ sumComposeSet" and Rdepth: "depth R ≤ depth(P' ∥ Q')"
      by(force dest: expandDepth' simp add: uhnf_def)
    
    from Exp P'hnf Q'hnf have P'Q'eqR: "P' ∥ Q' ≡⇩e R" by(force intro: Expand simp add: uhnf_def)
    from P'hnf Q'hnf validP' validQ' have "∀P ∈ (expandSet P' Q'). uhnf P ∧ valid P" by(blast dest: validExpand)
    with Exp obtain R' where R'hnf: "uhnf R'" and validR': "valid R'"
                                              and ReqR': "R ≡⇩e R'"
                                              and R'depth: "depth R' ≤ depth R"
      by(blast dest: expandHnf)
    from P'eqP Q'eqQ P'Q'eqR ReqR' have "P ∥ Q ≡⇩e R'" by(blast intro: Sym ParPres Trans)
    moreover from Rdepth P'depth Q'depth R'depth have "depth R' ≤ depth(P ∥ Q)" by auto
    ultimately show ?case using validR' R'hnf by(blast dest: Sym)
  next
    case(Res x P)
    have "valid (<νx>P)" by fact
    hence validP: "valid P" by simp
    moreover have "valid P ⟹ ∃Q. uhnf Q ∧ valid Q ∧ Q ≡⇩e P ∧ depth Q ≤ depth P" by fact
    ultimately obtain Q where Qhnf: "uhnf Q" and validQ: "valid Q" and QeqP: "Q ≡⇩e P"
                          and QPDepth: "depth Q ≤ depth P" by blast
    
    from validP show ?case
    proof(nominal_induct P avoiding: x rule: pi.strong_inducts)
      case PiNil
      have "uhnf 𝟬" by(simp add: uhnf_def)
      moreover have "valid 𝟬" by simp
      moreover have "𝟬 ≡⇩e <νx>𝟬"
      proof -
        have "x ♯ 𝟬" by simp
        thus ?thesis by(blast intro: Sym ResFresh)
      qed
      moreover have "depth 𝟬 ≤ depth (<νx>𝟬)" by simp
      ultimately show ?case by blast
    next
      case(Output a b P)
      have "valid(a{b}.P)" by fact
      hence validP: "valid P" by simp
      show ?case
      proof(case_tac "x=a")
        assume "x = a"
        moreover have "uhnf 𝟬" by(simp add: uhnf_def)
        moreover have "valid 𝟬" by simp
        moreover have "𝟬 ≡⇩e <νx>x{b}.P" by(blast intro: ResOutput' Sym)
        moreover have "depth 𝟬 ≤ depth(<νx>x{b}.P)" by simp
        ultimately show ?case by blast
      next
        assume xineqa: "x ≠ a"
        show ?case
        proof(case_tac "x=b")
          assume "x=b"
          moreover from xineqa have "uhnf(<νx>a{x}.P)" by(force simp add: uhnf_def)
          moreover from validP have "valid(<νx>a{x}.P)" by simp
          moreover have "<νx>a{x}.P ≡⇩e <νx>a{x}.P" by(rule Refl)
          moreover have "depth(<νx>a{x}.P) ≤ depth(<νx>a{x}.P)" by simp
          ultimately show ?case by blast
        next
          assume xineqb: "x ≠ b"
          have "uhnf(a{b}.(<νx>P))" by(simp add: uhnf_def)
          moreover from validP have "valid(a{b}.(<νx>P))" by simp
          moreover from xineqa xineqb have "a{b}.(<νx>P) ≡⇩e <νx>a{b}.P" by(blast intro: ResOutput Sym)
          moreover have "depth(a{b}.(<νx>P)) ≤ depth(<νx>a{b}.P)" by simp
          ultimately show ?case by blast
        qed
      qed
    next
      case(Tau P)
      have "valid(τ.(P))" by fact
      hence validP: "valid P" by simp
      
      have "uhnf(τ.(<νx>P))" by(simp add: uhnf_def)
      moreover from validP have "valid(τ.(<νx>P))" by simp
      moreover have "τ.(<νx>P) ≡⇩e <νx>τ.(P)" by(blast intro: ResTau Sym)
      moreover have "depth(τ.(<νx>P)) ≤ depth(<νx>τ.(P))" by simp
      ultimately show ?case by blast
    next
      case(Input a y P)
      have "valid(a<y>.P)" by fact
      hence validP: "valid P" by simp
      have "y ♯ x" by fact hence yineqx: "y ≠ x" by simp
      show ?case
      proof(case_tac "x=a")
        assume "x = a"
        moreover have "uhnf 𝟬" by(simp add: uhnf_def)
        moreover have "valid 𝟬" by simp
        moreover have "𝟬 ≡⇩e <νx>x<y>.P" by(blast intro: ResInput' Sym)
        moreover have "depth 𝟬 ≤ depth(<νx>x<y>.P)" by simp
        ultimately show ?case by blast
      next
        assume xineqa: "x ≠ a"
        have "uhnf(a<y>.(<νx>P))" by(simp add: uhnf_def)
        moreover from validP have "valid(a<y>.(<νx>P))" by simp
        moreover from xineqa yineqx have "a<y>.(<νx>P) ≡⇩e <νx>a<y>.P" by(blast intro: ResInput Sym)
        moreover have "depth(a<y>.(<νx>P)) ≤ depth(<νx>a<y>.P)" by simp
        ultimately show ?case by blast
      qed
    next
      case(Match a b P x)
      have "valid([a⌢b]P)" by fact hence "valid P" by simp
      moreover have "⋀x. valid P ⟹ ∃Q. uhnf Q ∧ valid Q ∧ Q ≡⇩e <νx>P ∧ 
                                           depth Q ≤ depth(<νx>P)"
        by fact
      ultimately obtain Q where Qhnf: "uhnf Q" and validQ: "valid Q"
                            and QeqP: "Q ≡⇩e (<νx>P)" 
                            and QPdepth: "depth Q ≤ depth(<νx>P)"
        by blast
      show ?case
      proof(case_tac "a = b")
        assume "a=b"
        moreover have "Q ≡⇩e <νx>[a⌢a]P"
        proof -
          have "P ≡⇩e [a⌢a]P" by(blast intro: equiv.Match Sym)
          hence "<νx>P ≡⇩e <νx>[a⌢a]P" by(rule ResPres)
          with QeqP show ?thesis by(blast intro: Trans)
        qed
        moreover from QPdepth have "depth Q ≤ depth(<νx>[a⌢a]P)" by simp
        ultimately show ?case using Qhnf validQ by blast
      next
        assume aineqb: "a≠b"
        have "uhnf 𝟬" by(simp add: uhnf_def)
        moreover have "valid 𝟬" by simp
        moreover have "𝟬 ≡⇩e <νx>[a⌢b]P"
        proof -
          from aineqb have "𝟬 ≡⇩e [a⌢b]P" by(blast intro: Match' Sym)
          hence "<νx>𝟬 ≡⇩e <νx>[a⌢b]P" by(rule ResPres)
          thus ?thesis by(blast intro: ResNil Trans Sym)
        qed
        moreover have "depth 𝟬 ≤ depth(<νx>[a⌢b]P)" by simp
        ultimately show ?case by blast
      qed
    next
      case(Mismatch a b P x)
      have "valid([a≠b]P)" by fact hence "valid P" by simp
      moreover have "⋀x. valid P ⟹ ∃Q. uhnf Q ∧ valid Q ∧ Q ≡⇩e <νx>P ∧ 
                                           depth Q ≤ depth(<νx>P)"
        by fact
      ultimately obtain Q where Qhnf: "uhnf Q" and validQ: "valid Q"
                            and QeqP: "Q ≡⇩e (<νx>P)" 
                            and QPdepth: "depth Q ≤ depth(<νx>P)"
        by blast
      show ?case
      proof(case_tac "a = b")
        assume "a=b"
        moreover have "uhnf 𝟬" by(simp add: uhnf_def)
        moreover have "valid 𝟬" by simp
        moreover have "𝟬 ≡⇩e <νx>[a≠a]P"
        proof -
          have "𝟬 ≡⇩e [a≠a]P" by(blast intro: Mismatch' Sym)
          hence "<νx>𝟬 ≡⇩e <νx>[a≠a]P" by(rule ResPres)
          thus ?thesis by(blast intro: ResNil Trans Sym)
        qed
        moreover have "depth 𝟬 ≤ depth(<νx>[a≠a]P)" by simp
        ultimately show ?case by blast
      next
        assume aineqb: "a≠b"
        have "Q ≡⇩e <νx>[a≠b]P"
        proof -
          from aineqb have "P ≡⇩e [a≠b]P" by(blast intro: equiv.Mismatch Sym)
          hence "<νx>P ≡⇩e <νx>[a≠b]P" by(rule ResPres)
          with QeqP show ?thesis by(blast intro: Trans)
        qed
        moreover from QPdepth have "depth Q ≤ depth(<νx>[a≠b]P)" by simp
        ultimately show ?case using Qhnf validQ by blast
      qed
    next
      case(Sum P Q x)
      have "valid(P ⊕ Q)" by fact
      hence validP: "valid P" and validQ: "valid Q" by simp+

      have "∃P'. uhnf P' ∧ valid P' ∧ P' ≡⇩e <νx>P ∧ (depth P') ≤ (depth(<νx>P))"
      proof -
        have "valid P ⟹ ∃P'. uhnf P' ∧ valid P' ∧ P' ≡⇩e <νx>P ∧ (depth P') ≤ (depth (<νx>P))" by fact
        with validP show ?thesis by simp
      qed
      then obtain P' where P'hnf: "uhnf P'" and P'eqP: "P' ≡⇩e <νx>P" and validP': "valid P'"
                       and P'depth: "(depth P') ≤ (depth(<νx>P))" by blast

      have "∃Q'. uhnf Q' ∧ valid Q' ∧ Q' ≡⇩e <νx>Q ∧ (depth Q') ≤ (depth(<νx>Q))"
      proof -
        have "valid Q ⟹ ∃Q'. uhnf Q' ∧ valid Q' ∧ Q' ≡⇩e <νx>Q ∧ (depth Q') ≤ (depth(<νx>Q))" by fact
        with validQ show ?thesis by simp
      qed

      then obtain Q' where Q'hnf: "uhnf Q'" and Q'eqQ: "Q' ≡⇩e <νx>Q" and validQ': "valid Q'"
                       and Q'depth: "(depth Q') ≤ (depth(<νx>Q))" by blast    
      
      from P'hnf Q'hnf validP' validQ' obtain R where Rhnf: "uhnf R" and validR: "valid R"
                                                and P'Q'eqR: "P' ⊕ Q' ≡⇩e R"
                                                and Rdepth: "depth R ≤ depth(P' ⊕ Q')"
        apply(drule_tac uhnfSum) apply assumption+ by blast
      
      from P'eqP Q'eqQ P'Q'eqR have "<νx>(P ⊕ Q) ≡⇩e R" by(blast intro: Sym SumPres' SumRes Trans)
      moreover from Rdepth P'depth Q'depth have "depth R ≤ depth(<νx>(P ⊕ Q))" by auto
      ultimately show ?case using validR Rhnf by(blast intro: Sym)
    next
      case(Par P Q x)
      have "valid(P ∥ Q)" by fact
      
      hence validP: "valid P" and validQ: "valid Q" by simp+
      have "∃P'. uhnf P' ∧ valid P' ∧ P' ≡⇩e P ∧ (depth P') ≤ (depth P)"
      proof -
        obtain x::name where xFreshP: "x ♯ P" by(rule name_exists_fresh)
        moreover have "⋀x. valid P ⟹ ∃P'. uhnf P' ∧ valid P' ∧ P' ≡⇩e (<νx>P) ∧ (depth P') ≤ (depth(<νx>P))" by fact
        with validP obtain P' where "uhnf P'" and "valid P'" and P'eqP: "P' ≡⇩e (<νx>P)" and P'depth: "(depth P') ≤ (depth(<νx>P))" by blast
        moreover from xFreshP P'eqP have "P' ≡⇩e P" by(blast intro: Trans ResFresh)
        moreover with P'depth have "depth P' ≤ depth P" by simp
        ultimately show ?thesis by blast
      qed

      then obtain P' where P'hnf: "uhnf P'" and P'eqP: "P' ≡⇩e P" and validP': "valid P'"
                       and P'depth: "(depth P') ≤ (depth P)" by blast

      have "∃Q'. uhnf Q' ∧ valid Q' ∧ Q' ≡⇩e Q ∧ (depth Q') ≤ (depth Q)"
      proof -
        obtain x::name where xFreshQ: "x ♯ Q" by(rule name_exists_fresh)
        moreover have "⋀x. valid Q ⟹ ∃Q'. uhnf Q' ∧ valid Q' ∧ Q' ≡⇩e (<νx>Q) ∧ (depth Q') ≤ (depth(<νx>Q))" by fact
        with validQ obtain Q' where "uhnf Q'" and "valid Q'" and Q'eqQ: "Q' ≡⇩e (<νx>Q)" and Q'depth: "(depth Q') ≤ (depth(<νx>Q))" by blast
        moreover from xFreshQ Q'eqQ have "Q' ≡⇩e Q" by(blast intro: Trans ResFresh)
        moreover with Q'depth have "depth Q' ≤ depth Q" by simp
        ultimately show ?thesis by blast
      qed
      
      then obtain Q' where Q'hnf: "uhnf Q'" and Q'eqQ: "Q' ≡⇩e Q" and validQ': "valid Q'"
                       and Q'depth: "(depth Q') ≤ (depth Q)" by blast
      
      from P'hnf Q'hnf obtain R where Exp: "(R, expandSet P' Q') ∈ sumComposeSet" and Rdepth: "depth R ≤ depth(P' ∥ Q')"
        by(force dest: expandDepth' simp add: uhnf_def)
    
      from Exp P'hnf Q'hnf have P'Q'eqR: "P' ∥ Q' ≡⇩e R" by(force intro: Expand simp add: uhnf_def)
      from P'hnf Q'hnf validP' validQ' have "∀P ∈ (expandSet P' Q'). uhnf P ∧ valid P" by(blast dest: validExpand)
      with Exp obtain R' where R'hnf: "uhnf R'" and validR': "valid R'"
                                                and ReqR': "R ≡⇩e R'"
                                                and R'depth: "depth R' ≤ depth R"
        by(blast dest: expandHnf)
      
      from P'eqP Q'eqQ P'Q'eqR ReqR' have "P ∥ Q ≡⇩e R'" by(blast intro: Sym ParPres Trans)
      hence ResTrans: "<νx>(P ∥ Q) ≡⇩e <νx>R'" by(rule ResPres)
      from validR' R'hnf obtain R'' where R''hnf: "uhnf R''" and validR'': "valid R''" and R'eqR'': "<νx>R' ≡⇩e R''" and R''depth: "depth R'' ≤ depth(<νx>R')"
        by(force dest: uhnfRes)
      from ResTrans R'eqR'' have "<νx>(P ∥ Q) ≡⇩e R''" by(rule Trans)
      moreover from Rdepth P'depth Q'depth R'depth R''depth have "depth R'' ≤ depth(<νx>(P ∥ Q))" by auto
      ultimately show ?case using validR'' R''hnf by(blast dest: Sym)
    next
      case(Res y P x)
      have "valid(<νy>P)" by fact hence "valid P" by simp
      moreover have "⋀x. valid P ⟹ ∃Q. uhnf Q ∧ valid Q ∧ Q ≡⇩e <νx>P ∧ depth Q ≤ depth(<νx>P)"
        by fact
      ultimately obtain Q where Qhnf: "uhnf Q" and validQ: "valid Q" and QeqP: "Q ≡⇩e <νy>P"
                            and QPdepth: "depth Q ≤ depth(<νy>P)" by blast

      from Qhnf validQ obtain Q' where Q'hnf: "uhnf Q'" and validQ': "valid Q'" and QeqQ': "<νx>Q ≡⇩e Q'"
                                   and Q'Qdepth: "depth Q' ≤ depth(<νx>Q)"
        by(force dest: uhnfRes)

      from QeqP have "<νx>Q ≡⇩e <νx><νy>P" by(rule ResPres)
      with QeqQ' have "Q' ≡⇩e <νx><νy>P" by(blast intro: Trans Sym)
      moreover from Q'Qdepth QPdepth have "depth Q' ≤ depth(<νx><νy>P)" by simp
      ultimately show ?case using Q'hnf validQ' by blast
    next
      case(Bang P x)
      have "valid(!P)" by fact
      hence False by simp
      thus ?case by simp
    qed
  next
    case(Bang P)
    have "valid(!P)" by fact
    hence False by simp
    thus ?case by simp
  qed
qed

lemma depthZero:
  fixes P :: pi
  
  assumes "depth P = 0"
  and     "uhnf P"

  shows "P = 𝟬"
using assms
apply(nominal_induct P rule: pi.strong_inducts, auto simp add: uhnf_def max_def if_split) 
apply(case_tac "depth pi1 ≤ depth pi2")
by auto

lemma completeAux:
  fixes n :: nat
  and   P :: pi
  and   Q :: pi

  assumes "depth P + depth Q ≤ n"
  and     "valid P"
  and     "valid Q"
  and     "uhnf P"
  and     "uhnf Q"
  and     "P ∼ Q"

  shows "P ≡⇩e Q"
using assms
proof(induct n arbitrary: P Q rule: nat.induct)
  case(zero P Q)
  have "depth P + depth Q ≤ 0" by fact
  hence Pdepth: "depth P = 0" and Qdepth: "depth Q = 0" by auto
  moreover have  "uhnf P" and "uhnf Q" by fact+
  ultimately have "P = 𝟬" and "Q = 𝟬" by(blast intro: depthZero)+
  thus ?case by(blast intro: Refl)
next
  case(Suc n P Q)
  have validP: "valid P" and validQ: "valid Q" by fact+
  have Phnf: "uhnf P" and Qhnf: "uhnf Q" by fact+
  have PBisimQ: "P ∼ Q" by fact
  have IH: "⋀P Q. ⟦depth P + depth Q ≤ n; valid P; valid Q; uhnf P; uhnf Q; P ∼ Q⟧ ⟹ P ≡⇩e Q"
    by fact
  have PQdepth: "depth P + depth Q ≤ Suc n" by fact
  
  have Goal: "⋀P Q Q'. ⟦depth P + depth Q ≤ Suc n; valid P; valid Q; uhnf P; uhnf Q; 
                        P ↝[bisim] Q; Q' ∈ summands Q⟧ ⟹ ∃P' ∈ summands P. Q' ≡⇩e P'"
  proof -
    fix P Q Q'
    assume PQdepth: "depth P + depth Q ≤ Suc n"
    assume validP: "valid P" and validQ: "valid Q"
    assume Phnf: "uhnf P" and Qhnf: "uhnf Q"
    assume PSimQ: "P ↝[bisim] Q"
    assume Q'inQ: "Q' ∈ summands Q"
    
    thus "∃P' ∈ summands P. Q' ≡⇩e P'" using PSimQ Phnf validP PQdepth
    proof(nominal_induct Q' avoiding: P rule: pi.strong_inducts)
      case PiNil
      have "𝟬 ∈ summands Q" by fact
      hence False by(nominal_induct Q rule: pi.strong_inducts, auto simp add: if_split)
      thus ?case by simp
    next
      case(Output a b Q' P)
      have validP: "valid P" and Phnf: "uhnf P" and PSimQ: "P ↝[bisim] Q" by fact+
      have PQdepth: "depth P + depth Q ≤ Suc n" by fact
      have "a{b}.Q' ∈ summands Q" by fact
      with Qhnf have QTrans: "Q ⟼a[b] ≺ Q'" by(simp add: summandTransition uhnf_def)
      with PSimQ obtain P' where PTrans: "P ⟼a[b] ≺ P'" and P'BisimQ': "P' ∼ Q'"
        by(blast dest: simE)
      
      from Phnf PTrans have "a{b}.P' ∈ summands P" by(simp add: summandTransition uhnf_def)
      moreover have "P' ≡⇩e Q'"
      proof -
        from validP PTrans have validP': "valid P'" by(blast intro: validTransition)
        from validQ QTrans have validQ': "valid Q'" by(blast intro: validTransition)
        
        from validP' obtain P'' where P''hnf: "uhnf P''" and validP'': "valid P''"
                                  and P''eqP': "P'' ≡⇩e P'" and P''depth: "depth P'' ≤ depth P'"
          by(blast dest: validToHnf)
        
        from validQ' obtain Q'' where Q''hnf: "uhnf Q''" and validQ'': "valid Q''"
                                  and Q''eqQ': "Q'' ≡⇩e Q'" and Q''depth: "depth Q'' ≤ depth Q'"
          by(blast dest: validToHnf)
        
        have "depth P'' + depth Q'' ≤ n"
        proof -
          from Phnf PTrans have "depth P' < depth P" 
            by(force intro: depthTransition simp add: uhnf_def)
          moreover from Qhnf QTrans have "depth Q' < depth Q"
            by(force intro: depthTransition simp add: uhnf_def)
          ultimately show ?thesis using PQdepth P''depth Q''depth by simp
        qed
        
        moreover have "P'' ∼ Q''"
        proof -
          from P''eqP' have "P'' ∼ P'" by(rule sound)
          moreover from Q''eqQ' have "Q'' ∼ Q'" by(rule sound)
          ultimately show ?thesis using P'BisimQ' by(blast dest: transitive symmetric)
        qed
        ultimately have "P'' ≡⇩e Q''" using validP'' validQ'' P''hnf Q''hnf by(rule_tac IH)
        with P''eqP' Q''eqQ' show ?thesis by(blast intro: Sym Trans)
      qed
      ultimately show ?case by(blast intro: Sym equiv.OutputPres)
    next
      case(Tau Q' P)
      have validP: "valid P" and Phnf: "uhnf P" and PSimQ: "P ↝[bisim] Q" by fact+
      have PQdepth: "depth P + depth Q ≤ Suc n" by fact
      have "τ.(Q') ∈ summands Q" by fact
      with Qhnf have QTrans: "Q ⟼τ ≺ Q'" by(simp add: summandTransition uhnf_def)
      with PSimQ obtain P' where PTrans: "P ⟼τ ≺ P'" and P'BisimQ': "P' ∼ Q'"
        by(blast dest: simE)
      
      from Phnf PTrans have "τ.(P') ∈ summands P" by(simp add: summandTransition uhnf_def)
      moreover have "P' ≡⇩e Q'"
      proof -
        from validP PTrans have validP': "valid P'" by(blast intro: validTransition)
        from validQ QTrans have validQ': "valid Q'" by(blast intro: validTransition)
        
        from validP' obtain P'' where P''hnf: "uhnf P''" and validP'': "valid P''"
                                  and P''eqP': "P'' ≡⇩e P'" and P''depth: "depth P'' ≤ depth P'"
          by(blast dest: validToHnf)
          
        from validQ' obtain Q'' where Q''hnf: "uhnf Q''" and validQ'': "valid Q''"
                                  and Q''eqQ': "Q'' ≡⇩e Q'" and Q''depth: "depth Q'' ≤ depth Q'"
          by(blast dest: validToHnf)
        
        have "depth P'' + depth Q'' ≤ n"
        proof -
          from Phnf PTrans have "depth P' < depth P"
            by(force intro: depthTransition simp add: uhnf_def)
          moreover from Qhnf QTrans have "depth Q' < depth Q" 
            by(force intro: depthTransition simp add: uhnf_def)
          ultimately show ?thesis using PQdepth P''depth Q''depth by simp
        qed
        
        moreover have "P'' ∼ Q''"
        proof -
          from P''eqP' have "P'' ∼ P'" by(rule sound)
          moreover from Q''eqQ' have "Q'' ∼ Q'" by(rule sound)
          ultimately show ?thesis using P'BisimQ' by(blast dest: transitive symmetric)
        qed
        ultimately have "P'' ≡⇩e Q''" using validP'' validQ'' P''hnf Q''hnf by(rule_tac IH)
        with P''eqP' Q''eqQ' show ?thesis by(blast intro: Sym Trans)
      qed
      ultimately show ?case by(blast intro: Sym equiv.TauPres)
    next
      case(Input a x Q' P)
      have validP: "valid P" and Phnf: "uhnf P" and PSimQ: "P ↝[bisim] Q" and xFreshP: "x ♯ P"  by fact+
      have PQdepth: "depth P + depth Q ≤ Suc n" by fact
      have "a<x>.Q' ∈ summands Q" by fact
      with Qhnf have QTrans: "Q ⟼a<x> ≺ Q'" by(simp add: summandTransition uhnf_def)
      with PSimQ xFreshP obtain P' where PTrans: "P ⟼a<x> ≺ P'"
                                     and P'derQ': "derivative P' Q' (InputS a) x bisim"
        by(blast dest: simE)

      from Phnf PTrans have "a<x>.P' ∈ summands P" by(simp add: summandTransition uhnf_def)
      moreover have "∀y ∈ supp(P', Q', x). P'[x::=y] ≡⇩e Q'[x::=y]"
      proof(rule ballI)
        fix y::name
        assume ysupp: "y ∈ supp(P', Q', x)"
        have validP': "valid(P'[x::=y])"
        proof -
          from validP PTrans have validP': "valid P'" by(blast intro: validTransition)
          thus ?thesis by simp
        qed
        have validQ': "valid(Q'[x::=y])"
        proof -
          from validQ QTrans have validQ': "valid Q'" by(blast intro: validTransition)
          thus ?thesis by simp
        qed
        
        from validP' obtain P'' where P''hnf: "uhnf P''" and validP'': "valid P''"
                                  and P''eqP': "P'' ≡⇩e P'[x::=y]" and P''depth: "depth P'' ≤ depth(P'[x::=y])"
          by(blast dest: validToHnf)
        
        from validQ' obtain Q'' where Q''hnf: "uhnf Q''" and validQ'': "valid Q''"
                                  and Q''eqQ': "Q'' ≡⇩e Q'[x::=y]" and Q''depth: "depth Q'' ≤ depth(Q'[x::=y])"
          by(blast dest: validToHnf)
        
        have "depth P'' + depth Q'' ≤ n"
        proof -
          from Phnf PTrans have "depth P' < depth P"
            by(force intro: depthTransition simp add: uhnf_def)
          moreover from Qhnf QTrans have "depth Q' < depth Q" 
            by(force intro: depthTransition simp add: uhnf_def)
          ultimately show ?thesis using PQdepth P''depth Q''depth by simp 
        qed
          
        moreover have "P'' ∼ Q''"
        proof -
          from P'derQ' have P'BisimQ': "P'[x::=y] ∼ Q'[x::=y]" 
            by(auto simp add: derivative_def)
          from P''eqP' have "P'' ∼ P'[x::=y]" by(rule sound)
          moreover from Q''eqQ' have "Q'' ∼ Q'[x::=y]" by(rule sound)
          ultimately show ?thesis using P'BisimQ' by(blast dest: transitive symmetric)
        qed
        ultimately have "P'' ≡⇩e Q''" using validP'' validQ'' P''hnf Q''hnf by(rule_tac IH)
        with P''eqP' Q''eqQ' show "P'[x::=y] ≡⇩e Q'[x::=y]" by(blast intro: Sym Trans)
      qed
      
      ultimately show ?case 
        apply -
        apply(rule_tac x="a<x>.P'" in bexI)
        apply(rule equiv.InputPres)
        apply(rule ballI)
        apply(erule_tac x=y in ballE)
        apply(blast dest: Sym)
        by(auto simp add: supp_prod)
    next
      case(Match a b P' P)
      have "[a⌢b]P' ∈ summands Q" by fact
      hence False by(nominal_induct Q rule: pi.strong_inducts, auto simp add: if_split)
      thus ?case by simp
    next
      case(Mismatch a b P' P)
      have "[a≠b]P' ∈ summands Q" by fact
      hence False by(nominal_induct Q rule: pi.strong_inducts, auto simp add: if_split)
      thus ?case by simp
    next
      case(Sum P' Q' P)
      have "P' ⊕ Q' ∈ summands Q" by fact
      hence False by(nominal_induct Q rule: pi.strong_inducts, auto simp add: if_split)
      thus ?case by simp
    next
      case(Par P' Q' P)
      have "P' ∥ Q' ∈ summands Q" by fact
      hence False by(nominal_induct Q rule: pi.strong_inducts, auto simp add: if_split)
      thus ?case by simp
    next
      case(Res x Q'' P)
      have xFreshP: "x ♯ P" by fact
      have validP: "valid P" and Phnf: "uhnf P" and PSimQ: "P ↝[bisim] Q" by fact+
      have PQdepth: "depth P + depth Q ≤ Suc n" by fact
      have Q''summQ: "<νx>Q'' ∈ summands Q" by fact
      hence "∃a Q'. a ≠ x ∧ Q'' = a{x}.Q'"
        by(nominal_induct Q rule: pi.strong_inducts, auto simp add: if_split pi.inject name_abs_eq name_calc)  
      then obtain a Q' where aineqx: "a ≠ x" and Q'eqQ'': "Q'' = a{x}.Q'"
        by blast
      with Qhnf  Q''summQ have QTrans: "Q ⟼a<νx> ≺ Q'" by(simp add: summandTransition uhnf_def)
      with PSimQ xFreshP obtain P' where PTrans: "P ⟼a<νx> ≺ P'" and P'BisimQ': "P' ∼ Q'"
        by(force dest: simE simp add: derivative_def)
        
      from Phnf PTrans aineqx have "(<νx>a{x}.P') ∈ summands P" by(simp add: summandTransition uhnf_def)
      moreover have "a{x}.P' ≡⇩e a{x}.Q'"
      proof -
        have "P' ≡⇩e Q'"
        proof -
          from validP PTrans have validP': "valid P'" by(blast intro: validTransition)
          from validQ QTrans have validQ': "valid Q'" by(blast intro: validTransition)
        
          from validP' obtain P'' where P''hnf: "uhnf P''" and validP'': "valid P''"
                                    and P''eqP': "P'' ≡⇩e P'" and P''depth: "depth P'' ≤ depth P'"
            by(blast dest: validToHnf)
          
          from validQ' obtain Q'' where Q''hnf: "uhnf Q''" and validQ'': "valid Q''"
                                    and Q''eqQ': "Q'' ≡⇩e Q'" and Q'''depth: "depth Q'' ≤ depth Q'"
            by(blast dest: validToHnf)
            
          have "depth P'' + depth Q'' ≤ n"
          proof -
            from Phnf PTrans have "depth P' < depth P"
              by(force intro: depthTransition simp add: uhnf_def)
            moreover from Qhnf QTrans have "depth Q' < depth Q" 
              by(force intro: depthTransition simp add: uhnf_def)
            ultimately show ?thesis using PQdepth P''depth Q'''depth by simp
          qed
            
          moreover have "P'' ∼ Q''"
          proof -
            from P''eqP' have "P'' ∼ P'" by(rule sound)
            moreover from Q''eqQ' have "Q'' ∼ Q'" by(rule sound)
            ultimately show ?thesis using P'BisimQ' by(blast dest: transitive symmetric)
          qed
          ultimately have "P'' ≡⇩e Q''" using validP'' validQ'' P''hnf Q''hnf by(rule_tac IH)
          with P''eqP' Q''eqQ' show ?thesis by(blast intro: Sym Trans)
        qed
        thus ?thesis by(rule OutputPres)
      qed
      ultimately show ?case using Q'eqQ'' by(blast intro: Sym equiv.ResPres)
    next
      case(Bang P' P)
      have "!P' ∈ summands Q" by fact
      hence False by(nominal_induct Q rule: pi.strong_inducts, auto simp add: if_split) 
      thus ?case by simp
    qed
  qed

  from Phnf Qhnf PQdepth validP validQ PBisimQ show ?case
    apply(rule_tac summandEquiv, auto)
    apply(rule Goal)
    apply auto
    apply(blast dest: bisimE symmetric)
    by(blast intro: Goal dest: bisimE)
qed

lemma complete: 
  fixes P :: pi
  and   Q :: pi

  assumes validP: "valid P"
  and     validQ: "valid Q"
  and     PBisimQ: "P ∼ Q"

  shows "P ≡⇩e Q"
proof -
  from validP obtain P' where validP': "valid P'" and P'hnf: "uhnf P'" and P'eqP: "P' ≡⇩e P"
    by(blast dest: validToHnf)
  from validQ obtain Q' where validQ': "valid Q'" and Q'hnf: "uhnf Q'" and Q'eqQ: "Q' ≡⇩e Q"
    by(blast dest: validToHnf)
  
  have "∃n. depth P' + depth Q' ≤ n" by auto
  then obtain n where "depth P' + depth Q' ≤ n" by blast
  moreover have "P' ∼ Q'"
  proof -
    from P'eqP have "P' ∼ P" by(rule sound)
    moreover from Q'eqQ have "Q' ∼ Q" by(rule sound)
    ultimately show ?thesis using PBisimQ by(blast intro: symmetric transitive)
  qed
  ultimately have "P' ≡⇩e Q'" using validP' validQ' P'hnf Q'hnf by(rule_tac completeAux)
  with P'eqP Q'eqQ show ?thesis by(blast intro: Sym Trans)
qed

end