added Curry-Howard

[lambda.git] / week6.mdwn

diff --git a/week6.mdwn b/week6.mdwn
index 57158c6..f26285f 100644 (file)
--- a/week6.mdwn
+++ b/week6.mdwn
@@ -261,26 +261,26 @@ Axiom: -----------
 
 Structural Rules:
 
-Exchange: Γ, x:A, y:B, Δ |- R:C
-          -------------------------------
+          Γ, x:A, y:B, Δ |- R:C
+Exchange: -------------------------------
           Γ, y:B, x:A, Δ |- R:C
 
-Contraction: Γ, x:A, x:A |- R:B
-             --------------------------
+             Γ, x:A, x:A |- R:B
+Contraction: --------------------------
              Γ, x:A |- R:B
 
-Weakening: Γ |- R:B
-           --------------------- 
+           Γ |- R:B
+Weakening: --------------------- 
            Γ, x:A |- R:B     [x chosen fresh]
 
 Logical Rules:
 
---> I:   Γ, x:A |- R:B
-         -------------------------
+         Γ, x:A |- R:B
+--> I:   -------------------------
          Γ |- \xM:A --> B  
 
---> E:   Γ |- f:(A --> B)      Γ |- x:A
-         -------------------------------------
+         Γ |- f:(A --> B)      Γ |- x:A
+--> E:   -------------------------------------
          Γ |- (fx):B
 </pre>