added Curry-Howard

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:
 
 
 Structural Rules:
 

-Exchange: Γ, x:A, y:B, Δ |- R:C
-          -------------------------------
+          Γ, x:A, y:B, Δ |- R:C
+Exchange: -------------------------------

           Γ, y:B, x:A, Δ |- R:C
 
           Γ, y:B, x:A, Δ |- R:C
 

-Contraction: Γ, x:A, x:A |- R:B
-             --------------------------
+             Γ, x:A, x:A |- R:B
+Contraction: --------------------------

              Γ, x:A |- R:B
 
              Γ, x:A |- R:B
 

-Weakening: Γ |- R:B
-           --------------------- 
+           Γ |- R:B
+Weakening: --------------------- 

            Γ, x:A |- R:B     [x chosen fresh]
 
 Logical Rules:
 
            Γ, x:A |- R:B     [x chosen fresh]
 
 Logical Rules:
 

---> I:   Γ, x:A |- R:B
-         -------------------------
+         Γ, x:A |- R:B
+--> I:   -------------------------

          Γ |- \xM:A --> B  
 
          Γ |- \xM:A --> B  
 

---> E:   Γ |- f:(A --> B)      Γ |- x:A
-         -------------------------------------
+         Γ |- f:(A --> B)      Γ |- x:A
+--> E:   -------------------------------------

          Γ |- (fx):B
 </pre>
 
          &Gamma; |- (fx):B
 </pre>