Theory Diagrams

theory Diagrams
imports HBDAlgebra
subsection{*Diagrams with Named Inputs and Outputs*}

(* Was: DiagramFeedbackless.thy *)

theory Diagrams imports HBDAlgebra
begin 
  
text{*This file contains the definition and properties for the named input output diagrams*}
  

record ('var, 'a) Dgr = 
    In:: "'var list"
    Out:: "'var list"
    Trs:: 'a
    
context BaseOperationFeedbacklessVars
begin
definition "Var A B = (Out A) ⊗ (In B)"

definition "io_diagram A = (TVs (In A) = TI (Trs A) ∧ TVs (Out A) = TO (Trs A) ∧ distinct (In A) ∧ distinct (Out A))"

definition  Comp :: "('var, 'a) Dgr ⇒ ('var, 'a) Dgr ⇒ ('var, 'a) Dgr"  (infixl ";;" 70) where
  "A ;; B = (let I = In B ⊖ Var A B in let O' = Out A ⊖ Var A B in
    ⦇In = (In A) ⊕ I, Out = O' @ Out B, 
    Trs = [(In A) ⊕ I ↝ In A @ I ] oo Trs A ∥ [I ↝ I] oo [Out A @ I ↝ O' @ In B]  oo ([O' ↝ O'] ∥ Trs B) ⦈)"

lemma io_diagram_Comp: "io_diagram A ⟹ io_diagram B
        ⟹ set (Out A ⊖ In B) ∩ set (Out B) = {} ⟹ io_diagram (A ;; B)"
  by (auto simp add: io_diagram_def Comp_def Let_def Var_def addvars_def set_diff set_inter)
        
lemma Comp_in_disjoint: 
  assumes "io_diagram A"
    and "io_diagram B"
    and "set (In A) ∩ set (In B) = {}"
    shows "A ;; B = (let I = In B ⊖ Var A B in let O' = Out A ⊖ Var A B in
      ⦇In = (In A) @ I, Out = O' @ Out B, Trs = Trs A ∥ [I ↝ I] oo [Out A @ I ↝ O' @ In B]  oo ([O' ↝ O'] ∥ Trs B) ⦈)"
proof -
  have [simp]: "In A ⊕ (In B ⊖ Var A B) = In A @ (In B ⊖ Var A B)"
    by (metis addvars_def assms(3) diff_emptyset diff_inter_right empty_inter_diff)
  have [simp]: "[In A @ (In B ⊖ Var A B) ↝ In A @ (In B ⊖ Var A B)] = ID (TVs (In A) @ TVs (In B ⊖ Var A B))"
    apply (subst distinct_id, simp_all)
    by (metis ‹In A ⊕ (In B ⊖ Var A B) = In A @ (In B ⊖ Var A B)› assms(1) assms(2) distinct_addvars distinct_append distinct_diff io_diagram_def)
      
  have [simp]: "TI (Trs A) = TVs (In A)"
    using assms(1) io_diagram_def by force       
  show ?thesis
    by (simp add: Comp_def Let_def)
qed

lemma Comp_full: "io_diagram A ⟹ io_diagram B ⟹ Out A = In B ⟹
  A ;; B = ⦇In = In A, Out = Out B, Trs = Trs A oo Trs B ⦈"
  by (simp_all add: Comp_def Let_def Var_def io_diagram_def diff_inter_left diff_eq addvars_def  par_empty_left par_empty_right)

lemma Comp_in_out: "io_diagram A ⟹ io_diagram B ⟹ set (Out A) ⊆ set (In B) ⟹
  A ;; B = (let I = diff (In B) (Var A B) in let O' = diff (Out A) (Var A B) in
          ⦇In = In A ⊕ I, Out = Out B, Trs = [In A ⊕ I ↝ In A @ I ] oo Trs A ∥ [I ↝ I] oo [Out A @ I ↝ In B] oo Trs B ⦈)"
  by (simp add: Comp_def Let_def Var_def diff_inter_left diff_inter_right diff_subset par_empty_left)

  
lemma Comp_assoc_new: "io_diagram A ⟹ io_diagram B ⟹ io_diagram C ⟹
          set (Out A ⊖ In B) ∩ set (Out B) = {} ⟹  set (Out A ⊗ In B) ∩ set (In C) = {}
          ⟹ A ;; B ;; C = A ;; (B ;; C)"
proof -
            assume [simp]: "io_diagram A"
            assume [simp]: "io_diagram B"
            assume [simp]: "io_diagram C"
            assume U: "set (Out A ⊖ In B) ∩ set (Out B) = {}"
            assume V: " set (Out A ⊗ In B) ∩ set (In C) = {}"
            have A: "In A ⊕ (In B ⊖ Out A ⊗ In B) ⊕ (In C ⊖ (Out A ⊖ Out A ⊗ In B) @ Out B ⊗ In C) = In A ⊕ (In B ⊕ (In C ⊖ Out B ⊗ In C) ⊖ Out A ⊗ (In B ⊕ (In C ⊖ Out B ⊗ In C)))"
             apply (simp add: diff_inter_left diff_inter_right)
             apply (simp add: addvars_def union_diff diff_union diff_cancel)
             apply (subst diff_sym [THEN sym])
             apply (subst (2) diff_sym [THEN sym])
             apply (subst ZZZ_b)
             using V apply (auto simp add: set_inter set_diff) [1]
             by (simp add: diff_sym)

            have B: "((Out A ⊖ Out A ⊗ In B) @ Out B ⊖ (Out A ⊖ Out A ⊗ In B) @ Out B ⊗ In C) = (Out A ⊖ Out A ⊗ (In B ⊕ (In C ⊖ Out B ⊗ In C))) @ (Out B ⊖ Out B ⊗ In C)"
              using U by (simp add: diff_inter_left diff_inter_right addvars_def union_diff diff_union diff_cancel diff_notin)

          define x where "x ≡ In A"
          define u where "u ≡ Out A"
          define y where "y ≡ In B"
          define v where "v ≡ Out B"
          define z where "z ≡ In C"
          define w where "w ≡ Out C"

          have [simp]: "TI (Trs A) = TVs x"
            by (metis ‹io_diagram A› io_diagram_def x_def)

          have [simp]: "TI (Trs B) = TVs y"
            by (metis ‹io_diagram B› io_diagram_def y_def)

          have [simp]: "TO (Trs A) = TVs u"
            by (metis ‹io_diagram A› io_diagram_def u_def)

          have [simp]: "distinct x"
           by (metis ‹io_diagram A› io_diagram_def x_def)

          have [simp]: "distinct u"
           by (metis ‹io_diagram A› io_diagram_def u_def)

          have [simp]: "distinct y"
           by (metis ‹io_diagram B› io_diagram_def y_def)

          have [simp]: "distinct z"
           by (metis ‹io_diagram C› io_diagram_def z_def)

          have [simp]: "distinct (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z)"
            by (simp add: )

          have [simp]: "distinct (x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))))"
            by (simp add: distinct_addvars )

          have [simp]: "distinct (x ⊕ (y ⊖ u ⊗ y))"
            by (simp add: distinct_addvars )

          have [simp]: "set (x ⊕ (y ⊖ u ⊗ y)) ⊆ set (x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))))"
            apply (simp add: set_addvars set_diff set_inter)
            by blast

          have [simp]: "set (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z) ⊆ set (x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))))"
            apply (simp add: diff_inter_left diff_inter_right diff_union addvars_minus set_addvars)
            apply (subgoal_tac "set (z ⊖ (u ⊖ y) ⊖ v) ⊆ set (z ⊖ v ⊖ u)")
            apply blast
            apply (subst diff_sym)
            apply (simp add: set_diff)
            by (metis diff_cancel_set Int_ac(3) V diff_inter_left eq_iff set_diff u_def y_def z_def)

          have [simp]: "set x ⊆ set (x ⊕ (y ⊖ u ⊗ y)) ∧ set (y ⊖ u ⊗ y) ⊆ set (x ⊕ (y ⊖ u ⊗ y))"
            by (simp add: set_addvars set_diff set_inter)

          have [simp]: "distinct (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)))"
            by (simp add: distinct_addvars )
            
          have [simp]: "set u ∩ set (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) = {}"
            by (simp add: set_diff set_inter set_addvars, auto)
            
          have [simp]: "distinct (y ⊕ (z ⊖ v ⊗ z))"
            by (simp add: distinct_addvars )
            
          have [simp]: "set (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ⊆ set u ∪ set (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)))"
            by (simp add: set_diff set_inter set_addvars, auto)
          have [simp]: "set (y ⊕ (z ⊖ v ⊗ z)) ⊆ set u ∪ set (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)))"
            by (simp add: set_diff set_inter set_addvars, auto)
          have [simp]: "set y ⊆ set (y ⊕ (z ⊖ v ⊗ z))"
            by (simp add: set_diff set_inter set_addvars)
            
          have [simp]: "set (z ⊖ v ⊗ z) ⊆ set (y ⊕ (z ⊖ v ⊗ z))"
            by (simp add: set_diff set_inter set_addvars)

          have [simp]: "TO (Trs B) = TVs v"
            by (metis ‹io_diagram B› io_diagram_def v_def)
          have [simp]: " TI (Trs C) = TVs z"
            by (metis ‹io_diagram C› io_diagram_def z_def)

          have "[x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ (x ⊕ (y ⊖ u ⊗ y)) @ (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z)] oo
              ([x ⊕ (y ⊖ u ⊗ y) ↝ x @ (y ⊖ u ⊗ y)] oo Trs A ∥ [y ⊖ u ⊗ y ↝ y ⊖ u ⊗ y] oo [u @ (y ⊖ u ⊗ y) ↝ (u ⊖ u ⊗ y) @ y] oo [u ⊖ u ⊗ y ↝ u ⊖ u ⊗ y] ∥ Trs B) ∥
              [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z] oo
              [(u ⊖ u ⊗ y) @ v @ (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z) @ z] oo
              [(u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z)] ∥ Trs C
              = 
              [x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ (x ⊕ (y ⊖ u ⊗ y)) @ (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z)] oo
              ([x ⊕ (y ⊖ u ⊗ y) ↝ x @ (y ⊖ u ⊗ y)] ∥ [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z]
              oo Trs A ∥ [y ⊖ u ⊗ y ↝ y ⊖ u ⊗ y] ∥ [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z]
              oo [u @ (y ⊖ u ⊗ y) ↝ (u ⊖ u ⊗ y) @ y] ∥ [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z]
              oo [u ⊖ u ⊗ y ↝ u ⊖ u ⊗ y] ∥ Trs B ∥ [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z]) oo
              [(u ⊖ u ⊗ y) @ v @ (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z) @ z] oo
              [(u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z)] ∥ Trs C" (is "?Tx = _")

          apply (subst comp_parallel_distrib, simp_all)
          apply (subst comp_parallel_distrib, simp_all )
            by (subst comp_parallel_distrib, simp_all)
               
          also have "... = [x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ (x ⊕ (y ⊖ u ⊗ y)) @ (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z)] oo
              [x ⊕ (y ⊖ u ⊗ y) ↝ x @ (y ⊖ u ⊗ y)] ∥ [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z]
              oo Trs A ∥ [y ⊖ u ⊗ y ↝ y ⊖ u ⊗ y] ∥ [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z]
              oo [u @ (y ⊖ u ⊗ y) ↝ (u ⊖ u ⊗ y) @ y] ∥ [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z]
              oo [u ⊖ u ⊗ y ↝ u ⊖ u ⊗ y] ∥ Trs B ∥ [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z] oo
              [(u ⊖ u ⊗ y) @ v @ (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z) @ z] oo
              [(u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z)] ∥ Trs C"
           by (simp add: comp_assoc )

           also have "... = [x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝x @ (y ⊖ u ⊗ y) @ (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z)]
              oo Trs A ∥ [y ⊖ u ⊗ y ↝ y ⊖ u ⊗ y] ∥ [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z]
              oo [u @ (y ⊖ u ⊗ y) ↝ (u ⊖ u ⊗ y) @ y] ∥ [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z]
              oo [u ⊖ u ⊗ y ↝ u ⊖ u ⊗ y] ∥ Trs B ∥ [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z] oo
              [(u ⊖ u ⊗ y) @ v @ (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z) @ z] oo
              [(u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z)] ∥ Trs C"
           by (subst switch_par_comp, simp_all)

           also have "... = [x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝x @ (y ⊖ u ⊗ y) @ (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z)]
              oo Trs A ∥ [y ⊖ u ⊗ y ↝ y ⊖ u ⊗ y] ∥ [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z]
              oo ([u @ (y ⊖ u ⊗ y) ↝ (u ⊖ u ⊗ y) @ y] ∥ [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z]
              oo [u ⊖ u ⊗ y ↝ u ⊖ u ⊗ y] ∥ Trs B ∥ [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z] oo
              [(u ⊖ u ⊗ y) @ v @ (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z) @ z] oo
              [(u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z)] ∥ Trs C)" (is "_ = ?Ty")
           by (simp add: comp_assoc  )

          finally have E: "?Tx = ?Ty"
            by simp

          thm comp_parallel_distrib

          have [simp]: "distinct (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) )"
            by (simp add: diff_inter_left diff_inter_right)

          have "[x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ x @ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)))] 
              oo Trs A ∥ [y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] oo
              [u @ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (y ⊕ (z ⊖ v ⊗ z))] oo
              [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥
              ([y ⊕ (z ⊖ v ⊗ z) ↝ y @ (z ⊖ v ⊗ z)] oo Trs B ∥ [z ⊖ v ⊗ z ↝ z ⊖ v ⊗ z] oo [v @ (z ⊖ v ⊗ z) ↝ (v ⊖ v ⊗ z) @ z] oo [v ⊖ v ⊗ z ↝ v ⊖ v ⊗ z] ∥ Trs C)
              = 
                [x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ x @ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)))] 
                oo Trs A ∥ [y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] oo
                [u @ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (y ⊕ (z ⊖ v ⊗ z))] oo
                  ([u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥ [y ⊕ (z ⊖ v ⊗ z) ↝ y @ (z ⊖ v ⊗ z)] oo 
                  [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥ (Trs B ∥ [z ⊖ v ⊗ z ↝ z ⊖ v ⊗ z]) oo 
                  [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥ [v @ (z ⊖ v ⊗ z) ↝ (v ⊖ v ⊗ z) @ z] oo 
                  [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥ ([v ⊖ v ⊗ z ↝ v ⊖ v ⊗ z] ∥ Trs C))" (is "?Ta = _")

          apply (subst comp_parallel_distrib, simp_all)
          apply (subst comp_parallel_distrib, simp_all )
          by (subst comp_parallel_distrib, simp_all )

          also have "... =  [x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ x @ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)))] 
                oo Trs A ∥ [y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] oo
                  ([u @ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (y ⊕ (z ⊖ v ⊗ z))] oo
                  [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥ [y ⊕ (z ⊖ v ⊗ z) ↝ y @ (z ⊖ v ⊗ z)]) oo 
                  [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥ (Trs B ∥ [z ⊖ v ⊗ z ↝ z ⊖ v ⊗ z]) oo 
                  [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥ [v @ (z ⊖ v ⊗ z) ↝ (v ⊖ v ⊗ z) @ z] oo 
                  [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥ ([v ⊖ v ⊗ z ↝ v ⊖ v ⊗ z] ∥ Trs C)"
           by (simp add: comp_assoc  )

           also have "... = [x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ x @ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)))] 
                oo Trs A ∥ [y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] oo
                  [u @ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (y @ (z ⊖ v ⊗ z))] oo
                  [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥ (Trs B ∥ [z ⊖ v ⊗ z ↝ z ⊖ v ⊗ z]) oo 
                  [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥ [v @ (z ⊖ v ⊗ z) ↝ (v ⊖ v ⊗ z) @ z] oo 
                  [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥ ([v ⊖ v ⊗ z ↝ v ⊖ v ⊗ z] ∥ Trs C)"
           by (subst switch_par_comp, simp_all)

           also have "... = [x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ x @ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)))] 
                oo Trs A ∥ [y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] oo
                  ([u @ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (y @ (z ⊖ v ⊗ z))] oo
                  [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥ Trs B ∥ [z ⊖ v ⊗ z ↝ z ⊖ v ⊗ z] oo 
                  [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥ [v @ (z ⊖ v ⊗ z) ↝ (v ⊖ v ⊗ z) @ z] oo 
                  [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥ [v ⊖ v ⊗ z ↝ v ⊖ v ⊗ z] ∥ Trs C)" (is "_ = ?Tb")
           by (simp add: comp_assoc par_assoc  )

          finally have F: "?Ta = ?Tb"
            by simp


          have [simp]: "distinct  (z ⊖ (u ⊖ y) @ v)"
            by (metis ‹distinct (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z)› diff_inter_left diff_inter_right)


          define z' where "z' ≡ newvars (y ⊖ u) (TVs (z ⊖ (u ⊖ y) @ v))"

          have [simp]: "distinct (x ⊕ (y ⊕ (z ⊖ v) ⊖ u))"
            by (metis ‹distinct (x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))))› diff_inter_right)
          have "distinct (y ⊖ u)"
            by (simp add: )

          have [simp]: "distinct z'"
            by (simp add: z'_def)

          have [simp]: "set (y ⊖ u) ∩ set z' = {}"
            by (simp add: z'_def)

          have [simp]: "distinct (y ⊕ (z ⊖ v) ⊖ u)"
            by (simp add:  distinct_addvars)

          have [simp]: "TVs (z ⊖ (u ⊖ y) @ v) = TVs z'"
            by (simp add: z'_def)

          have [simp]:"set x ⊆ set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u))"
            by (simp add: set_diff set_inter set_addvars)
            
          have [simp]:"set (y ⊖ u) ⊆ set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u))"
            by (simp add: set_diff set_inter set_addvars, auto)
          
          have [simp]:"set (z ⊖ (u ⊖ y) @ v) ⊆ set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u))"
            by (metis ‹set (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z) ⊆ set (x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))))› diff_inter_left diff_inter_right)

          have [simp]:"set (y ⊕ (z ⊖ v) ⊖ u) ⊆ set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u))"
            by (simp add: set_addvars)

          have [simp]: "distinct (y ⊖ u)"
            by (simp add: )

          have H: "Trs A ∥ [y ⊖ u ↝ y ⊖ u] ∥ [z ⊖ (u ⊖ y) @ v ↝ z ⊖ (u ⊖ y) @ v] = Trs A ∥ [(y ⊖ u) @ z' ↝ (y ⊖ u) @ z']"
            by (simp add: par_assoc distinct_id)

          define u' where "u' ≡ newvars (x @ y @ z @ v) (TVs u)"

          have b: "set (x @ y @ z @ v) ∩ set u' = {}"
            by (simp add: u'_def del: set_append)
            

          have [simp]: "distinct u'"
            by (simp add: u'_def)
          from b have [simp]: "set u' ∩ set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u)) = {}"
            by (simp add: set_addvars set_diff, auto)
          have [simp]: "set u ∩ set (y ⊕ (z ⊖ v) ⊖ u) = {}"
            by (metis ‹set u ∩ set (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) = {}› diff_inter_right)
          have [simp]: "TVs u' = TVs u"
            by (simp add: u'_def)

 
          have Ha: "[u ↝ u] ∥ [x ⊕ (y ⊕ (z ⊖ v) ⊖ u) ↝ (y ⊖ u) @ (z ⊖ (u ⊖ y) @ v)] =  [u' @ (x ⊕ (y ⊕ (z ⊖ v) ⊖ u)) ↝ u' @ ((y ⊖ u) @ (z ⊖ (u ⊖ y) @ v))]"
            proof -
            have "[u ↝ u] ∥ [x ⊕ (y ⊕ (z ⊖ v) ⊖ u) ↝ (y ⊖ u) @ (z ⊖ (u ⊖ y) @ v)] = [u' ↝ u'] ∥ [x ⊕ (y ⊕ (z ⊖ v) ⊖ u) ↝ (y ⊖ u) @ (z ⊖ (u ⊖ y) @ v)]"
              by (simp add: par_assoc distinct_id)
            also have "... = [u' @ (x ⊕ (y ⊕ (z ⊖ v) ⊖ u)) ↝ u' @ ((y ⊖ u) @ (z ⊖ (u ⊖ y) @ v))]"
              by (simp add: par_switch)
            finally show ?thesis by simp
            qed
       
          have Hb: "[u ↝ u] ∥ [x ⊕ (y ⊕ (z ⊖ v) ⊖ u) ↝ y ⊕ (z ⊖ v) ⊖ u] = [u' @ (x ⊕ (y ⊕ (z ⊖ v) ⊖ u)) ↝ u' @ (y ⊕ (z ⊖ v) ⊖ u)]"
            proof -
            have "[u ↝ u] ∥ [x ⊕ (y ⊕ (z ⊖ v) ⊖ u) ↝ y ⊕ (z ⊖ v) ⊖ u] = [u' ↝ u'] ∥ [x ⊕ (y ⊕ (z ⊖ v) ⊖ u) ↝ y ⊕ (z ⊖ v) ⊖ u]"
              by (simp add: par_assoc distinct_id)
            also have "... =  [u' @ (x ⊕ (y ⊕ (z ⊖ v) ⊖ u)) ↝ u' @ (y ⊕ (z ⊖ v) ⊖ u)]"
              by (simp add: par_switch)
            finally show ?thesis by simp
            qed

         have [simp]: " Subst (z ⊖ (u ⊖ y) @ v) (z ⊖ (u ⊖ y) @ v) (z ⊖ (u ⊖ y) @ v) = (z ⊖ (u ⊖ y) @ v)"
          by (simp add: Subst_eq)

         have [simp]: "Subst (u @ (y ⊖ u)) (u' @ (y ⊖ u)) ((u ⊖ y) @ y) = Subst u u' (u ⊖ y) @ Subst u u' y"
          apply (simp add: Subst_append, safe)
          apply (subst Subst_cancel_left, simp_all)
          apply (rule TVs_length_eq, simp)
          apply (subst Subst_cancel_left, simp_all)
          by (rule TVs_length_eq, simp)
        
         have Hc: "[u' @ (x ⊕ (y ⊕ (z ⊖ v) ⊖ u)) ↝ u' @ (y ⊖ u) @ (z ⊖ (u ⊖ y) @ v)] oo [u @ (y ⊖ u) ↝ (u ⊖ y) @ y] ∥ [z ⊖ (u ⊖ y) @ v ↝ z ⊖ (u ⊖ y) @ v]
          = [u' @ (x ⊕ (y ⊕ (z ⊖ v) ⊖ u)) ↝ Subst u u' (u ⊖ y) @ Subst u u' y @ (z ⊖ (u ⊖ y) @ v)]"
            apply (subst append_assoc [THEN sym])
            apply (subst switch_par_comp_Subst, simp_all)
            apply (simp_all add: set_diff set_addvars )
            apply auto
            using  V  by (auto simp add: set_inter set_diff u_def y_def x_def v_def z_def) [1]

         have [simp]: "Subst (u @ (y ⊕ (z ⊖ v) ⊖ u)) (u' @ (y ⊕ (z ⊖ v) ⊖ u)) ((u ⊖ y ⊕ (z ⊖ v)) @ y @ (z ⊖ v)) 
            = Subst u  u' ((u ⊖ y ⊕ (z ⊖ v)) @ y @ (z ⊖ v))"
          apply (subst Subst_cancel_left, simp_all)
          by (rule TVs_length_eq, simp)

         thm par_switch_eq_a

         have J: "[u ⊖ (y ⊕ (z ⊖ v)) ↝ u ⊖ (y ⊕ (z ⊖ v))] ∥ [v ⊖ z ↝ v ⊖ z] =  [(u ⊖ (y ⊕ (z ⊖ v))) @ (v ⊖ z) ↝ (u ⊖ (y ⊕ (z ⊖ v))) @ (v ⊖ z)]"
          apply (subst par_switch, simp_all, safe)
          using ‹io_diagram B› distinct_diff io_diagram_def v_def apply blast
          apply (simp add: set_diff set_addvars set_inter, auto)
          using U by (auto simp add: set_inter set_diff u_def y_def v_def z_def) [1]

         have [simp]: "distinct v"
          using ‹io_diagram B› io_diagram_def v_def by blast

         have [simp]: "distinct (z ⊖ v)"
          by (simp add: )

         have [simp]: "distinct (u ⊖ y)"
          by (simp add: )

         have [simp]: "distinct (u ⊖ (y ⊕ (z ⊖ v)))"
          by (simp add: )

          have [simp]: "length u' = length u"
            by (rule TVs_length_eq, simp)

         have [simp]: "set (Subst u u' (u ⊖ y)) ⊆ set u' ∪ set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u))"
          by (rule set_SubstI, simp_all add: set_diff set_addvars, auto)

         have [simp]: "set (Subst u u' y) ⊆ set u' ∪ set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u))"
          by (rule set_SubstI, simp_all add: set_diff set_addvars, auto)

        have [simp]: "set (z ⊖ (u ⊖ y) @ v) ⊆ set u' ∪ set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u))"
          apply (simp add: set_diff set_addvars, auto)
          using  V  by (auto simp add: set_inter set_diff u_def y_def x_def v_def z_def) [1]

        have [simp]: "set (Subst u u' (u ⊖ (y ⊕ (z ⊖ v)))) ⊆ set u' ∪ set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u))"
          by (rule set_SubstI, simp_all add: set_diff set_addvars, auto)
        
        have [simp]: "set (Subst u u' (z ⊖ v)) ⊆ set u' ∪ set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u))"
          by (rule set_SubstI, simp_all add: set_diff set_addvars, auto)

         define v' where "v' ≡ newvars (u' @ u @ x @ y @ z) (TVs v)"  

         have [simp]: "distinct v'"
          by (simp add: v'_def)

        have a: "set (u' @ u @ x @ y @ z) ∩ set v' = {}"
          by (simp add: v'_def del: set_append)

        from this have [simp]: "set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u)) ∩ set v' = {}"
          by (simp add: set_diff set_addvars, auto)
          

         from a have [simp]: "set u' ∩ set v' = {}"
          by auto

         have [simp]: "TVs v' = TVs v"
          by (simp add: v'_def)

         have [simp]: "set (Subst u u' (u ⊖ (y ⊕ (z ⊖ v)))) ⊆ set u' ∪ (set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u)) ∪ set v')"
          by (rule set_SubstI, simp_all add: set_diff set_addvars, auto)

          have [simp]: " set v' ⊆ set u' ∪ (set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u)) ∪ set v')"
            by auto

         have [simp]: "set (Subst u u' (z ⊖ v)) ⊆ set u' ∪ (set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u)) ∪ set v')"
          by (rule set_SubstI, simp_all add: set_diff set_addvars, auto)

          thm Subst_Subst_a
          thm Subst_Subst
         have [simp]: "length v' = length v"
          by (rule TVs_length_eq, simp)

         have [simp]: "set v ∩ set (u ⊖ (y ⊕ (z ⊖ v))) = {}"
          using U by (auto simp add: set_inter set_diff set_addvars u_def y_def x_def v_def z_def) [1]

        thm Subst_not_in

        thm Subst_Subst

      have "set (u ⊖ y) ⊆ set (u ⊖ v)"
        using U by (auto simp add: set_inter set_diff set_addvars u_def y_def x_def v_def z_def) [1]
            

       have Ka:"Subst ((u ⊖ y) @ v) (Subst u u' (u ⊖ y) @ v') z = Subst ((u ⊖ y ⊖ v) @ v) (Subst u u' (u ⊖ y ⊖ v) @ v') z"
        apply (subgoal_tac "(u ⊖ y ⊖ v) = (u ⊖ y)")
        apply simp
        apply (rule diff_disjoint)
        using U by (auto simp add: set_inter set_diff set_addvars u_def y_def x_def v_def z_def) [1]

      from a have [simp]: "set v' ∩ set (z ⊖ v) = {}"
        by (simp add: set_diff set_addvars, auto)

      from a have [simp]: " set v' ∩ set (u ⊖ y ⊖ v) = {}"
       by  (simp add: set_diff set_addvars, auto)

      have [simp]: "set (Subst u u' (z ⊖ v)) ∩ set v = {}"
        apply (subgoal_tac "set (Subst u u' (z ⊖ v)) ⊆ - set v")
        apply auto [1]
        apply (rule set_SubstI, simp_all add: set_diff)
        using b by auto
 
      have [simp]: "set (Subst u u' (u ⊖ y ⊖ v)) ∩ set v = {}"
        apply (subgoal_tac "set (Subst u u' (u ⊖ y ⊖ v)) ⊆ - set v")
        apply auto [1]
        apply (rule set_SubstI, simp_all add: set_diff)
        using b by auto

      have [simp]: "set u ∩ set y ∩ set z = {}"
        using V by (auto simp add: set_inter set_diff set_addvars u_def y_def x_def v_def z_def) [1]
  
      have Kb: "Subst (v @ (z ⊖ v)) (v' @ Subst u u' (z ⊖ v)) z = Subst (v @ (u ⊖ y ⊖ v)) (v' @ Subst u u' (u ⊖ y ⊖ v)) z"
        apply (subst Subst_switch, simp_all)
        apply (subst Subst_comp, simp_all)
        apply (simp add: set_diff)
        apply auto [1]
        apply (subst Comp_assoc_new_subst_aux [of _ y], simp_all)

        apply (subst Subst_switch, simp_all)
        apply (subst Subst_comp, simp_all)
        by (auto simp add: set_diff) [1]

         have K: "Subst ((u ⊖ y) @ v @ (z ⊖ (u ⊖ y) @ v)) (Subst u u' (u ⊖ y) @ v' @ (z ⊖ (u ⊖ y) @ v)) ((u ⊖ (y ⊕ (z ⊖ v))) @ (v ⊖ z) @ z)
            = Subst u u' (u ⊖ (y ⊕ (z ⊖ v))) @ Subst (v @ (z ⊖ v)) (v' @ Subst u u' (z ⊖ v)) ((v ⊖ z) @ z)"
            apply (simp add: Subst_append, safe)
            apply (unfold append_assoc [THEN sym])
            apply (subst Subst_cancel_left)
            apply (auto simp add: set_diff) [2]
            apply (subst Subst_not_in, simp_all)
            apply (subst Subst_Subst, simp_all)
            apply (simp add: set_diff set_addvars, auto)

            apply (unfold append_assoc [THEN sym])
            apply (subst Subst_not_in, simp_all)
            apply (simp add: set_diff, auto)

            apply (subst (2) Subst_not_in, simp_all)
            apply (simp add: set_diff, auto)
            apply (subst Subst_not_in_a, simp_all)
            apply (simp add: set_diff, auto)
            using U apply (auto simp add: set_inter set_diff set_addvars u_def y_def x_def v_def z_def) [1]


            apply (unfold append_assoc [THEN sym])
            apply (subst Subst_cancel_left)
            apply (auto simp add: set_diff) [2]
            apply (simp add: Ka Kb)
            apply (subst Subst_switch, simp_all)
            by (simp add: set_diff, auto)
 
         have I: "[u' @ (x ⊕ (y ⊕ (z ⊖ v) ⊖ u)) ↝ Subst u u' (u ⊖ y) @ Subst u u' y @ (z ⊖ (u ⊖ y) @ v)] oo [u ⊖ y ↝ u ⊖ y] ∥ Trs B ∥ [z ⊖ (u ⊖ y) @ v ↝ z ⊖ (u ⊖ y) @ v] oo
            [(u ⊖ y) @ v @ (z ⊖ (u ⊖ y) @ v) ↝ (u ⊖ (y ⊕ (z ⊖ v))) @ (v ⊖ z) @ z]
             =
            [u' @ (x ⊕ (y ⊕ (z ⊖ v) ⊖ u)) ↝ Subst u u' (u ⊖ (y ⊕ (z ⊖ v))) @ Subst u u' y @ Subst u u' (z ⊖ v)] oo [u ⊖ (y ⊕ (z ⊖ v)) ↝ u ⊖ (y ⊕ (z ⊖ v))] ∥ Trs B ∥ [z ⊖ v ↝ z ⊖ v] oo
            [u ⊖ (y ⊕ (z ⊖ v)) ↝ u ⊖ (y ⊕ (z ⊖ v))] ∥ [v @ (z ⊖ v) ↝ (v ⊖ z) @ z]"
          apply (rule_tac v = v' in par_switch_eq_a, simp_all add:  )
           apply (subst switch_comp_subst, simp_all) 
             (*
          apply (simp add: set_diff)
          using U  apply (simp add: v_def u_def z_def y_def set_diff set_inter set_addvars)*)
          apply auto [1]
          apply safe         
          apply (meson UnE ‹set (Subst u u' (u ⊖ y)) ⊆ set u' ∪ set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u))› subsetCE)
          using ‹set (z ⊖ (u ⊖ y) @ v) ⊆ set (x ⊕ (y ⊕ (z ⊖ v) ⊖ u))› apply blast
          using U V apply (simp add: v_def u_def z_def y_def set_diff set_inter set_addvars)
          using U V apply (simp add: v_def u_def z_def y_def set_diff set_inter set_addvars)
          using U V apply (simp add: v_def u_def z_def y_def set_diff set_inter set_addvars)
          apply (subst switch_par_comp_Subst)
          apply (simp_all add: set_diff)
          by (simp add: K)

         have "?Ty = ?Tb"
            apply (simp add: diff_inter_left diff_inter_right H)
            apply (rule par_switch_eq, simp_all add:  )
            apply (simp add: comp_assoc [THEN sym]  )
            apply (simp add: Ha Hb Hc)
            apply (subst switch_comp_subst, simp_all)         
            apply (simp add: le_supI2)
            apply (metis ‹set (u ⊖ (u ⊗ (y ⊕ (z ⊖ v ⊗ z)))) ⊆ set u ∪ set (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)))› ‹set (y ⊕ (z ⊖ v ⊗ z)) ⊆ set u ∪ set (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)))› ‹set (z ⊖ v ⊗ z) ⊆ set (y ⊕ (z ⊖ v ⊗ z))› ‹set y ⊆ set (y ⊕ (z ⊖ v ⊗ z))› diff_inter_left diff_inter_right subset_trans)
            apply (simp add: Subst_append)
            using I apply (simp add: comp_assoc  )
            apply (subst J)

            by (simp add: J)


         from this E and F have " [x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ (x ⊕ (y ⊖ u ⊗ y)) @ (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z)] oo
              ([x ⊕ (y ⊖ u ⊗ y) ↝ x @ (y ⊖ u ⊗ y)] oo Trs A ∥ [y ⊖ u ⊗ y ↝ y ⊖ u ⊗ y] oo [u @ (y ⊖ u ⊗ y) ↝ (u ⊖ u ⊗ y) @ y] oo [u ⊖ u ⊗ y ↝ u ⊖ u ⊗ y] ∥ Trs B) ∥
              [z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z ↝ z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z] oo
              [(u ⊖ u ⊗ y) @ v @ (z ⊖ (u ⊖ u ⊗ y) @ v ⊗ z) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z) @ z] oo
              [(u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (v ⊖ v ⊗ z)] ∥ Trs C 
              =
              [x ⊕ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ x @ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)))] oo Trs A ∥ [y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] oo
              [u @ (y ⊕ (z ⊖ v ⊗ z) ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) ↝ (u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))) @ (y ⊕ (z ⊖ v ⊗ z))] oo
              [u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z)) ↝ u ⊖ u ⊗ (y ⊕ (z ⊖ v ⊗ z))] ∥
              ([y ⊕ (z ⊖ v ⊗ z) ↝ y @ (z ⊖ v ⊗ z)] oo Trs B ∥ [z ⊖ v ⊗ z ↝ z ⊖ v ⊗ z] oo [v @ (z ⊖ v ⊗ z) ↝ (v ⊖ v ⊗ z) @ z] oo [v ⊖ v ⊗ z ↝ v ⊖ v ⊗ z] ∥ Trs C)"
          by simp


          from this have C: "[In A ⊕ (In B ⊕ (In C ⊖ Out B ⊗ In C) ⊖ Out A ⊗ (In B ⊕ (In C ⊖ Out B ⊗ In C))) ↝ (In A ⊕ (In B ⊖ Out A ⊗ In B)) @ (In C ⊖ (Out A ⊖ Out A ⊗ In B) @ Out B ⊗ In C)] oo
              ([In A ⊕ (In B ⊖ Out A ⊗ In B) ↝ In A @ (In B ⊖ Out A ⊗ In B)] oo Trs A ∥ [In B ⊖ Out A ⊗ In B ↝ In B ⊖ Out A ⊗ In B] oo [Out A @ (In B ⊖ Out A ⊗ In B) ↝ (Out A ⊖ Out A ⊗ In B) @ In B] oo
               [Out A ⊖ Out A ⊗ In B ↝ Out A ⊖ Out A ⊗ In B] ∥ Trs B) ∥
              [In C ⊖ (Out A ⊖ Out A ⊗ In B) @ Out B ⊗ In C ↝ In C ⊖ (Out A ⊖ Out A ⊗ In B) @ Out B ⊗ In C] oo
              [(Out A ⊖ Out A ⊗ In B) @ Out B @ (In C ⊖ (Out A ⊖ Out A ⊗ In B) @ Out B ⊗ In C) ↝ (Out A ⊖ Out A ⊗ (In B ⊕ (In C ⊖ Out B ⊗ In C))) @ (Out B ⊖ Out B ⊗ In C) @ In C] oo
              [(Out A ⊖ Out A ⊗ (In B ⊕ (In C ⊖ Out B ⊗ In C))) @ (Out B ⊖ Out B ⊗ In C) ↝ (Out A ⊖ Out A ⊗ (In B ⊕ (In C ⊖ Out B ⊗ In C))) @ (Out B ⊖ Out B ⊗ In C)] ∥ Trs C =
              [In A ⊕ (In B ⊕ (In C ⊖ Out B ⊗ In C) ⊖ Out A ⊗ (In B ⊕ (In C ⊖ Out B ⊗ In C))) ↝ In A @ (In B ⊕ (In C ⊖ Out B ⊗ In C) ⊖ Out A ⊗ (In B ⊕ (In C ⊖ Out B ⊗ In C)))] oo
              Trs A ∥ [In B ⊕ (In C ⊖ Out B ⊗ In C) ⊖ Out A ⊗ (In B ⊕ (In C ⊖ Out B ⊗ In C)) ↝ In B ⊕ (In C ⊖ Out B ⊗ In C) ⊖ Out A ⊗ (In B ⊕ (In C ⊖ Out B ⊗ In C))] oo
              [Out A @ (In B ⊕ (In C ⊖ Out B ⊗ In C) ⊖ Out A ⊗ (In B ⊕ (In C ⊖ Out B ⊗ In C))) ↝ (Out A ⊖ Out A ⊗ (In B ⊕ (In C ⊖ Out B ⊗ In C))) @ (In B ⊕ (In C ⊖ Out B ⊗ In C))] oo
              [Out A ⊖ Out A ⊗ (In B ⊕ (In C ⊖ Out B ⊗ In C)) ↝ Out A ⊖ Out A ⊗ (In B ⊕ (In C ⊖ Out B ⊗ In C))] ∥
              ([In B ⊕ (In C ⊖ Out B ⊗ In C) ↝ In B @ (In C ⊖ Out B ⊗ In C)] oo Trs B ∥ [In C ⊖ Out B ⊗ In C ↝ In C ⊖ Out B ⊗ In C] oo [Out B @ (In C ⊖ Out B ⊗ In C) ↝ (Out B ⊖ Out B ⊗ In C) @ In C] oo
               [Out B ⊖ Out B ⊗ In C ↝ Out B ⊖ Out B ⊗ In C] ∥ Trs C)"
             by (simp add: x_def [THEN symmetric] y_def [THEN symmetric] z_def [THEN symmetric] u_def [THEN symmetric] v_def [THEN symmetric] w_def [THEN symmetric])

          show "A ;; B ;; C = A ;; (B ;; C)"
            by (simp add: Comp_def Let_def Var_def A B C)
      qed

    lemma Comp_assoc_a: "io_diagram A ⟹ io_diagram B ⟹ io_diagram C ⟹
          set (In B) ∩ set (In C) = {} ⟹
          set (Out A) ∩ set (Out B) = {} ⟹
          A ;; B ;; C = A ;; (B ;; C)"
        apply (rule Comp_assoc_new, simp_all)
         apply (metis diff.simps(1) inter_diff_distrib set_empty2 set_inter)
        by (simp add: inf_assoc set_inter)

    (*to do too many conditions in next, replace with the theorem above*)
(*
    lemma Comp_assoc: "io_diagram A ⟹ io_diagram B ⟹ io_diagram C ⟹
          set (In A) ∩ set (In B) = {} ⟹ set (In B) ∩ set (In C) = {} ⟹ set (In A) ∩ set (In C) = {} ⟹
          set (Out A) ∩ set (Out B) = {} ⟹ set (Out B) ∩ set (Out C) = {} ⟹ set (Out A) ∩ set (Out C) = {} ⟹
          A ;; B ;; C = A ;; (B ;; C)"
      apply (rule Comp_assoc_new)
          apply simp
         apply simp
        apply simp
         apply (metis diff.simps(1) inter_diff_distrib set_empty2 set_inter)
        by (simp add: inf_assoc set_inter)
*)

definition Parallel :: "('var, 'a) Dgr ⇒ ('var, 'a) Dgr ⇒ ('var, 'a) Dgr"  (infixl "|||" 80) where
   "A ||| B = ⦇In = In A ⊕ In B, Out = Out A @ Out B, Trs = [In A ⊕ In B ↝ In A @ In B] oo (Trs A ∥ Trs B) ⦈"
       

      lemma io_diagram_Parallel: "io_diagram A ⟹ io_diagram B  ⟹ set (Out A) ∩ set (Out B) = {} ⟹ io_diagram (A ||| B)"
        by (simp add: io_diagram_def Parallel_def   distinct_addvars)

 
      lemma Parallel_indep: "io_diagram A ⟹ io_diagram B  ⟹ set (In A) ∩ set (In B) = {} ⟹
        A ||| B = ⦇In = In A @ In B, Out = Out A @ Out B, Trs = (Trs A ∥ Trs B) ⦈"
        apply (simp add: Parallel_def, safe)
        apply (simp add: addvars_def diff_distinct)
        apply (subgoal_tac "In A ⊕ In B = In A @ In B")
        apply simp
        apply (subst distinct_id)
        apply (simp add: io_diagram_def)
        apply (subst comp_id_left_simp)
        apply (simp add: io_diagram_def)
        apply simp
        by (simp add: addvars_def diff_distinct)


      lemma Parallel_assoc_gen: "io_diagram A ⟹ io_diagram B ⟹ io_diagram C ⟹ 
            A ||| B ||| C = A ||| (B ||| C)"
        proof -
          assume [simp]: "io_diagram A"
          assume [simp]: "io_diagram B"
          assume [simp]: "io_diagram C"

          have [simp]: "TVs (In A) = TI (Trs A)"
            apply (subgoal_tac "io_diagram A")
            apply (simp only: io_diagram_def)
            by simp

          have [simp]: "distinct (In A)"
            apply (subgoal_tac "io_diagram A")
            apply (simp only: io_diagram_def)
            by simp

          have [simp]: "TVs (In B) = TI (Trs B)"
            apply (subgoal_tac "io_diagram B")
            apply (simp only: io_diagram_def)
            by simp

          have [simp]: "distinct (In B)"
            apply (subgoal_tac "io_diagram B")
            apply (simp only: io_diagram_def)
            by simp

          have [simp]: "TVs (In C) = TI (Trs C)"
            apply (subgoal_tac "io_diagram C")
            apply (simp only: io_diagram_def)
            by simp

          have [simp]: "distinct (In C)"
            apply (subgoal_tac "io_diagram C")
            apply (simp only: io_diagram_def)
            by simp

          have [simp]: "distinct (In A ⊕ (In B ⊕ In C))"
            by (simp add: distinct_addvars)

          have [simp]: "set (In A ⊕ In B) ⊆ set (In A ⊕ (In B ⊕ In C))"
            apply (simp add: addvars_def set_diff)
            by blast

          have [simp]: "set (In C) ⊆ set (In A ⊕ (In B ⊕ In C))"
            apply (simp add: addvars_def set_diff)
            by blast

          have [simp]: "set (In A) ⊆ set (In A ⊕ (In B ⊕ In C))"
            by (simp add: addvars_def set_diff)

          have [simp]: "set (In B ⊕ In C) ⊆ set (In A ⊕ (In B ⊕ In C))"
            by (simp add: addvars_def set_diff)

          have "Trs (A ||| B ||| C) = [In A ⊕ (In B ⊕ In C) ↝ (In A ⊕ In B) @ In C] oo ([In A ⊕ In B ↝ In A @ In B] oo Trs A ∥ Trs B) ∥ Trs C"
            by (simp add: Parallel_def addvars_assoc)
          also have "... = [In A ⊕ (In B ⊕ In C) ↝ (In A ⊕ In B) @ In C] oo 
              ([In A ⊕ In B ↝ In A @ In B] ∥ [In C ↝ In C] oo Trs A ∥ Trs B ∥ Trs C)"
            apply (subst comp_parallel_distrib)
            by (simp_all)
          also have "... = ([In A ⊕ (In B ⊕ In C) ↝ (In A ⊕ In B) @ In C] oo [In A ⊕ In B ↝ In A @ In B] ∥ [In C ↝ In C]) oo 
              Trs A ∥ Trs B ∥ Trs C"
            by (simp add: comp_assoc)
          also have "... = [In A ⊕ (In B ⊕ In C) ↝ In A @ In B @ In C] oo Trs A ∥ Trs B ∥ Trs C"
            apply (rule_tac f = "λ X . X oo (Trs A ∥ Trs B ∥ Trs C)" in arg_cong)
            apply (simp add: addvars_assoc [THEN sym])
            by (subst switch_par_comp_Subst, simp_all add: distinct_addvars set_addvars Subst_eq)            
          also have "... = [In A ⊕ (In B ⊕ In C) ↝ In A @ (In B @ In C)] oo 
              Trs A ∥ (Trs B ∥ Trs C)"
            by (simp add: par_assoc)
          also have "... = ([In A ⊕ (In B ⊕ In C) ↝ In A @ (In B ⊕ In C)] oo [In A ↝ In A] ∥ [In B ⊕ In C ↝ In B @ In C]) oo
              Trs A ∥ (Trs B ∥ Trs C)"
            apply (rule_tac f = "λ X . X oo (Trs A ∥ (Trs B ∥ Trs C))" in arg_cong)
            apply (simp add: addvars_assoc [THEN sym])
            by (subst switch_par_comp_Subst, simp_all add: distinct_addvars set_addvars Subst_eq, auto)
          also have "... = [In A ⊕ (In B ⊕ In C) ↝ In A @ (In B ⊕ In C)] oo 
              (([In A ↝ In A] oo Trs A) ∥ ([In B ⊕ In C ↝ In B @ In C] oo Trs B ∥ Trs C))"
            apply (simp add: comp_assoc par_assoc)
            apply (subst comp_parallel_distrib)
            by (simp_all )
          also have "... = [In A ⊕ (In B ⊕ In C) ↝ In A @ (In B ⊕ In C)] oo 
               Trs A ∥ ([In B ⊕ In C ↝ In B @ In C] oo Trs B ∥ Trs C)"
            apply (subst comp_id_switch)
            by simp_all
          also have "... = Trs (A ||| (B ||| C))"
            by (simp add: Parallel_def)

        show  "A ||| B ||| C = A ||| (B ||| C)"
          using Parallel_def addvars_assoc calculation by fastforce
      qed
        
definition "VarFB A = Var A A"
definition "InFB A= In A ⊖ VarFB A"
definition "OutFB A = Out A ⊖ VarFB A"

definition FB :: "('var, 'a) Dgr ⇒ ('var, 'a) Dgr" where
  "FB A = (let I = In A ⊖ Var A A in let O' = Out A ⊖ Var A A in
      ⦇In = I, Out = O', Trs = (fb ^^ (length (Var A A))) ([Var A A @ I ↝ In A] oo Trs A oo [Out A ↝ Var A A @ O']) ⦈)"


lemma Type_ok_FB: "io_diagram A ⟹ io_diagram (FB A)"
        apply (simp add: io_diagram_def FB_def Let_def Var_def, safe)
        apply (cut_tac t="TVs(Out A ⊗ In A)" and ts="TVs ((In A ⊖ Out A ⊗ In A))" and ts'="TVs ((Out A ⊖ Out A ⊗ In A))" and
            S="([(Out A ⊗ In A) @ (In A ⊖ Out A ⊗ In A) ↝ In A] oo Trs A oo [Out A ↝ (Out A ⊗ In A) @ (Out A ⊖ Out A ⊗ In A)])" in TI_fb_fbtype_n)
        apply (simp add: fbtype_def)
        apply (subgoal_tac "length (TVs (Out A ⊗ In A)) = length (Out A ⊗ In A)")
        apply simp
        apply (simp add: length_TVs)
        apply (cut_tac t="TVs (Out A ⊗ In A)" and ts="TVs (In A ⊖ Out A ⊗ In A)" and ts'="TVs (Out A ⊖ Out A ⊗ In A)" and
            S="([(Out A ⊗ In A) @ (In A ⊖ Out A ⊗ In A) ↝ In A] oo Trs A oo [Out A ↝ (Out A ⊗ In A) @ (Out A ⊖ Out A ⊗ In A)])" in TO_fb_fbtype_n)
        apply (simp add: fbtype_def)
        apply (subgoal_tac " length (TVs (Out A ⊗ In A)) =  length (Out A ⊗ In A)")
        apply simp
        by (simp add: length_TVs)

lemma perm_var_Par: "io_diagram A ⟹ io_diagram B ⟹ set (In A) ∩ set (In B) = {} 
  ⟹ perm (Var (A ||| B) (A ||| B)) (Var A A @ Var B B @ Var A B @ Var B A)"
        apply (simp add: Parallel_indep Var_def append_inter)
        apply (frule_tac x = "Out A" in inter_append)
        apply (drule_tac x = "Out B" in inter_append)
        by (simp add: perm_mset union_commute union_lcomm)

      lemma distinct_Parallel_Var[simp]: "io_diagram A ⟹ io_diagram B  
        ⟹ set (Out A) ∩ set (Out B) = {} ⟹ distinct (Var (A ||| B) (A ||| B))"
        apply (simp add: Parallel_def Var_def append_inter, safe)
        apply (simp add:  io_diagram_def)
         apply (simp add:  io_diagram_def)
        by (metis IntI notin_inter)

      lemma distinct_Parallel_In[simp]: "io_diagram A ⟹ io_diagram B ⟹ distinct (In (A ||| B))"
        apply (simp add: Parallel_def Var_def append_inter io_diagram_def)
        using distinct_addvars by auto

      lemma drop_assumption: "p ⟹ True"
        by simp


(*
New proof
      theorem FP_IC_res_new: "io_diagram A ⟹ io_diagram B ⟹ set (In A) ∩ set (In B) = {} 
      ⟹ set (Out A) ∩ set (Out B) = {} ⟹ FB (A ||| B) = FB (FB (A) ;; FB (B))"
        proof -
          assume A [simp]: "set (In A) ∩ set (In B) = {}"
          assume B [simp]: "set (Out A) ∩ set (Out B) = {}"
          have [simp]: "In A ⊕ In B = In A @ In B"
            by (simp add: addvars_distinct)
          assume "io_diagram A"
          assume "io_diagram B"
          have [simp]: "distinct (In A)" and [simp]: "distinct (In B)"
            using ‹io_diagram A› io_diagram_def apply auto[1]
            using ‹io_diagram B› io_diagram_def by auto[1]
          have [simp]: "TI (Trs A) = TVs (In A)" and "TO (Trs A) = TVs (Out A)"
            using ‹io_diagram A› io_diagram_def apply force
            using ‹io_diagram A› io_diagram_def by force
          have [simp]: "TI (Trs B) = TVs (In B)" and "TO (Trs B) = TVs (Out B)"
            using ‹io_diagram B› io_diagram_def apply force
            using ‹io_diagram B› io_diagram_def by force

          have [simp]: "In A ⊖ Out A ⊖ (Out B ⊖ In B) = (In A ⊖ Out A ⊖ Out B)"
            apply (subst diff_notin, simp_all add: set_diff)
            using A by blast

          thm diff_commute

          have [simp]: "In B ⊖ Out B ⊖ (Out A ⊖ In A) = (In B ⊖ Out A ⊖ Out B)"
            apply (subst diff_notin, simp_all add: set_diff diff_sym)
            using A by blast

          have [simp]: "Out A ⊖ In A ⊖ (In B ⊖ Out B) = (Out A ⊖ In A ⊖ In B)"
            apply (subst diff_notin, simp_all add: set_diff)
            using B by blast

          have [simp]: "Out B ⊖ In B ⊖ (In A ⊖ Out A) = (Out B ⊖ In A ⊖ In B)"
            apply (subst diff_notin, simp_all add: set_diff diff_sym)
            using B by blast

          have [simp]: "⋀ x y x' y' . (In A ⊖ x ⊖ y) ⊕ (In B ⊖ x' ⊖ y') = (In A ⊖ x ⊖ y) @ (In B ⊖ x' ⊖ y')"
            apply (subst addvars_distinct, simp_all add: set_diff)
            using A by blast

          have [simp]: "⋀ x x' y' . (In A ⊖ x) ⊕ (In B ⊖ x' ⊖ y') = (In A ⊖ x) @ (In B ⊖ x' ⊖ y')"
            apply (subst addvars_distinct, simp_all add: set_diff)
            using A by blast
          have [simp]: "distinct (In B ⊖ Out A ⊖ Out B)"
            by (simp add: distinct_diff)

          show ?thesis
            apply (simp add: Parallel_def FB_def Comp_def Let_def Var_def, safe)
            apply (simp_all add: diff_inter_left diff_inter_right)
            apply (simp_all add: addvars_minus diff_union distinct_id union_diff diff_addvars diff_redundant_a 
                diff_redundant_b diff_redundant_c diff_redundant_d)
            sorry
        qed
*)

   lemma  Dgr_eq: "In A = x ⟹ Out A = y ⟹ Trs A = S ⟹  ⦇In = x, Out = y, Trs = S⦈ = A"
        by auto


      lemma Var_FB[simp]: "Var (FB A) (FB A) = []"
        by (simp add: FB_def Var_def Let_def)

      theorem FB_idemp: "io_diagram A ⟹ FB (FB A) = FB A"
        apply (subst FB_def)
        apply (simp add: Let_def diff_emptyset)
        apply (rule Dgr_eq, simp_all)
        by (metis (no_types, lifting) io_diagram_def  Type_ok_FB comp_id_right comp_id_switch distinct_id)

    definition VarSwitch :: "'var list ⇒ 'var list ⇒ ('var, 'a) Dgr" ("[[_ ↝ _]]") where
      "VarSwitch x y = ⦇In = x, Out = y, Trs = [x ↝ y]⦈"
      

      definition "in_equiv  A B = (perm (In A) (In B) ∧ Trs A = [In A ↝ In B] oo Trs B ∧ Out A  = Out B)"
      definition "out_equiv A B = (perm (Out A) (Out B) ∧ Trs A = Trs B oo [Out B ↝ Out A] ∧ In A = In B)"

      definition "in_out_equiv A B = (perm (In A) (In B) ∧ perm (Out A) (Out B) ∧ Trs A = [In A ↝ In B] oo Trs B oo [Out B ↝ Out A])"

      lemma in_equiv_io_diagram: "in_equiv A B ⟹ io_diagram B ⟹ io_diagram A"
        apply (simp add: io_diagram_def in_equiv_def, safe)
        using dist_perm perm_sym by blast

      lemma in_out_equiv_io_diagram: "in_out_equiv A B ⟹ io_diagram B ⟹ io_diagram A"
        apply (simp add: io_diagram_def in_out_equiv_def, safe)
        using dist_perm perm_sym apply blast
        using dist_perm perm_sym by blast

      lemma in_equiv_sym: "io_diagram B ⟹ in_equiv A B ⟹ in_equiv B A"
        by (auto simp add: in_equiv_def perm_sym  comp_assoc[THEN sym] io_diagram_def switch_comp )
      
      lemma in_equiv_eq: "io_diagram A ⟹ A = B ⟹ in_equiv A B"
        by (simp add: in_equiv_def perm_mset io_diagram_def)

      lemma [simp]: "io_diagram A ⟹ [In A ↝ In A] oo Trs A oo [Out A ↝ Out A] = Trs A"
        by (simp add: io_diagram_def)

      lemma in_equiv_tran: "io_diagram C ⟹ in_equiv A B ⟹ in_equiv B C ⟹ in_equiv A C"
        apply (subgoal_tac "io_diagram B")
        apply (subgoal_tac "io_diagram A")
        apply (simp add: in_equiv_def)
        apply (simp_all add: in_equiv_io_diagram)
        apply (cut_tac x="In A" and y="In B" and z="In C" in  perm_trans)
        apply simp_all
        apply (subst comp_assoc [THEN sym])
        apply simp_all
        apply (unfold io_diagram_def, simp_all)
        apply (subst switch_comp)
           apply simp
          apply simp
         apply simp
          by simp

    lemma in_out_equiv_refl: "io_diagram A ⟹ in_out_equiv A A"
      by (simp add: in_out_equiv_def perm_mset)

    lemma in_out_equiv_sym: "io_diagram A ⟹ io_diagram B ⟹ in_out_equiv A B ⟹ in_out_equiv B A"
      apply (simp add: in_out_equiv_def, safe)
      apply (simp add: perm_mset)
      apply (simp add: perm_mset)
      apply (simp add: io_diagram_def)
      apply (simp add: comp_assoc)
      apply (subgoal_tac "[Out B ↝ Out A] oo [Out A ↝ Out B] = ID (TVs (Out B))")
      apply simp_all
      apply (simp add: comp_assoc [THEN sym])
      apply (subgoal_tac "[In B ↝ In A] oo [In A ↝ In B] =  ID (TVs (In B))")
      apply simp_all
      apply (simp add: distinct_vars_comp perm_sym)
      by (simp add: distinct_vars_comp perm_sym)

    lemma in_out_equiv_tran: "io_diagram A ⟹ io_diagram B ⟹ io_diagram C ⟹ in_out_equiv A B ⟹ in_out_equiv B C ⟹ in_out_equiv A C"
      apply (simp add: in_out_equiv_def, safe)
      apply (simp add: perm_mset)
      apply (simp add: perm_mset)
      apply (unfold io_diagram_def, safe)
      proof -
        assume [simp]: "TVs (In A) = TI (Trs A)" 
        assume [simp]: "TVs (In B) = TI (Trs B) "
        assume [simp]: "TVs (In C) = TI (Trs C) "
        assume [simp]: "TVs (Out A) = TO (Trs A) "
        assume [simp]: "TVs (Out B) = TO (Trs B) "
        assume [simp]: "TVs (Out C) = TO (Trs C) "
        have [simp]: "[In A ↝ In B] oo ([In B ↝ In C] oo Trs C oo [Out C ↝ Out B]) oo [Out B ↝ Out A]
          = ([In A ↝ In B] oo [In B ↝ In C]) oo Trs C oo ([Out C ↝ Out B] oo [Out B ↝ Out A])"
          by (simp add: comp_assoc)
        assume [simp]: "perm (In A) (In B)"
        assume "perm (In B) (In C)"
        assume "perm (Out A) (Out B)"
        assume "perm (Out B) (Out C)"
        assume [simp]: "distinct (In A)"
        assume [simp]: "distinct (Out C)"

        have [simp]: "[In A ↝ In B] oo [In B ↝ In C] = [In A ↝ In C]"
          apply (subst  switch_comp, simp_all)
          using ‹perm (In B) (In C)› perm_set_eq by auto

        have [simp]: "[Out C ↝ Out B] oo [Out B ↝ Out A] = [Out C ↝ Out A]"
          apply (subst  switch_comp, simp_all)
          apply (simp add: ‹perm (Out B) (Out C)› perm_sym)
          using ‹perm (Out A) (Out B)› perm_set_eq by auto
        show " [In A ↝ In B] oo ([In B ↝ In C] oo Trs C oo [Out C ↝ Out B]) oo [Out B ↝ Out A] = [In A ↝ In C] oo Trs C oo [Out C ↝ Out A]"
          by simp
     qed


    lemma [simp]: "distinct (Out A) ⟹ distinct (Var A B)"
      by (simp add: Var_def)

    lemma [simp]: "set (Var A B) ⊆ set (Out A)"
      by (auto simp add: Var_def set_inter)
    lemma [simp]: "set (Var A B) ⊆ set (In B)"
      by (auto simp add: Var_def set_inter)



    lemmas fb_indep_sym = fb_indep [THEN sym]

declare length_TVs [simp] 
  
  end
  

  primrec op_list :: "'a ⇒ ('a ⇒ 'a ⇒'a) ⇒ 'a list ⇒ 'a" where
    "op_list e opr [] = e" |
    "op_list e opr (a # x) = opr a (op_list e opr x)"

primrec inter_set :: "'a list ⇒ 'a set ⇒ 'a list" where
  "inter_set [] X = []" |
  "inter_set (x # xs) X = (if x ∈ X then x # inter_set xs X else inter_set xs X)"

lemma list_inter_set: "x ⊗ y = inter_set x (set y)"
      by (induction x, simp_all)

fun map2 :: "('a ⇒ 'b ⇒ bool) ⇒ 'a list ⇒ 'b list ⇒ bool" where
  "map2 f [] [] = True" |
  "map2 f (a # x) (b # y) = (f a b ∧ map2 f x y)" |
  "map2 _ _ _ = False"
  
thm map_def
  
context BaseOperationFeedbacklessVars
begin
definition ParallelId :: "('var, 'a) Dgr" ("□")
  where "□ =  ⦇In = [], Out = [], Trs = ID []⦈"
    
lemma [simp]: "Out □ = []"
  by (simp add: ParallelId_def)

lemma [simp]: "In □ = []"
  by (simp add: ParallelId_def)

lemma [simp]: "Trs □ = ID []"
  by (simp add: ParallelId_def)
    
lemma ParallelId_right[simp]: "io_diagram A ⟹ A ||| □ = A"
  apply (simp add: Parallel_def ParallelId_def)
  apply (subst comp_id_switch)
    apply (simp add: io_diagram_def)
   apply (simp add: io_diagram_def)
  apply (cut_tac x="[]" in  distinct_id)
   apply simp
  apply (subgoal_tac "TVs [] = []")
  using par_empty_right apply auto[1]
  by (simp add: TVs_def)

lemma ParallelId_left: "io_diagram A ⟹ □ ||| A = A"
  apply (simp add: Parallel_def ParallelId_def)
  apply (subst comp_id_switch)
  by (simp_all add: io_diagram_def)

definition "parallel_list = op_list (ID []) (op ∥)"
  
definition "Parallel_list = op_list □ (op |||)"
  
lemma [simp]: "Parallel_list [] = □"
  by (simp add: Parallel_list_def)

definition "io_distinct As = (distinct (concat (map In As)) ∧ distinct (concat (map Out As)) ∧ (∀ A ∈ set As . io_diagram A))"
       
definition "io_rel A = set (Out A) × set (In A)"

definition "IO_Rel As = ⋃ (set (map io_rel As))"

definition "out A = hd (Out A)" (*the first output of A*)

definition "Type_OK As = ((∀ B ∈ set As . io_diagram B ∧ length (Out B) = 1) 
                    ∧ distinct (concat (map Out As)))"

      lemma concat_map_out: "(∀ A ∈ set As . length (Out A) = 1) ⟹ concat (map Out As) = map out As"
        apply (induction As, simp_all)
        apply (case_tac "Out a", simp_all)
        by (simp add: out_def)

      lemma Type_OK_simp: "Type_OK As =  ((∀ B ∈ set As . io_diagram B ∧ length (Out B) = 1) ∧ distinct (map out As))"
        apply (simp add: Type_OK_def, safe)
        by (simp_all add: concat_map_out)

      definition "single_out A = (io_diagram A ∧ length (Out A) = 1)"


definition CompA :: "('var, 'a) Dgr ⇒ ('var, 'a) Dgr ⇒ ('var, 'a) Dgr" (infixl "⊳" 75) where
(*  "A ⊳ B = (if set(Out A) ⊆ set (In B) then A ;; B else B)"*)
  "A ⊳ B = (if out A ∈ set (In B) then A ;; B else B)"

  
definition "internal As = {x . (∃ A ∈ set As . ∃ B ∈ set As . x ∈ set (Out A) ∧ x ∈ set (In B))}"


primrec get_comp_out :: "'var ⇒ ('var, 'a) Dgr list ⇒ ('var, 'a) Dgr" where
    "get_comp_out x [] = ⦇In = [x], Out = [x], Trs = [ [x] ↝ [x] ]⦈" | (*can be undefined also. Using identity to be more convenient*)
    "get_comp_out x (A # As) = (if x ∈ set (Out A) then A else get_comp_out x As)" 
        

primrec get_other_out :: "'c ⇒ ('c, 'd) Dgr list ⇒ ('c, 'd) Dgr list" where
    "get_other_out x [] = []" |
    "get_other_out x (A # As) = (if x ∈ set (Out A) then get_other_out x As else A # get_other_out x As)"
    
      (*we assume the A is not in As*)
definition "fb_less_step A As = map (CompA A) As" 

      
definition "fb_out_less_step x As = fb_less_step (get_comp_out x As) (get_other_out x As)"

primrec fb_less :: "'var list ⇒ ('var, 'a) Dgr list ⇒ ('var, 'a) Dgr list" where
      "fb_less [] As = As" |
      "fb_less (x # xs) As = fb_less xs (fb_out_less_step x As)"
  

lemma [simp]: "VarFB □ = []"
  by (simp add: VarFB_def Var_def)
lemma [simp]: "InFB □ = []"
  by (simp add: VarFB_def Var_def InFB_def)
lemma [simp]: "OutFB □ = []"
  by (simp add: VarFB_def Var_def OutFB_def)
    

      definition "loop_free As = (∀ x . (x,x) ∉ (IO_Rel As)+)"

lemma [simp]: "Parallel_list (A # As) = (A ||| Parallel_list As)"
  by (simp add: Parallel_list_def)

lemma [simp]: "Out (A ||| B) = Out A @ Out B"
  by (simp add: Parallel_def)

lemma [simp]: "In (A ||| B) = In A ⊕ In B"
  by (simp add: Parallel_def)

lemma Type_OK_cons: "Type_OK (A # As) = (io_diagram A ∧ length (Out A) = 1 ∧ set (Out A) ∩ (⋃a∈set As. set (Out a)) = {} ∧ Type_OK As)"
  by (simp add: Type_OK_def io_diagram_def, auto)

    
lemma Out_Parallel: "Out (Parallel_list As) = concat (map Out As)"
  by (induction As, simp_all)

      lemma internal_cons: "internal (A # As) = {x. x ∈ set (Out A) ∧ (x ∈ set (In A) ∨ (∃B∈set As. x ∈ set (In B)))} ∪ {x . (∃Aa∈set As. x ∈ set (Out Aa) ∧ (x ∈ set (In A)))}
          ∪ internal As"
        by (auto simp add: internal_def)
          
      lemma Out_out: "length (Out A) = Suc 0 ⟹ Out A = [out A]"
        apply (simp add: out_def)
        by (case_tac "Out A", simp_all)

      lemma Type_OK_out: "Type_OK As ⟹ A ∈ set As  ⟹ Out A = [out A]"
        apply (simp add: out_def Type_OK_def)
        by (case_tac "Out A", simp_all, auto)


      lemma In_Parallel: "In (Parallel_list As) = op_list [] (op ⊕) (map In As)"
        by (induction As, simp_all)

      lemma [simp]: "set (op_list [] op ⊕ xs) = ⋃ set (map set xs)"
        apply (induction xs, simp_all)
        by (simp add: set_addvars)

      lemma internal_VarFB: "Type_OK As ⟹ internal As = set (VarFB (Parallel_list As))"
        apply (induction As)
        apply (simp add: VarFB_def Var_def internal_def Parallel_list_def ParallelId_def)
        apply (subgoal_tac "Out a = [out a]")
        apply (simp add: Type_OK_cons VarFB_def Var_def set_inter set_addvars internal_cons Type_OK_out Out_Parallel, safe)
        apply (simp_all add: Type_OK_out subsetset_inter)
        apply (rule_tac x = Aa in bexI)
        apply (simp add: Type_OK_out, simp)
        apply (rule_tac x = xa in bexI)
        apply (simp add: Type_OK_out, simp)
        apply blast
        apply blast
        apply blast
        apply auto
        by (simp_all add: In_Parallel)


      lemma map_Out_fb_less_step: "length (Out A) = 1 ⟹  map Out (fb_less_step A As) = map Out As"
        apply (induction As)
        apply (simp_all add: fb_less_step_def CompA_def Comp_def Let_def Var_def diff_inter_left, safe)
        by (case_tac "Out A", simp_all add: out_def)

      lemma mem_get_comp_out: "Type_OK As ⟹ A ∈ set As ⟹ get_comp_out (out A) As = A"
        apply (induction As, simp, auto)
         apply (simp add: Type_OK_def, auto)
          apply (metis (no_types, lifting) Out_out   list.set_intros(1))
         apply (simp add: Type_OK_def Out_out)
        prefer 2
        using Type_OK_cons apply blast
        proof -
          fix a :: "('var, 'a) Dgr" and Asa :: "('var, 'a) Dgr list"
          assume a1: "io_diagram a ∧ length (Out a) = Suc 0 ∧ (∀B∈set Asa. io_diagram B ∧ length (Out B) = Suc 0) ∧ distinct (Out a) ∧ distinct (concat (map Out Asa)) ∧ set (Out a) ∩ (⋃a∈set Asa. set (Out a)) = {}"
          assume a2: "A ∈ set Asa"
          assume "out A = out a"
          then have "¬ distinct (map out (a # Asa))"
            using a2 by (metis (no_types) distinct.simps(2) image_eqI list.map(2) set_map)
          then show "a = A"
            using a1 by (metis (no_types) One_nat_def Type_OK_cons Type_OK_def Type_OK_simp)
        qed
 
      lemma map_Out_fb_out_less_step: "A ∈ set As ⟹ Type_OK As ⟹ a = out A ⟹ map Out (fb_out_less_step a As) = map Out (get_other_out a As)"
        apply (induction As, simp add: fb_out_less_step_def fb_less_step_def)
        apply simp
        apply safe
        apply (simp add: fb_out_less_step_def)
        apply (subst map_Out_fb_less_step)
        apply (simp add: Type_OK_def)
        apply simp
        apply (simp add: fb_out_less_step_def)
        apply (subst map_Out_fb_less_step, simp_all)
          apply (simp add: Type_OK_def)
          using Out_out apply force
        apply (simp add: fb_out_less_step_def)
           apply (subst map_Out_fb_less_step, simp_all)
            
            using Type_OK_cons apply auto[1]
            apply (simp add: Type_OK_cons)
              by (simp add: Type_OK_simp fb_out_less_step_def map_Out_fb_less_step mem_get_comp_out)


lemma [simp]: "Type_OK (A # As) ⟹ Type_OK As"
        by (simp add: Type_OK_cons)

      lemma Type_OK_Out: "Type_OK (A # As) ⟹ Out A = [out A]"
        by (rule Type_OK_out, simp_all, auto)

      lemma  concat_map_Out_get_other_out: "Type_OK As ⟹ concat (map Out (get_other_out a As)) = (concat (map Out As) ⊖ [a])"
        apply (induction As, simp_all)
        by (simp_all add: union_diff Type_OK_Out)
      thm Out_out
      lemma VarFB_cons_out: "Type_OK As ⟹ VarFB (Parallel_list As) = a # L ⟹ ∃ A ∈ set As . out A = a"
        apply (cut_tac As = As in internal_VarFB, simp_all)
        apply (simp add: internal_def)
        apply (unfold set_eq_iff)
        apply (drule_tac x = a in spec, simp_all add: Out_out, safe)
        apply (subst (asm) Out_out)
         apply (simp add: Type_OK_def)
        by auto
          


      lemma VarFB_cons_out_In: "Type_OK As ⟹ VarFB (Parallel_list As) = a # L ⟹ ∃ B ∈ set As . a ∈ set (In B)"
        apply (cut_tac As = As in internal_VarFB, simp_all)
        apply (simp add: internal_def)
        apply (unfold set_eq_iff)
        by (drule_tac x = a in spec, simp_all)


      (*todo: find better names to next lemmas*)
      lemma AAA_a: "Type_OK (A # As) ⟹ A ∉ set As"
        apply (simp add: Type_OK_def, auto)
        by (case_tac "Out A", simp_all, auto)


      lemma AAA_b: "(∀ A ∈ set As. a ∉ set (Out A)) ⟹ get_other_out a As = As"
        by (induction As, simp_all)

     
      lemma AAA_d: "Type_OK (A # As) ⟹ ∀Aa∈set As. out A ≠ out Aa"
        apply (simp add: Type_OK_def)
        apply (unfold set_eq_iff)
        apply (case_tac "Out A", simp_all, safe)
        apply (drule_tac x = "a" in spec, safe, auto)
        apply (drule_tac x = Aa in bspec, simp_all)
        apply (drule_tac x = Aa in bspec, simp_all)
        apply (case_tac "Out Aa", simp_all, auto)
        by (simp add: out_def)

      lemma  mem_get_other_out: "Type_OK As ⟹ A ∈ set As ⟹ get_other_out (out A) As = (As ⊖ [A])"
        apply (induction As)
        apply simp
        apply simp
        apply safe   
        apply simp_all
        apply (subst AAA_c)
        apply (subst AAA_a, simp_all)
            apply (subst AAA_b, simp_all)
          
        using Type_OK_cons apply blast
          
           apply (simp add: Type_OK_Out)
          
        using Type_OK_cons apply blast
          
         apply (simp add: Out_out Type_OK_simp)
        using AAA_a by blast

(*
lemma In_CompA: "In (A ⊳ B) = (if set (Out A) ⊆ set (In B) then In A ⊕ (In B ⊖ Out A) else In B)"
  by (simp add: CompA_def Comp_def Let_def Var_def diff_inter_right)
*)

lemma In_CompA: "In (A ⊳ B) = (if out A ∈ set (In B) then In A ⊕ (In B ⊖ Out A) else In B)"
  by (simp add: CompA_def Comp_def Let_def Var_def diff_inter_right)
      
  
lemma union_set_In_CompA: "⋀ B . length (Out A) = 1 ⟹ B ∈ set As ⟹ out A ∈ set (In B) 
    ⟹ (⋃x∈set As. set (In (CompA A x))) = set (In A) ∪ ((⋃ B ∈ set As . set (In B)) - {out A})"
  proof (induction As)
    case Nil
    then show ?case by simp
  next
    case (Cons a As)
    have [simp]: "out A ∈ set (In B)"
      by (simp add: Cons.prems(3))
    have [simp]: "Out A = [out A]"
      by (simp add: Cons.prems(1) Out_out)
    show ?case
      proof (cases "∀ C ∈ set As . out A ∉ set (In C)")
        case True
        have [simp]: "a = B"
          using Cons.prems(2) Cons.prems(3) True by auto
        from True show ?thesis
          by (auto simp add:  In_CompA set_addvars set_diff)
      next
        case False
        from this obtain C where [simp]: "C ∈ set As" and [simp]: "out A ∈ set (In C)"
          by blast
        show ?thesis
          apply simp
          apply (subst Cons(1) [of C])
          by (auto simp add:  In_CompA set_addvars set_diff)
      qed
    qed

lemma BBBB_e: "Type_OK As ⟹ VarFB (Parallel_list As) = out A # L ⟹ A ∈ set As ⟹ out A ∉ set L"
  apply (simp add: VarFB_def Var_def Out_Parallel Type_OK_def, safe)
  by (drule_tac y = "In (Parallel_list As)" in distinct_inter, simp)

lemma BBBB_f: "loop_free As ⟹
     Type_OK As ⟹ A ∈ set As  ⟹ B ∈ set As ⟹ out A ∈ set (In B) ⟹ B ≠ A"
        apply (simp add: loop_free_def)
        apply (drule_tac x = "out A" in spec)
        apply (simp add: IO_Rel_def io_rel_def)
        apply (case_tac "B = A", simp_all)
          apply (simp add: io_rel_def)
          apply (subgoal_tac "(out A, out A) ∈ (⋃x∈set As. set (Out x) × set (In x))+", simp)
          
        apply (rule r_into_trancl')
        apply simp  
        apply (rule_tac x = A in bexI)
        by (simp_all add: Type_OK_out)
          
      thm union_set_In_CompA
        
lemma [simp]: "x ∈ set (Out (get_comp_out x As))"
  by (induction As, auto simp add: out_def)

lemma comp_out_in: "A ∈ set As ⟹ a ∈ set (Out A) ⟹ (get_comp_out a As) ∈ set As"
  apply (induction As, simp)
  by auto
    
lemma  [simp]: "a ∈ internal As ⟹ get_comp_out a As ∈ set As"
  apply (simp_all add: internal_def)
   using comp_out_in by blast
    
lemma out_CompA: "length (Out A) = 1 ⟹ out (CompA A B) = out B"
  apply (simp add: CompA_def)
  apply (simp add: Comp_def Let_def Var_def out_def)
  by (case_tac "Out A", simp_all)
    
lemma Type_OK_loop_free_elem: "Type_OK As ⟹ loop_free As ⟹ A ∈ set As ⟹ out A ∉ set (In A)"
        apply (simp add: loop_free_def)
        apply (drule_tac x = "out A" in spec)
        apply (simp add: IO_Rel_def io_rel_def)
        apply (case_tac "out A ∈ set (In A)", simp_all)
          apply (simp add: io_rel_def)
        apply (drule_tac P =  "(out A, out A) ∈ (⋃x∈set As. set (Out x) × set (In x))+" in notE, simp_all)
        apply (rule r_into_trancl')
        apply simp
        apply (rule_tac x = A in bexI)
  by (simp_all add: Type_OK_out)
    
      lemma BBB_a: "length (Out A) = 1 ⟹ Out (CompA A B) = Out B"
        apply (simp add: CompA_def, safe)
        apply (simp add: Comp_def Let_def Var_def diff_inter_left out_def)
        by (case_tac "Out A", simp_all)

      lemma BBB_b: "length (Out A) = 1 ⟹ map (Out ∘ CompA A) As = map Out As"
        apply (induction As, simp_all)
        by (simp add: BBB_a)
  
lemma VarFB_fb_out_less_step_gen:
  assumes "loop_free As"
    assumes "Type_OK As"
    and internal_a: "a ∈ internal As"
    shows "VarFB (Parallel_list (fb_out_less_step a As)) = (VarFB (Parallel_list As)) ⊖ [a]"
proof -
  define A where "A = get_comp_out a As"
  have [simp]: "A ∈ set As"
    using A_def internal_a by auto [1]
      
  from this have "length (Out A) = 1"
    using ‹Type_OK As› by (unfold Type_OK_def, simp) 
  from this have "Out A = [out A]"
    by (simp add: Out_out)
      
  have "a ∈ set (Out A)"
    by (simp add: ‹A ≡ get_comp_out a As›)
      
  have Out_a: "out A = a"
    using ‹Out A = [out A]› ‹a ∈ set (Out A)› by auto
      
  have [simp]: "get_other_out a As = As ⊖ [A]"
    using Out_a ‹A ∈ set As› assms(2) mem_get_other_out by blast
      
  from internal_a obtain C where [simp]: "C ∈ set As" and [simp]: "a ∈ set (In C)" and [simp]: "C ≠ A"
    apply (unfold internal_def, safe)
    by (metis Out_a Type_OK_loop_free_elem assms(1) assms(2))
      
  have a_not_in_A: "a ∉ set (In A)"
    using BBBB_f Out_a ‹A ∈ set As› assms(1) assms(2) by blast
 
  have [simp]: "⋀ A . A ∈ set As ⟹ Out A = [out A]"
    using Type_OK_out assms(2) by blast

  have [simp]: "concat (map Out (As ⊖ [A])) = (concat (map Out As) ⊖ [a])"
    by (metis ‹get_other_out a As = As ⊖ [A]› assms(2) concat_map_Out_get_other_out)
      
  have [simp]: "UNION (set (As ⊖ [A])) (set ∘ (In ∘ CompA A)) = set (op_list [] op ⊕ (map In As) ⊖ [a])"
    apply (simp add: set_diff, simp, safe)
      apply (case_tac "out A ∈ set (In xa)")
       apply (simp add: CompA_def Comp_def Let_def set_addvars set_diff)
       apply auto[2]
     apply (case_tac "out A ∈ set (In xa)")
      apply (simp add: CompA_def Comp_def Let_def set_addvars set_diff)
      apply (simp add: a_not_in_A Var_def)
    using CompA_def apply auto[1]
    apply (case_tac "a ∈ set (In xa)", simp_all)
       apply (simp add: Out_a CompA_def Comp_def Let_def set_addvars set_diff)
      apply (simp add: Out_a Var_def a_not_in_A)
       apply (simp add: Out_a CompA_def Comp_def Let_def set_addvars set_diff)
    apply (case_tac "xa = A", simp_all)
     apply (drule_tac x = C in bspec)
      apply simp_all
     apply (simp add: CompA_def Comp_def Let_def set_addvars set_diff Out_a)
    apply (drule_tac x = xa in bspec, simp)
      apply (case_tac "a ∈ set (In xa)")
     by (simp_all add: CompA_def Comp_def Let_def set_addvars set_diff Out_a Var_def)
      
  show "VarFB (Parallel_list (fb_out_less_step a As)) = (VarFB (Parallel_list As)) ⊖ [a]"
    apply (simp add: VarFB_def Var_def Out_Parallel In_Parallel fb_out_less_step_def A_def [THEN sym] fb_less_step_def)
    apply (subst BBB_b, simp_all)
    apply (simp add: listinter_diff)
    apply (rule set_listinter)
    by simp
qed
  
thm internal_VarFB
thm VarFB_fb_out_less_step_gen
  

lemma VarFB_fb_out_less_step: "loop_free As ⟹ Type_OK As ⟹ VarFB (Parallel_list As) = a # L ⟹ VarFB (Parallel_list (fb_out_less_step a As)) = L"
  apply (subst VarFB_fb_out_less_step_gen, simp_all)
   apply (simp add: internal_VarFB)
  apply (subgoal_tac "distinct (VarFB (Parallel_list As))")
   apply (metis AAA_c distinct.simps(2))
  by (metis Out_Parallel Type_OK_def VarFB_def Var_def distinct_inter)
    
                
lemma Parallel_list_cons:"Parallel_list (a # As) = a ||| Parallel_list As"
  by simp

lemma io_diagram_parallel_list: "Type_OK As ⟹ io_diagram (Parallel_list As)"
        apply (induction As)
        apply (simp add: ParallelId_def io_diagram_def)
        apply (simp only: Parallel_list_cons)
        apply (subst io_diagram_Parallel)
        by (simp_all add: Type_OK_def Out_Parallel)

      lemma BBB_c: "distinct (map f As) ⟹ distinct (map f (As ⊖ Bs))"
        by (induction As, simp_all add: image_def set_diff)

      lemma io_diagram_CompA: "io_diagram A ⟹ length (Out A) = 1 ⟹ io_diagram B ⟹ io_diagram (CompA A B)"
        apply (simp add: CompA_def, safe)
        apply (subst Comp_in_out)
           apply simp_all

        using Out_out apply fastforce
        by (simp add: Let_def Var_def diff_inter_left diff_inter_right io_diagram_def addvars_def set_diff)


      lemma Type_OK_fb_out_less_step_aux: "Type_OK As ⟹ A ∈ set As ⟹  Type_OK (fb_less_step A (As ⊖ [A]))"
        apply (unfold fb_less_step_def)
        apply (subst Type_OK_def, safe, simp_all add: image_def, safe)
        apply (subst io_diagram_CompA, simp_all)
        apply (simp add: Type_OK_def)
        apply (simp add: Type_OK_def)
        apply (simp add: Type_OK_def set_diff)
        apply (subst BBB_a)
        apply (simp add: Type_OK_def)
        apply (simp add: Type_OK_def set_diff)
        apply (subst BBB_b)
        apply (simp add: Type_OK_def)
        apply (subst concat_map_out)
        apply (simp add: Type_OK_def set_diff)
        by (simp add: Type_OK_simp BBB_c)

    
          
      thm VarFB_cons_out
        
theorem Type_OK_fb_out_less_step_new: "Type_OK As ⟹
      a ∈ internal As ⟹
      Bs = fb_out_less_step a As ⟹ Type_OK Bs"
  apply (simp add: internal_def, safe)
  apply (simp add: fb_out_less_step_def)
    apply (subgoal_tac "Out A = [out A]", simp) 
  apply (subgoal_tac "(get_comp_out (out A) As) = A", simp_all)
  apply (subgoal_tac "get_other_out (out A) As = (As ⊖ [A])", simp_all)
  apply (rule Type_OK_fb_out_less_step_aux, simp_all)
  using mem_get_other_out apply blast
  using mem_get_comp_out apply blast
  by (simp add: Type_OK_def Out_out)
    
theorem Type_OK_fb_out_less_step: "loop_free As ⟹ Type_OK As ⟹
        VarFB (Parallel_list As) = a # L ⟹ Bs = fb_out_less_step a As ⟹ Type_OK Bs"
  apply (rule Type_OK_fb_out_less_step_new, simp_all)
  by (simp add: internal_VarFB)


lemma perm_FB_Parallel[simp]: "loop_free As ⟹ Type_OK As
      ⟹ VarFB (Parallel_list As) = a # L ⟹ Bs = fb_out_less_step a As 
      ⟹ perm (In (FB (Parallel_list As))) (In (FB (Parallel_list Bs)))"
  apply (frule VarFB_cons_out, simp_all, safe)
  apply (frule VarFB_cons_out_In, simp_all, safe)
  apply (rule set_perm)
    apply (drule io_diagram_parallel_list)
        apply (drule Type_ok_FB)
        apply (simp add: io_diagram_def)
        apply (frule Type_OK_fb_out_less_step, simp_all)
        apply (drule_tac As = "(fb_out_less_step (out A) As)" in io_diagram_parallel_list)
        apply (drule Type_ok_FB)
        apply (simp add: io_diagram_def)
        apply (frule VarFB_fb_out_less_step, simp_all)
        apply (simp add: FB_def Let_def In_Parallel )
        apply (simp add: VarFB_def)
        apply (simp add: set_diff fb_out_less_step_def fb_less_step_def)
        apply (simp add: mem_get_other_out mem_get_comp_out)
        apply (subst union_set_In_CompA, simp_all)
        apply (simp add: Type_OK_def)
        apply (simp add: set_diff)
         apply (rule BBBB_f, simp_all)
        apply (simp add: set_diff)
        apply (unfold set_eq_iff, auto)
        by (simp add: Type_OK_loop_free_elem)


      lemma [simp]: "loop_free As ⟹ Type_OK As ⟹
          VarFB (Parallel_list As) = a # L ⟹  
          Out (FB (Parallel_list (fb_out_less_step a As))) = Out (FB (Parallel_list As))"
        apply (frule VarFB_cons_out, simp_all, safe)
        apply (frule VarFB_fb_out_less_step, simp_all)
        apply (simp add: FB_def Let_def VarFB_def)
        apply (simp add: Out_Parallel)
        apply (subst map_Out_fb_out_less_step, simp_all)
        apply (simp add: concat_map_Out_get_other_out)
        by (metis diff_cons)

      lemma TI_Parallel_list: "(∀ A ∈ set As . io_diagram A) ⟹ TI (Trs (Parallel_list As)) = TVs (op_list [] op ⊕ (map In As))"
        apply (induction As)
        apply simp
        apply (simp add: ParallelId_def)
        apply (simp add: Parallel_def)
        apply (subst TI_comp)
        apply simp_all
        apply (simp_all add: In_Parallel)
        by (simp add: io_diagram_def)

      lemma TO_Parallel_list: "(∀ A ∈ set As . io_diagram A) ⟹ TO (Trs (Parallel_list As)) = TVs (concat (map Out As))"
        apply (induction As, simp_all)
        apply (simp add: Parallel_def)
        apply (subst TO_comp)
        apply simp_all
        apply (simp_all add: In_Parallel TI_Parallel_list)
        by (simp_all add: io_diagram_def)

      lemma fbtype_aux: "(Type_OK As) ⟹ loop_free As ⟹ VarFB (Parallel_list As) = a # L ⟹
            fbtype ([L @ (In (Parallel_list (fb_out_less_step a As)) ⊖ L) ↝ In (Parallel_list (fb_out_less_step a As))] oo Trs (Parallel_list (fb_out_less_step a As)) oo
              [Out (Parallel_list (fb_out_less_step a As)) ↝ L @ (Out (Parallel_list (fb_out_less_step a As)) ⊖ L)])
              (TVs L) (TO [In (Parallel_list As) ⊖ a # L ↝ In (Parallel_list (fb_out_less_step a As)) ⊖ L]) (TVs (Out (Parallel_list (fb_out_less_step a As)) ⊖ L))"
        apply (frule Type_OK_fb_out_less_step, simp_all)
        apply (simp add: fbtype_def, safe)
        apply (subst TI_comp, simp_all)
        apply (subst TO_comp, simp_all)
        apply (simp add: In_Parallel)
        apply (subst TI_Parallel_list)
        apply (simp add: Type_OK_def)
        apply simp
        apply (simp add: Out_Parallel)
        apply (subst TO_Parallel_list)
        apply (simp add: Type_OK_def)
        apply simp
        apply (subst TI_comp, simp_all)
        apply (simp add: In_Parallel)
        apply (subst TI_Parallel_list)
        apply (simp add: Type_OK_def)
        apply simp
        apply (subst TO_comp, simp_all)
        apply (subst TO_comp, simp_all)
        apply (simp add: In_Parallel)
        apply (subst TI_Parallel_list)
        apply (simp add: Type_OK_def)
        apply simp
        apply (simp add: Out_Parallel)
        apply (subst TO_Parallel_list)
        apply (simp add: Type_OK_def)
        by simp
 

      lemma fb_indep_left_a: "fbtype S tsa (TO A) ts ⟹ A oo (fb^^(length tsa)) S = (fb^^(length tsa)) ((ID tsa ∥ A) oo S)" 
        by (simp add: fb_indep_left)


      lemma parallel_list_cons: "parallel_list (A # As) = A ∥ parallel_list As"
        by (simp add: parallel_list_def)
  
      lemma TI_parallel_list: "(∀ A ∈ set As . io_diagram A) ⟹ TI (parallel_list (map Trs As)) = TVs (concat (map In As))"
        apply (induction As)
        by (simp_all add: parallel_list_def io_diagram_def)
  
      lemma TO_parallel_list: "(∀ A ∈ set As . io_diagram A) ⟹TO (parallel_list (map Trs As)) = TVs (concat (map Out As))"
        apply (induction As)
        by (simp_all add: parallel_list_def io_diagram_def)


      lemma Trs_Parallel_list_aux_a: "Type_OK As ⟹ io_diagram a ⟹
            [In a ⊕ In (Parallel_list As) ↝ In a @ In (Parallel_list As)] oo Trs a ∥ ([In (Parallel_list As) ↝ concat (map In As)] oo parallel_list (map Trs As)) =
            [In a ⊕ In (Parallel_list As) ↝ In a @ In (Parallel_list As)] oo ([In a ↝ In a ] ∥ [In (Parallel_list As) ↝ concat (map In As)] oo Trs a ∥ parallel_list (map Trs As))"
        apply (subst comp_parallel_distrib)
        apply (simp add:   io_diagram_def)
        apply (simp )
        apply (subst TI_parallel_list)
        apply (simp add: Type_OK_def)
        apply simp
        apply (subst comp_id_switch) 
        by (simp_all add: io_diagram_def)
  
      lemma Trs_Parallel_list_aux_b :"distinct x ⟹ distinct y ⟹  set z ⊆ set y ⟹ [x ⊕ y ↝ x @ y] oo [x ↝ x] ∥ [y ↝ z] = [x ⊕ y ↝ x @ z]"
        by (subst switch_par_comp_Subst, simp_all add: distinct_addvars set_addvars Subst_eq)
  
  
      lemma Trs_Parallel_list: "Type_OK As ⟹ Trs (Parallel_list As) = [In (Parallel_list As) ↝ concat (map In As)] oo parallel_list (map Trs As)"
        apply (induction As)
        apply (simp add: Parallel_list_def ParallelId_def parallel_list_def)
        apply (simp add: distinct_id)
        apply simp
        apply (simp add: Parallel_def Let_def parallel_list_cons)
        apply (simp add: Type_OK_cons)
        apply (simp add: Trs_Parallel_list_aux_a)
        apply (subst comp_assoc[THEN sym])
        apply (simp_all)
        apply (simp add: io_diagram_def)
        apply (subst TI_parallel_list)
        apply (simp add: Type_OK_def)
        apply simp
        apply (subst Trs_Parallel_list_aux_b)
        apply (simp add: io_diagram_def)
        using io_diagram_def io_diagram_parallel_list apply blast
        apply (subst In_Parallel)
        by auto
(*
CompA update
      lemma CompA_Id[simp]: "CompA A □ = □"
        by (simp add: CompA_def comp_def ParallelId_def)
*) 
          
lemma CompA_Id[simp]: "A ⊳ □ = □"
  by (simp add: CompA_def comp_def ParallelId_def)
    

lemma io_diagram_ParallelId[simp]: "io_diagram □"
  by (simp add: io_diagram_def ParallelId_def)

(*move*)
lemma in_equiv_aux_a :"distinct x ⟹ distinct y ⟹  set z ⊆ set x ⟹ [x ⊕ y ↝ x @ y] oo [x ↝ z] ∥ [y ↝ y] = [x ⊕ y ↝ z @ y]"
  by (subst switch_par_comp_Subst, simp_all add: distinct_addvars set_addvars Subst_eq)

(*move*)
lemma in_equiv_Parallel_aux_d: "distinct x ⟹ distinct y ⟹ set u ⊆ set x ⟹ perm y v
           ⟹ [x ⊕ y ↝ x @ v] oo [x ↝ u] ∥ [v ↝ v] = [x ⊕ y ↝ u @ v]"
        proof -
          assume [simp]: "distinct x"
          assume [simp]: "distinct y"
          assume [simp]: "set u ⊆ set x"
          assume [simp]: "perm y v"

          define v' where "v' ≡ newvars x (TVs v)"

          have [simp]: "distinct v"
            apply (subgoal_tac "perm y v")
            apply (subgoal_tac "distinct y")
            using dist_perm apply blast
            by simp_all

          have [simp]: "distinct v'"
            by (simp add: v'_def)

          have [simp]: "set x ∩ set v' = {}"
            by (simp add: v'_def)

          have [simp]: "distinct (x ⊕ y)"
            by (simp add: distinct_addvars)

          have [simp]: "set v' ∩ set u = {}"
            apply (subgoal_tac "set v' ∩ set x = {}")
            apply (subgoal_tac "set u ⊆ set x")
            apply blast
            apply simp
            using ‹set x ∩ set v' = {}› by blast

          have A: "TVs v' = TVs v"
            by (simp add: v'_def)
            
          have [simp]: "length v' = length v"
            by (metis ‹TVs v' = TVs v› length_TVs)

          have [simp]: "Subst (x @ v') (x @ v) (u @ v') = u @ v"
            apply (simp add: Subst_append)
            apply (subst Subst_not_in)
            apply (simp_all)
            apply (subst Subst_not_in_a)
            by (simp_all add: Subst_eq)

          have "[x ⊕ y ↝ x @ v] oo [x ↝ u] ∥ [v ↝ v] = [x ⊕ y ↝ x @ v] oo [x ↝ u] ∥ [v' ↝ v']"
            by (simp add: v'_def switch_newvars)
          also have "... = [x ⊕ y ↝ x @ v] oo [x @ v' ↝ u @ v']"
            apply (subst par_switch)
            by (simp_all)
          also have "... = [x ⊕ y ↝ u @ v]"
            apply (subst switch_comp_subst)
            apply (simp_all)
            apply (simp add: set_addvars)
            using ‹perm y v› perm_set_eq apply blast
            apply (simp add: le_supI1)
            by (simp add: v'_def)
          finally show ?thesis
            by simp
        qed

(*move*)
lemma comp_par_switch_subst: "distinct x ⟹ distinct y ⟹ set u ⊆ set x ⟹ set v ⊆ set y 
      ⟹ [x ⊕ y ↝ x @ y] oo [x ↝ u] ∥ [y ↝ v] = [x ⊕ y ↝ u @ v]"
        proof -
          assume [simp]: "distinct x"
          assume [simp]: "distinct y"
          assume [simp]: "set u ⊆ set x"
          assume [simp]: "set v ⊆ set y"
        
          define x' where "x' ≡ newvars (x@y) (TVs x)"

          have [simp]: "distinct x'"
            by (simp add: x'_def)

          have [simp]: "set x ∩ set x' = {}"
            by (metis Int_empty_right inf.commute inf.left_commute inf_sup_absorb newvars_old_distinct set_append x'_def)

          have [simp]: "TVs x = TVs x'"
            by (simp add: x'_def)

          have [simp]: "length x = length x'"
            by (metis ‹TVs x = TVs x'› length_TVs)

          have [simp]: "set x' ∩ set y = {}"
            by (metis Diff_disjoint diff_distinct diff_inter_left diff_union inf_bot_left newvars_old_distinct_a set_diff set_inter x'_def)            

          have [simp]: "set (Subst x x' u) ⊆ set x'"
            by (simp add: Subst_set_incl)

          have [simp]: "distinct (x ⊕ y)"
            by (simp add: distinct_addvars)

          have [simp]: "set y ∩ set (Subst x x' u) = {}"
            apply (subgoal_tac "set (Subst x x' u) ⊆ set x'")
            apply (subgoal_tac "set y ∩ set x' = {}")
            apply blast
            by (simp_all add: Int_commute)

          have [simp]: "set x' ∩ set v = {}"
            apply (subgoal_tac "set v ⊆ set y")
            apply (subgoal_tac "set x' ∩ set y = {}")
            apply blast
            by simp_all

          have [simp]: "Subst (x' @ y) (x @ y) ((Subst x x' u) @ v) = u @ v"
            apply (simp add: Subst_append)
            apply (subst Subst_not_in, simp_all)
            apply (subst Subst_not_in_a, simp_all)
            by (simp add: Subst_eq)
         

          have "[x ⊕ y ↝ x @ y] oo [x ↝ u] ∥ [y ↝ v] = [x ⊕ y ↝ x @ y] oo [Subst x x' x ↝ Subst x x' u] ∥ [y ↝ v]"
            apply (cut_tac u=x and v=x' and x=x and y=u in Subst_switch_more_general)
            apply simp_all
            by (simp add: Int_commute)
          also have "... = [x ⊕ y ↝ x @ y] oo [x' ↝ Subst x x' u] ∥ [y ↝ v]"
            by simp
          also have "... = [x ⊕ y ↝ x @ y] oo [x' @ y ↝ (Subst x x' u) @ v]"
            by (simp add: par_switch)
          also have "... = [x ⊕ y ↝ Subst (x' @ y) (x @ y) ((Subst x x' u) @ v)]"
            apply (subst switch_comp_subst, simp_all add: set_addvars)
            apply safe
            using ‹set (Subst x x' u) ⊆ set x'› apply blast
            using ‹set v ⊆ set y› by blast
          also have "... = [x ⊕ y ↝ u @ v]"
            by simp_all

          finally show ?thesis
            by simp
        qed
          
(*move*)
      lemma in_equiv_Parallel_aux_b :"distinct x ⟹ distinct y ⟹ perm u x ⟹ perm y v ⟹ [x ⊕ y ↝ x @ y] oo [x ↝ u] ∥ [y ↝ v] = [x ⊕ y ↝ u @ v]"
        by (subst comp_par_switch_subst, simp_all )

(*move*)
lemma [simp]: "set x ⊆ set (x ⊕ y)"
  by (simp add: set_addvars)
    
(*move*)
lemma [simp]: "set y ⊆ set (x ⊕ y)"
  by (simp add: set_addvars)

      declare distinct_addvars [simp]

lemma in_equiv_Parallel: "io_diagram B ⟹ io_diagram B' ⟹ in_equiv A B ⟹ in_equiv A' B' ⟹ in_equiv (A ||| A') (B ||| B')"
  apply (frule in_equiv_io_diagram, simp_all)
  apply (frule_tac A = A' in in_equiv_io_diagram, simp)
  apply (frule_tac A = A in in_equiv_io_diagram, simp)
  apply (simp add: in_equiv_def io_diagram_def, safe)
  apply (simp add: Parallel_def)
  apply (subst comp_parallel_distrib[THEN sym], simp_all)
  apply (subst comp_assoc[THEN sym], simp_all)
  apply (subst comp_par_switch_subst, simp_all)
  apply (subst comp_assoc[THEN sym], simp_all)
  by (simp add: switch_comp)


      (*todo: change name to Out_CompA*)
      thm local.BBB_a

      lemma map_Out_CompA: "length (Out A) = 1 ⟹ map (out ∘ CompA A) As = map out As"
        by (induction As, simp_all add: BBB_a out_def)

(*
lemma CompA_in[simp]: "length (Out A) = 1 ⟹ out A ∈ set (In B) ⟹ A ⊳ B = A ;; B"
  by (simp add: CompA_def)

lemma CompA_not_in[simp]: "length (Out A) = 1 ⟹ out A ∉ set (In B) ⟹ CompA A B = B"
  by (simp add: CompA_def out_def)
*)

lemma CompA_in[simp]: "out A ∈ set (In B) ⟹ A ⊳ B = A ;; B"
  by (simp add: CompA_def)

lemma CompA_not_in[simp]: "out A ∉ set (In B) ⟹ A ⊳ B = B"
  by (simp add: CompA_def out_def)

          
lemma in_equiv_CompA_Parallel_a: " deterministic (Trs A) ⟹ length (Out A) = 1 ⟹ io_diagram A ⟹ io_diagram B ⟹ io_diagram C 
  ⟹ out A ∈ set (In B) ⟹ out A ∈ set (In C) 
  ⟹ in_equiv ((A ⊳ B) ||| (A ⊳ C)) (A ⊳ (B ||| C))"
        apply (simp add: in_equiv_def, safe)
        apply (simp add: In_CompA set_addvars)
        apply (simp_all add: Comp_def CompA_def Parallel_def Let_def Var_def set_addvars diff_inter_right diff_inter_left)
        apply (simp_all add: Out_out par_empty_left)
        apply (simp add: addvars_assoc [THEN sym])
        apply (metis addvars_assoc addvars_minus perm_mset)
        apply (simp_all add: set_addvars)
        proof -
          assume [simp]: "deterministic (Trs A)"
          assume [simp]: "length (Out A) = Suc 0"
          assume [simp]: "io_diagram A"
          assume [simp]: "io_diagram B"
          assume [simp]: "io_diagram C"
          assume [simp]: "out A ∈ set (In B)"
          assume [simp]: "out A ∈ set (In C)"

          define IA where "IA ≡ In A"
          define IB where "IB ≡ In B"
          define IC  where "IC ≡ In C"
          define OA where "OA ≡ Out A"
          define IBA where "IBA ≡ IB ⊖ OA"
          define ICA where "ICA ≡ IC ⊖ OA"

          define IBA' where "IBA' ≡ newvars (IA @ OA @ ICA @ IBA) (TVs IBA)"
          define IA' where "IA' ≡ newvars (IBA' @ IA @ ICA) (TVs IA)"
          define ICA' where "ICA' ≡ newvars (IA' @ IBA' @ IA @ OA) (TVs ICA)"
          define OA' where "OA' ≡ newvars (OA @ IBA' @ ICA' @ IBA @ ICA @ IA) (TVs OA)"

          have [simp]: "TVs IA = TI (Trs A)"
            using ‹io_diagram A› io_diagram_def IA_def by fastforce

          have [simp]: "distinct IA"
            using ‹io_diagram A› io_diagram_def IA_def by fastforce

          have [simp]: "TVs OA = TO (Trs A)"
            using ‹io_diagram A› io_diagram_def OA_def by fastforce

          have [simp]: "distinct OA "
            using ‹io_diagram A› io_diagram_def OA_def by fastforce
            
          have [simp]: "TVs IB = TI (Trs B)"
            using ‹io_diagram B› io_diagram_def IB_def by fastforce

          have [simp]: "distinct IB"
            using ‹io_diagram B› io_diagram_def IB_def by fastforce

          have [simp]: "TVs IC = TI (Trs C)"
            using ‹io_diagram C› io_diagram_def IC_def by fastforce

          have [simp]: "distinct IC"
            using ‹io_diagram C› io_diagram_def IC_def by fastforce

          have [simp]: "distinct IBA"
            by (simp add: IBA_def)

          have [simp]: "distinct ICA"
            by (simp add: ICA_def)

          have [simp]: "distinct (IA ⊕ IBA)"
            by (simp)

          have [simp]: "distinct (IA ⊕ ICA)"
            by (simp)

          have [simp]: "distinct IBA'"
            by (simp add: IBA'_def)

          have [simp]: "set IBA' ∩ set IA = {}"
            by (metis IBA'_def Int_commute bot_eq_sup_iff inf_sup_distrib2 newvars_old_distinct_a set_append)

          have a[simp]: "set OA ∩ set IBA' = {}"
            by (metis IBA'_def bot_eq_sup_iff inf_sup_distrib2 newvars_old_distinct_a set_append)

          have [simp]: "set IBA' ∩ set ICA = {}"
            by (metis IBA'_def Int_commute bot_eq_sup_iff inf_sup_distrib2 newvars_old_distinct_a set_append)

          have [simp]: "TVs IBA' = TVs IBA"
            by (simp add: IBA'_def)

          have [simp]: "distinct IA'"
            by (simp add: IA'_def)

          have [simp]: "set IA' ∩ set IBA' = {}"
            by (metis IA'_def Int_commute bot_eq_sup_iff inf_sup_distrib1 newvars_old_distinct_a set_append)

          have [simp]: "set IA' ∩ set IA = {}"
            by (metis IA'_def Int_commute bot_eq_sup_iff inf_sup_distrib1 newvars_old_distinct_a set_append)

          have [simp]:"distinct ICA'"
            by (simp add: ICA'_def)

          have [simp]: "set IA ∩ set ICA' = {}"
            by (metis ICA'_def Int_empty_right inf_commute inf_left_commute inf_sup_absorb inf_sup_aci(5) newvars_old_distinct set_append)

          have [simp]: "set IBA' ∩ set ICA' = {}"
            by (metis ICA'_def Int_empty_right inf_commute inf_left_commute inf_sup_absorb inf_sup_aci(5) newvars_old_distinct set_append)

          have [simp]: "set IA' ∩ set ICA' = {}"
            by (metis ICA'_def Int_empty_right inf_commute inf_left_commute inf_sup_absorb newvars_old_distinct set_append)

          have [simp]: "TVs (IA') = TI (Trs A) "
            by (simp add: IA'_def)

          have [simp]: "TVs ICA = TVs ICA'"
            by (simp add: ICA'_def)

          have [simp]: "length IA' = length IA"
            by (simp add: TVs_length_eq)

          have [simp]: "length IBA' = length IBA"
            by (metis ‹TVs IBA' = TVs IBA› length_TVs)

          have [simp]: "length ICA' = length ICA"
            by (metis ‹TVs ICA = TVs ICA'› length_TVs)

          have [simp]: "Subst (IA' @ IBA' @ IA @ ICA') (IA @ IBA @ IA @ ICA) IA' = IA"
            apply (subst Subst_not_in, simp_all)
            by (simp add: Int_commute)

          have [simp]: "Subst (IA' @ IBA' @ IA @ ICA') (IA @ IBA @ IA @ ICA) IA = IA"
            apply (subst Subst_not_in_a, simp_all)
            apply (subst Subst_not_in_a, simp_all)
            by (subst Subst_not_in, simp_all add: Int_commute)

          have [simp]: "Subst (IA' @ IBA' @ IA @ ICA') (IA @ IBA @ IA @ ICA) IBA' = IBA"
            apply (subst Subst_not_in_a, simp_all)
            apply (subst Subst_not_in, simp_all add: Int_commute)
            using ‹set IBA' ∩ set IA = {}› by blast

          have [simp]: "Subst (IA' @ IBA' @ IA @ ICA') (IA @ IBA @ IA @ ICA) ICA' = ICA"
            apply (subst Subst_not_in_a, simp_all)
            apply (subst Subst_not_in_a, simp_all)
            by (subst Subst_not_in_a, simp_all)

          have [simp]: "Subst (IA' @ IBA' @ IA @ ICA') (IA @ IBA @ IA @ ICA) (IA' @ IA @ IBA' @ ICA') = IA @ IA @ IBA @ ICA"
            by (simp add: Subst_append)

          have [simp]: "distinct OA'"
            by (simp add: OA'_def)

          have [simp]: "TVs OA' = TO (Trs A)"
            by (simp add: OA'_def)

          have [simp]: "set OA' ∩ set OA = {}"
            by (metis OA'_def Int_commute bot_eq_sup_iff inf_sup_distrib1 newvars_old_distinct_a set_append)

          have [simp]: "set OA' ∩ set IBA' = {}"
            by (metis OA'_def Int_commute bot_eq_sup_iff inf_sup_distrib1 newvars_old_distinct_a set_append)

          have [simp]: "set OA' ∩ set ICA' = {}"
            by (metis OA'_def Int_commute bot_eq_sup_iff inf_sup_distrib1 newvars_old_distinct_a set_append)

          have [simp]: "set OA' ∩ set IBA = {}"
            by (metis OA'_def Int_commute bot_eq_sup_iff inf_sup_distrib1 newvars_old_distinct_a set_append)

          have [simp]: "set OA' ∩ set ICA = {}"
            by (metis OA'_def Int_commute bot_eq_sup_iff inf_sup_distrib1 newvars_old_distinct_a set_append)

          have [simp]: "set OA ∩ set ICA' = {}"
            by (metis ICA'_def Int_commute bot_eq_sup_iff inf_sup_distrib1 newvars_old_distinct_a set_append)

          have [simp]: "set IBA' ∩ set IBA = {}"
            by (metis IBA'_def Int_commute bot_eq_sup_iff inf_sup_distrib1 newvars_old_distinct_a set_append)

          have [simp]: "set IBA ∩ set OA = {}"
            apply (simp add: IBA_def set_diff)
            by blast

          have [simp]: "length OA = length OA'"
            by (simp add: TVs_length_eq)

          have [simp]: "[IA ↝ IA @ IA] oo Trs A ∥ Trs A = Trs A oo [OA ↝ OA @ OA]"
            apply (subgoal_tac "deterministic (Trs A)")
            apply (simp add: deterministicE)
            by simp

          have [simp]: "Subst (OA' @ OA @ IBA' @ ICA') (OA @ OA @ IBA' @ ICA) OA' = OA"
            apply (subst Subst_not_in, simp_all)
            using ‹set OA' ∩ set IBA' = {}› ‹set OA' ∩ set ICA' = {}› ‹set OA' ∩ set OA = {}› by blast

          have [simp]: "Subst (OA' @ OA @ IBA' @ ICA') (OA @ OA @ IBA' @ ICA) IBA' = IBA'"
            apply (subst Subst_not_in_a, simp_all)
            apply (subst Subst_not_in_a, simp_all)
            apply (subst Subst_not_in, simp_all)
            by (simp add: Int_commute)

          have [simp]: "Subst (OA' @ OA @ IBA' @ ICA') (OA @ OA @ IBA' @ ICA) OA = OA "
            apply (subst Subst_not_in_a, simp_all)
            apply (subst Subst_not_in, simp_all)
            by (metis Int_commute Un_absorb ‹set OA ∩ set ICA' = {}› a inf_sup_distrib2)
            
          have [simp]: "Subst (OA' @ OA @ IBA' @ ICA') (OA @ OA @ IBA' @ ICA) ICA' = ICA"
            apply (subst Subst_not_in_a, simp_all)
            apply (subst Subst_not_in_a, simp_all)
            by (subst Subst_not_in_a, simp_all)

          have [simp]: "Subst (OA' @ OA @ IBA' @ ICA') (OA @ OA @ IBA' @ ICA) (OA' @ IBA' @ OA @ ICA') = OA @ IBA' @ OA @ ICA"
            by (simp add: Subst_append)

          have [simp]: "distinct (IA ⊕ IBA ⊕ (IA ⊕ ICA))"
            by (simp)

          have [simp]: "perm (IA ⊕ IBA ⊕ (IA ⊕ ICA)) (IA ⊕ (IB ⊕ IC ⊖ OA))"
            apply (simp add: IBA_def ICA_def)
            by (metis diff_eq addvars_assoc addvars_def addvars_empty addvars_minus perm_tp perm_trans)

          have [simp]: "distinct (IB ⊕ IC ⊖ OA)"
            by (simp )

          have [simp]: "set OA ∩ set (IB ⊕ IC ⊖ OA) = {}"
            by (simp add: set_diff)

          have [simp]: "OA ⊗ IB = OA"
            by (simp add: OA_def IB_def Out_out)

          have [simp]: "OA ⊗ IC = OA"
            by (simp add: OA_def IC_def Out_out)

          have [simp]: "OA ⊗ (IB ⊕ IC) = OA"
            apply (simp add: addvars_def)
            by (metis (mono_tags, lifting) diff_eq Diff_Int_distrib ‹OA ⊗ IB = OA› ‹OA ⊗ IC = OA› empty_set inter_addvars_empty set_diff set_inter)
            
          have [simp]: "perm (OA @ (IB ⊕ IC ⊖ OA)) (IB ⊕ IC)"
            by (subst perm_aux_a, simp_all)

          have [simp]: "set OA' ∩ set IA = {}"
            by (metis OA'_def Int_commute bot_eq_sup_iff inf_sup_distrib1 newvars_old_distinct_a set_append)

          have [simp]: "set OA' ∩ set (IA ⊕ IBA ⊕ (IA ⊕ ICA)) = {}"
            by (simp add: set_addvars)

          have [simp]: "Subst (OA @ IBA' @ ICA) (OA' @ IBA @ ICA) OA = OA'"
            apply (subst Subst_not_in, simp_all)
            by (metis Diff_disjoint ICA_def Int_Un_distrib2 Un_empty_left a inf_commute set_diff)

          have [simp]: "Subst (OA @ IBA' @ ICA) (OA' @ IBA @ ICA) IBA' = IBA"
            apply (subst Subst_not_in_a, simp_all)
            apply (subst Subst_not_in, simp_all)
            by (simp add: Int_commute)

          have [simp]: "Subst (OA @ IBA' @ ICA) (OA' @ IBA @ ICA) ICA = ICA"
            apply (subst Subst_not_in_a, simp_all)
            apply (simp add: ICA_def set_diff)
            by (subst Subst_not_in_a, simp_all)

          have [simp]: "Subst (OA @ IBA' @ ICA) (OA' @ IBA @ ICA) (OA @ IBA' @ OA @ ICA) = OA' @ IBA @ OA' @ ICA"
            by (simp add: Subst_append)

          have [simp]: "Subst (OA @ (IBA ⊕ ICA)) (OA' @ (IBA ⊕ ICA)) IB = Subst (OA @ IBA) (OA' @ IBA) IB"
            apply (subst Subst_cancel_left, simp_all)
            apply (simp add: IBA_def ICA_def set_addvars set_diff)
            apply (subst Subst_cancel_left, simp_all)
            by (simp add: IBA_def set_addvars set_diff)

          have [simp]: "Subst (OA @ (IBA ⊕ ICA)) (OA' @ (IBA ⊕ ICA)) IC = Subst (OA @ ICA) (OA' @ ICA) IC"
            apply (subst Subst_cancel_left, simp_all)
            apply (simp add: IBA_def ICA_def set_addvars set_diff)
            apply (subst Subst_cancel_left, simp_all)
            by (simp add: ICA_def set_addvars set_diff)
            
          have [simp]: "Subst (OA @ (IBA ⊕ ICA)) (OA' @ (IBA ⊕ ICA)) (IB @ IC) = (Subst (OA @ IBA) (OA' @ IBA ) IB) @ (Subst (OA @ ICA) (OA' @ ICA) IC)"
            by (simp add: Subst_append)

            
          have A: "[In A ⊕ (In B ⊖ [out A]) ⊕ (In A ⊕ (In C ⊖ [out A])) ↝ (In A ⊕ (In B ⊖ [out A])) @ (In A ⊕ (In C ⊖ [out A]))] oo
                ([In A ⊕ (In B ⊖ [out A]) ↝ In A @ (In B ⊖ [out A])] oo Trs A ∥ [In B ⊖ [out A] ↝ In B ⊖ [out A] ] oo [out A # (In B ⊖ [out A]) ↝ In B] oo Trs B) ∥
                ([In A ⊕ (In C ⊖ [out A]) ↝ In A @ (In C ⊖ [out A])] oo Trs A ∥ [In C ⊖ [out A] ↝ In C ⊖ [out A] ] oo [out A # (In C ⊖ [out A]) ↝ In C] oo Trs C) =
                [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IBA @ ICA] oo 
                Trs A  ∥ [IBA' @ ICA ↝ IBA' @ ICA] oo 
                ([OA @ IBA' @ ICA ↝ OA @ IBA' @ OA @ ICA] oo [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C)"
            proof -
              have "[In A ⊕ (In B ⊖ [out A]) ⊕ (In A ⊕ (In C ⊖ [out A])) ↝ (In A ⊕ (In B ⊖ [out A])) @ (In A ⊕ (In C ⊖ [out A]))] oo
                  ([In A ⊕ (In B ⊖ [out A]) ↝ In A @ (In B ⊖ [out A])] oo Trs A ∥ [In B ⊖ [out A] ↝ In B ⊖ [out A] ] oo [out A # (In B ⊖ [out A]) ↝ In B] oo Trs B) ∥
                  ([In A ⊕ (In C ⊖ [out A]) ↝ In A @ (In C ⊖ [out A])] oo Trs A ∥ [In C ⊖ [out A] ↝ In C ⊖ [out A] ] oo [out A # (In C ⊖ [out A]) ↝ In C] oo Trs C) =
                  [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ (IA ⊕ IBA) @ (IA ⊕ ICA)] oo
                  ([IA ⊕ IBA ↝ IA @ IBA] oo Trs A ∥ [IBA ↝ IBA] oo [OA @ IBA ↝ IB] oo Trs B) ∥
                  ([IA ⊕ ICA ↝ IA @ ICA] oo Trs A ∥ [ICA ↝ ICA] oo [OA @ ICA ↝ IC] oo Trs C)"
                by (simp add: IA_def IB_def IC_def IBA_def ICA_def OA_def Out_out)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ (IA ⊕ IBA) @ (IA ⊕ ICA)] oo
                  ([IA ⊕ IBA ↝ IA @ IBA] ∥ [IA ⊕ ICA ↝ IA @ ICA] oo
                   (Trs A ∥ [IBA ↝ IBA]) ∥ (Trs A ∥ [ICA ↝ ICA]) oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C)"
                by (simp add: comp_parallel_distrib )
              also have "... = ([(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ (IA ⊕ IBA) @ (IA ⊕ ICA)] oo [IA ⊕ IBA ↝ IA @ IBA] ∥ [IA ⊕ ICA ↝ IA @ ICA]) oo
                   (Trs A ∥ [IBA ↝ IBA]) ∥ (Trs A ∥ [ICA ↝ ICA]) oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by (simp add: comp_assoc )
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ (IA @ IBA) @ (IA @ ICA)] oo
                   (Trs A ∥ [IBA ↝ IBA]) ∥ (Trs A ∥ [ICA ↝ ICA]) oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                apply (subst comp_par_switch_subst)
                by (simp_all add: set_addvars)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ (IA @ IBA) @ (IA @ ICA)] oo
                   Trs A ∥ ([IBA ↝ IBA] ∥ Trs A) ∥ [ICA ↝ ICA] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by (simp add: par_assoc)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ (IA @ IBA) @ (IA @ ICA)] oo
                   Trs A ∥ ([IBA' ↝ IBA'] ∥ Trs A) ∥ [ICA ↝ ICA] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by (simp add: IBA'_def switch_newvars)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ (IA @ IBA) @ (IA @ ICA)] oo
                   Trs A ∥ ([IBA' @ IA ↝ IA @ IBA'] oo Trs A ∥ [IBA' ↝ IBA'] oo [OA @ IBA' ↝ IBA' @ OA]) ∥ [ICA ↝ ICA] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                apply (cut_tac y=IA and x="IBA'" and T="Trs A" and S="[IBA' ↝ IBA']" and u=OA and v="IBA'" in switch_par)
                by simp_all
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ (IA @ IBA) @ (IA @ ICA)] oo
                   ([IA ↝ IA] ∥ [IBA' @ IA ↝ IA @ IBA'] ∥ [ICA ↝ ICA] oo Trs A ∥ (Trs A ∥ [IBA' ↝ IBA']) ∥ [ICA ↝ ICA] oo [OA ↝ OA] ∥ [OA @ IBA' ↝ IBA' @ OA] ∥ [ICA ↝ ICA]) oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by (simp add: comp_parallel_distrib )
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ (IA @ IBA) @ (IA @ ICA)] oo
                   [IA ↝ IA] ∥ [IBA' @ IA ↝ IA @ IBA'] ∥ [ICA ↝ ICA] oo 
                   Trs A ∥ (Trs A ∥ [IBA' ↝ IBA']) ∥ [ICA ↝ ICA] oo 
                   [OA ↝ OA] ∥ [OA @ IBA' ↝ IBA' @ OA] ∥ [ICA ↝ ICA] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by (simp add: comp_assoc  )
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ (IA @ IBA) @ (IA @ ICA)] oo
                   [IA ↝ IA] ∥ [IBA' @ IA ↝ IA @ IBA'] ∥ [ICA ↝ ICA] oo 
                   (Trs A ∥ Trs A) ∥ [IBA' ↝ IBA'] ∥ [ICA ↝ ICA] oo 
                   [OA ↝ OA] ∥ [OA @ IBA' ↝ IBA' @ OA] ∥ [ICA ↝ ICA] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by (simp add: par_assoc)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ (IA @ IBA) @ (IA @ ICA)] oo
                   [IA' ↝ IA'] ∥ [IBA' @ IA ↝ IA @ IBA'] ∥ [ICA ↝ ICA] oo 
                   (Trs A ∥ Trs A) ∥ [IBA' ↝ IBA'] ∥ [ICA ↝ ICA] oo 
                   [OA ↝ OA] ∥ [OA @ IBA' ↝ IBA' @ OA] ∥ [ICA ↝ ICA] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by (simp add: IA'_def distinct_id)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ (IA @ IBA) @ (IA @ ICA)] oo
                   [IA' ↝ IA'] ∥ [IBA' @ IA ↝ IA @ IBA'] ∥ [ICA' ↝ ICA'] oo 
                   (Trs A ∥ Trs A) ∥ [IBA' ↝ IBA'] ∥ [ICA ↝ ICA] oo 
                   [OA ↝ OA] ∥ [OA @ IBA' ↝ IBA' @ OA] ∥ [ICA ↝ ICA] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by (metis (full_types) switch_newvars ICA'_def ‹distinct ICA›)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ (IA @ IBA) @ (IA @ ICA)] oo
                   [IA' @ IBA' @ IA @ ICA' ↝ IA' @ IA @ IBA' @ ICA'] oo 
                   (Trs A ∥ Trs A) ∥ [IBA' ↝ IBA'] ∥ [ICA ↝ ICA] oo 
                   [OA ↝ OA] ∥ [OA @ IBA' ↝ IBA' @ OA] ∥ [ICA ↝ ICA] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                apply (subst par_switch, simp_all)
                apply (subst par_switch, simp_all)
                by auto
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IA @ IBA @ ICA] oo 
                   (Trs A ∥ Trs A) ∥ [IBA' ↝ IBA'] ∥ [ICA ↝ ICA] oo 
                   [OA ↝ OA] ∥ [OA @ IBA' ↝ IBA' @ OA] ∥ [ICA ↝ ICA] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                apply (subst switch_comp_subst, simp_all )
                by (auto simp add: IA_def IBA_def IB_def OA_def ICA_def IC_def set_diff set_inter set_addvars)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IA @ IBA @ ICA] oo 
                   (Trs A ∥ Trs A) ∥ [IBA' @ ICA  ↝ IBA' @ ICA ] oo 
                   [OA ↝ OA] ∥ [OA @ IBA' ↝ IBA' @ OA] ∥ [ICA ↝ ICA] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                apply (simp add: par_assoc)
                by (subst par_switch, simp_all)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IA @ IBA @ ICA] oo 
                   (Trs A ∥ Trs A) ∥ [IBA' @ ICA  ↝ IBA' @ ICA ] oo 
                   [OA ↝ OA] ∥ [OA @ IBA' ↝ IBA' @ OA] ∥ [ICA' ↝ ICA'] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by (metis (full_types) switch_newvars ICA'_def ‹distinct ICA›)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IA @ IBA @ ICA] oo 
                   (Trs A ∥ Trs A) ∥ [IBA' @ ICA  ↝ IBA' @ ICA ] oo 
                   [OA' ↝ OA'] ∥ [OA @ IBA' ↝ IBA' @ OA] ∥ [ICA' ↝ ICA'] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by (metis switch_newvars  OA'_def ‹distinct OA›)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IA @ IBA @ ICA] oo 
                   (Trs A ∥ Trs A) ∥ [IBA' @ ICA  ↝ IBA' @ ICA ] oo 
                   [OA' @ OA @ IBA' @ ICA' ↝ OA' @ IBA' @ OA @ ICA'] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                apply (subst par_switch, simp_all)
                apply (subst par_switch, simp_all)
                by blast
              also have "... = ([(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IBA @ ICA] oo [IA ↝ IA @ IA] ∥ [IBA' @ ICA ↝ IBA' @ ICA]) oo 
                   (Trs A ∥ Trs A) ∥ [IBA' @ ICA  ↝ IBA' @ ICA ] oo 
                   [OA' @ OA @ IBA' @ ICA' ↝ OA' @ IBA' @ OA @ ICA'] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                apply (subst switch_par_comp_Subst, simp_all add: set_addvars Subst_eq )
                apply blast
                by blast
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IBA @ ICA] oo 
                   ([IA ↝ IA @ IA] ∥ [IBA' @ ICA ↝ IBA' @ ICA] oo (Trs A ∥ Trs A) ∥ [IBA' @ ICA  ↝ IBA' @ ICA ]) oo 
                   [OA' @ OA @ IBA' @ ICA' ↝ OA' @ IBA' @ OA @ ICA'] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by (simp add: comp_assoc  )
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IBA @ ICA] oo 
                   (([IA ↝ IA @ IA] oo (Trs A ∥ Trs A)) ∥ [IBA' @ ICA ↝ IBA' @ ICA]) oo 
                   [OA' @ OA @ IBA' @ ICA' ↝ OA' @ IBA' @ OA @ ICA'] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by (simp add: comp_parallel_distrib)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IBA @ ICA] oo 
                   ((Trs A oo [OA ↝ OA @ OA]) ∥ [IBA' @ ICA ↝ IBA' @ ICA]) oo 
                   [OA' @ OA @ IBA' @ ICA' ↝ OA' @ IBA' @ OA @ ICA'] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                 by simp
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IBA @ ICA] oo 
                   (Trs A  ∥ [IBA' @ ICA ↝ IBA' @ ICA] oo [OA ↝ OA @ OA] ∥ [IBA' @ ICA ↝ IBA' @ ICA]) oo 
                   [OA' @ OA @ IBA' @ ICA' ↝ OA' @ IBA' @ OA @ ICA'] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by (simp add: comp_parallel_distrib)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IBA @ ICA] oo 
                   (Trs A  ∥ [IBA' @ ICA ↝ IBA' @ ICA] oo [OA @ IBA' @ ICA ↝ OA @ OA @ IBA' @ ICA]) oo 
                   [OA' @ OA @ IBA' @ ICA' ↝ OA' @ IBA' @ OA @ ICA'] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                apply (subst par_switch, simp_all)
                by (simp add: ICA_def set_diff)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IBA @ ICA] oo 
                   Trs A  ∥ [IBA' @ ICA ↝ IBA' @ ICA] oo 
                   ([OA @ IBA' @ ICA ↝ OA @ OA @ IBA' @ ICA] oo [OA' @ OA @ IBA' @ ICA' ↝ OA' @ IBA' @ OA @ ICA']) oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by (simp add: comp_assoc  )
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IBA @ ICA] oo 
                   Trs A  ∥ [IBA' @ ICA ↝ IBA' @ ICA] oo 
                   [OA @ IBA' @ ICA ↝ Subst (OA' @ OA @ IBA' @ ICA') (OA @ OA @ IBA' @ ICA) (OA' @ IBA' @ OA @ ICA')] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                 apply (subst switch_comp_subst, simp_all)
                 by auto
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IBA @ ICA] oo 
                   Trs A  ∥ [IBA' @ ICA ↝ IBA' @ ICA] oo 
                   [OA @ IBA' @ ICA ↝ OA @ IBA' @ OA @ ICA] oo
                   [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo
                   Trs B ∥ Trs C"
                by simp
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ IBA @ ICA] oo 
                   Trs A  ∥ [IBA' @ ICA ↝ IBA' @ ICA] oo 
                   ([OA @ IBA' @ ICA ↝ OA @ IBA' @ OA @ ICA] oo [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C)"              
                by (simp add: comp_assoc  )
              finally show ?thesis
                by simp
            qed

          have B: "[In A ⊕ (In B ⊖ [out A]) ⊕ (In A ⊕ (In C ⊖ [out A])) ↝ In A ⊕ (In B ⊕ In C ⊖ [out A])] oo
              ([In A ⊕ (In B ⊕ In C ⊖ [out A]) ↝ In A @ (In B ⊕ In C ⊖ [out A])] oo Trs A ∥ [In B ⊕ In C ⊖ [out A] ↝ In B ⊕ In C ⊖ [out A] ] oo [out A # (In B ⊕ In C ⊖ [out A]) ↝ In B ⊕ In C] oo
              ([In B ⊕ In C ↝ In B @ In C] oo Trs B ∥ Trs C)) =
               [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ IC ⊖ OA)] oo 
              Trs A ∥ [IB ⊕ IC ⊖ OA ↝ IB ⊕ IC ⊖ OA] oo 
              ([OA @ (IB ⊕ IC ⊖ OA) ↝ IB @ IC] oo Trs B ∥ Trs C)"
            proof - 
              have "[In A ⊕ (In B ⊖ [out A]) ⊕ (In A ⊕ (In C ⊖ [out A])) ↝ In A ⊕ (In B ⊕ In C ⊖ [out A])] oo
                  ([In A ⊕ (In B ⊕ In C ⊖ [out A]) ↝ In A @ (In B ⊕ In C ⊖ [out A])] oo Trs A ∥ [In B ⊕ In C ⊖ [out A] ↝ In B ⊕ In C ⊖ [out A] ] oo [out A # (In B ⊕ In C ⊖ [out A]) ↝ In B ⊕ In C] oo
                  ([In B ⊕ In C ↝ In B @ In C] oo Trs B ∥ Trs C)) =
                  [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA ⊕ (IB ⊕ IC ⊖ OA)] oo
                  ([IA ⊕ (IB ⊕ IC ⊖ OA) ↝ IA @ (IB ⊕ IC ⊖ OA)] oo Trs A ∥ [IB ⊕ IC ⊖ OA ↝ IB ⊕ IC ⊖ OA] oo [OA @ (IB ⊕ IC ⊖ OA) ↝ IB ⊕ IC] oo
                  ([IB ⊕ IC ↝ IB @ IC] oo Trs B ∥ Trs C))"
                by (simp add: IA_def IB_def IC_def OA_def IBA_def ICA_def Out_out)
              also have "... = ([(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA ⊕ (IB ⊕ IC ⊖ OA)] oo [IA ⊕ (IB ⊕ IC ⊖ OA) ↝ IA @ (IB ⊕ IC ⊖ OA)]) oo 
                  Trs A ∥ [IB ⊕ IC ⊖ OA ↝ IB ⊕ IC ⊖ OA] oo [OA @ (IB ⊕ IC ⊖ OA) ↝ IB ⊕ IC] oo
                  ([IB ⊕ IC ↝ IB @ IC] oo Trs B ∥ Trs C)"
                by (simp add: comp_assoc  )
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ IC ⊖ OA)] oo 
                  Trs A ∥ [IB ⊕ IC ⊖ OA ↝ IB ⊕ IC ⊖ OA] oo [OA @ (IB ⊕ IC ⊖ OA) ↝ IB ⊕ IC] oo
                  ([IB ⊕ IC ↝ IB @ IC] oo Trs B ∥ Trs C)"
                by (subst switch_comp, simp_all)
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ IC ⊖ OA)] oo 
                  Trs A ∥ [IB ⊕ IC ⊖ OA ↝ IB ⊕ IC ⊖ OA] oo 
                  (([OA @ (IB ⊕ IC ⊖ OA) ↝ IB ⊕ IC] oo [IB ⊕ IC ↝ IB @ IC]) oo Trs B ∥ Trs C)"
                by (simp add: comp_assoc  )
              also have "... = [(IA ⊕ IBA) ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ IC ⊖ OA)] oo 
                  Trs A ∥ [IB ⊕ IC ⊖ OA ↝ IB ⊕ IC ⊖ OA] oo 
                  ([OA @ (IB ⊕ IC ⊖ OA) ↝ IB @ IC] oo Trs B ∥ Trs C)"
                by (subst switch_comp, simp_all)
              finally show ?thesis
                by simp
            qed

          have C: "[OA ↝ OA] ∥ [IA ⊕ IBA ⊕ (IA ⊕ ICA) ↝ IBA @ ICA] oo [OA @ IBA' @ ICA ↝ OA @ IBA' @ OA @ ICA] oo [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] =
                   [OA' @ (IA ⊕ IBA ⊕ (IA ⊕ ICA)) ↝ (Subst (OA @ IBA) (OA' @ IBA ) IB) @ (Subst (OA @ ICA) (OA' @ ICA) IC)]"
            proof -
              have "[OA ↝ OA] ∥ [IA ⊕ IBA ⊕ (IA ⊕ ICA) ↝ IBA @ ICA] oo [OA @ IBA' @ ICA ↝ OA @ IBA' @ OA @ ICA] oo [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] =
                    [OA' ↝ OA'] ∥ [IA ⊕ IBA ⊕ (IA ⊕ ICA) ↝ IBA @ ICA] oo [OA @ IBA' @ ICA ↝ OA @ IBA' @ OA @ ICA] oo [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC]"
                by (metis ‹distinct OA› OA'_def switch_newvars)
              also have "... = [OA' @ (IA ⊕ IBA ⊕ (IA ⊕ ICA)) ↝ OA' @ IBA @ ICA ] oo [OA @ IBA' @ ICA ↝ OA @ IBA' @ OA @ ICA] oo [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC]"
                apply (subst par_switch, simp_all add: set_addvars)
                by blast
              also have "... = [OA' @ (IA ⊕ IBA ⊕ (IA ⊕ ICA)) ↝ OA' @ IBA @ OA' @ ICA] oo [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC]"
                apply (subst switch_comp_subst, simp_all)
                apply (simp_all add: ICA_def set_diff)
                by (auto simp add: set_addvars set_diff)
              also have "... = [OA' @ (IA ⊕ IBA ⊕ (IA ⊕ ICA)) ↝ (OA' @ IBA) @ (OA' @ ICA)] oo [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC]"
                by simp
              also have "... = [OA' @ (IA ⊕ IBA ⊕ (IA ⊕ ICA)) ↝ (Subst (OA @ IBA) (OA' @ IBA ) IB) @ (Subst (OA @ ICA) (OA' @ ICA) IC)]"
                apply (subst switch_par_comp_Subst, simp_all)
                apply (simp add: IBA_def set_diff)
                apply (simp add: ICA_def set_diff)
                apply (simp_all add: set_addvars)
                apply blast
                apply blast
                by (simp_all add: IBA_def ICA_def set_diff)
              finally show ?thesis
                by simp
            qed
         
          have D: "[OA ↝ OA] ∥ [IA ⊕ IBA ⊕ (IA ⊕ ICA) ↝ IB ⊕ IC ⊖ OA] oo [OA @ (IB ⊕ IC ⊖ OA) ↝ IB @ IC] = 
                   [OA' @ (IA ⊕ IBA ⊕ (IA ⊕ ICA)) ↝ (Subst (OA @ IBA) (OA' @ IBA ) IB) @ (Subst (OA @ ICA) (OA' @ ICA) IC)]"
            proof -
              have "[OA ↝ OA] ∥ [IA ⊕ IBA ⊕ (IA ⊕ ICA) ↝ IB ⊕ IC ⊖ OA] oo [OA @ (IB ⊕ IC ⊖ OA) ↝ IB @ IC] = 
                    [OA' ↝ OA'] ∥ [IA ⊕ IBA ⊕ (IA ⊕ ICA) ↝ IB ⊕ IC ⊖ OA] oo [OA @ (IB ⊕ IC ⊖ OA) ↝ IB @ IC]"
                by (metis ‹distinct OA› OA'_def switch_newvars)
              also have "... = [OA' @ (IA ⊕ IBA ⊕ (IA ⊕ ICA)) ↝ OA' @ (IB ⊕ IC ⊖ OA)] oo [OA @ (IB ⊕ IC ⊖ OA) ↝ IB @ IC]"
                apply (subst par_switch, simp_all)
                apply (simp add: IBA_def ICA_def set_diff set_addvars)
                by blast
              also have "... = [OA' @ (IA ⊕ IBA ⊕ (IA ⊕ ICA))  ↝ Subst (OA @ (IB ⊕ IC ⊖ OA)) (OA' @ (IB ⊕ IC ⊖ OA)) (IB @ IC)]"
                apply (subst switch_comp_subst, simp_all)
                by (auto simp add: set_addvars set_diff OA_def IBA_def IC_def ICA_def)
              also have "... = [OA' @ (IA ⊕ IBA ⊕ (IA ⊕ ICA)) ↝ Subst (OA @ (IBA ⊕ ICA)) (OA' @ (IBA ⊕ ICA)) (IB @ IC)]"
                by (simp add: addvars_minus IBA_def[THEN symmetric] ICA_def [THEN symmetric])
              also have "... = [OA' @ (IA ⊕ IBA ⊕ (IA ⊕ ICA)) ↝ (Subst (OA @ IBA) (OA' @ IBA ) IB) @ (Subst (OA @ ICA) (OA' @ ICA) IC)]"
                by simp
              finally show ?thesis
                by simp
            qed

          have E: "[OA ↝ OA] ∥ [IA ⊕ IBA ⊕ (IA ⊕ ICA) ↝ IBA @ ICA] oo ([OA @ IBA' @ ICA ↝ OA @ IBA' @ OA @ ICA] oo [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C) =
                   [OA ↝ OA] ∥ [IA ⊕ IBA ⊕ (IA ⊕ ICA) ↝ IB ⊕ IC ⊖ OA] oo ([OA @ (IB ⊕ IC ⊖ OA) ↝ IB @ IC] oo Trs B ∥ Trs C)"
            apply (subgoal_tac "[OA ↝ OA] ∥ [IA ⊕ IBA ⊕ (IA ⊕ ICA) ↝ IBA @ ICA] oo [OA @ IBA' @ ICA ↝ OA @ IBA' @ OA @ ICA] oo [OA @ IBA ↝ IB] ∥ [OA @ ICA ↝ IC] = [OA ↝ OA] ∥ [IA ⊕ IBA ⊕ (IA ⊕ ICA) ↝ IB ⊕ IC ⊖ OA] oo [OA @ (IB ⊕ IC ⊖ OA) ↝ IB @ IC]")
            apply (simp add: comp_assoc [THEN sym]  )
            by (simp add: C D)

          show "[In A ⊕ (In B ⊖ [out A]) ⊕ (In A ⊕ (In C ⊖ [out A])) ↝ (In A ⊕ (In B ⊖ [out A])) @ (In A ⊕ (In C ⊖ [out A]))] oo
              ([In A ⊕ (In B ⊖ [out A]) ↝ In A @ (In B ⊖ [out A])] oo Trs A ∥ [In B ⊖ [out A] ↝ In B ⊖ [out A] ] oo [out A # (In B ⊖ [out A]) ↝ In B] oo Trs B) ∥
              ([In A ⊕ (In C ⊖ [out A]) ↝ In A @ (In C ⊖ [out A])] oo Trs A ∥ [In C ⊖ [out A] ↝ In C ⊖ [out A] ] oo [out A # (In C ⊖ [out A]) ↝ In C] oo Trs C) =
              [In A ⊕ (In B ⊖ [out A]) ⊕ (In A ⊕ (In C ⊖ [out A])) ↝ In A ⊕ (In B ⊕ In C ⊖ [out A])] oo
              ([In A ⊕ (In B ⊕ In C ⊖ [out A]) ↝ In A @ (In B ⊕ In C ⊖ [out A])] oo Trs A ∥ [In B ⊕ In C ⊖ [out A] ↝ In B ⊕ In C ⊖ [out A] ] oo [out A # (In B ⊕ In C ⊖ [out A]) ↝ In B ⊕ In C] oo
              ([In B ⊕ In C ↝ In B @ In C] oo Trs B ∥ Trs C))"
            apply (simp add: A B)
            apply (rule_tac v="OA" in par_switch_eq, simp_all add:   set_addvars set_diff)
            apply blast
            apply blast
            apply (simp add: IBA_def ICA_def set_diff)
            apply blast
            by (simp add: E)
        qed

      lemma in_equiv_CompA_Parallel_c: "length (Out A) = 1 ⟹ io_diagram A ⟹ io_diagram B ⟹ io_diagram C ⟹ out A ∉ set (In B) ⟹ out A ∈ set (In C) ⟹ 
              in_equiv (CompA A B ||| CompA A C) (CompA A (B ||| C))"
        apply (simp add: in_equiv_def, safe)
        apply (simp add: Comp_def Let_def In_CompA set_addvars Var_def diff_inter_left diff_inter_right)
        apply (simp add: addvars_minus diff_disjoint Out_out)
        apply (subst set_perm)
        apply (simp add:  io_diagram_def )
        apply (simp add:  io_diagram_def )
        apply (simp add: set_addvars set_diff)
        apply blast
        apply simp
        apply (simp_all add: Comp_def Let_def BBB_a Var_def)
        apply (simp_all add: Out_out)
        apply (simp add: Let_def Parallel_def In_CompA Var_def Comp_def par_empty_left set_addvars diff_inter_left diff_inter_right Out_out[THEN sym] diff_union)
        apply (simp add: Out_out set_addvars par_empty_left)
        apply (simp add: Out_out[THEN sym])
        proof -
          assume [simp]: "io_diagram A"
          assume [simp]: "io_diagram B"
          assume [simp]: "io_diagram C"
          assume [simp]: "length (Out A) = Suc 0"
          assume [simp]: "out A ∉ set (In B)"
          assume [simp]: "out A ∈ set (In C)"

          define IA where "IA ≡ In A"
          define IB where "IB ≡ In B"
          define IC where "IC ≡ In C"
          define OA where "OA ≡ Out A"

          define ICA where "ICA ≡ IC ⊖ OA"

          define IB' where "IB' ≡ newvars (IA @ OA @ ICA) (TVs IB)"

          define ICA' where "ICA' ≡ newvars (IA @ IB' @ OA @ ICA) (TVs ICA)"

          have [simp]: "TVs IB = TI (Trs B)"
            using IB_def ‹io_diagram B› io_diagram_def by blast

          have [simp]: "TVs IA = TI (Trs A)"
            using IA_def ‹io_diagram A› io_diagram_def by blast

          have [simp]: "TVs OA = TO (Trs A)"
            using OA_def ‹io_diagram A› io_diagram_def by blast

          have [simp]: "TVs IC = TI (Trs C)"
            using IC_def ‹io_diagram C› io_diagram_def by blast

          have [simp]: "distinct IB"
            using IB_def ‹io_diagram B› io_diagram_def by blast

          have [simp]: "distinct IB'"
            by (simp add: IB'_def)

          have [simp]: "distinct IA"
            using IA_def ‹io_diagram A› io_diagram_def by blast

          have [simp]: "distinct IC"
            using IC_def ‹io_diagram C› io_diagram_def by blast

          have [simp]: "set IB' ∩ set IA = {}"
            by (metis IB'_def UnCI disjoint_iff_not_equal newvars_old_distinct set_append)

          have [simp]: "distinct OA"
            using OA_def ‹io_diagram A› io_diagram_def by blast

          have [simp]: "set OA ∩ set IB' = {}"
            by (metis IB'_def UnCI disjoint_iff_not_equal newvars_old_distinct set_append)

          have [simp]: "distinct ICA"
            by (simp add: ICA_def )

          have [simp]: "TVs IB' = TI (Trs B)"
            by (simp add: IB'_def)

          have [simp]: "distinct (IA ⊕ ICA)"
            by (simp )

          have [simp]:"set IB' ∩ set (ICA) = {}"
            by (metis Diff_disjoint IB'_def diff_disjoint diff_union newvars_old_distinct_a set_diff)

          have [simp]: "set (IA ⊕ ICA) ∩ set IB' = {}"
            by (metis Int_commute ‹set IB' ∩ set ICA = {}› ‹set IB' ∩ set IA = {}› addvars_def empty_inter_diff inter_addvars_empty set_empty set_inter)

          have [simp]: "length IB' = length IB"
            by (simp add: TVs_length_eq)

          have [simp]: "length (IB' @ (IA ⊕ ICA)) = length (IB @ (IA ⊕ ICA))"
            by simp          

          have [simp]: "Subst (IB' @ (IA ⊕ ICA)) (IB @ (IA ⊕ ICA)) (IB' @ IA @ ICA) = IB @ IA @ ICA"
            by (simp add: Subst_append Subst_not_in Subst_not_in_a Subst_eq)

          have [simp]: "distinct (IB ⊕ (IA ⊕ (ICA)))"
            by (simp )

          have [simp]: "distinct (IB' @ (IA ⊕ ICA))"
            using ‹distinct (IA ⊕ ICA)› ‹distinct IB'› ‹set (IA ⊕ ICA) ∩ set IB' = {}› distinct_append by blast

          have [simp]: "distinct ICA'"
            by (simp add: ICA'_def)

          have [simp]: "set IA ∩ set ICA' = {}"
            by (metis ICA'_def append_is_Nil_conv empty_inter filter_append inter_filter newvars_old_distinct_a set_inter)

          have [simp]: "set IB' ∩ set ICA' = {}"
            by (metis ICA'_def append_is_Nil_conv empty_inter filter_append inter_filter newvars_old_distinct_a set_inter)

          have a: "TVs ICA = TVs ICA'"
            by (simp add: ICA_def ICA'_def)

          have [simp]: "length ICA' = length ICA"
            by (metis length_TVs a)


          have b: "Subst (IB' @ IA @ ICA') (IB @ IA @ ICA) IA = IA"
            apply (subst Subst_not_in_a)
            apply (simp_all)
            apply (subst Subst_not_in)
            by (simp_all add: Int_commute)
 
          have c: "Subst (IB' @ IA @ ICA') (IB @ IA @ ICA) IB' = IB"
            apply (subst Subst_not_in)
            apply simp_all
            using ‹set IB' ∩ set IA = {}› ‹set IB' ∩ set ICA' = {}› by blast

          have d: "Subst (IB' @ IA @ ICA') (IB @ IA @ ICA) ICA' = ICA"
            apply (cut_tac x="IB' @ IA " and x'="ICA'" and y="IB @ IA" and y'="ICA" and z="ICA'" in Subst_not_in_a)
            apply simp_all
            using ‹set IB' ∩ set ICA' = {}› ‹set IA ∩ set ICA' = {}› by blast

          have [simp]: "Subst (IB' @ IA @ ICA') (IB @ IA @ ICA) (IA @ IB' @ ICA') = IA @ IB @ ICA"
            by (simp add: Subst_append b c d)

          have [simp]: "set OA ∩ set ICA' = {}"
            by (metis ICA'_def Int_commute bot_eq_sup_iff inf_sup_distrib1 newvars_old_distinct_a set_append)

          have [simp]: "set OA ∩ set ICA = {}"
            by (simp add: ICA_def set_diff)

          have [simp]: "set IB' ∩ set OA = {}"
            using ‹set OA ∩ set IB' = {}› by blast

          have [simp]: "set IC ⊆ set OA ∪ set ICA"
            by (simp add: ICA_def set_diff)

          have [simp]: "set ICA' ∩ set ICA = {}"
            by (metis newvars_old_distinct_a ICA'_def Int_commute bot_eq_sup_iff inf_sup_distrib2 set_append)

          have e: "Subst ICA' ICA (OA @ IB' @ ICA') = OA @ IB' @ ICA"
            by (simp add: Subst_append)

          have f: "Subst ICA' ICA (IB' @ OA @ ICA') = IB' @ OA @ ICA"
            by (simp add: Subst_append)

          have [simp]: "set OA ∩ set (IB ⊕ ICA) = {}"
            apply (simp add: set_addvars)
            by (simp add: OA_def IB_def Out_out)

          have g: "IB ⊕ ICA = (IB ⊕ IC ⊖ OA)"
            apply (simp add: ICA_def addvars_def union_diff)
            apply (subgoal_tac "set IB ∩ set OA = {}")
            apply (simp add: diff_disjoint diff_sym)
            by (simp add: OA_def IB_def Out_out)


          have A: "[In B ⊕ (In A ⊕ (In C ⊖ Out A)) ↝ In B @ (In A ⊕ (In C ⊖ Out A))] oo
                      Trs B ∥ ([In A ⊕ (In C ⊖ Out A) ↝ In A @ (In C ⊖ Out A)] oo Trs A ∥ [In C ⊖ Out A ↝ In C ⊖ Out A] oo [out A # (In C ⊖ Out A) ↝ In C] oo Trs C) = 
                   [IB ⊕ (IA ⊕ ICA) ↝ IA @ IB @ ICA] oo Trs A ∥ [IB' @ ICA' ↝ IB' @ ICA'] oo [OA @ IB' @ ICA ↝ IB' @ IC] oo Trs B ∥ Trs C"
            proof-
              have "[In B ⊕ (In A ⊕ (In C ⊖ Out A)) ↝ In B @ (In A ⊕ (In C ⊖ Out A))] oo
                    Trs B ∥ ([In A ⊕ (In C ⊖ Out A) ↝ In A @ (In C ⊖ Out A)] oo Trs A ∥ [In C ⊖ Out A ↝ In C ⊖ Out A] oo [out A # (In C ⊖ Out A) ↝ In C] oo Trs C) = 
                    [IB ⊕ (IA ⊕ ICA) ↝ IB @ (IA ⊕ ICA)] oo
                    Trs B ∥ ([IA ⊕ ICA ↝ IA @ ICA] oo Trs A ∥ [ICA ↝ ICA] oo [OA @ ICA ↝ IC] oo Trs C)" (is "?lhs = ?T")
                by (simp add: IA_def IB_def IC_def ICA_def OA_def Out_out)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IB @ (IA ⊕ ICA)] oo
                    ([IB ↝ IB] ∥ ([IA ⊕ ICA ↝ IA @ ICA] oo Trs A ∥ [ICA ↝ ICA] oo [OA @ ICA ↝ IC]) oo Trs B ∥ Trs C)"
                by (simp add: comp_parallel_distrib  )
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IB @ (IA ⊕ ICA)] oo
                    (([IB ↝ IB] ∥ ([IA ⊕ ICA ↝ IA @ ICA] oo Trs A ∥ [ICA ↝ ICA]) oo [IB ↝ IB] ∥ [OA @ ICA ↝ IC]) oo Trs B ∥ Trs C)"
                by (subst(2) comp_parallel_distrib, simp_all )
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IB @ (IA ⊕ ICA)] oo
                    ([IB ↝ IB] ∥ [IA ⊕ ICA ↝ IA @ ICA] oo [IB ↝ IB] ∥ (Trs A ∥ [ICA ↝ ICA]) oo [IB ↝ IB] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C)"
                by (simp add: comp_parallel_distrib  )
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IB @ (IA ⊕ ICA)] oo
                    ([IB ↝ IB] ∥ [IA ⊕ ICA ↝ IA @ ICA] oo ([IB ↝ IB] ∥ Trs A) ∥ [ICA ↝ ICA] oo [IB ↝ IB] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C)"
                by (simp add: par_assoc)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IB @ (IA ⊕ ICA)] oo
                    ([IB' ↝ IB'] ∥ [IA ⊕ ICA ↝ IA @ ICA] oo ([IB' ↝ IB'] ∥ Trs A) ∥ [ICA ↝ ICA] oo [IB' ↝ IB'] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C)"
                by (simp add: IB'_def distinct_id)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IB @ (IA ⊕ ICA)] oo
                    ([IB' ↝ IB'] ∥ [IA ⊕ ICA ↝ IA @ ICA] oo 
                    ([IB' @ IA ↝ IA @ IB'] oo Trs A ∥ [IB' ↝ IB'] oo [OA @ IB' ↝ IB' @ OA]) ∥ [ICA ↝ ICA] oo 
                    [IB' ↝ IB'] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C)"
                apply (cut_tac S="[IB' ↝ IB']" and T ="Trs A" and x="IB'" and y="IA" and u="OA" and v="IB'" in switch_par)
                by simp_all
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IB @ (IA ⊕ ICA)] oo
                    ([IB' ↝ IB'] ∥ [IA ⊕ ICA ↝ IA @ ICA] oo 
                    (([IB' @ IA ↝ IA @ IB'] oo Trs A ∥ [IB' ↝ IB']) ∥ [ICA ↝ ICA]  oo [OA @ IB' ↝ IB' @ OA] ∥ [ICA ↝ ICA]) oo 
                    [IB' ↝ IB'] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C)"
                by (subst(2) comp_parallel_distrib, simp_all add:   switch_comp)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IB @ (IA ⊕ ICA)] oo
                    ([IB' ↝ IB'] ∥ [IA ⊕ ICA ↝ IA @ ICA] oo 
                    (([IB' @ IA ↝ IA @ IB'] ∥ [ICA ↝ ICA] oo Trs A ∥ [IB' ↝ IB'] ∥ [ICA ↝ ICA]) oo [OA @ IB' ↝ IB' @ OA] ∥ [ICA ↝ ICA]) oo 
                    [IB' ↝ IB'] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C)"
                by (subst(2) comp_parallel_distrib, simp_all)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IB @ (IA ⊕ ICA)] oo
                    [IB' ↝ IB'] ∥ [IA ⊕ ICA ↝ IA @ ICA] oo 
                    [IB' @ IA ↝ IA @ IB'] ∥ [ICA ↝ ICA] oo Trs A ∥ [IB' ↝ IB'] ∥ [ICA ↝ ICA] oo [OA @ IB' ↝ IB' @ OA] ∥ [ICA ↝ ICA] oo 
                    [IB' ↝ IB'] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C"
                by (simp add: comp_assoc [THEN sym]  )
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IB @ (IA ⊕ ICA)] oo
                    [IB' @ (IA ⊕ ICA) ↝ IB' @  (IA @ ICA)] oo 
                    [IB' @ IA ↝ IA @ IB'] ∥ [ICA ↝ ICA] oo Trs A ∥ [IB' ↝ IB'] ∥ [ICA ↝ ICA] oo [OA @ IB' ↝ IB' @ OA] ∥ [ICA ↝ ICA] oo 
                    [IB' ↝ IB'] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C"
                by (simp add: par_switch set_addvars)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IB @  (IA @ ICA)] oo 
                    [IB' @ IA ↝ IA @ IB'] ∥ [ICA ↝ ICA] oo Trs A ∥ [IB' ↝ IB'] ∥ [ICA ↝ ICA] oo [OA @ IB' ↝ IB' @ OA] ∥ [ICA ↝ ICA] oo 
                    [IB' ↝ IB'] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C"
                by (simp add: switch_comp_subst set_addvars)
    
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IB @  (IA @ ICA)] oo 
                    [IB' @ IA ↝ IA @ IB'] ∥ [ICA' ↝ ICA'] oo Trs A ∥ [IB' ↝ IB'] ∥ [ICA' ↝ ICA'] oo [OA @ IB' ↝ IB' @ OA] ∥ [ICA' ↝ ICA'] oo 
                    [IB' ↝ IB'] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C"
                by (simp add: ICA'_def switch_newvars)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IB @  (IA @ ICA)] oo 
                    [IB' @ IA @ ICA'↝ IA @ IB' @ ICA'] oo Trs A ∥ [IB' ↝ IB'] ∥ [ICA' ↝ ICA'] oo [OA @ IB' ↝ IB' @ OA] ∥ [ICA' ↝ ICA'] oo 
                    [IB' ↝ IB'] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C"
                by (simp add: par_switch)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ IB @ ICA] oo 
                    Trs A ∥ [IB' ↝ IB'] ∥ [ICA' ↝ ICA'] oo [OA @ IB' ↝ IB' @ OA] ∥ [ICA' ↝ ICA'] oo 
                    [IB' ↝ IB'] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C"
                apply (subst switch_comp_subst, simp_all add: a)
                by (auto simp add: set_addvars set_diff)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ IB @ ICA] oo 
                    Trs A ∥ [IB' @ ICA' ↝ IB' @ ICA'] oo [OA @ IB' ↝ IB' @ OA] ∥ [ICA' ↝ ICA'] oo 
                    [IB' ↝ IB'] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C"
                by (simp add: par_assoc par_switch)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ IB @ ICA] oo 
                    Trs A ∥ [IB' @ ICA' ↝ IB' @ ICA'] oo [OA @ IB'@ ICA' ↝ IB' @ OA @ ICA'] oo 
                    [IB' ↝ IB'] ∥ [OA @ ICA ↝ IC] oo Trs B ∥ Trs C"
                by (simp add: par_switch)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ IB @ ICA] oo 
                    Trs A ∥ [IB' @ ICA' ↝ IB' @ ICA'] oo [OA @ IB'@ ICA' ↝ IB' @ OA @ ICA'] oo 
                    [IB' @ OA @ ICA ↝ IB' @ IC] oo Trs B ∥ Trs C"
                by (subst par_switch, simp_all)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ IB @ ICA] oo 
                    Trs A ∥ [IB' @ ICA' ↝ IB' @ ICA'] oo 
                    ([OA @ IB'@ ICA' ↝ IB' @ OA @ ICA'] oo [IB' @ OA @ ICA ↝ IB' @ IC]) oo 
                    Trs B ∥ Trs C"
                by (simp add: comp_assoc a  )
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ IB @ ICA] oo 
                    Trs A ∥ [IB' @ ICA' ↝ IB' @ ICA'] oo 
                    ([OA @ IB'@ ICA ↝ IB' @ OA @ ICA] oo [IB' @ OA @ ICA ↝ IB' @ IC]) oo 
                    Trs B ∥ Trs C"
                apply (cut_tac x="OA @ IB'@ ICA'" and y="IB' @ OA @ ICA'" and u="ICA'" and v="ICA" in Subst_switch_more_general)
                apply simp_all
                using ‹set IB' ∩ set ICA = {}› ‹set ICA' ∩ set ICA = {}› ‹set OA ∩ set ICA = {}› apply blast
                apply blast
                by (simp_all add: a e f)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ IB @ ICA] oo 
                    Trs A ∥ [IB' @ ICA' ↝ IB' @ ICA'] oo 
                    [OA @ IB' @ ICA ↝ IB' @ IC] oo 
                    Trs B ∥ Trs C"
                apply (subst switch_comp, simp_all)
                  apply (metis append_assoc perm_append2 perm_append_swap)
                by (auto simp add: IC_def ICA_def set_addvars set_diff)
              finally show ?thesis
                by simp
            qed

          have [simp]: "distinct (IA ⊕ (IB ⊕ ICA))"
            by (simp )

          have [simp]: "perm (IB ⊕ (IA ⊕ ICA)) (IA ⊕ (IB ⊕ ICA))"
            apply (subst set_perm)
            apply simp_all
            apply (simp add: set_addvars)
            by blast

          have [simp]: "distinct (IB ⊕ ICA)"
            by (simp )

          have [simp]: "IC ⊗ OA = OA"
            apply (subgoal_tac "distinct IC")
            apply (simp add: IC_def OA_def Out_out)
            apply (subgoal_tac "out A ∈ set (In C)")
            apply (simp add: inter_subset_l1)
            by simp_all            

          have [simp]: "IB ⊗ OA = []"
            apply (simp add: IB_def OA_def Out_out)
            apply (subgoal_tac "out A ∉ set (In B)")
            apply (simp add: empty_inter)
            by simp            

          have [simp]: "perm (OA @ (IB ⊕ ICA)) (IB ⊕ IC)"
            apply (simp add: ICA_def addvars_def diff_sym)
            apply (subgoal_tac "perm (OA @ IB @ (IC ⊖ IB ⊖ OA)) (IB @ OA @ (IC ⊖ IB ⊖ OA))")
            apply (subgoal_tac "perm (OA @ (IC ⊖ IB ⊖ OA)) (IC ⊖ IB)")
            using perm_trans perm_union_right apply blast
            apply (subgoal_tac "OA = ((IC ⊖ IB) ⊗ OA)")
            apply (metis mset_inter_diff perm_mset union_code)
             apply (simp add: inter_diff_distrib diff_emptyset)
              by (metis append_assoc perm_append2 perm_append_swap)
            

          have B: "[In B ⊕ (In A ⊕ (In C ⊖ Out A)) ↝ In A ⊕ (In B ⊕ In C ⊖ Out A)] oo
                ([In A ⊕ (In B ⊕ In C ⊖ Out A) ↝ In A @ (In B ⊕ In C ⊖ Out A)] oo Trs A ∥ [In B ⊕ In C ⊖ Out A ↝ In B ⊕ In C ⊖ Out A] oo [out A # (In B ⊕ In C ⊖ Out A) ↝ In B ⊕ In C] oo
                ([In B ⊕ In C ↝ In B @ In C] oo Trs B ∥ Trs C)) 
                = [IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo
                Trs A ∥ [IB ⊕ ICA ↝ IB ⊕ ICA] oo 
                [OA @ (IB ⊕ ICA) ↝ IB @ IC]
                oo Trs B ∥ Trs C"
            proof-        
              have "[In B ⊕ (In A ⊕ (In C ⊖ Out A)) ↝ In A ⊕ (In B ⊕ In C ⊖ Out A)] oo
                    ([In A ⊕ (In B ⊕ In C ⊖ Out A) ↝ In A @ (In B ⊕ In C ⊖ Out A)] oo Trs A ∥ [In B ⊕ In C ⊖ Out A ↝ In B ⊕ In C ⊖ Out A] oo [out A # (In B ⊕ In C ⊖ Out A) ↝ In B ⊕ In C] oo
                    ([In B ⊕ In C ↝ In B @ In C] oo Trs B ∥ Trs C)) =
                    [IB ⊕ (IA ⊕ ICA) ↝ IA ⊕ (IB ⊕ ICA)] oo
                    ([IA ⊕ (IB ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo Trs A ∥ [IB ⊕ ICA ↝ IB ⊕ ICA] oo [OA @ (IB ⊕ ICA) ↝ (IB ⊕ IC)] oo
                    ([IB ⊕ IC ↝ IB @ IC] oo Trs B ∥ Trs C))"
                apply (simp only: g)
                by (simp add: IA_def IB_def ICA_def IC_def OA_def Out_out)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA ⊕ (IB ⊕ ICA)] oo
                    [IA ⊕ (IB ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo Trs A ∥ [IB ⊕ ICA ↝ IB ⊕ ICA] oo [OA @ (IB ⊕ ICA) ↝ (IB ⊕ IC)] oo
                    [IB ⊕ IC ↝ IB @ IC] oo Trs B ∥ Trs C"
                by (simp add: comp_assoc[THEN sym]  )
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo
                    Trs A ∥ [IB ⊕ ICA ↝ IB ⊕ ICA] oo [OA @ (IB ⊕ ICA) ↝ (IB ⊕ IC)] oo
                    [IB ⊕ IC ↝ IB @ IC] oo Trs B ∥ Trs C"
                by (subst switch_comp, simp_all)
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo
                    Trs A ∥ [IB ⊕ ICA ↝ IB ⊕ ICA] oo 
                    ([OA @ (IB ⊕ ICA) ↝ (IB ⊕ IC)] oo [IB ⊕ IC ↝ IB @ IC])
                    oo Trs B ∥ Trs C"
                by (simp add: comp_assoc  )
              also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo
                    Trs A ∥ [IB ⊕ ICA ↝ IB ⊕ ICA] oo 
                    [OA @ (IB ⊕ ICA) ↝ IB @ IC]
                    oo Trs B ∥ Trs C"
                by (subst switch_comp, simp_all)
              finally show ?thesis
                by simp
            qed

          have h: "Subst (OA @ IB' @ ICA) (OA @ IB @ ICA) IB' = IB"
            apply (subst Subst_not_in_a, simp_all)
            by (subst Subst_not_in, simp_all add: Int_commute)

          have i: "Subst (OA @ IB' @ ICA) (OA @ IB @ ICA) IC = IC"
            apply (subst Subst_cancel_right, simp_all)
            apply (subst Subst_not_in_a, simp_all)
            apply (metis ICA_def ‹set IB' ∩ set ICA = {}› ‹set IB' ∩ set OA = {}› inter_diff_empty set_inter)
            by (simp add: Subst_eq)
            

          have [simp]: "Subst (OA @ IB' @ ICA) (OA @ IB @ ICA) (IB' @ IC) = IB @ IC"
            by (simp add: Subst_append h i)

          have C: "[OA @ (IB ⊕ ICA) ↝ IB @ IC] = [OA @ (IB ⊕ ICA) ↝ OA @ IB @ ICA] oo [OA @ IB' @ ICA ↝ IB' @ IC]"
            apply (subst switch_comp_subst, simp_all)
            by (auto simp add: set_addvars set_diff IC_def ICA_def)

          from this have D: "[IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo Trs A ∥ [IB ⊕ ICA ↝ IB ⊕ ICA] oo [OA @ (IB ⊕ ICA) ↝ IB @ IC]
            = [IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo Trs A ∥ [IB ⊕ ICA ↝ IB ⊕ ICA] oo [OA @ (IB ⊕ ICA) ↝ OA @ IB @ ICA] oo [OA @ IB' @ ICA ↝ IB' @ IC]"
            apply simp
            by (simp add: comp_assoc  )

          have [simp]: "set OA ∩ set IB = {}"
            by (simp add: OA_def IB_def Out_out)

          define IA' where "IA' ≡ newvars (IB ⊕ ICA) (TVs IA)"

          have [simp]: "distinct IA'"
            by (simp add: IA'_def)

          have [simp]: "TI (Trs A) = TVs IA'"
            by (simp add: IA'_def)

          have [simp]: "set IA' ∩ set (IB ⊕ ICA) = {}"
            by (simp only: IA'_def newvars_old_distinct)

          have [simp]: "length IA' = length IA"
            by (metis TVs_length_eq ‹TI (Trs A) = TVs IA'› ‹TVs IA = TI (Trs A)›)

          have j: "Subst (IA' @ (IB ⊕ ICA)) (IA @ (IB ⊕ ICA)) IA' = IA"
            by (subst Subst_not_in, simp_all add: Int_commute)

          have [simp]: "set IA' ∩ set IB = {}"
            by (metis UnCI ‹set IA' ∩ set (IB ⊕ ICA) = {}› disjoint_iff_not_equal set_addvars)

          have [simp]: "set IA' ∩ set ICA = {}"
            by (metis UnCI ‹set IA' ∩ set (IB ⊕ ICA) = {}› disjoint_iff_not_equal set_addvars)

          have k: "Subst (IA' @ (IB ⊕ ICA)) (IA @ (IB ⊕ ICA)) (IB @ ICA) = IB @ ICA"
            by (simp add: Subst_not_in_a Subst_eq)

          have [simp]: " Subst (IA' @ (IB ⊕ ICA)) (IA @ (IB ⊕ ICA)) (IA' @ IB @ ICA) = IA @ IB @ ICA"
            apply (subst Subst_append)
            by (simp add: j k)

          have "[IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo Trs A ∥ [IB ⊕ ICA ↝ IB ⊕ ICA] oo [OA @ (IB ⊕ ICA) ↝ OA @ IB @ ICA]
            = [IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo Trs A ∥ [IB ⊕ ICA ↝ IB ⊕ ICA] oo [OA ↝ OA] ∥ [IB ⊕ ICA ↝ IB @ ICA]"
            by (subst par_switch, simp_all add: set_addvars)
          also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo (Trs A ∥ [IB ⊕ ICA ↝ IB ⊕ ICA] oo [OA ↝ OA] ∥ [IB ⊕ ICA ↝ IB @ ICA])"
            by (subst comp_assoc, simp_all add:  )
          also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo Trs A ∥ [IB ⊕ ICA ↝ IB @ ICA]"
            by (subst comp_parallel_distrib, simp_all)
          also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo ([IA' ↝ IA'] oo Trs A) ∥ ([IB ⊕ ICA ↝ IB @ ICA] oo [IB' @ ICA' ↝ IB' @ ICA'])"
            apply (subst comp_id_switch, simp_all)
            apply (subst comp_switch_id, simp_all)
            by (simp add: a)
          also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo ([IA' @ (IB ⊕ ICA) ↝ IA' @ IB @ ICA] oo Trs A ∥ [IB' @ ICA' ↝ IB' @ ICA'])"
            apply (subst comp_parallel_distrib [THEN sym], simp_all add: a)
            by (subst par_switch, simp_all)
         also have "... = [IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo [IA' @ (IB ⊕ ICA) ↝ IA' @ IB @ ICA] oo Trs A ∥ [IB' @ ICA' ↝ IB' @ ICA']"
           by (subst comp_assoc, simp_all add: comp_assoc  a)
         also have "... =  [IB ⊕ (IA ⊕ ICA) ↝ IA @ IB @ ICA] oo Trs A ∥ [IB' @ ICA' ↝ IB' @ ICA']"
          apply (subst switch_comp_subst, simp_all)
          by (auto simp add: set_addvars set_diff)
            

         finally have E: "[IB ⊕ (IA ⊕ ICA) ↝ IA @ IB @ ICA] oo Trs A ∥ [IB' @ ICA' ↝ IB' @ ICA'] 
              = [IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo Trs A ∥ [IB ⊕ ICA ↝ IB ⊕ ICA] oo [OA @ (IB ⊕ ICA) ↝ OA @ IB @ ICA]"
           by simp

          show "[In B ⊕ (In A ⊕ (In C ⊖ Out A)) ↝ In B @ (In A ⊕ (In C ⊖ Out A))] oo
              Trs B ∥ ([In A ⊕ (In C ⊖ Out A) ↝ In A @ (In C ⊖ Out A)] oo Trs A ∥ [In C ⊖ Out A ↝ In C ⊖ Out A] oo [out A # (In C ⊖ Out A) ↝ In C] oo Trs C) =
              [In B ⊕ (In A ⊕ (In C ⊖ Out A)) ↝ In A ⊕ (In B ⊕ In C ⊖ Out A)] oo
              ([In A ⊕ (In B ⊕ In C ⊖ Out A) ↝ In A @ (In B ⊕ In C ⊖ Out A)] oo Trs A ∥ [In B ⊕ In C ⊖ Out A ↝ In B ⊕ In C ⊖ Out A] oo [out A # (In B ⊕ In C ⊖ Out A) ↝ In B ⊕ In C] oo
              ([In B ⊕ In C ↝ In B @ In C] oo Trs B ∥ Trs C))"
            apply (simp add: A B)
            apply (subgoal_tac " [IB ⊕ (IA ⊕ ICA) ↝ IA @ IB @ ICA] oo Trs A ∥ [IB' @ ICA' ↝ IB' @ ICA'] oo [OA @ IB' @ ICA ↝ IB' @ IC] = [IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo Trs A ∥ [IB ⊕ ICA ↝ IB ⊕ ICA] oo [OA @ (IB ⊕ ICA) ↝ IB @ IC]")
            apply (simp_all)
            apply (subst D)
            apply (subgoal_tac " [IB ⊕ (IA ⊕ ICA) ↝ IA @ IB @ ICA] oo Trs A ∥ [IB' @ ICA' ↝ IB' @ ICA'] = [IB ⊕ (IA ⊕ ICA) ↝ IA @ (IB ⊕ ICA)] oo Trs A ∥ [IB ⊕ ICA ↝ IB ⊕ ICA] oo [OA @ (IB ⊕ ICA) ↝ OA @ IB @ ICA]")
            apply simp_all
            by (simp add: E)
        qed



      lemmas distinct_addvars distinct_diff

lemma io_diagram_distinct: assumes A: "io_diagram A" shows [simp]: "distinct (In A)" 
  and [simp]: "distinct (Out A)" and [simp]: "TI (Trs A) = TVs (In A)" 
  and [simp]: "TO (Trs A) = TVs (Out A)"
  using A by (simp_all add: io_diagram_def)
    


      declare Subst_not_in_a  [simp]
      declare Subst_not_in  [simp]

      (*move*)
      lemma [simp]: "set x' ∩ set z = {} ⟹ TVs x = TVs y ⟹ TVs x' = TVs y' ⟹ Subst (x @ x') (y @ y') z = Subst x y z"
        by (metis Subst_not_in length_TVs)

      lemma [simp]: "set x ∩ set z = {} ⟹ TVs x = TVs y ⟹ TVs x' = TVs y' ⟹ Subst (x @ x') (y @ y') z = Subst x' y' z"
        by (metis Subst_not_in_a length_TVs)

      lemma [simp]: "set x ∩ set z = {} ⟹ TVs x = TVs y ⟹ Subst x y z = z"
        by (metis Subst_inex length_TVs)

      lemma [simp]: "distinct x ⟹ TVs x = TVs y ⟹ Subst x y x = y"
        by (metis Subst_all length_TVs)

      lemma "TVs x = TVs y ⟹ length x = length y"
        by (metis length_TVs)

        thm length_TVs

(*end simplification rules*)

      lemma in_equiv_switch_Parallel: "io_diagram A ⟹ io_diagram B ⟹ set (Out A) ∩ set (Out B) = {}  ⟹ 
        in_equiv (A ||| B) ((B ||| A) ;; [[ Out B @ Out A ↝ Out A @ Out B]])"
        apply (simp add: in_equiv_def Let_def Parallel_def Comp_def VarSwitch_def Var_def diff_inter_left diff_inter_right diff_eq par_empty_left par_empty_right)
        apply safe
        apply (metis addvars_def perm_switch perm_tp perm_trans io_diagram_def)
        proof -
          assume [simp]: "io_diagram A"
          assume [simp]: "io_diagram B"

          assume [simp]: "set (Out A) ∩ set (Out B) = {}"
          from this have [simp]: "set (Out B) ∩ set (Out A) = {}"
            by blast

          have [simp]: "perm (In A ⊕ In B) (In B ⊕ In A)"
            by (rule distinct_perm_switch, simp_all)

         from paralle_switch obtain x y u v where
            B: "distinct (x @ y)" and C: "distinct (u @ v)" and [simp]: "TVs x = TI (Trs B)" and [simp]: "TVs u = TO (Trs B)" and [simp]: "TVs y = TI (Trs A)" 
            and [simp]: "TVs v = TO (Trs A)" and A: "Trs B ∥ Trs A = [x @ y ↝ y @ x] oo (Trs A ∥ Trs B) oo [v @ u ↝ u @ v]"
            by blast

          from C have [simp]: "distinct u" and [simp]: "distinct v" and [simp]: "set u ∩ set v = {}" and [simp]: "set v ∩ set u = {}"
            by auto

          from B have [simp]: "distinct x" and [simp]: "distinct y" and [simp]: "set x ∩ set y = {}" and [simp]: "set y ∩ set x = {}"
            by auto

          have [simp]: "Subst (x @ y) (In B @ In A) (y @ x) = In A @ In B"
            by (simp add: Subst_append)

          have [simp]: "Subst (Out B @ Out A) (u @ v) (Out A @ Out B) = v @ u"
            by (simp add: Subst_append)


            thm comp_id_left
          have "[In A ⊕ In B ↝ In B ⊕ In A] oo ([In B ⊕ In A ↝ In B ⊕ In A] oo ([In B ⊕ In A ↝ In B @ In A] oo Trs B ∥ Trs A) oo [Out B @ Out A ↝ Out B @ Out A] oo [Out B @ Out A ↝ Out A @ Out B])
            = [In A ⊕ In B ↝ In B ⊕ In A] oo ([In B ⊕ In A ↝ In B @ In A] oo Trs B ∥ Trs A oo [Out B @ Out A ↝ Out B @ Out A] oo [Out B @ Out A ↝ Out A @ Out B])"
          by (simp add: distinct_id)
          also have "... = ([In A ⊕ In B ↝ In B ⊕ In A] oo [In B ⊕ In A ↝ In B @ In A]) oo Trs B ∥ Trs A oo ([Out B @ Out A ↝ Out B @ Out A] oo [Out B @ Out A ↝ Out A @ Out B])"
            by (simp add: comp_assoc)

          also have "... = [In A ⊕ In B ↝ In B @ In A] oo Trs B ∥ Trs A oo [Out B @ Out A  ↝ Out A @ Out B]"
            apply (subst switch_comp)
            by (auto simp add: set_addvars set_diff)

          also have "... = [In A ⊕ In B ↝ In B @ In A] oo ([x @ y ↝ y @ x] oo (Trs A ∥ Trs B) oo [v @ u ↝ u @ v]) oo [Out B @ Out A  ↝ Out A @ Out B]"
            by (simp add: A)
          also have "... = ([In A ⊕ In B ↝ In B @ In A] oo [x @ y ↝ y @ x]) oo Trs A ∥ Trs B oo ([v @ u ↝ u @ v] oo [Out B @ Out A  ↝ Out A @ Out B])"
            using B C by (simp add: comp_assoc)

          also have "... = [In A ⊕ In B ↝ In A @ In B] oo Trs A ∥ Trs B"
            using B C by (simp add: switch_comp_subst distinct_id set_addvars set_diff)

          finally show "[In A ⊕ In B ↝ In A @ In B] oo Trs A ∥ Trs B 
                      = [In A ⊕ In B ↝ In B ⊕ In A] oo ([In B ⊕ In A ↝ In B @ In A] oo Trs B ∥ Trs A oo [Out B @ Out A ↝ Out B @ Out A] oo [Out B @ Out A ↝ Out A @ Out B])"
          by simp
       qed

lemma in_out_equiv_Parallel: "io_diagram A ⟹ io_diagram B ⟹ set (Out A) ∩ set (Out B) = {}  ⟹  in_out_equiv (A ||| B) (B ||| A)"
    apply (frule in_equiv_switch_Parallel, simp_all)
    apply (simp add: in_equiv_def in_out_equiv_def Parallel_def VarSwitch_def Let_def Comp_def Var_def par_empty_left par_empty_right, safe)
    using distinct_perm_switch io_diagram_distinct(1) apply blast
    using perm_tp apply blast
    apply (unfold io_diagram_def)
    apply (simp add: comp_assoc)
    by (subst switch_comp, auto)


      declare Subst_eq [simp]

lemma assumes "in_equiv A A'" shows [simp]: "perm (In A) (In A')" 
  using assms in_equiv_def by blast
    

lemma Subst_cancel_left_type: "set x ∩ set z = {} ⟹ TVs x = TVs y ⟹ Subst (x @ z) (y @ z) w = Subst x y w"
  by (metis Subst_cancel_left length_TVs)
    

lemma diff_eq_set_right: "set y = set z ⟹ (x ⊖ y) = (x ⊖ z)"
  by (induction x, simp_all)

      lemma [simp]: "set (y ⊖ x) ∩ set x = {}"
        by (auto simp add: set_diff)

lemma in_equiv_Comp: "io_diagram A' ⟹ io_diagram B' ⟹ in_equiv A A' ⟹ in_equiv B B' ⟹ in_equiv (A ;; B) (A' ;; B')"
        proof -
          assume [simp]: "io_diagram A'"
          assume [simp]: "io_diagram B'"
          assume [simp]: "in_equiv A A'"
          assume [simp]: "in_equiv B B'"

          have [simp]: "io_diagram A"
            using ‹in_equiv A A'› ‹io_diagram A'› in_equiv_io_diagram by blast
          have [simp]: "io_diagram B"
            using ‹in_equiv B B'› ‹io_diagram B'› in_equiv_io_diagram by blast

          have [simp]: "Out A = Out A'"
            using ‹in_equiv A A'› in_equiv_def by blast

          have [simp]: "Out B = Out B'"
            using ‹in_equiv B B'› in_equiv_def by blast

          from ‹in_equiv A A'› have [simp]: "Trs A = [In A ↝ In A'] oo Trs A'"
            by (simp add: in_equiv_def)

          from ‹in_equiv B B'› have [simp]: "Trs B = [In B ↝ In B'] oo Trs B'"
            by (simp add: in_equiv_def)

          have [simp]: "set (In A') = set (In A)"
            using ‹in_equiv A A'› in_equiv_def perm_set_eq by blast
    
          have [simp]: "set (In B') = set (In B)"
            using ‹in_equiv B B'› in_equiv_def perm_set_eq by blast

          have [simp]: "(Out A' ⊖ In B') = (Out A' ⊖ In B)"
            by (rule diff_eq_set_right, simp)

          define v where "v ≡ newvars (In A @ In B) (TVs (Out A'))"

          have [simp]: "distinct v"
            by (simp add: v_def)

          have U: "set v ∩ set (In A @ In B) = {}"
            using newvars_old_distinct v_def by blast



        have [simp]:" set (In A ⊕ (In B ⊖ Out A')) ∩ set v = {}"
          using U by (unfold set_addvars set_diff, auto)

        have [simp]:" set v ∩ set (In A ⊕ (In B ⊖ Out A')) = {}"
          using U by (unfold set_addvars set_diff, auto)
          
          from U have [simp]: "set v ∩ set (In A) = {}"
            by simp
          from U have [simp]: "set v ∩ set (In B) = {}"
            by simp
          
        have [simp]: "TVs v = TVs (Out A')"
          by (simp add: v_def)


        have [simp]:"set (In A') ⊆ set (In A ⊕ (In B ⊖ Out A'))"
          by (simp add: set_diff set_addvars)

        have [simp]:"set (In B ⊖ Out A') ⊆ set (In A ⊕ (In B ⊖ Out A'))"
          by (simp add: set_diff set_addvars)

        have [simp]:"set (In B' ⊖ Out A') ⊆ set (In A ⊕ (In B ⊖ Out A'))"
          by (simp add: set_diff set_addvars)


        have A: "([In A ↝ In A'] oo Trs A') ∥ [In B ⊖ Out A' ↝ In B ⊖ Out A'] = [In A ↝ In A'] ∥ [In B ⊖ Out A' ↝ In B ⊖ Out A'] oo Trs A' ∥ [In B ⊖ Out A' ↝ In B ⊖ Out A']"
          by (simp add: comp_parallel_distrib)

        have [simp]: "[Out A' ⊖ In B ↝ Out A' ⊖ In B] ∥ ([In B ↝ In B'] oo Trs B') = [(Out A' ⊖ In B) ↝ (Out A' ⊖ In B)] ∥ [In B ↝ In B'] oo [Out A' ⊖ In B ↝ Out A' ⊖ In B] ∥ Trs B'"
          by (simp add: comp_parallel_distrib)

        have [simp]: "... = [(Out A' ⊖ In B) @ In B ↝ (Out A' ⊖ In B) @ In B'] oo [Out A' ⊖ In B ↝ Out A' ⊖ In B] ∥ Trs B'"
          by (subst par_switch, simp_all)

        have "[In A ⊕ (In B ⊖ Out A') ↝ In A @ (In B ⊖ Out A')] oo ([In A ↝ In A'] oo Trs A') ∥ [In B ⊖ Out A' ↝ In B ⊖ Out A'] 
              oo ([Out A' @ (In B ⊖ Out A') ↝ (Out A' ⊖ In B) @ In B] oo [(Out A' ⊖ In B) @ In B ↝ (Out A' ⊖ In B) @ In B'])
                =
              [In A ⊕ (In B ⊖ Out A') ↝ In A' ⊕ (In B' ⊖ Out A')] oo
              [In A' ⊕ (In B' ⊖ Out A') ↝ In A' @ (In B' ⊖ Out A')] oo Trs A' ∥ [In B' ⊖ Out A' ↝ In B' ⊖ Out A'] 
              oo [Out A' @ (In B' ⊖ Out A') ↝ (Out A' ⊖ In B) @ In B']"

          apply (subst switch_comp_a, simp_all)
          apply (auto simp add: set_diff) [1]
          apply (subst A, simp add: comp_assoc [THEN sym])
          apply (subst switch_par_comp_Subst, simp_all)
          apply (subst switch_comp, simp_all)
          apply (simp add: set_diff set_addvars)
          apply (rule_tac v = v in par_switch_eq_dist, simp_all)
          apply (subst switch_comp_subst, simp_all)
          apply (auto simp add: set_diff set_addvars)
          apply (subst switch_comp_subst, simp_all)
          apply (auto simp add: set_diff set_addvars)
          by (simp add: Subst_append Subst_cancel_left_type)

         thm par_switch_eq_dist
         from this show "in_equiv (A ;; B) (A' ;; B')"
          apply (simp add: in_equiv_def Comp_def Let_def Var_def diff_inter_left diff_inter_right, simp)
          by (simp add: comp_assoc [THEN sym])
      qed


      lemma "io_diagram A' ⟹ io_diagram B' ⟹ in_equiv A A' ⟹ in_equiv B B' ⟹ in_equiv (CompA A  B) (CompA A' B')"
        apply (simp add: CompA_def, safe)
        apply (rule in_equiv_Comp, simp_all)
        apply (metis in_equiv_def out_def perm_set_eq)
        by (metis in_equiv_def out_def perm_set_eq)

      thm in_equiv_tran

      thm in_equiv_CompA_Parallel_c

      lemma comp_parallel_distrib_a: "TO A = TI B ⟹ (A oo B) ∥ C = (A ∥ (ID (TI C))) oo (B ∥ C)"
        by (subst comp_parallel_distrib, simp_all)

      lemma comp_parallel_distrib_b: "TO A = TI B ⟹ C ∥ (A oo B) = ((ID (TI C)) ∥ A) oo (C ∥ B)"
        by (subst comp_parallel_distrib, simp_all)


      thm switch_comp_subst

      lemma CCC_d: "distinct x ⟹ distinct y' ⟹ set y ⊆ set x ⟹ set z ⊆ set x ⟹ set u ⊆ set y' ⟹ TVs y = TVs y' ⟹ 
        TVs z = ts ⟹ [x ↝ y @ z] oo [y' ↝ u] ∥ (ID ts) = [x ↝ Subst y' y u @ z]"
        proof -
        assume [simp]: "distinct x"
        assume [simp]: "distinct y'"
        assume [simp]: "set y ⊆ set x"
        assume [simp]: "set z ⊆ set x"
        assume [simp]: "set u ⊆ set y'"
        assume [simp]: "TVs y = TVs y'"
        assume [simp]: "TVs z = ts"
        define z' where "z' ≡ newvars y' (TVs z)"

        have [simp]: "set y' ∩ set z' = {}"
          by (simp add: z'_def)
        have [simp]: "set z' ∩ set y' = {}"
          by (simp add: z'_def)
        have [simp]: "set u ∩ set z' = {}"
          using ‹set u ⊆ set y'› ‹set y' ∩ set z' = {}› by blast
        have [simp]: "set z' ∩ set u = {}"
          using ‹set u ⊆ set y'› ‹set y' ∩ set z' = {}› by blast
        have [simp]: "TVs z' = TVs z"
          by (simp add: z'_def)
        have [simp]: "distinct z'"
          by (simp add: z'_def)

        have " [x ↝ y @ z] oo [y' ↝ u] ∥ (ID ts) =  [x ↝ y @ z] oo [y' ↝ u] ∥ [z' ↝ z']"
          by (subst distinct_id, simp_all add: z'_def)
        also have "... =  [x ↝ y @ z] oo [y' @ z' ↝ u @ z']"
          by (subst par_switch, simp_all add: z'_def)
        also have "... = [x ↝ Subst y' y u @ z]"
          apply (subst switch_comp_subst, simp_all add: Subst_append)
          by (simp add: le_supI1)

        finally show ?thesis
          by simp
     qed

      lemma CCC_e: "distinct x ⟹ distinct y' ⟹ set y ⊆ set x ⟹ set z ⊆ set x ⟹ set u ⊆ set y' ⟹ TVs y = TVs y' ⟹ 
        TVs z = ts ⟹ [x ↝ z @ y] oo (ID ts) ∥ [y' ↝ u] = [x ↝ z @ Subst y' y u]"
        proof -
        assume [simp]: "distinct x"
        assume [simp]: "distinct y'"
        assume [simp]: "set y ⊆ set x"
        assume [simp]: "set z ⊆ set x"
        assume [simp]: "set u ⊆ set y'"
        assume [simp]: "TVs y = TVs y'"
        assume [simp]: "TVs z = ts"
        define z' where "z' ≡ newvars y' (TVs z)"

        have [simp]: "set y' ∩ set z' = {}"
          by (simp add: z'_def)
        have [simp]: "set z' ∩ set y' = {}"
          by (simp add: z'_def)
        have [simp]: "set u ∩ set z' = {}"
          using ‹set u ⊆ set y'› ‹set y' ∩ set z' = {}› by blast
        have [simp]: "set z' ∩ set u = {}"
          using ‹set u ⊆ set y'› ‹set y' ∩ set z' = {}› by blast
        have [simp]: "TVs z' = TVs z"
          by (simp add: z'_def)
        have [simp]: "distinct z'"
          by (simp add: z'_def)

        have " [x ↝ z @ y] oo ID ts ∥ [y' ↝ u] =  [x ↝ z @ y] oo [z' ↝ z'] ∥ [y' ↝ u]"
          by (subst distinct_id, simp_all add: z'_def)
        also have "... =  [x ↝ z @ y] oo [z' @ y' ↝ z' @ u]"
          by (subst par_switch, simp_all add: z'_def)
        also have "... = [x ↝ z @ Subst y' y u]"
          apply (subst switch_comp_subst, simp_all add: Subst_append)
          by (simp add: sup.coboundedI2)
        finally show ?thesis
          by simp
     qed


lemma CCC_a: "distinct x ⟹ distinct y ⟹ set y ⊆ set x ⟹ set z ⊆ set x ⟹ set u ⊆ set y ⟹ TVs z = ts 
    ⟹ [x ↝ y @ z] oo [y ↝ u] ∥ (ID ts) = [x ↝ u @ z]"
  by (subst CCC_d, simp_all)
    
        

lemma CCC_b: "distinct x ⟹ distinct z ⟹ set y ⊆ set x ⟹ set z ⊆ set x ⟹ set u ⊆ set z 
    ⟹ TVs y = ts ⟹ [x ↝ y @ z] oo  (ID ts) ∥ [z ↝ u] = [x ↝ y @ u]"
  by (subst CCC_e, simp_all)
    


      thm par_switch_eq_dist

      lemma in_equiv_CompA_Parallel_b: "length (Out A) = 1 ⟹ io_diagram A ⟹ io_diagram B ⟹ io_diagram C ⟹ out A ∈ set (In B) 
        ⟹  out A ∉ set (In C) ⟹ in_equiv (CompA A B ||| CompA A C) (CompA A (B ||| C))"
        proof simp
          assume [simp]: "length (Out A) = Suc 0"
          assume [simp]: "out A ∉ set (In C)"
          assume [simp]: "out A ∈ set (In B)"

          assume [simp]: "io_diagram A"
          assume [simp]: "io_diagram B"
          assume [simp]: "io_diagram C"
        
          have [simp]: "CompA A (B ||| C) = A ;; (B ||| C)"
            apply (subgoal_tac "out A ∈ set (In (B ||| C))")
            by (simp_all add: set_addvars)

         have [simp]: "set (Out A) ∩ set (In C) = {}"
          by (subst Out_out, simp_all)

          have [simp]: "(In C ⊖ Out A) = In C"
            by (simp add: diff_distinct)

          have B: "(In A ⊕ (In B ⊖ Out A) ⊕ In C) = (In A ⊕ (In B ⊕ In C ⊖ Out A))"
            by (simp add: addvars_minus addvars_assoc)

          from B have [simp]: "perm (In A ⊕ (In B ⊖ Out A) ⊕ In C) (In A ⊕ (In B ⊕ In C ⊖ Out A))"
            by simp

          have A: "Out A = [out A]"
            by (subst Out_out, simp_all)

          have [simp]: "(Out A ⊖ In B ⊕ In C) = (Out A ⊖ In B)"
            by (simp add: A set_addvars)

         define v where "v ≡ newvars (In A @ In B @ In C) (TVs (Out A))"

         from this have "set v ∩ set (In A @ In B @ In C) = {}"
          using newvars_old_distinct by blast

         from this have [simp]: "set (In A ⊕ (In B ⊖ Out A) ⊕ In C) ∩ set v = {}"
           by (simp add: set_addvars set_diff, auto)

          from this have [simp]: "set v ∩ set (In A ⊕ (In B ⊖ Out A) ⊕ In C) = {}"
            by blast

         have [simp]: "distinct v"
          by (simp add: v_def)
         have [simp]: "TVs v = TVs (Out A)"
          by (simp add: v_def)


         have A: "[In A ⊕ (In B ⊖ Out A) ⊕ In C ↝ (In A ⊕ (In B ⊖ Out A)) @ In C] oo 
            [In A ⊕ (In B ⊖ Out A) ↝ In A @ (In B ⊖ Out A)] ∥ ID (TVs (In C)) oo Trs A ∥ [In B ⊖ Out A ↝ In B ⊖ Out A] ∥ ID (TVs (In C)) oo
              [Out A @ (In B ⊖ Out A) ↝ (Out A ⊖ In B) @ In B] ∥ ID (TVs (In C)) = 
            [In A ⊕ (In B ⊖ Out A) ⊕ In C ↝ In A ⊕ (In B ⊕ In C ⊖ Out A)] oo [In A ⊕ (In B ⊕ In C ⊖ Out A) ↝ In A @ (In B ⊕ In C ⊖ Out A)] 
              oo Trs A ∥ [In B ⊕ In C ⊖ Out A ↝ In B ⊕ In C ⊖ Out A] oo
              [Out A @ (In B ⊕ In C ⊖ Out A) ↝ (Out A ⊖ In B) @ (In B ⊕ In C)] oo
              ID (TVs (Out A ⊖ In B)) ∥ [In B ⊕ In C ↝ In B @ In C]"
          apply (subst CCC_a, simp_all)
          apply (subst switch_comp, simp_all)
          apply (simp add: distinct_id)
          apply (simp add: par_assoc)
          apply (simp add: comp_assoc)
          apply (subst CCC_b, simp_all add: set_addvars set_diff)
          apply auto [1]
          apply (simp add: comp_assoc [THEN sym])
          apply (rule_tac v = v in par_switch_eq_dist_a, simp_all)
          apply (simp_all add: set_addvars set_diff)
          apply auto [3]
          apply (subst switch_comp_subst, simp_all)
          apply (auto simp add: set_addvars set_diff) [1]
          apply (auto simp add: set_addvars set_diff) [1]
          apply (subst append_assoc [THEN sym])
          apply (subst CCC_d, simp_all)
          apply (simp_all add: set_addvars set_diff)
          apply auto [3]
          apply (simp add: Subst_cancel_left_type)
          by (simp add: Subst_append)

         have "[In A ⊕ (In B ⊖ Out A) ⊕ In C ↝ (In A ⊕ (In B ⊖ Out A)) @ In C] oo
            ([In A ⊕ (In B ⊖ Out A) ↝ In A @ (In B ⊖ Out A)] oo Trs A ∥ [In B ⊖ Out A ↝ In B ⊖ Out A] 
            oo [Out A @ (In B ⊖ Out A) ↝ (Out A ⊖ In B) @ In B] oo [Out A ⊖ In B ↝ Out A ⊖ In B] ∥ Trs B) ∥ Trs C 
            =
            [In A ⊕ (In B ⊖ Out A) ⊕ In C ↝ In A ⊕ (In B ⊕ In C ⊖ Out A)] oo
            ([In A ⊕ (In B ⊕ In C ⊖ Out A) ↝ In A @ (In B ⊕ In C ⊖ Out A)] oo Trs A ∥ [In B ⊕ In C ⊖ Out A ↝ In B ⊕ In C ⊖ Out A] 
            oo [Out A @ (In B ⊕ In C ⊖ Out A) ↝ (Out A ⊖ In B) @ (In B ⊕ In C)] oo
             [Out A ⊖ In B ↝ Out A ⊖ In B] ∥ ([In B ⊕ In C ↝ In B @ In C] oo Trs B ∥ Trs C))"
           apply (simp add: comp_parallel_distrib_a comp_parallel_distrib_b)
           apply (simp add: comp_assoc [THEN sym] par_assoc [THEN sym])
           by (simp add: A) 
          
          from this show "in_equiv ((A ;; B) ||| C) (CompA A (B ||| C))"
            apply (simp)
            by (simp add: in_equiv_def Comp_def Let_def Var_def diff_inter_left diff_inter_right  Parallel_def)
        qed

      lemma in_equiv_CompA_Parallel_d: "length (Out A) = 1 ⟹ io_diagram A ⟹ io_diagram B ⟹ io_diagram C ⟹ out A ∉ set (In B) ⟹ out A ∉ set (In C) ⟹ 
              in_equiv (CompA A B ||| CompA A C) (CompA A (B ||| C))"
        by (simp add: in_equiv_def In_CompA set_addvars BBB_a Parallel_def )

lemma in_equiv_CompA_Parallel: " deterministic (Trs A) ⟹ length (Out A) = 1 ⟹ io_diagram A ⟹ io_diagram B ⟹ io_diagram C ⟹
          in_equiv ((A ⊳ B) ||| (A ⊳ C)) (A ⊳ (B ||| C))"
        apply (case_tac "out A ∈ set (In B)")
        apply (case_tac "out A ∈ set (In C)")
        apply (rule in_equiv_CompA_Parallel_a, simp)
        apply simp
        apply simp
        apply simp
        apply simp
        apply simp
        apply simp
        apply (rule in_equiv_CompA_Parallel_b, simp)
        apply simp
        apply simp
        apply simp
        apply simp
        apply simp
        apply simp
        apply (case_tac "out A ∈ set (In C)")
        apply (cut_tac in_equiv_CompA_Parallel_c, simp_all)
        by(cut_tac A = A and B = B and C = C in in_equiv_CompA_Parallel_d, simp_all)
 

lemma fb_less_step_compA: "deterministic (Trs A) ⟹ length (Out A) = 1 ⟹ io_diagram A ⟹ Type_OK As 
  ⟹ in_equiv (Parallel_list (fb_less_step A As)) (CompA A (Parallel_list As))"
        apply (induction As)
        apply (simp_all add: fb_less_step_def in_equiv_eq)
        apply (rule_tac B = "(CompA A a ||| CompA A (Parallel_list As))" in in_equiv_tran)
        apply (rule io_diagram_CompA, simp_all)
        apply (rule io_diagram_Parallel)
        apply (simp add: Type_OK_simp)
        apply (rule io_diagram_parallel_list)
        apply (simp add: Type_OK_simp, safe)
        apply (simp add: Out_Parallel BBB_a Type_OK_out)
        apply (simp add: Type_OK_simp image_def)
        apply (rule in_equiv_Parallel)
        apply (rule io_diagram_CompA, simp_all)
        apply (simp add: Type_OK_simp)
        apply (rule io_diagram_CompA, simp_all)
        apply (rule io_diagram_parallel_list, simp)
        apply (rule in_equiv_eq)
        apply (rule io_diagram_CompA, simp_all)
        apply (simp add: Type_OK_simp)
        apply (rule in_equiv_CompA_Parallel, simp_all)
        apply (simp add: Type_OK_simp)
        by (rule io_diagram_parallel_list, simp)
      

(*simp rules*)

          (*move*)
lemma switch_eq_Subst: "distinct x ⟹ distinct u ⟹ set y ⊆ set x ⟹ set v ⊆ set u ⟹ TVs x = TVs u 
    ⟹ Subst x u y = v ⟹ [x ↝ y] = [u ↝ v]"
  using Subst_switch_a by blast

(*move*)
lemma [simp]: "set y ⊆ set y1 ⟹ distinct x1 ⟹ TVs x1 = TVs y1 ⟹ Subst x1 y1 (Subst y1 x1 y) = y"
  by (metis Subst_Subst_inv length_TVs)
    
(*move*)
lemma [simp]: "set z ⊆ set x ⟹ TVs x  = TVs y ⟹ set (Subst x y z) ⊆ set y"
  by (metis Subst_set_incl length_TVs)
    

      thm distinct_Subst

(*move*)
      lemma distinct_Subst_aa: "⋀ y . 
            distinct y ⟹ length x = length y ⟹ a ∉ set y ⟹ set z ∩ (set y - set x) = {} ⟹ a ≠ aa 
      ⟹ a ∉ set z ⟹ aa ∉ set z ⟹ distinct z  ⟹ aa ∈ set x 
      ⟹ subst x y a ≠ subst x y aa"
        apply (induction x, simp_all)
        apply (case_tac y, simp_all, safe)
        apply (metis subst_in_set subst_notin)
        apply (simp add: subst_in_set)
        apply (metis subst_subst_inv subst_notin) 
        by (metis subst_subst_inv subst_notin)

lemma distinct_Subst_ba: "distinct y ⟹ length x = length y ⟹ set z ∩ (set y - set x) = {}  
    ⟹ a ∉ set z ⟹ distinct z  ⟹ a ∉ set y ⟹ subst x y a ∉ set (Subst x y z)"
        apply (induction z, simp_all, safe)
        apply (simp add: distinct_Subst_a)
        by (simp add: distinct_Subst_aa)

lemma distinct_Subst_ca: "distinct y ⟹ length x = length y ⟹ set z ∩ (set y - set x) = {} 
    ⟹ a ∉ set z ⟹ distinct z ⟹ a ∈ set x ⟹ subst x y a ∉ set (Subst x y z)"
        apply (induction z, simp_all, safe)
        apply (metis distinct_Subst_aa)
        by (metis subst_subst_inv)

lemma [simp]: "set z ∩ (set y - set x) = {} ⟹  distinct y ⟹ distinct z ⟹ length x = length y 
  ⟹ distinct (Subst x y z)"
        apply (induction z, simp_all, safe)
        apply (simp add: distinct_Subst_ba)
        by (simp add: distinct_Subst_ca)

(*end simp rules*)



lemma deterministic_Comp: "io_diagram A ⟹ io_diagram B ⟹ deterministic (Trs A) ⟹ deterministic (Trs B) 
  ⟹ deterministic (Trs (A ;; B))"
        apply (simp add: Comp_def Let_def)
        apply (rule deterministic_comp)
        apply (rule deterministic_comp)
        apply (rule deterministic_comp)
        apply (rule deterministic_switch, simp_all)

        apply (rule deterministic_par, simp_all)
        apply (rule deterministic_switch, simp_all)
        apply (rule deterministic_switch, simp_all)

        apply (simp add: set_diff set_addvars Var_def set_inter)
        apply auto [1]
        apply (simp add: set_diff set_addvars Var_def set_inter)
        apply auto [1]

        apply (rule deterministic_par)
        apply (rule deterministic_switch)
        by simp_all

lemma deterministic_CompA: "io_diagram A ⟹ io_diagram B ⟹ deterministic (Trs A) ⟹ deterministic (Trs B) 
  ⟹ deterministic (Trs (A ⊳ B))"
        by (simp add: CompA_def deterministic_Comp)


      lemma parallel_list_empty[simp]: "parallel_list [] = ID []"
        by (simp add: parallel_list_def)

      lemma parallel_list_append: "parallel_list (As @ Bs) = parallel_list As ∥ parallel_list Bs"
        apply (induction As)
        apply (simp_all)
        by (simp add: parallel_list_cons par_assoc)

          (*move*)
lemma par_swap_aux: "distinct p ⟹ distinct (v @ u @ w) ⟹ 

          TI A = TVs x ⟹ TI B = TVs y ⟹ TI C = TVs z ⟹
          TO A = TVs u ⟹ TO B = TVs v ⟹ TO C = TVs w ⟹
          set x ⊆ set p ⟹ set y ⊆ set p ⟹ set z ⊆ set p ⟹ set q ⊆ set (u @ v @ w) ⟹
          [p ↝ x @ y @ z] oo (A ∥ B ∥ C) oo [u @ v @ w ↝ q] = [p ↝ y @ x @ z] oo (B ∥ A ∥ C) oo [v @ u @ w ↝ q]"
        proof -
          define x' where "x' ≡ newvars [] (TI A)"
          define y' where "y' ≡ newvars x' (TI B)"
          define z' where "z' ≡ newvars (x' @ y') (TI C)"
          assume " distinct (v @ u @ w)"
          from this have [simp]: "distinct u" and [simp]: "distinct v" and [simp]: "distinct w"
            and [simp]: "set u ∩ set w = {}" and [simp]: "set v ∩ set u = {}" and [simp]: "set v ∩ set w = {}"
            by simp_all
          assume [simp]: "TI A = TVs x" and [simp]: "TI B = TVs y" and [simp]: "TI C = TVs z"
          assume [simp]: "TO A = TVs u" and [simp]: "TO B = TVs v" and [simp]: "TO C = TVs w"
          assume [simp]: "distinct p"
          assume [simp]: "set x ⊆ set p" and [simp]:"set y ⊆ set p" and [simp]: "set z ⊆ set p" and "set q ⊆ set (u @ v @ w)"

          have A: "distinct (x' @ y' @ z')"
            by (metis newvars_distinct newvars_old_distinct_a append_assoc distinct_append x'_def y'_def z'_def)

          have [simp]: "set x' ∩ set y' = {}"
            by (simp add: y'_def)

          have [simp]: "length x' = length x"
            by (simp add: x'_def newvars_length )

          have [simp]: "length y' = length y"
            by (simp add: y'_def newvars_length )

          have [simp]: "length z' = length z"
            by (simp add: z'_def newvars_length )

          have [simp]: "set z' ∩ set y' = {}"
            using A by auto

          have [simp]: "distinct y'"
            using A by auto

          have [simp]: "distinct x'"
            using A by auto

          have [simp]: "distinct z'"
            using A by auto

          have [simp]: "set x' ∩ set z' = {}"
            using A by auto
            

          have [simp]: "Subst (x' @ y' @ z') (x @ y @ z) y' = y"
            by (simp )

          have [simp]: "Subst (x' @ y' @ z') (x @ y @ z) x' = x"
            apply (subst Subst_not_in)
            apply simp_all
            by (metis A Int_commute distinct_append set_append)

          have [simp]: "Subst (x' @ y' @ z') (x @ y @ z) z' = z"
            apply (simp )
            apply (subst Subst_not_in_a)
            apply simp_all
            using ‹set z' ∩ set y' = {}› by blast
            

          have [simp]: "Subst (x' @ y' @ z') (x @ y @ z) (y' @ x' @ z') = y @ x @ z"
            by (simp add: Subst_append)

          have "[p ↝ x @ y @ z] oo (A ∥ B ∥ C) oo [u @ v @ w ↝ q] = [p ↝ x @ y @ z] oo (([x' @ y' ↝ y' @ x'] oo B ∥ A oo [v @ u ↝ u @ v]) ∥ C) oo [u @ v @ w ↝ q]"
            by (subst switch_par [THEN sym], simp_all add: x'_def y'_def)
          also have "... = [p ↝ x @ y @ z] oo (([x' @ y' ↝ y' @ x'] oo B ∥ A oo [v @ u ↝ u @ v]) ∥ ([z' ↝ z'] oo C oo [w ↝ w])) oo [u @ v @ w ↝ q]"
            by (simp add: z'_def)
          also have "... = [p ↝ x @ y @ z] oo ([x' @ y' ↝ y' @ x'] ∥ [z' ↝ z'] oo B ∥ A ∥ C oo [v @ u ↝ u @ v] ∥ [w ↝ w]) oo [u @ v @ w ↝ q]"
            by (simp add: comp_parallel_distrib x'_def y'_def z'_def)
          also have "... = [p ↝ x @ y @ z] oo ([x' @ y' @ z' ↝ y' @ x' @ z'] oo B ∥ A ∥ C oo [v @ u @ w ↝ u @ v @ w]) oo [u @ v @ w ↝ q]"
            apply (subst par_switch, simp_all)
            apply (metis newvars_old_distinct_a append_assoc distinct_append newvars_distinct x'_def y'_def z'_def)
            by (subst par_switch, simp_all)
          also have "... = ([p ↝ x @ y @ z] oo [x' @ y' @ z' ↝ y' @ x' @ z']) oo B ∥ A ∥ C oo ([v @ u @ w ↝ u @ v @ w] oo [u @ v @ w ↝ q])"
            by (simp add: comp_assoc y'_def x'_def z'_def )
          also have "... = ([p ↝ x @ y @ z] oo [x' @ y' @ z' ↝ y' @ x' @ z']) oo B ∥ A ∥ C oo [v @ u @ w ↝ q]"
            apply (subst switch_comp, simp_all add:)
              apply (metis append.assoc perm_tp perm_union_left)
            using ‹set q ⊆ set (u @ v @ w)› by auto
            
(*
            by (metis ‹distinct (v @ u @ w)› append_assoc perm_tp perm_union_left switch_comp)
*)
          also have "... =  [p ↝ y @ x @ z] oo B ∥ A ∥ C oo [v @ u @ w ↝ q]"
            apply (cut_tac A, subst switch_comp_subst, simp_all)
            apply auto [1]
            by (simp add: x'_def y'_def z'_def)

          finally show "[p ↝ x @ y @ z] oo (A ∥ B ∥ C) oo [u @ v @ w ↝ q] = [p ↝ y @ x @ z] oo (B ∥ A ∥ C) oo [v @ u @ w ↝ q]"
            by simp
        qed

      lemma Type_OK_distinct: "Type_OK As ⟹ distinct As"
        by (induction As, simp_all add: Type_OK_simp, auto)
          
      lemma TI_parallel_list_a: "TI (parallel_list As) = concat (map TI As)"
        by (induction As, simp_all add: parallel_list_cons)


      lemma fb_CompA_aux: "Type_OK As ⟹ A ∈ set As ⟹ out A = a ⟹ a ∉ set (In A) ⟹
        InAs = In (Parallel_list As) ⟹ OutAs = Out (Parallel_list As) ⟹ perm (a # y) InAs ⟹ perm (a # z) OutAs ⟹
        InAs' = In (Parallel_list (As ⊖ [A])) ⟹
        fb ([a # y ↝  concat (map In As)] oo parallel_list (map Trs As) oo [OutAs ↝ a # z]) =
                [y ↝ In A @ (InAs' ⊖ [a])] 
                oo (Trs A ∥ [(InAs' ⊖ [a]) ↝  (InAs' ⊖ [a])])
                oo [a # (InAs' ⊖ [a]) ↝ InAs'] oo Trs (Parallel_list (As ⊖ [A])) 
                oo [OutAs ⊖ [a] ↝ z]" (is "_⟹ _ ⟹ _ ⟹ _ ⟹ _ ⟹ _ ⟹ _  ⟹ _ ⟹ _  ⟹ fb ?Ta = ?Tb")
        proof -
          assume [simp]:"Type_OK As"
          assume [simp]:"A ∈ set As"
          assume X[simp]: "out A = a"
          assume InAs': "InAs' = In (Parallel_list (As ⊖ [A]))"

          assume InAs: "InAs = In (Parallel_list As)"
          assume OutAs: "OutAs = Out (Parallel_list As)"

          assume permInAs: "perm (a # y) InAs"
          assume PermOutAs: "perm (a # z) OutAs"

          assume [simp]: "a ∉ set (In A)"
          
          obtain Cs Ds where A: "As = Cs @ (A # Ds)" by (cut_tac split_list, auto)

          from OutAs have OutAs_simp: "OutAs = concat (map Out As)"
            by (simp add: OutAs Out_Parallel)

          have [simp]: "distinct InAs"
            using InAs ‹Type_OK As› io_diagram_def io_diagram_parallel_list by blast

          have "distinct OutAs"
            using Type_OK_def OutAs_simp ‹Type_OK As› by blast

          have distinctAs: "distinct As"
            by (rule Type_OK_distinct, simp)

          from distinctAs have Ba: "As ⊖ [A] = Cs @ Ds"
            apply (simp add: A union_diff)
            by (simp add: AAA_c)

          have [simp]: "Type_OK (Cs @ Ds)"
            apply (subgoal_tac "Type_OK As")
            apply (unfold Type_OK_simp A) [1]
            by (simp_all)


          have [simp]: "distinct InAs'"
            apply (simp add: InAs' Ba)
            using ‹Type_OK (Cs @ Ds)› io_diagram_def io_diagram_parallel_list by blast


          define C where "C ≡ parallel_list (map Trs Cs)"
          define D where "D ≡ parallel_list (map Trs Ds)"
          define InCs where "InCs ≡ concat (map In Cs)"
          define InDs where "InDs ≡ concat (map In Ds)"
          define OutCs where "OutCs ≡ Out (Parallel_list Cs)"
          define OutDs where "OutDs ≡ Out (Parallel_list Ds)"

          have [simp]: "Out A = [a]"
            using Type_OK_out ‹A ∈ set As› ‹Type_OK As› ‹out A = a› by blast
        
          from A have [simp]: "parallel_list (map Trs As) = C ∥ Trs A ∥ D"
            by (simp add: parallel_list_append parallel_list_cons C_def D_def par_assoc)


          from A have [simp]: "concat (map In As) = InCs @ In A @ InDs"
            by (simp add:  InCs_def InDs_def par_assoc) 

          from A have [simp]: "OutAs = OutCs @ [a] @ OutDs"
            by (simp add:  OutCs_def OutDs_def par_assoc OutAs Out_Parallel)

          have [simp]:"a ∉ set y" and [simp]: "distinct y"
            apply (meson ‹distinct InAs› dist_perm distinct.simps(2) permInAs perm_sym)
            by (meson ‹distinct InAs› dist_perm distinct.simps(2) permInAs perm_sym)
    
          have [simp]: "distinct OutCs"
            by (metis Type_OK_def OutAs_simp ‹OutAs = OutCs @ [a] @ OutDs› ‹Type_OK As› distinct_append)

          have [simp]: " a ∉ set OutDs"
            by (metis OutAs_simp Out_Parallel ‹OutAs = OutCs @ [a] @ OutDs› ‹Type_OK As› append.simps(2) disjoint_iff_not_equal distinct_append list.set_intros(1) io_diagram_def io_diagram_parallel_list)
  
          have [simp]: " distinct OutDs "
            by (metis Type_OK_def OutAs_simp ‹OutAs = OutCs @ [a] @ OutDs› ‹Type_OK As› distinct_append)

          have [simp]: " a ∉ set OutCs "
            by (metis OutAs_simp Out_Parallel ‹OutAs = OutCs @ [a] @ OutDs› ‹Type_OK As› append.simps(2) disjoint_iff_not_equal distinct_append list.set_intros(1) io_diagram_def io_diagram_parallel_list)

          have [simp]: "set OutCs ∩ set OutDs = {}"
            by (metis Type_OK_def OutAs_simp ‹OutAs = OutCs @ [a] @ OutDs› ‹Type_OK As› append_assoc dist_perm distinct_append perm_tp)

          have Type_OK_Cs: "Type_OK Cs"
            apply (subgoal_tac "Type_OK As")
            apply (unfold A Type_OK_simp) [1]
            by simp_all

          from this have [simp]: " TI C = TVs InCs"
            apply (simp add: C_def InCs_def)
            apply (subst TI_parallel_list)
            by (simp add: Type_OK_def, simp)

          have Type_OK_Ds: "Type_OK Ds"
            apply (subgoal_tac "Type_OK As")
            apply (unfold A Type_OK_simp) [1]
            by simp_all

          from this have [simp]: " TI D = TVs InDs"
            apply (simp add: D_def InDs_def)
            apply (subst TI_parallel_list)
            by (simp add: Type_OK_def, simp)


          from Type_OK_Cs have [simp]: " TO C = TVs OutCs"
            apply (simp add: C_def OutCs_def)
            apply (subst TO_parallel_list)
            apply (simp add: Type_OK_def)
            by (simp add: Out_Parallel)

          from Type_OK_Ds have [simp]: "TO D = TVs OutDs"
            apply (simp add: D_def OutDs_def)
            apply (subst TO_parallel_list)
            apply (simp add: Type_OK_def)
            by (simp add: Out_Parallel)

          from ‹Type_OK As› have [simp]: "io_diagram A"
            by (unfold Type_OK_def, simp)

          have B: "?Ta = [a # y ↝ In A @ InCs @ InDs] oo (Trs A ∥ C ∥ D) oo [ [ a ] @ OutCs @ OutDs ↝ a # z]"
            apply (subst par_swap_aux, simp_all)
            apply (cut_tac ‹perm (a#y) InAs›)
            apply (drule perm_set_eq, simp add: InAs In_Parallel)
            apply auto [1]
            apply (cut_tac ‹perm (a#y) InAs›)
            apply (drule perm_set_eq, simp add: InAs InCs_def A In_Parallel)
            apply auto [1]
            apply (cut_tac ‹perm (a#y) InAs›)
            apply (drule perm_set_eq, simp add: InAs InDs_def A In_Parallel)
            apply auto [1]
            apply (cut_tac ‹perm (a # z) OutAs›)
            by (drule perm_set_eq, simp add: OutCs_def OutDs_def A Out_Parallel In_Parallel, auto)

            

          define E where "E ≡ C ∥ D"
          define InE where "InE ≡ InCs @ InDs"
          define OutE where "OutE ≡ OutCs @ OutDs"

          from B have C: "?Ta = [a # y ↝ In A @ InE] oo (Trs A ∥ E) oo [ [a ] @ OutE ↝ a # z]"
            by (unfold E_def InE_def OutE_def par_assoc, simp)

          define y' where "y' ≡ newvars (a#y) (TVs y)"

          have [simp]: "a ∉ set y'"
            by (metis newvars_old_distinct_a IntI distinct.simps(2) distinct_singleton list.set(1) list.set_intros(1) y'_def)

          have [simp]: "distinct y'"
            by (simp add: y'_def)

          have [simp]: "set y ∩ set y' = {}"
            by (metis Int_insert_right_if0 ‹a ∉ set y'› inf.commute list.set(2) newvars_old_distinct y'_def)

          have [simp]: "TVs y' = TVs y"
            by (simp add: y'_def)

          have [simp]: "length y' = length y"
            apply (simp add: y'_def)
            by (simp add: newvars_length)

          have [simp]: "Subst (y @ y') (y @ y) y = y"
            by (simp add: inf_aci(1))

          have [simp]: "Subst (y @ y') (y @ y) y' = y"
            using Subst_cons_aux_a ‹TVs y' = TVs y› ‹distinct y'› ‹distinct y› ‹set y ∩ set y' = {}› TVs_length_eq by blast

          have [simp]: "Subst (a # y @ y') (a # y @ y) (y @ a # y') = y @ a # y"
            by (simp add: Subst_append)

          have Au: "set InAs = set InCs ∪ (set (In A) ∪ set InDs)"
            by (simp add: InAs In_Parallel A InCs_def InDs_def, auto)

          have Av: "set InAs = insert a (set y)"
            using ListProp.perm_set_eq permInAs by fastforce

          have [simp]: "set (In A) ⊆ set y"
            by (metis Au Av Un_left_commute Un_upper1 ‹a ∉ set (In A)› subset_insert)
            

          have [simp]: "set (In A) ∩ set y' = {}"
            using ‹set (In A) ⊆ set y› ‹set y ∩ set y' = {}› by blast

          have [simp]: "Subst (y @ a # y') (y @ a # y) (In A) = In A"
            by (simp add: Subst_cancel_right)

          have [simp]: "set InCs ⊆ insert a (set y)"
            using Au Av by auto

          have [simp]: "Subst (a # y') (a # y) (Subst (a # y) (a # y') InCs) = InCs"
            by (subst Subst_Subst_id, simp_all) 

          from this have [simp]: "Subst y' y (Subst y y' InCs) = InCs"
            by (simp add: Subst_cancel_right_a)

          have [simp]: "set InDs ⊆ insert a (set y)"
            using Au Av by auto

          from this have [simp]: "Subst (a # y') (a # y) (Subst (a # y) (a # y') InDs) = InDs"
            by (subst Subst_Subst_id, simp_all)

          from this have [simp]: "Subst y' y (Subst y y' InDs) = InDs"
            by (simp add: Subst_cancel_right_a)

          have [simp]: "Subst (y @ a # y') (y @ a # y) (In A @ Subst (a # y) (a # y') InE) = In A @ InE"
            by (simp add: InE_def Subst_append Subst_cancel_right)
            
          have [simp]: "a ∉ set OutE"
            by (simp add: OutE_def)

          have