wip29

2 files changed, 315 insertions, 291 deletions

diff --git a/vikalpa.scm b/vikalpa.scm
index 74dbe6c..cc88c06 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -33,6 +33,7 @@
             define-primitive-function
             define-function
             define-proof
+            define-totality-claim
             define-syntax-rules
             total/natural?
             induction
@@ -214,77 +215,6 @@
               (environment (cdr x))))
         (else #f)))
 
-(define* (rebuild expr preconds
-                  #:key
-                  (quoted-proc (lambda (expr preconds) expr))
-                  (variable-proc (lambda (expr preconds) expr))
-                  (if-proc (lambda (expr preconds next) (next)))
-                  (app-form-proc (lambda (expr preconds next) (next))))
-  (let rec ((expr expr)
-            (preconds preconds))
-    (cond
-     ((expr-quoted? expr)
-      (quoted-proc expr preconds))
-     ((variable? expr)
-      (variable-proc expr preconds))
-     ((if-form? expr)
-      (letrec ((next
-                (lambda* (#:optional (expr expr))
-                  (let* ((expr/test (rec (if-form-test expr) preconds))
-                         (expr/then (rec (if-form-then expr) (cons (if-form-test expr) preconds)))
-                         (expr/else (rec (if-form-else expr) (cons (expr-not (if-form-test expr)) preconds))))
-                    (if-form expr/test expr/then expr/else)))))
-        (if-proc expr preconds next)))
-     ((app-form? expr)
-      (letrec ((next
-                (lambda* (#:optional (expr expr))
-                  (let f ((expr-args (app-form-args expr)))
-                    (cond ((null? expr-args) '())
-                          (else
-                           (cons (rec (car expr-args) preconds)
-                                 (f (cdr expr-args)))))))))
-        (app-form-proc expr preconds next)))
-     (else
-      (error "(vikalpa) rebuild: error")))))
-
-(define* (expr-fold expr acc preconds
-                    #:key
-                    (quoted-proc (lambda (expr acc preconds) acc))
-                    (variable-proc (lambda (expr acc preconds) acc))
-                    (if-proc (lambda (expr acc preconds next) (next)))
-                    (app-form-proc (lambda (expr acc preconds next) (next))))
-  (let rec ((expr expr)
-            (acc acc)
-            (preconds preconds))
-    (cond
-     ((expr-quoted? expr)
-      (quoted-proc expr acc preconds))
-     ((variable? expr)
-      (variable-proc expr acc preconds))
-     ((if-form? expr)
-      (letrec ((next
-                (lambda* (#:optional (expr expr) (acc acc) (preconds preconds))
-                  (let* ((acc/test
-                          (rec (if-form-test expr) acc preconds))
-                         (acc/then
-                          (rec (if-form-then expr) acc/test (cons (if-form-test expr) preconds))))
-                    (rec (if-form-else expr) acc/then (cons (expr-not (if-form-test expr)) preconds))))))
-        (if-proc expr acc preconds next)))
-     ((app-form? expr)
-      (letrec ((next
-                (lambda* (#:optional (expr expr) (acc acc) (preconds preconds))
-                  (let fold ((expr-args (app-form-args expr))
-                             (acc acc))
-                    (cond ((null? expr-args) acc)
-                          (else
-                           (fold (cdr expr-args)
-                                 (rec (car expr-args)
-                                      acc
-                                      preconds))))))))
-        (app-form-proc expr acc preconds next)))
-     (else
-      (error "(vikalpa) expr-fold: error")))))
-
 (define (substitute env expr)
   (cond ((expr-quoted? expr) expr)
         ((pair? expr)
@@ -390,13 +320,14 @@
 
 (define (system? x)
   (and (list? x)
-       (= 3 (length x))
+       (= 4 (length x))
        (eq? 'system (list-ref x 0))
        (system-definitions? (system-definitions x))
-       (system-proofs? (system-proofs x))))
+       (system-proofs? (system-proofs x))
+       ((const #t) (system-totality-claims x))))
 
-(define (make-system defs prfs)
-  (list 'system defs prfs))
+(define (make-system defs prfs totality-claims)
+  (list 'system defs prfs totality-claims))
 
 (define (system-definitions sys)
   (list-ref sys 1))
@@ -404,6 +335,21 @@
 (define (system-proofs sys)
   (list-ref sys 2))
 
+(define (system-totality-claims sys)
+  (list-ref sys 3))
+
+(define (totality-claim id nat? less-than)
+  (list id nat? less-than))
+
+(define (totality-claim-id x)
+  (list-ref x 0))
+
+(define (totality-claim-natural x)
+  (list-ref x 1))
+
+(define (totality-claim-less-than x)
+  (list-ref x 2))
+
 (define (lookup x sys)
   (assoc x (system-definitions sys)))
 
@@ -462,7 +408,7 @@
 (define/guard (function (name variable?)
                         (vars vars?)
                         (expr expression?)
-                        (code any?)
+                        (code (const #t))
                         (primitive boolean?))
   (list name 'function vars expr code primitive))
 
@@ -599,7 +545,7 @@
               (eq? (macro-name m) (car expr)))
          (let loop ((rs (macro-mrules m)))
            (cond ((null? rs)
-                  (error "macro fail" m expr))
+                  (error "(vikalpa) macro fail" m expr))
                  ((apply-mrule (car rs) (macro-literals m) expr) => identity)
                  (else (loop (cdr rs))))))
         (else #f)))
@@ -827,9 +773,10 @@
               (values extracted-expr
                       (case i
                         ((1) '())
-                        ((2) (cons precond extracted-preconds))
-                        ((3) (cons (expr-not precond) extracted-preconds))
-                        (else (fail "(if) invaild path" path)))
+                        ((2) (cons (prop-not (prop-not precond))
+                                   extracted-preconds))
+                        ((3) (cons (prop-not precond) extracted-preconds))
+                        (else (fail 'if-invaild-path path)))
                       (lambda (x)
                         (append (list-head expr i)
                                 (list (builder x))
@@ -844,7 +791,7 @@
                               (list (builder x))
                               (list-tail expr (+ i 1)))))))
          (else
-          (fail "invalid path" path))))))
+          (fail 'invalid-path path))))))
 
 (define (function->rules x)
   (list (rule (function-vars x)
@@ -865,27 +812,27 @@
               (cons (function-name f) args)
               '()))
 
-(define (parse-options/theorem ops)
+(define (parse-options/theorem ops fail)
   (if (null? ops)
       (values '())
       (receive (env)
-          (parse-options/theorem (cdr ops))
+          (parse-options/theorem (cdr ops) fail)
         (case (caar ops)
           ((set) (let ((op (car ops)))
                    (cons (cons (list-ref op 1)
                                (list-ref op 2))
                          env)))
           (else
-           (error "invalid option:" (car ops)))))))
+           (fail 'invalid-option (car ops)))))))
 
 (define (rewrite/theorem cmd b thm preconds expr fail)
   (receive (env)
-      (parse-options/theorem (command-options cmd))
+      (parse-options/theorem (command-options cmd) fail)
     (cond
      ((any (cut apply-rule preconds <> expr env)
            (theorem*-rules thm)) => identity)
      (else
-      (fail (format #f "no match theorem ~a: ~s" cmd expr))))))
+      (fail 'apply-theorem cmd expr)))))
 
 ;; (rewrite system? rewriter? expression? procedure?) -> expr
 (define (rewrite1 sys expr fail r)
@@ -901,7 +848,8 @@
            (('equal? `(quote ,x) `(quote ,y))
             (expr-quote (equal? x y)))
            (else
-            (fail "error: equal? ~a" extracted-expr))))
+            (fail 'equal? 'extracted-expr))))
+        ((eq? 'error cmd/name) (fail extracted-expr))
         ((and (symbol? cmd/name)
               (lookup cmd/name sys))
          => (lambda (x)
@@ -913,10 +861,10 @@
                  ((any (cut apply-rule '() <> extracted-expr '())
                        (function->rules x)) => identity)
                  (else
-                  (fail (format #f "no match-function (~a)" cmd)))))
+                  (fail 'apply-function cmd extracted-expr))))
                (else
-                (fail "rewrite error" cmd)))))
-        (else (fail "no cmd" cmd extracted-expr)))))))
+                (fail 'invalid-command cmd extracted-expr)))))
+        (else (fail 'command-not-found cmd extracted-expr)))))))
 
 (define/guard (rewrite (sys system?) (expr expression?) (seq sequence?))
   (debug "rewrite ~y~%" expr)
@@ -924,20 +872,25 @@
              (seq seq))
     (debug "~y~%" expr)
     #;(format #t "~y~%" expr)
-    (if (null? seq)
-        expr
-        (loop (rewrite1 sys
-                        expr
-                        (lambda (x . args)
-                          (apply error
-                                 (format #f "rewrite: ~a" x)
-                                 args))
-                        (car seq))
-              (cdr seq)))))
+    (reset
+     (if (null? seq)
+         expr
+         (loop (rewrite1 sys
+                         expr
+                         (lambda args
+                           (shift k (cons 'error args)))
+                         (car seq))
+               (cdr seq))))))
 
 (define (expr-not x)
   (list 'not x))
 
+(define (prop-not x)
+  (match x
+    (('not ('not expr)) (prop-not expr))
+    (('not expr) expr)
+    (expr (expr-not expr))))
+
 (define (expr-equal? x)
   (and (list? x)
        (= 3 (length x))
@@ -954,10 +907,14 @@
 (define (expression->rules vars preconds expr)
   (if (if-form? expr)
       (append (expression->rules vars
-                                 (cons (if-form-test expr) preconds)
+                                 (cons (prop-not
+                                        (prop-not
+                                         (if-form-test expr)))
+                                       preconds)
                                  (if-form-then expr))
               (expression->rules vars
-                                 (cons (expr-not (if-form-test expr)) preconds)
+                                 (cons (prop-not (if-form-test expr))
+                                       preconds)
                                  (if-form-else expr)))
       (if (expr-equal? expr)
           (list (rule vars
@@ -975,18 +932,20 @@
                      '()
                      (theorem*-expression def)))
 
-(define current-system (make-parameter (make-system '() '())))
+(define current-system (make-parameter (make-system '() '() '())))
 
 (define (add-definition x)
   (let ((sys (current-system)))
     (current-system
-     (cond ((lookup (theorem*-name x) sys)
-            => (lambda (thm)
-                 (if (equal? x thm)
-                     sys
-                     (error "add-definition: error"))))
+     (cond ((lookup (definition-name x) sys)
+            => (lambda (d)
+                 (if (equal? x d)
+                     x
+                     (error "(vikalpa) add-definition: duplicated"
+                            (definition-name d)))))
            (else (make-system (cons x (system-definitions sys))
-                              (system-proofs sys)))))
+                              (system-proofs sys)
+                              (system-totality-claims sys)))))
     x))
 
 (define (add-proof x)
@@ -996,12 +955,13 @@
             => (lambda (prf)
                  (if (equal? x prf)
                      sys
-                     (error "add-proof: error"))))
+                     (error "add-proof: duplicated"))))
            (else (make-system (system-definitions sys)
-                              (cons x (system-proofs sys))))))
+                              (cons x (system-proofs sys))
+                              (system-totality-claims sys)))))
     x))
 
-(define reserved-symbols '(quote let if))
+(define reserved-symbols '(quote let if error))
 (define (reserved? x)
   (member x reserved-symbols))
 
@@ -1059,63 +1019,52 @@
        (add-definition m)
        m))))
 
-(define (size x)
-  (if (pair? x)
-      (+ 1
-         (size (car x))
-         (size (cdr x)))
-      0))
-(define (add1 n) (1+ n))
-(define (sub1 n) (1- n))
-
-(define (core-primitive-function)
-  (list (primitive-function 'not '(x))
-        (primitive-function 'equal? '(x y))
-        (primitive-function 'pair? '(x))
-        (primitive-function 'cons '(x y))
-        (primitive-function 'car '(x))
-        (primitive-function 'cdr '(x))
-        (primitive-function 'size '(x))
-        (primitive-function 'natural? '(x))
-        (primitive-function 'add1 '(x))
-        (primitive-function 'sub1 '(x))
-        (primitive-function '< '(x y))))
-
-(define* (empty-system #:optional (parent (make-system '() '())))
+(define (find-totality-claim name sys)
+  (assoc name (system-totality-claims sys)))
+
+(define (add-totality-claim tc)
+  (let ((sys (current-system)))
+    (cond ((find-totality-claim (totality-claim-id tc) sys)
+           => (lambda (tc2)
+                (unless (equal? tc tc2)
+                  (error "(vikalpa) define-totality-claim: duplicated"
+                         tc)))))
+    (unless (and (symbol? (totality-claim-id tc))
+                 (cond ((lookup (totality-claim-natural tc) sys)
+                        => function*?)
+                       (else #f))
+                 (cond ((lookup (totality-claim-less-than tc) sys)
+                        => function*?)
+                       (else #f)))
+      (error "(vikalpa) define-totality-claim: invalid totality-claim"
+             tc))
+    (current-system
+     (make-system (system-definitions sys)
+                  (system-proofs sys)
+                  (cons tc (system-totality-claims sys))))
+    tc))
+
+(define-syntax-rule (define-totality-claim name nat? <)
+  (add-totality-claim (totality-claim 'name 'nat? '<)))
+
+(define* (core-system #:optional (parent (make-system '() '() '())))
   (parameterize ([current-system parent])
     (define-primitive-function not (x))
     (define-primitive-function equal? (x y))
-    (define-primitive-function pair? (x))
-    (define-primitive-function cons (x y))
-    (define-primitive-function car (x))
-    (define-primitive-function cdr (x))
-    (define-primitive-function size (x))
-    (define-primitive-function natural? (x))
-    (define-primitive-function add1 (x))
-    (define-primitive-function sub1 (x))
-    (define-primitive-function < (x y))
-    (unless (system? (current-system))
-      (error "define-system: error"))
     (current-system)))
 
 (define-syntax define-system
   (syntax-rules ()
     ((_ name (systems ...) expr ...)
-     (define* (name #:optional (parent (make-system '() '())))
+     (define* (name #:optional (parent (make-system '() '() '())))
        (parameterize ([current-system
-                       ((compose systems ... empty-system) parent)])
+                       ((compose systems ... core-system) parent)])
          expr
          ...
          (unless (system? (current-system))
-           (error "define-system: error"))
+           (error "define-system: invalid system"))
          (current-system))))))
 
-
-(define (atom? x)
-  (not (pair? x)))
-
-(define (any? x) #t)
-
 (define (measure? x)
   (and (pair? x)
        (variable? (car x))
@@ -1131,9 +1080,6 @@
 (define (function-app-form f)
   (cons (function-name f) (function-vars f)))
 
-(define (expand-all b expr)
-  (expand* (filter macro? b) expr))
-
 (define (single? x)
   (and (pair? x)
        (null? (cdr x))))
@@ -1164,7 +1110,7 @@
    (else
     (if/if x y ''#t))))
 
-(define (make-total-claim/natural m-expr f)
+(define (make-totality-claim tc m-expr f)
   (let* ((name (function-name f)))
     (define (convert app-form)
       (cond
@@ -1176,9 +1122,11 @@
                     app-form
                     '())
         => identity)
-       (else (error "make-total-claim/natural: convert error"
+       (else (error "make-totality-claim: convert error"
+                    (function-name f)
+                    m-expr
                     app-form))))
-    (if/if `(natural? ,m-expr)
+    (if/if `(,(totality-claim-natural tc) ,m-expr)
            (let loop ((expr (function-expression f)))
              (cond
               ((expr-quoted? expr) ''#t)
@@ -1199,10 +1147,14 @@
                               (else (and/if (loop (car args))
                                             (f (cdr args))))))))
                  (if (eq? name (app-form-name expr))
-                     (and/if `(< ,(convert expr) ,m-expr)
+                     (and/if `(,(totality-claim-less-than tc)
+                               ,(convert expr)
+                               ,m-expr)
                              rest)
                      rest)))
-              (else (error "(vikalpa) make-total-claim: error"))))
+              (else (error "(vikalpa) make-totality-claim: error"
+                           (function-name f)
+                           m-expr))))
            ''#t)))
 
 (define/guard (make-induction-claim (f function*?)
@@ -1216,13 +1168,14 @@
             (cons expr rest)
             rest)))
      ((if-form? expr)
-      (error "make-induction-claim: FAILED m(- -)m"))
+      (error "make-induction-claim(find-app-forms): not supported"
+             expr))
      (else '())))
   (let ((c (theorem*-expression t)))
     (define (prop app-form)
       (cond
        ((apply-rule '()
-                    (rule (function-vars f)
+                    (rule vars
                           '()
                           (cons (function-name f) vars)
                           c)
@@ -1230,7 +1183,7 @@
                     '())
         => identity)
        (else
-        (error "make-induction-claim: fail"))))
+        (error "make-induction-claim: fail" app-form))))
     (cond
      ((apply-function f vars)
       => (lambda (expr)
@@ -1273,24 +1226,12 @@
 (define seed? (const #t))
 
 (define-syntax define-proof
-  (syntax-rules (total natural? induction)
-    ((_ name
-        (total/natural? m-expr)
-        (((n ...) cmd ...) ...))
-     (add-proof (proof 'name
-                       '(total/natural? m-expr)
-                       '(((n ...) cmd ...) ...))))
-    ((_ name
-        (induction (f var ...))
-        (((n ...) cmd ...) ...))
-     (add-proof (proof 'name
-                       '(induction (f var ...))
-                       '(((n ...) cmd ...) ...))))
+  (syntax-rules ()
     ((_ name
-        ()
+        (seed ...)
         (((n ...) cmd ...) ...))
      (add-proof (proof 'name
-                       '()
+                       '(seed ...)
                        '(((n ...) cmd ...) ...))))))
 
 (define (function*? x)
@@ -1337,12 +1278,18 @@
 
 (define (prove/theorem sys t pf)
   (match (proof-seed pf)
-    (('induction (f . vars))
-     (rewrite sys
-              (make-induction-claim (lookup f sys)
-                                    vars
-                                    t)
-              (proof-sequence pf)))
+    ((f . vars)
+     (cond
+      ((lookup f sys)
+       => (lambda (seed)
+            (rewrite sys
+                     (make-induction-claim seed
+                                           vars
+                                           t)
+                     (proof-sequence pf))))
+      (else (error "(vikalpa) define-proof: induction function is not found."
+                   (proof-name pf)
+                   (cons f vars)))))
     (()
      (rewrite sys
               (theorem*-expression t)
@@ -1352,12 +1299,20 @@
 
 (define (prove/function sys f pf)
   (match (proof-seed pf)
-    (('total/natural? m-expr)
-     (rewrite sys
-              (make-total-claim/natural m-expr f)
-              (proof-sequence pf)))
+    ((id m-expr)
+     (cond
+      ((find-totality-claim id sys)
+       => (lambda (tc)
+            (rewrite sys
+                     (make-totality-claim tc m-expr f)
+                     (proof-sequence pf))))
+      (else
+       (error "(vikalpa) define-proof: totality-claim is not found:"
+              (proof-name pf)
+              (proof-seed pf)))))
     (else
-     (error "prove/function: fail"))))
+     (error "define-proof: fail"
+            (proof-name pf) (proof-seed pf)))))
 
 (define (system->scheme sys)
   `(begin
@@ -1375,7 +1330,8 @@
     (let ((defs (system-definitions sys)))
       (define* (next #:optional fail)
         (loop (make-system (cdr defs)
-                           (system-proofs sys))
+                           (system-proofs sys)
+                           (system-totality-claims sys))
               (if fail
                   (cons fail fails)
                   fails)))
@@ -1383,12 +1339,9 @@
        ((null? defs) fails)
        ((or (theorem? (car defs))
             (function? (car defs)))
-        (cond
+       (cond
          ((and (function? (car defs))
                (trivial-total? (car defs)))
-          #;
-          (format #t "`~a` is trivial total function.~%"
-                  (definition-name (car defs)))
           (next))
          (else
           (cond
@@ -1397,61 +1350,44 @@
                  (let ((result (prove sys (car defs) pf)))
                    (cond
                     ((equal? result ''#t)
-                     #;
-                     (format #t "`~a` is ~a.~%"
-                             (definition-name (car defs))
-                             (if (function? (car defs))
-                                 "total function"
-                                 "true"))
                      (next))
                     (else
-                     #;
-                     (format #t "`~a`'s proof is failed:~%~y"
-                             (definition-name (car defs))
-                             result)
                      (next (list (definition-name (car defs))
                                  result)))))))
            (else
-            #;
-            (format #t "`~a`'s proof is not found.~%"
-                    (definition-name (car defs)))
             (next (list (definition-name (car defs)))))))))
        (else
         (next))))))
 
+(define (pp x)
+  (pretty-print x
+                #:width 79
+                #:max-expr-width 50))
+
 (define/guard (show (sys system?) (name symbol?))
-  (define (pp x)
-    (pretty-print x
-                  #:width 79
-                  #:max-expr-width 50))
   (cond
    ((lookup name sys)
     => (lambda (def)
          (cond
           ((function? def)
-           (pp
-            `(define-function ,(function-name def) ,(function-vars def)
-               ,(function-expression def))))
+           `(define-function ,(function-name def) ,(function-vars def)
+              ,(function-expression def)))
           ((theorem? def)
-           (pp
-            `(define-theorem ,(theorem*-name def) ,(theorem*-vars def)
-               ,(theorem*-expression def))))
+           `(define-theorem ,(theorem*-name def) ,(theorem*-vars def)
+              ,(theorem*-expression def)))
           ((axiom? def)
-           (pp
-            `(define-axiom ,(theorem*-name def) ,(theorem*-vars def)
-               ,(theorem*-expression def))))
+           `(define-axiom ,(theorem*-name def) ,(theorem*-vars def)
+              ,(theorem*-expression def)))
           ((primitive-function? def)
-           (pp
-            `(define-primitive-function
-               ,(primitive-function-name def)
-               ,(primitive-function-vars def))))
+           `(define-primitive-function
+              ,(primitive-function-name def)
+              ,(primitive-function-vars def)))
           ((macro? def)
-           (pp
-            `(define-syntax-rules ,(macro-name def))))
+           `(define-syntax-rules ,(macro-name def)))
           (else
-           (error "show: error")))))
+           `(error 'fatal-error ,name)))))
    (else
-    (format #t "~a: not found~%" name))))
+    `(error 'not-found ,name))))
 
 (define/guard (load-system (sys system?))
   (primitive-eval (system->scheme sys)))
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 8816131..c55ea48 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -17,23 +17,9 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa prelude)
-  #:export (atom? size implies natural? prelude)
+  #:export (implies prelude)
   #:use-module (vikalpa))
 
-(define (atom? x)
-  (not (pair? x)))
-
-(define (natural? x)
-  (and (integer? x)
-       (not (negative? x))))
-
-(define (size x)
-  (if (pair? x)
-      (+ 1
-         (size (car x))
-         (size (cdr x)))
-      0))
-
 (define-syntax implies
   (syntax-rules ()
     ((_ x y) (if x y #t))
@@ -41,8 +27,16 @@
      (if x (implies y z rest ...) #t))))
 
 (define-system prelude ()
-  (define-function atom? (x)
-    (not (pair? x)))
+  (define-primitive-function pair? (x y))
+  (define-primitive-function cons (x y))
+  (define-primitive-function car (x))
+  (define-primitive-function cdr (x))
+  (define-primitive-function sub1 (x))
+  (define-primitive-function add1 (x))
+  (define-primitive-function < (x y))
+  (define-primitive-function natural? (x))
+  (define-totality-claim natural? natural? <)
+
   (define-syntax-rules list ()
     ((list) '())
     ((list x . y) (cons x (list . y))))
@@ -62,23 +56,23 @@
     ((implies x y) (if x y #t))
     ((implies x y z . rest)
      (if x (implies y z . rest) #t)))
-
+  
   (define-axiom equal-same (x)
     (equal? (equal? x x) '#t))
   (define-axiom equal-swap (x y)
     (equal? (equal? x y) (equal? y x)))
   (define-axiom equal-if (x y)
     (implies (equal? x y) (equal? x y)))
-  (define-axiom atom/cons (x y)
-    (equal? (atom? (cons x y)) '#f))
+  (define-axiom pair/cons (x y)
+    (equal? (pair? (cons x y)) '#t))
   (define-axiom car/cons (x y)
     (equal? (car (cons x y)) x))
   (define-axiom cdr/cons (x y)
     (equal? (cdr (cons x y)) y))
   (define-axiom cons/car+cdr (x)
-    (if (atom? x)
-        '#t
-        (equal? (cons (car x) (cdr x)) x)))
+    (if (pair? x)
+        (equal? (cons (car x) (cdr x)) x)
+        '#t))
   (define-axiom if-nest (x y z)
     (if x
         (equal? (if x y z) y)
@@ -89,65 +83,153 @@
     (equal? (if '#f x y) y))
   (define-axiom if-same (x y)
     (equal? (if x y y) y))
-  (define-axiom natural?/size (x)
-    (equal? (natural? (size x))
-            '#t))
-  (define-axiom </size/car (x)
-    (if (atom? x)
-        '#t
-        (equal? (< (size (car x)) (size x))
-                '#t)))
-  (define-axiom </size/cdr (x)
-    (if (atom? x)
-        '#t
-        (equal? (< (size (cdr x)) (size x))
-                '#t)))
   (define-axiom if-not (x y z)
     (equal? (if (not x) y z)
             (if x z y)))
+
+  (define-axiom axiom-less-than (x y)
+    (implies (natural? x)
+             (natural? y)
+             (equal? (< x y)
+                     (if (equal? '0 x)
+                         (if (equal? '0 y)
+                             #f
+                             #t)
+                         (if (equal? '0 y)
+                             #f
+                             (< (sub1 x) (sub1 y)))))))
+  (define-function natural-induction (n)
+    (if (natural? n)
+        (if (equal? '0 n)
+            '0
+            (add1 (natural-induction (sub1 n))))
+        'undefined))
+
+  (define-proof natural-induction
+    (natural? n)
+    ())
+
+  (define-axiom false-if (x)
+    (if x #t (equal? #f x)))
+  
   (define-axiom sub1/add1 (x)
     (implies (natural? x)
              (equal? (sub1 (add1 x)) x)))
-  (define-axiom natural?/0 (x)
+
+  (define-axiom natural/zero ()
     (equal? (natural? '0) '#t))
-  (define-axiom natural?/add1 (x)
-    (implies (natural? x)
-             (equal? (natural? (add1 x)) '#t)))
-  (define-axiom sub1/add1 (x)
+
+  (define-axiom not/true ()
+    (equal? (not #t) #f))
+
+  (define-axiom not/false ()
+    (equal? (not #f) #t))
+
+  (define-theorem equal/zero-less-than (x)
     (implies (natural? x)
-             (equal? (sub1 (add1 x)) x)))
-  (define-axiom </sub1 (x)
+             (equal? (not (< '0 x))
+                     (equal? x '0))))
+
+  (define-proof equal/zero-less-than
+    (natural-induction x)
+    (((2 2) if-nest)
+     ((3) if-nest)
+     ((2 2 1) if-same (set x (natural? '0)))
+     ((2 2 1 2 1) axiom-less-than)
+     ((2 2 1 1) natural/zero)
+     ((2 2 1) if-true)
+     ((2 2 1 1 1) equal-same)
+     ((2 2 1 1) if-true)
+     ((2 2 1 1 1 2) equal-if)
+     ((2 2 1 1 1) equal-same)
+     ((2 2 1 1) if-true)
+     ((2 2 1) not/false)
+     ((2 2 2 1) equal-if)
+     ((2 2 2) equal-same)
+     ((2 2) equal-same)
+     ((2 3 2 2) if-same (set x (natural? '0)))
+     ((2 3 2 2 2 1 1) axiom-less-than)
+     ((2 3 2 2 2 1 1 1) equal-same)
+     ((2 3 2 2 2 1 1) if-true)
+     ((2 3 2 2 2 1 1) if-nest)
+     ((2 3 2 2 2 1) not/true)
+     ((2 3 2 2 2 2) equal-swap)
+     ((2 3 2 2 2 2) false-if)
+     ((2 3 2 2 2) equal-same)
+     ((2 3 2 2 1) natural/zero)
+     ((2 3 2 2) if-true)
+     ((2 3 2) if-same)
+     ((2 3) if-same)
+     ((2) if-same)
+     (() if-same)))
+  
+  (define-axiom natural/sub1 (x)
     (implies (natural? x)
-             (equal? (< (sub1 x) x) '#t)))
-  (define-theorem common-add1 (x y)
+             (if (equal? '0 x)
+                 '#t
+                 (equal? (natural? (sub1 x)) #t))))
+  
+;; (define-proof natural-induction
+;;     (total/natural? n)
+;;     (((2) if-nest)
+;;      ((2 3) </sub1)
+;;      ((2) if-same)
+;;      (() if-same)))
+
+(define-theorem natural/add1 (x)
     (implies (natural? x)
-             (natural? y)
-             (equal? (equal? (add1 x) (add1 y))
-                     (equal? x y))))
-  (define-axiom false-if (x)
-    (if x '#t (equal? x '#f)))
-  (define-axiom equal?/01 (x)
-    (equal? (equal? '0 '1) #f))
-  (define-axiom natural?/sub1 (x)
+             (equal? (natural? (add1 x)) #t)))
+
+  #;
+  (define-axiom natural/sub1 (x)
     (if (natural? x)
-        (if (equal? '0 x)
-            '#t
-            (equal? (natural? (sub1 x)) '#t))
+        (if (< '0 x)
+            (equal? (natural? (sub1 x)) '#t)
+            '#t)
         '#t))
+
+  #;
+  (define-theorem less-than/sub1 (x)
+    (implies (natural? x)
+             (< '0 x)
+             (equal? (< (sub1 x) x) '#t)))
+
+  #;
   (define-axiom add1/sub1 (x)
     (if (natural? x)
         (if (equal? '0 x)
             '#t
             (equal? (add1 (sub1 x)) x))
         '#t))
-  
+
+  #;
   (define-primitive-function + (x y)
     (if (natural? x)
         (if (equal? '0 x)
             y
             (add1 (+ (sub1 x) y)))
         'undefined))
+  
+  #;
+  (define-axiom natural/size (x)
+    (equal? (natural? (size x))
+            '#t))
 
+  #;
+  (define-axiom size/car (x)
+    (if (pair? x)
+        (equal? (< (size (car x)) (size x))
+                '#t)
+        '#t))
+
+  #;
+  (define-axiom size/cdr (x)
+    (if (pair? x)
+        (equal? (< (size (cdr x)) (size x))
+                '#t)
+        '#t))
+  
+  #;
   (define-proof +
     (total/natural? x)
     (((2) if-nest)
@@ -155,9 +237,11 @@
      ((2) if-same)
      (() if-same)))
 
+  #;
   (define-theorem thm-1+1=2 ()
     (equal? (+ 1 1) 2))
-  
+
+  #;
   (define-function natural-induction (n)
     (if (natural? n)
         (if (equal? '0 n)
@@ -165,6 +249,7 @@
             (add1 (natural-induction (sub1 n))))
         'undefined))
 
+  #;
   (define-proof natural-induction
     (total/natural? n)
     (((2) if-nest)
@@ -172,11 +257,13 @@
      ((2) if-same)
      (() if-same)))
 
+  #;
   (define-theorem equal?/add1 (n)
     (if (natural? n)
         (equal? (equal? n (add1 n)) #f)
         #t))
-  
+
+  #;
   (define-proof equal?/add1
     (induction (natural-induction n))
     (((2 2 2 1 1) equal-if)
@@ -205,7 +292,8 @@
      ((2) if-same)
      ((3) if-nest)
      (() if-same)))
-  
+
+  #;
   (define-proof thm-1+1=2
     ()
     ((() if-same (set x (natural? '0)))