X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=curry-howard;h=f3c1be7590eb348711cee3bd4d25e993f1272749;hp=7840e37716f9307fe64d6bb005007bf7cd4f57a1;hb=e519121696a33c116b0942cb289e74d4d978b80c;hpb=37309e8fca0040224958bf089c024d301e39de09

diff --git a/curry-howard b/curry-howard
index 7840e377..f3c1be75 100644
--- a/curry-howard
+++ b/curry-howard
@@ -139,4 +139,28 @@ show beta reduction, so "normal" proof.
 
 [To do: add pairs and destructors; unit and negation...]
 
-Excercise: construct a proof whose labeling is the combinator S.
+Excercise: construct a proof whose labeling is the combinator S,
+something like this:
+
+           --------- Ax  --------- Ax   ------- Ax
+           !a --> !a     !b --> !b      c --> c
+           ----------------------- L->  -------- L!
+              !a,!a->!b --> !b          !c --> c
+--------- Ax  ---------------------------------- L->
+!a --> !a           !a,!b->!c,!a->!b --> c
+------------------------------------------ L->
+      !a,!a,!a->!b->!c,!a->!b --> c
+      ----------------------------- C!
+       !a,!a->!b->!c,!a->!b --> c
+       ------------------------------ L!
+       !a,!a->!b->!c,! (!a->!b) --> c
+       ---------------------------------- L!
+       !a,! (!a->!b->!c),! (!a->!b) --> c
+       ----------------------------------- R!
+       !a,! (!a->!b->!c),! (!a->!b) --> !c
+       ------------------------------------ R->
+       ! (!a->!b->!c),! (!a->!b) --> !a->!c
+       ------------------------------------- R->
+       ! (!a->!b) --> ! (!a->!b->!c)->!a->!c
+       --------------------------------------- R->
+        --> ! (!a->!b)->! (!a->!b->!c)->!a->!c