[Examined if _⊕_ is commutative.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080501182645] hunk ./AlgebraicProperties.agda 139
+------------------------------------------------------------------------
+-- Commutativity
+
+-- _⊕_ is commutative if the language is total.
+
+⊕-comm : Total -> Commutative _⊕_
+⊕-comm total x y = equal (⟶ _ _) (⟶ _ _)
+  where
+  comm = CommutativeSemiring.+-comm ℕ-commutativeSemiring
+
+  ⟶ : forall x y -> x ⊕ y ⊑ y ⊕ x
+  ⟶ _ _         Int          = Int
+  ⟶ _ _         (Add₃ x⇓ y⇑) = Add₂ y⇑
+  ⟶ x y {i = i} (Add₂ x⇑)    with total y i
+  ⟶ x y {i = i} (Add₂ x⇑)    | returns y⇓ = Add₃ y⇓ x⇑
+  ⟶ x y {i = i} (Add₂ x⇑)    | throws  y⇑ = Add₂ y⇑
+  ⟶ x y {i = i} (Add₁ {m = m} {n = n} x⇓ y⇓) =
+    cast (≡-sym (comm m n)) (Add₁ y⇓ x⇓)
+
+-- _⊕_ is not commutative if the language is non-total.
+
+¬⊕-comm : NonTotal -> ¬ Commutative _⊕_
+¬⊕-comm (¬⇓ x i ¬x⇓) ⊕-comm with ⊕-comm throw x
+¬⊕-comm (¬⇓ x i ¬x⇓) ⊕-comm | equal ⟵ ⟶ = helper (⟵ (Add₂ Throw))
+  where
+  ¬x⇓B : ¬ Σ₀ (\v -> x ⇓[ B ] v)
+  ¬x⇓B (v , x⇓) = ¬x⇓ (v , Bto· x⇓)
+
+  helper : ¬ (x ⊕ throw ⇓[ B ] throw)
+  helper (Add₂ x⇑)   = ¬x⇓B (throw , x⇑)
+  helper (Add₃ x⇓ _) = ¬x⇓B (_ , x⇓)
+