Replace context's constructors and add new theorems.

diff --git a/src/Type.agda b/src/Type.agda
index 153acd398f44d385fceea12a40bebe6e9d0a5429..255f3e2980c3844aa259b3c7f9eb3ebf8a6803b0 100644 (file)
--- a/src/Type.agda
+++ b/src/Type.agda
@@ -2,7 +2,7 @@ module Type where
 
 open import Data.Nat using (ℕ)
 open import Data.String using (String)
-open import Data.Vec using (Vec) renaming (_∷_ to _∷-Vec_)
+open import Data.Vec using (Vec; _∷_)
 open import Variable
 
 
@@ -27,16 +27,16 @@ Ctx : ℕ → Set
 Ctx = Vec TypeDecl
 
 data Context : Set where
-  â\97\86 : â\88\80 {n} â\86\92 Ctx n â\86\92 Context
-  ■ : Context → Context → Context
+  â\8b\86 : â\88\80 {n} â\86\92 Ctx n â\86\92 Context
+  & : Context → Context → Context
 
 infix 4 _∈_
 
 data _∈_ : TypeDecl → Context → Set where
-  here-â\97\86 : â\88\80 {n} {x} {xs : Ctx n} â\86\92 x â\88\88 â\97\86 (x â\88·-Vec xs)
-  there-â\97\86 : â\88\80 {n} {x y} {xs : Ctx n} (xâ\88\88xs : x â\88\88 â\97\86 xs) â\86\92 x â\88\88 â\97\86 (y â\88·-Vec xs)
-  here-left-â\96  : â\88\80 {n m} {x} {xs : Ctx n} {ys : Ctx m} â\86\92 x â\88\88 â\96   (â\97\86 (x â\88·-Vec xs)) (â\97\86 ys)
-  here-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ ■ (◆ xs) (◆ (x ∷-Vec ys))
-  there-left-â\96  : â\88\80 {n m} {x} {xs : Ctx n} {ys : Ctx m} (xâ\88\88xs : x â\88\88 â\96  (â\97\86 xs) (â\97\86 ys)) â\86\92 x â\88\88 â\96  (â\97\86 (x â\88·-Vec xs)) (â\97\86 ys)
-  there-right-■ : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ ■ (◆ xs) (◆ ys)) → x ∈ ■ (◆ xs) (◆ (x ∷-Vec ys))
+  here-â\8b\86 : â\88\80 {n} {x} {xs : Ctx n} â\86\92 x â\88\88 â\8b\86 (x â\88· xs)
+  there-â\8b\86 : â\88\80 {n} {x y} {xs : Ctx n} (xâ\88\88xs : x â\88\88 â\8b\86 xs) â\86\92 x â\88\88 â\8b\86 (y â\88· xs)
+  here-left-& : â\88\80 {n m} {x} {xs : Ctx n} {ys : Ctx m} â\86\92 x â\88\88 & (â\8b\86 (x â\88· xs)) (â\8b\86 ys)
+  here-right-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} → x ∈ & (⋆ xs) (⋆ (x ∷ ys))
+  there-left-& : â\88\80 {n m} {x} {xs : Ctx n} {ys : Ctx m} (xâ\88\88xs : x â\88\88 & (â\8b\86 xs) (â\8b\86 ys)) â\86\92 x â\88\88 & (â\8b\86 (x â\88· xs)) (â\8b\86 ys)
+  there-right-& : ∀ {n m} {x} {xs : Ctx n} {ys : Ctx m} (x∈xs : x ∈ & (⋆ xs) (⋆ ys)) → x ∈ & (⋆ xs) (⋆ (x ∷ ys))
 

diff --git a/src/TypingBehaviour.agda b/src/TypingBehaviour.agda
index 4cab90f9e9d9a133599b3de5a4978995e8640e09..f4c19154d29f640b69d1e3ce3936a84c9b49656d 100644 (file)
--- a/src/TypingBehaviour.agda
+++ b/src/TypingBehaviour.agda
@@ -53,7 +53,7 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
         → Γ₁ ⊢B b1 ▹ Γ₁'
         → Γ₂ ⊢B b2 ▹ Γ₂'
         ------------------------------------
-        → (■ Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (■ Γ₁' Γ₂')
+        → (& Γ₁ Γ₂) ⊢B b1 ∥ b2 ▹ (& Γ₁' Γ₂')
 
   t-seq : {Γ Γ₁ Γ₂ : Context} {b₁ b₂ : Behaviour}
         → Γ ⊢B b₁ ▹ Γ₁
@@ -69,22 +69,22 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                  → Γ ⊢B output (o at l [ var e ]) ▹ Γ
 
   t-assign-new : ∀ {n} {Γ : Ctx n} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
-               â\86\92 â\97\86 Î\93 â\8a¢â\82\91 e â\88¶ Tâ\82\91 -- Î\93 â\8a¢ e : bool
-               â\86\92 ¬ (var x Tâ\82\93 â\88\88 â\97\86 Î\93) -- x â\88\89 Î\93
+               â\86\92 â\8b\86 Î\93 â\8a¢â\82\91 e â\88¶ Tâ\82\91 -- Î\93 â\8a¢ e : bool
+               â\86\92 ¬ (var x Tâ\82\93 â\88\88 â\8b\86 Î\93) -- x â\88\89 Î\93
                ---------------------------------
-               â\86\92 â\97\86 Î\93 â\8a¢B x â\89\83 e â\96¹ â\97\86 (var x Tâ\82\91 â\88· Î\93)
+               â\86\92 â\8b\86 Î\93 â\8a¢B x â\89\83 e â\96¹ â\8b\86 (var x Tâ\82\91 â\88· Î\93)
 
   t-assign-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m}  {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
-                    → â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81) â\8a¢â\82\91 e â\88¶ Tâ\82\91 -- Î\93 â\8a¢ e : bool
-                    → ¬ (var x Tₓ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81)) -- x â\88\89 Î\93
+                    → & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81) â\8a¢â\82\91 e â\88¶ Tâ\82\91 -- Î\93 â\8a¢ e : bool
+                    → ¬ (var x Tₓ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81)) -- x â\88\89 Î\93
                     -------------------------------------------------------
-                    → â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81) â\8a¢B x â\89\83 e â\96¹ â\96  (â\97\86 (var x Tâ\82\91 â\88· Î\93)) (â\97\86 Î\93â\82\81)
+                    → & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81) â\8a¢B x â\89\83 e â\96¹ & (â\8b\86 (var x Tâ\82\91 â\88· Î\93)) (â\8b\86 Î\93â\82\81)
 
   t-assign-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m}  {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
-                     → â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81) â\8a¢â\82\91 e â\88¶ Tâ\82\91 -- Î\93 â\8a¢ e : bool
-                     → ¬ (var x Tₓ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81)) -- x â\88\89 Î\93
+                     → & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81) â\8a¢â\82\91 e â\88¶ Tâ\82\91 -- Î\93 â\8a¢ e : bool
+                     → ¬ (var x Tₓ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81)) -- x â\88\89 Î\93
                      ------------------------------------------------------
-                     → â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81) â\8a¢B x â\89\83 e â\96¹ â\96  (â\97\86 Î\93) (â\97\86 (var x Tâ\82\91 â\88· Î\93â\82\81))
+                     → & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81) â\8a¢B x â\89\83 e â\96¹ & (â\8b\86 Î\93) (â\8b\86 (var x Tâ\82\91 â\88· Î\93â\82\81))
 
   t-assign-exists : {Γ : Context} {x : Variable} {e : Expr} {Tₓ Tₑ : Type}
                   → Γ ⊢ₑ e ∶ Tₑ
@@ -94,22 +94,22 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                   → Γ ⊢B x ≃ e ▹ Γ
 
   t-oneway-new : ∀ {n} {Γ : Ctx n} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
-               â\86\92 inOneWay o Táµ¢ â\88\88 â\97\86 Î\93
-               â\86\92 ¬ (var x Tâ\82\93 â\88\88 â\97\86 Î\93)
+               â\86\92 inOneWay o Táµ¢ â\88\88 â\8b\86 Î\93
+               â\86\92 ¬ (var x Tâ\82\93 â\88\88 â\8b\86 Î\93)
                -------------------------------------------
-               â\86\92 â\97\86 Î\93 â\8a¢B input (o [ x ]) â\96¹ â\97\86 (var x Táµ¢ â\88· Î\93)
+               â\86\92 â\8b\86 Î\93 â\8a¢B input (o [ x ]) â\96¹ â\8b\86 (var x Táµ¢ â\88· Î\93)
 
   t-oneway-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
-                    → inOneWay o Tᵢ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81)
-                    → ¬ (var x Tₓ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81))
+                    → inOneWay o Tᵢ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81)
+                    → ¬ (var x Tₓ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81))
                     -----------------------------------------------------------------
-                    → â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81) â\8a¢B input (o [ x ]) â\96¹ â\96  (â\97\86 (var x Táµ¢ â\88· Î\93)) (â\97\86 Î\93â\82\81)
+                    → & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81) â\8a¢B input (o [ x ]) â\96¹ & (â\8b\86 (var x Táµ¢ â\88· Î\93)) (â\8b\86 Î\93â\82\81)
 
   t-oneway-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
-                     → inOneWay o Tᵢ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81)
-                     → ¬ (var x Tₓ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81))
+                     → inOneWay o Tᵢ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81)
+                     → ¬ (var x Tₓ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81))
                      -----------------------------------------------------------------
-                     → â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81) â\8a¢B input (o [ x ]) â\96¹ â\96  (â\97\86 Î\93) (â\97\86 (var x Táµ¢ â\88· Î\93â\82\81))
+                     → & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81) â\8a¢B input (o [ x ]) â\96¹ & (â\8b\86 Î\93) (â\8b\86 (var x Táµ¢ â\88· Î\93â\82\81))
 
   t-oneway-exists : {Γ : Context} {Tₓ Tᵢ : Type} {o : Operation} {x : Variable}
                   → inOneWay o Tᵢ ∈ Γ
@@ -119,25 +119,25 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                   → Γ ⊢B input (o [ x ]) ▹ Γ
 
   t-solresp-new : ∀ {n} {Γ : Ctx n} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
-                â\86\92 outSolRes o l Tâ\82\92 Táµ¢ â\88\88 â\97\86 Î\93
+                â\86\92 outSolRes o l Tâ\82\92 Táµ¢ â\88\88 â\8b\86 Î\93
                 → Tₑ ⊆ Tₒ
-                â\86\92 ¬ (var x Tâ\82\93 â\88\88 â\97\86 Î\93)
+                â\86\92 ¬ (var x Tâ\82\93 â\88\88 â\8b\86 Î\93)
                 ------------------------------------------------------
-                â\86\92 â\97\86 Î\93 â\8a¢B output (o at l [ e ][ x ]) â\96¹ â\97\86 (var x Táµ¢ â\88· Î\93)
+                â\86\92 â\8b\86 Î\93 â\8a¢B output (o at l [ e ][ x ]) â\96¹ â\8b\86 (var x Táµ¢ â\88· Î\93)
 
   t-solresp-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
-                     → outSolRes o l Tₒ Tᵢ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81)
+                     → outSolRes o l Tₒ Tᵢ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81)
                      → Tₑ ⊆ Tₒ
-                     → ¬ (var x Tₓ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81))
+                     → ¬ (var x Tₓ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81))
                      ----------------------------------------------------------------------------
-                     → â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81) â\8a¢B output (o at l [ e ][ x ]) â\96¹ â\96  (â\97\86 (var x Táµ¢ â\88· Î\93)) (â\97\86 Î\93â\82\81)
+                     → & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81) â\8a¢B output (o at l [ e ][ x ]) â\96¹ & (â\8b\86 (var x Táµ¢ â\88· Î\93)) (â\8b\86 Î\93â\82\81)
 
   t-solresp-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
-                      → outSolRes o l Tₒ Tᵢ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81)
+                      → outSolRes o l Tₒ Tᵢ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81)
                       → Tₑ ⊆ Tₒ
-                      → ¬ (var x Tₓ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81))
+                      → ¬ (var x Tₓ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81))
                       ----------------------------------------------------------------------------
-                      → â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81) â\8a¢B output (o at l [ e ][ x ]) â\96¹ â\96  (â\97\86 Î\93) (â\97\86 (var x Táµ¢ â\88· Î\93â\82\81))
+                      → & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81) â\8a¢B output (o at l [ e ][ x ]) â\96¹ & (â\8b\86 Î\93) (â\8b\86 (var x Táµ¢ â\88· Î\93â\82\81))
 
   t-solresp-exists : {Γ : Context} {o : Operation} {l : Location} {Tₒ Tᵢ Tₑ Tₓ : Type} {e : Expr} {x : Variable}
                    → outSolRes o l Tₒ Tᵢ ∈ Γ
@@ -148,31 +148,31 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                    → Γ ⊢B output (o at l [ e ][ x ]) ▹ Γ
 
   t-reqresp-new : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
-                â\86\92 inReqRes o Táµ¢ Tâ\82\92 â\88\88 â\97\86 Î\93
-                â\86\92 ¬ (var x Tâ\82\93 â\88\88 â\97\86 Î\93)
-                â\86\92 â\97\86 (var x Tâ\82\93 â\88· Î\93) â\8a¢B b â\96¹ â\97\86 Î\93â\82\81
-                â\86\92 var a Tâ\82\90 â\88\88 â\97\86 Î\93â\82\81
+                â\86\92 inReqRes o Táµ¢ Tâ\82\92 â\88\88 â\8b\86 Î\93
+                â\86\92 ¬ (var x Tâ\82\93 â\88\88 â\8b\86 Î\93)
+                â\86\92 â\8b\86 (var x Tâ\82\93 â\88· Î\93) â\8a¢B b â\96¹ â\8b\86 Î\93â\82\81
+                â\86\92 var a Tâ\82\90 â\88\88 â\8b\86 Î\93â\82\81
                 → Tₐ ⊆ Tₒ
                 --------------------------------------
-                â\86\92 â\97\86 Î\93 â\8a¢B input (o [ x ][ a ] b) â\96¹ â\97\86 Î\93â\82\81
+                â\86\92 â\8b\86 Î\93 â\8a¢B input (o [ x ][ a ] b) â\96¹ â\8b\86 Î\93â\82\81
 
   t-reqresp-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ₂ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
-                     → inReqRes o Tᵢ Tₒ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81)
-                     → ¬ (var x Tₓ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81))
-                     → â\96  (â\97\86 (var x Tâ\82\93 â\88· Î\93)) (â\97\86 Î\93â\82\81) â\8a¢B b â\96¹ Î\93â\82\82
+                     → inReqRes o Tᵢ Tₒ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81)
+                     → ¬ (var x Tₓ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81))
+                     → & (â\8b\86 (var x Tâ\82\93 â\88· Î\93)) (â\8b\86 Î\93â\82\81) â\8a¢B b â\96¹ Î\93â\82\82
                      → var a Tₐ ∈ Γ₂
                      → Tₐ ⊆ Tₒ
                      ------------------------------------
-                     â\86\92 â\97\86 Î\93 â\8a¢B input (o [ x ][ a ] b) â\96¹ Î\93â\82\82
+                     â\86\92 â\8b\86 Î\93 â\8a¢B input (o [ x ][ a ] b) â\96¹ Î\93â\82\82
 
   t-reqresp-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {Γ₂ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {x a : Variable} {b : Behaviour}
-                      → inReqRes o Tᵢ Tₒ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81)
-                      → ¬ (var x Tₓ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81))
-                      → â\96  (â\97\86 Î\93) (â\97\86 (var x Tâ\82\93 â\88· Î\93â\82\81)) â\8a¢B b â\96¹ Î\93â\82\82
+                      → inReqRes o Tᵢ Tₒ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81)
+                      → ¬ (var x Tₓ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81))
+                      → & (â\8b\86 Î\93) (â\8b\86 (var x Tâ\82\93 â\88· Î\93â\82\81)) â\8a¢B b â\96¹ Î\93â\82\82
                       → var a Tₐ ∈ Γ₂
                       → Tₐ ⊆ Tₒ
                       ------------------------------------
-                      â\86\92 â\97\86 Î\93 â\8a¢B input (o [ x ][ a ] b) â\96¹ Î\93â\82\82
+                      â\86\92 â\8b\86 Î\93 â\8a¢B input (o [ x ][ a ] b) â\96¹ Î\93â\82\82
 
   t-reqresp-exists : {Γ Γ₁ : Context} {o : Operation} {Tᵢ Tₒ Tₓ Tₐ : Type} {b : Behaviour} {x a : Variable}
                    → (inReqRes o Tᵢ Tₒ) ∈ Γ
@@ -185,22 +185,22 @@ data _⊢B_▹_ : Context → Behaviour → Context → Set where
                    → Γ ⊢B input (o [ x ][ a ] b) ▹ Γ₁
 
   t-wait-new : ∀ {n} {Γ : Ctx n} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
-             â\86\92 outSolRes o l Tâ\82\92 Táµ¢ â\88\88 â\97\86 Î\93
-             â\86\92 ¬ (var x Tâ\82\93 â\88\88 â\97\86 Î\93)
+             â\86\92 outSolRes o l Tâ\82\92 Táµ¢ â\88\88 â\8b\86 Î\93
+             â\86\92 ¬ (var x Tâ\82\93 â\88\88 â\8b\86 Î\93)
              ----------------------------------------
-             â\86\92 â\97\86 Î\93 â\8a¢B wait r o l x â\96¹ â\97\86 (var x Táµ¢ â\88· Î\93)
+             â\86\92 â\8b\86 Î\93 â\8a¢B wait r o l x â\96¹ â\8b\86 (var x Táµ¢ â\88· Î\93)
 
   t-wait-new-left : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
-                  → outSolRes o l Tₒ Tᵢ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81)
-                  → ¬ (var x Tₓ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81))
+                  → outSolRes o l Tₒ Tᵢ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81)
+                  → ¬ (var x Tₓ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81))
                   --------------------------------------------------------------
-                  → â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81) â\8a¢B wait r o l x â\96¹ â\96  (â\97\86 (var x Táµ¢ â\88· Î\93)) (â\97\86 Î\93â\82\81)
+                  → & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81) â\8a¢B wait r o l x â\96¹ & (â\8b\86 (var x Táµ¢ â\88· Î\93)) (â\8b\86 Î\93â\82\81)
 
   t-wait-new-right : ∀ {n m} {Γ : Ctx n} {Γ₁ : Ctx m} {o : Operation} {Tₒ Tᵢ Tₓ : Type} {l : Location} {r : Channel} {x : Variable}
-                   → outSolRes o l Tₒ Tᵢ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81)
-                   → ¬ (var x Tₓ ∈ â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81))
+                   → outSolRes o l Tₒ Tᵢ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81)
+                   → ¬ (var x Tₓ ∈ & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81))
                    --------------------------------------------------------------
-                   → â\96  (â\97\86 Î\93) (â\97\86 Î\93â\82\81) â\8a¢B wait r o l x â\96¹ â\96  (â\97\86 Î\93) (â\97\86 (var x Táµ¢ â\88· Î\93â\82\81))
+                   → & (â\8b\86 Î\93) (â\8b\86 Î\93â\82\81) â\8a¢B wait r o l x â\96¹ & (â\8b\86 Î\93) (â\8b\86 (var x Táµ¢ â\88· Î\93â\82\81))
 
   t-wait-exists : {Γ : Context} {Tₒ Tᵢ Tₓ : Type} {o : Operation} {l : Location} {r : Channel} {x : Variable}
                 → outSolRes o l Tₒ Tᵢ ∈ Γ
@@ -223,12 +223,22 @@ struct-congruence : {Γ Γ₁ : Context} {b₁ b₂ : Behaviour}
                   → Γ ⊢B b₂ ▹ Γ₁
 struct-congruence t refl = t
 
+struct-cong-seq-nil : {Γ Γ₁ : Context} {b : Behaviour}
+                    → Γ ⊢B nil ∶ b ▹ Γ₁
+                    → Γ ⊢B b ▹ Γ₁
+struct-cong-seq-nil (t-seq t-nil x) = x
+
 struct-cong-par-nil : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b : Behaviour}
-                    → ■ Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ ■ Γ₁' Γ₂'
+                    → & Γ₁ Γ₂ ⊢B (b ∥ nil) ▹ & Γ₁' Γ₂'
                     → Γ₁ ⊢B b ▹ Γ₁'
 struct-cong-par-nil (t-par x _) = x
 
 struct-cong-par-sym : {Γ₁ Γ₂ Γ₁' Γ₂' : Context} {b₁ b₂ : Behaviour}
-                    → ■ Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ ■ Γ₁' Γ₂'
-                    → ■ Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ ■ Γ₂' Γ₁'
+                    → & Γ₁ Γ₂ ⊢B (b₁ ∥ b₂) ▹ & Γ₁' Γ₂'
+                    → & Γ₂ Γ₁ ⊢B (b₂ ∥ b₁) ▹ & Γ₂' Γ₁'
 struct-cong-par-sym (t-par t₁ t₂) = t-par t₂ t₁
+
+struct-cong-par-assoc : {Γ₁ Γ₂ Γ₃ Γ₁' Γ₂' Γ₃' : Context} {b₁ b₂ b₃ : Behaviour}
+                      → & (& Γ₁ Γ₂) Γ₃ ⊢B (b₁ ∥ b₂) ∥ b₃ ▹ & (& Γ₁' Γ₂') Γ₃'
+                      → & Γ₁ (& Γ₂ Γ₃) ⊢B b₁ ∥ (b₂ ∥ b₃) ▹ & Γ₁' (& Γ₂' Γ₃')
+struct-cong-par-assoc (t-par (t-par t1 t2) t3) = t-par t1 (t-par t2 t3)