From 35c4714a8cc38b2a8106b54b87684483b5a94f62 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 18 Dec 2020 09:41:23 +0900
Subject: wip58

---
 examples/the-little-prover.scm | 50 +-----------------------------------------
 1 file changed, 1 insertion(+), 49 deletions(-)

(limited to 'examples/the-little-prover.scm')

diff --git a/examples/the-little-prover.scm b/examples/the-little-prover.scm
index 3d0329f..0a0303e 100644
--- a/examples/the-little-prover.scm
+++ b/examples/the-little-prover.scm
@@ -2,52 +2,4 @@
              (vikalpa the-little-prover))
 
 (define-system the-little-prover-0 (the-little-prover)
-  (define-theorem simple-list-induction (x)
-    (equal? (if (natural? (size x))
-                (if (atom? x) '#t (< (size (cdr x)) (size x)))
-                '#t)
-            #t))
-
-  (define-proof simple-list-induction
-    ()
-    (((1 2 3) size/cdr)
-     ((1 2) if-same)
-     ((1) if-same)
-     (() equal-same)))
-
-  (define-function list-length (xs)
-    (if (atom? xs)
-        '0
-        (+ '1 (list-length (cdr xs)))))
-
-  (define-proof list-length
-    (natural? (size xs))
-    ((() simple-list-induction)))
-
-  (define-theorem natural?/1 ()
-    (equal? (natural? 1) #t))
-
-  (define-proof natural?/1
-    ()
-    ((() if-same (set x (natural? '0)))
-     ((2 1) natural?/succ)
-     ((2) equal-same)
-     ((1) natural?/0)
-     (() if-true)))
-
-  (define-theorem natural?/list-length (xs)
-    (natural? (list-length xs)))
-
-  (define-proof natural?/list-length
-    (list-induction xs)
-    (((2 1) list-length)
-     ((2 1) if-nest-A)
-     ((2) natural?/0)
-     ((3 2 1) list-length)
-     ((3 2 1) if-nest-E)
-     ((3) if-same (set x (natural? (succ '0))))
-     ((3 2 2) natural?/+)
-     ((3 2) if-same)
-     ((3 1) natural?/1)
-     ((3) if-true)
-     (() if-same))))
+  )
-- 
cgit v1.2.3