From 99c01cbd393cb80a9555644370fb4550318fa901 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Sun, 29 Nov 2020 03:59:20 +0900
Subject: wip37

---
 vikalpa/prelude.scm | 51 +++++++++------------------------------------------
 1 file changed, 9 insertions(+), 42 deletions(-)

diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 1ee56af..9a25348 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -56,11 +56,10 @@
 
   (define-function natural? (x)
     (and (integer? x)
-         (or (equal? x 0)
+         (or (zero? x)
              (< x 0))))
 
   (define-totality-claim natural? natural? <)
-  
 
   (define-axiom equal-same (x)
     (equal? (equal? x x) '#t))
@@ -84,7 +83,7 @@
 
   (define-axiom if-same (x y)
     (equal? (if x y y) y))
-
+  
   (define-axiom if-not (x y z)
     (equal? (if (not x) y z)
             (if x z y)))
@@ -119,44 +118,15 @@
              (not (zero? x))
              (equal? (succ (pred x)) x)))
 
-  (define-theorem less-than/pred-1 (x)
-    (implies (not (zero? x))
-             (natural? x)
-             (natural? (pred x))
-             (not (zero? (pred x)))
-             (equal? (< (pred (pred x)) (pred x)) '#t)
-             (equal?
-              (if (zero? (pred x))
-                  '#t
-                  (< (pred (pred x)) (pred x)))
-              '#t)))
-  
-  (define-theorem if-implies (x y z w)
-    (equal? (if (if x y #t)
-                z
-                w)
-            (if x
-                (if y
-                    z
-                    w)
-                z)))
-
-  (define-theorem less-than/pred-2 (x)
-    (implies (not (natural? x))
-             (equal? (zero? x) #f)))
-
-  (define-primitive-function natural-induction (x)
-    (if (natural? x)
-        (if (zero? x)
-            0
-            (succ (natural-induction (pred x))))
-        #f))
-
-  (define-theorem less-than/pred (x)
+  (define-axiom less/pred (x)
     (implies (natural? x)
-             (not (zero? x))
              (equal? (< (pred x) x) #t)))
 
+  (define-function + (x y)
+    (if (zero? 0 x)
+        y
+        (succ (+ (pred x) y))))
+
   ;; (define-proof if-implies
   ;;   ()
   ;;   (((1) if-same (set x x))
@@ -189,10 +159,7 @@
   ;;    ;; ((2 2 3 1) if-false)
   ;;    ))
   
-  (define-function + (x y)
-    (if (equal? 0 x)
-        y
-        (succ (+ (pred x) y))))
+
 
   ;; (define-theorem natural/add1 (x)
   ;;     (implies (natural? x)
-- 
cgit v1.2.3