[Started proving the last few lemmas, but they are too awkward.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20080312223843
 + I don't want to push this any further without first simplifying
   things.
] hunk ./Wand.agda 24
+open import Relation.Binary.PropositionalEquality1
+open import Algebra.Structures
+open import Data.Nat.Properties
hunk ./Wand.agda 364
-    data LinearExp : (n : ℕ) -> (V ^ n → C) -> Set where
+    data LinearExp : (n : ℕ) -> V ^ n → C -> Set where
hunk ./Wand.agda 399
-  ⟦_⟧' : forall {n} -> (V ^ n → C) -> Stack n -> C
+  ⟦_⟧' : forall {a n} -> V ^ n → a -> Stack n -> a
hunk ./Wand.agda 403
-  ⟦_⟧ : forall {n} -> (V ^ n → C) -> Stack n -> C
+  ⟦_⟧ : forall {a n} -> V ^ n → a -> Stack n -> a
hunk ./Wand.agda 406
+  -- ⟦ B″ n₁ n₂ f g ⟧ (y_n₁ ∷ … ∷ y₁ ∷ x_n₂ ∷ … ∷ x₁ ∷ [])
+
+  -- B″ n₁ n₂ f g ≈ \x₁ … x_n₂ y₁ … y_n₁ -> f (g x₁ … x_n₂) y₁ … y_n₁
+
+  --   ⟦ B″ n₁ n₂ f g ⟧ (y_n₁ ∷ … ∷ y₁ ∷ x_n₂ ∷ … ∷ x₁ ∷ []) σ
+  -- ≈ f (g x₁ … x_n₂) y₁ … y_n₁ σ
+  -- ≈ f (⟦ g ⟧ (x_n₂ ∷ … ∷ x₁ ∷ []) y₁ … y_n₁ σ
+  -- ≈ ⟦ f (⟦ g ⟧ (x_n₂ ∷ … ∷ x₁ ∷ [])) ⟧ (y_n₁ ∷ … ∷ y₁ ∷ []) σ
+
+  --   ⟦ B″ 2 n Step₁.add g ⟧ (x ∷ y ∷ s) σ
+  -- ≈ ⟦ \x₁ … x_n y₁ y₂ -> Step₁.add (g x₁ … x_n) y₁ y₂ ⟧ (x ∷ y ∷ s) σ
+  -- ≈ ⟦ \x₁ … x_n y₁ y₂ -> Step₁.add (g x₁ … x_n) y₁ y₂ ⟧' (reverse s ++ y ∷ x ∷ []) σ
+  -- ≈ Step₁.add (⟦ g ⟧ s) y x σ
+  -- ≈ (\κ v₁ v₂ -> κ (v₁ + v₂)) (⟦ g ⟧ s) y x σ
+  -- ≈ ⟦ g ⟧ s (y + x) σ
+
+  --   ⟦ B″ 2 n Step₁.add g ⟧ (x ∷ y ∷ z ∷ []) σ
+  -- ≈ ⟦ \x y₁ y₂ -> Step₁.add (g x) y₁ y₂ ⟧ (x ∷ y ∷ z ∷ []) σ
+  -- ≈ ⟦ \x y₁ y₂ -> Step₁.add (g x) y₁ y₂ ⟧' (z ∷ y ∷ x ∷ []) σ
+  -- ≈ Step₁.add (⟦ g ⟧ (z ∷ [])) y x σ
+  -- ≈ (\κ v₁ v₂ -> κ (v₁ + v₂)) (⟦ g ⟧ (z ∷ [])) y x σ
+  -- ≈ ⟦ g ⟧ (z ∷ []) (y + x) σ
+  -- ≈ g z (y + x) σ
+
+  -- test : forall x y z (g : V ^ 2 → C) -> C
+  -- test = \x y z g σ -> ⟦ B″ 2 1 Step₁.add g ⟧ (x ∷ y ∷ z ∷ []) σ
+
+  -- test₂ : forall x y z₁ z₂ z₃ (g : V ^ 4 → C) -> C
+  -- test₂ = \x y z₁ z₂ z₃ g σ -> ⟦ B″ 2 3 Step₁.add g ⟧ (x ∷ y ∷ z₁ ∷ z₂ ∷ z₃ ∷ []) σ
+
+  lemma' : forall {n₁ n₂}
+                  (f : K -> V ^ n₁ → C) (g : V ^ suc n₂ → C)
+                  (s₁ : Stack n₁) (s₂ : Stack n₂) (σ : S) ->
+           let open IsCommutativeSemiring _ ℕ-isCommutativeSemiring in
+           ⟦ B″ n₁ n₂ f g ⟧' (≡-subst Stack (+-comm n₂ n₁) (s₂ ++ s₁)) σ ≡
+           ⟦ f (⟦ ≡₁-subst (shift n₂) g ⟧' s₂) ⟧' s₁ σ
+  lemma' {n₁} {n₂} f g s₁ s₂ σ = {! !}
+
+  lemma : forall {n₁ n₂}
+                 (f : K -> V ^ n₁ → C) (g : V ^ suc n₂ → C)
+                 (s₁ : Stack n₁) (s₂ : Stack n₂) (σ : S) ->
+          ⟦ B″ n₁ n₂ f g ⟧ (s₁ ++ s₂) σ ≡
+          ⟦ f (⟦ ≡₁-subst (shift n₂) g ⟧ s₂) ⟧ s₁ σ
+  lemma {n₁} {n₂} f g s₁ s₂ σ = {! !}
+
+  shift-lemma' : forall {b n} (g : V ^ suc n → b) (s : Stack n) x ->
+                 ⟦ ≡₁-subst (shift n) g ⟧' s x ≡
+                 ⟦ ≡₁-subst (swap 1 n) g ⟧' (s ++ x ∷ [])
+  shift-lemma' g []      x = ≡-refl
+  shift-lemma' g (y ∷ s) x = {! !}
+
+  shift-lemma : forall {b n} (g : V ^ suc n → b) (s : Stack n) x ->
+                ⟦ ≡₁-subst (shift n) g ⟧ s x ≡ ⟦ g ⟧ (x ∷ s)
+  shift-lemma {n = n} g s x = begin
+    ⟦ ≡₁-subst (shift n) g ⟧ s x
+      ≡⟨ shift-lemma' g (reverse s) x ⟩
+    ⟦ ≡₁-subst (swap 1 n) g ⟧' (reverse s ++ x ∷ [])
+      ≡⟨ {! !} ⟩
+    ⟦ ≡₁-subst (swap 1 n) g ⟧' (reverse (reverse (reverse s ++ x ∷ [])))
+      ≡⟨ ≡-refl ⟩
+    ⟦ ≡₁-subst (swap 1 n) g ⟧ (reverse (reverse s ++ x ∷ []))
+      ≡⟨ {! !} ⟩
+    ⟦ g ⟧ (x ∷ s)
+      ∎
+
hunk ./Wand.agda 473
-  lemma₁ g x y []      σ = ≡-refl
-  lemma₁ g x y (z ∷ s) σ = {! !}
+  lemma₁ {n} g x y s σ = begin
+    ⟦ B″ 2 n Step₁.add g ⟧ (x ∷ y ∷ s) σ
+      ≡⟨ lemma Step₁.add g (x ∷ y ∷ []) s σ ⟩
+    ⟦ Step₁.add (⟦ ≡₁-subst (shift n) g ⟧ s) ⟧ (x ∷ y ∷ []) σ
+      ≡⟨ ≡-refl ⟩
+    ⟦ ≡₁-subst (shift n) g ⟧ s (y + x) σ
+      ≡⟨ ≡-cong (\f -> f σ) (shift-lemma g s (y + x)) ⟩
+    ⟦ g ⟧ (y + x ∷ s) σ
+      ∎
hunk ./Wand.agda 485
-  lemma₂ g I []      σ = ≡-refl
-  lemma₂ g I (z ∷ s) σ = {! !}
+  lemma₂ {n} g I s σ = begin
+    ⟦ B″ 0 n (Step₁.fetch I) g ⟧ s σ
+      ≡⟨ lemma (Step₁.fetch I) g [] s σ ⟩
+    ⟦ Step₁.fetch I (⟦ ≡₁-subst (shift n) g ⟧ s) ⟧ [] σ
+      ≡⟨ ≡-refl ⟩
+    ⟦ ≡₁-subst (shift n) g ⟧ s (σ I) σ
+      ≡⟨ ≡-cong (\f -> f σ) (shift-lemma g s (σ I)) ⟩
+    ⟦ g ⟧ (σ I ∷ s) σ
+      ∎