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 +--------
 vikalpa.scm                    | 242 +++++++++++++++++++++++------------------
 vikalpa/prelude.scm            | 220 +++++++++++++++++++++----------------
 vikalpa/the-little-prover.scm  | 104 +++++++++++-------
 4 files changed, 328 insertions(+), 288 deletions(-)

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))))
+  )
diff --git a/vikalpa.scm b/vikalpa.scm
index ab87b7d..40b4bf1 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -17,19 +17,23 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa)
-  #:export (rewrite
-            describe
-            system?
+  #:export (system?
+            system-rewrite
             system-check
             system-apropos
             system-code
             system-load
+            system-eval
+            system-lookup
             set-measure-predicate
             set-measure-less-than
             define-system
             define-proof
             define-core-function
             define-function
+            define-trivial-total-function
+            define-syntax-rules
+            define-axiom
             define-theorem)
   #:use-module (ice-9 match)
   #:use-module (ice-9 format)
@@ -37,7 +41,8 @@
   #:use-module (ice-9 exceptions)
   #:use-module (ice-9 regex)
   #:use-module ((srfi srfi-1)
-                #:select (every any lset-union fold append-map find))
+                #:select (every any lset-union fold append-map find
+                                filter-map))
   #:use-module (srfi srfi-8)
   #:use-module (srfi srfi-11)
   #:use-module (srfi srfi-26)
@@ -216,28 +221,6 @@
     ...
     b b* ...))
 
-(define-syntax define-type
-  (syntax-rules ()
-    ((_ name
-        constractor
-        (m p?)
-        (n t? getter-var getter) ...)
-     (begin
-       (define (constractor getter-var ...)
-         (let ((data (make-list (+ 1 (length (list t? ...))))))
-           (list-set! data m 'name)
-           (list-set! data n getter-var)
-           ...
-           data))
-       (define (p? x)
-         (and (list? x)
-              (= (+ 1 (length (list t? ...))) (length x))
-              (eq? 'name (list-ref x m))
-              (t? (list-ref x n)) ...))
-       (define (getter x)
-         (list-ref x n))
-       ...))))
-
 ;; (natural? x) -> boolean?
 (define (natural? x)
   (and (exact-integer? x)
@@ -367,25 +350,21 @@
 (define (variable=? v1 v2)
   (eq? v1 v2))
 
-(define-type rule
-  rule
-  (0 rule?)
-  (1 (lambda (vars)
-       (and (list? vars)
-            (every variable? vars)))
-     vars
-     rule-vars)
-  (2 (lambda (ps)
-       (and (list? ps)
-            (every expression? ps)))
-     ps
-     rule-preconds)
-  (3 expression?
-     lhs
-     rule-lhs)
-  (4 expression?
-     rhs
-     rule-rhs))
+(define-class <rule> ()
+  (vars #:getter rule-vars #:init-keyword #:vars)
+  (preconds #:getter rule-preconds #:init-keyword #:preconds)
+  (lhs #:getter rule-lhs #:init-keyword #:lhs)
+  (rhs #:getter rule-rhs #:init-keyword #:rhs))
+
+(define (rule var preconds lhs rhs)
+  (make <rule>
+    #:vars var
+    #:preconds preconds
+    #:lhs lhs
+    #:rhs rhs))
+
+(define (rule? x)
+  (is-a? x <rule>))
 
 (define (binding? x)
   (and (pair? x)
@@ -689,19 +668,26 @@
                      '()
                      (get-expression x)))
 
+(define (error? x)
+  (and (pair? x)
+       (eq? 'error (car x))))
+
 (define (rewrite/eval expr sys)
   (let eval ((expr expr))
     (cond
+     ((error? expr) expr)
      ((expr-quoted? expr) expr)
      ((app-form? expr)
       (let ((args (map eval (app-form-args expr)))
             (name (app-form-name expr)))
-        (or (find error? args)
-            (eval (rewrite1 sys
-                            `(,name ,@args)
-                            (lambda args
-                              (cons* 'error 'rewrite name args))
-                            (rewriter '() `(,name)))))))
+        (cond
+         ((find error? args) => identity)
+         (else
+          (eval (rewrite1 sys
+                          `(,name ,@args)
+                          (lambda args
+                            (cons* 'error 'rewrite name args))
+                          (rewriter '() `(,name))))))))
      ((if-form? expr)
       (let ((test (eval (if-form-test expr))))
         (if (error? test)
@@ -709,6 +695,8 @@
             (if (expr-unquote test)
                 (eval (if-form-then expr))
                 (eval (if-form-else expr))))))
+     ((variable? expr)
+      `(error eval variable-found ,expr))
      (else
       `(error eval invalid-expression ,expr)))))
 
@@ -765,7 +753,7 @@
 (define (command-options x)
   (cdr x))
 
-(define/guard (system-eval (expr (const #t)) (sys (cut is-a? <> <system>)))
+(define/guard (system-eval (sys system?) (expr (const #t)))
   (rewrite/eval (parameterize ((current-system sys))
                   (convert-to-expression expr))
                 sys))
@@ -851,6 +839,16 @@
     => (cut make-induction-claim <> vars expr))
    (else (fail 'induction 'not-found fname))))
 
+(define (rewrite/core-function sys f expr fail)
+  (if (and (app-form? expr)
+           (eq? (get-name f) (app-form-name expr))
+           (= (length (get-variables f)) (length (app-form-args expr)))
+           (every expr-quoted? (app-form-args expr)))
+      (let ((result (apply (get-procedure f)
+                           (map expr-unquote (app-form-args expr)))))
+        (expr-quote result))
+      (fail 'apply-core-function (get-name f) expr)))
+
 (define (rewrite1 sys expr fail r)
   (let* ((cmd (rewriter-command r))
          (cmd/name (command-name cmd)))
@@ -860,11 +858,16 @@
       (builder
        (cond
         ((equal? '(eval) cmd/name)
-         (rewrite/eval extracted-expr sys))
+         (let ((result (rewrite/eval extracted-expr sys)))
+           (if (error? result)
+               (fail 'eval (cddr result) extracted-expr)
+               result)))
         ((and (symbol? cmd/name)
               (lookup cmd/name sys))
          => (lambda (x)
               (cond
+               ((is-a? x <core-function>)
+                (rewrite/core-function sys x extracted-expr fail))
                ((is-a? x <theorem*>)
                 (rewrite/theorem cmd sys x preconds extracted-expr fail))
                ((is-a? x <expandable-function>)
@@ -878,19 +881,18 @@
                 (fail 'invalid-command cmd extracted-expr)))))
         (else (fail 'command-not-found cmd extracted-expr)))))))
 
-(define/guard (rewrite (sys (cut is-a? <> <system>)) (expr (const #t)) (seq (const #t)))
-  (let ((expr (convert-to-expression expr)))
-    (let loop ((expr expr)
-               (seq seq))
-      (reset
-       (if (null? seq)
-           expr
-           (loop (rewrite1 sys
-                           expr
-                           (lambda args
-                             (shift k (cons 'error args)))
-                           (car seq))
-                 (cdr seq)))))))
+(define (rewrite sys expr seq)
+  (let loop ((expr expr)
+             (seq 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))
@@ -974,11 +976,11 @@
 
 (define-syntax define-core-function
   (syntax-rules ()
-    ((_ name (var ...) precond ... proc)
+    ((_ name (var ...) proc)
      (let ((f (make <core-function>
                 #:name 'name
                 #:variables '(var ...)
-                #:conditions '(precond ...)
+                #:conditions '()
                 #:procedure proc)))
        (current-system (add-definition f (current-system)))
        (validate f)
@@ -1033,6 +1035,12 @@
   (syntax-rules ()
     ((_ name (systems ...) expr ...)
      (define* (name #:optional (parent (core-system)))
+       (when (member 'name (list 'systems ...))
+         (raise-exception
+          (make-exception
+           (make-exception-with-origin 'name)
+           (make-exception-with-message "recursive system")
+           (make-exception-with-irritants '(systems ...)))))
        (parameterize ((current-system
                        ((compose systems ... identity) parent)))
          expr
@@ -1432,24 +1440,59 @@
   (when (dup? vars)
     (err)))
 
+(define-method (get-type (s <axiom>)) 'axiom)
+(define-method (get-type (s <theorem>)) 'theorem)
+(define-method (get-type (s <conjecture>)) 'conjecture)
+(define-method (get-type (s <core-function>)) 'core-function)
+(define-method (get-type (s <function>)) 'function)
+(define-method (get-type (s <total-function>)) 'total-function)
+(define-method (get-type (s <trivial-total-function>)) 'trivial-total-function)
+(define-method (get-type (s <macro>)) 'macro)
+
+(define-method (show (d <macro>))
+  (list (get-type d)))
+(define-method (show (d <theorem*>))
+  (list (get-type d)
+        (get-variables d)
+        (get-expression d)))
+(define-method (show (d <core-function>))
+  (list (get-type d)
+        (get-variables d)))
+(define-method (show (d <expandable-function>))
+  (list (get-type d)
+        (get-variables d)
+        (get-expression d)))
 
 (define/guard (system-apropos (sys system?) (str string?))
-  (filter (lambda (name)
-            (string-match (string-append ".*"
-                                         (regexp-quote str)
-                                         ".*")
-                          (symbol->string name)))
-          (map get-name (get-definitions sys))))
-
-(define/guard (system-code (sys system?))
+  (filter-map (lambda (d)
+                (if (string-match (string-append ".*"
+                                                 (regexp-quote str)
+                                                 ".*")
+                                  (symbol->string (get-name d)))
+                    (list (get-name d) (show d))
+                    #f))
+              (get-definitions sys)))
+
+(define (system-code/definition d)
+  (and (is-a? d <expandable-function>)
+       (get-code d)
+       `(define (,(get-name d) ,@(get-variables d))
+          ,(code-expr (get-code d)))))
+
+(define/guard (system-code/name (sys system?) (name symbol?))
+  (cond
+   ((lookup name sys) => system-code/definition)
+   (else #f)))
+
+(define/guard (system-code/all (sys system?))
   `(begin
-     ,@(map (lambda (f)
-              `(define (,(get-name f) ,@(get-variables f))
-                 ,(code-expr (get-code f))))
-            (reverse (filter (lambda (x)
-                               (and (is-a? x <expandable-function>)
-                                    (get-code x)))
-                             (get-definitions sys))))))
+     ,@(filter-map system-code/definition
+                   (reverse (get-definitions sys)))))
+
+(define* (system-code sys #:optional (name #f))
+  (if name
+      (system-code/name sys name)
+      (system-code/all sys)))
 
 (define (system-check sys)
   (let loop ((sys sys)
@@ -1485,28 +1528,19 @@
 (define (system? x)
   (is-a? x <system>))
 
-(define/guard (describe (sys system?) (name symbol?))
+(define/guard (system-lookup (sys system?) (name symbol?))
   (cond
-   ((lookup name sys)
-    => (lambda (def)
-         (cond
-          ((is-a? def <core-function>)
-           `(define-core-function ,(get-name def) ,(get-variables def)))
-          ((is-a? def <expandable-function>)
-           `(define-function ,(get-name def) ,(get-variables def)
-              ,(get-expression def)))
-          ((is-a? def <axiom>)
-           `(define-axiom ,(get-name def) ,(get-variables def)
-              ,(get-expression def)))
-          ((is-a? def <theorem*>)
-           `(define-theorem ,(get-name def) ,(get-variables def)
-              ,(get-expression def)))
-          (((cut is-a? <> <macro>) def)
-           `(define-syntax-rules ,(get-name def)))
-          (else
-           `(error 'fatal-error ,name)))))
-   (else
-    `(error 'not-found ,name))))
+   ((lookup name sys) => show)
+   (else #f)))
+
+(define/guard (system-load/name (sys system?) (name symbol?))
+  (primitive-eval (system-code sys name)))
+
+(define/guard (system-load/all (sys system?))
+  (primitive-eval (system-code sys)))
 
 (define/guard (system-load (sys system?))
   (primitive-eval (system-code sys)))
+
+(define/guard (system-rewrite (sys system?) (expr (const #t)) (seq sequence?))
+  (rewrite sys (convert-to-expression expr) seq))
diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index bd8b409..125c8d6 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -20,140 +20,170 @@
   #:export (prelude)
   #:use-module (vikalpa))
 
-(define-system prelude ()
-  (define-core-function natural? (x) (lambda (x)
-                                       (and (integer? x)
-                                            (< 0 x))))
-  (define-core-function < (x y) (natural? x) (natural? y) <)
-  (define-core-function pair? (x) pair?)
-  (define-core-function cons (x y) cons)
-  (define-core-function car (x) (pair? x)
-    (lambda (x) (if (pair? x) (car x) '())))
-  (define-core-function cdr (x) (pair? x)
-    (lambda (x) (if (pair? x) (cdr x) '())))
-  (define-core-function + (x y)
-    (lambda (x y)
-      (if (number? x)
-          (if (number? y)
-              (+ x y)
-              x)
-          (if (number? y)
-              y
-              0))))
-  (set-measure-predicate natural?)
-  (set-measure-less-than <)
-  (define-trivial-total-function list-induction (x)
-    (if (not (pair? x))
-        x
-        (cons (car x)
-              (list-induction (cdr x)))))
-  (define-trivial-total-function size (x)
-    (if (not (pair? x))
-        0
-        (+ 1
-           (+ (size (car x))
-              (size (cdr x))))))
-
+(define-syntax-rule (define-proof/is name p t1 t2)
+  (define-proof name
+    (((2) if-same (set x (p x)))
+     ((2 2 1) t1)
+     ((2 2) equal-same)
+     ((2) t2)
+     (() if-same))))
+
+(define-system prelude/macros ()
   (define-syntax-rules and ()
     ((and) '#t)
     ((and x) x)
     ((and x . xs) (if x (and . xs) #f)))
-
   (define-syntax-rules or ()
     ((or) '#f)
     ((or x) x)
     ((or x . xs) (if x x (or . xs))))
-
   (define-syntax-rules cond (else)
     ((cond (else e)) e)
     ((cond (test then) . rest)
      (if test then (cond . rest))))
-
   (define-syntax-rules implies ()
     ((implies x y) (if x y #t))
     ((implies x y z . rest)
-     (if x (implies y z . rest) #t)))
-  
+     (if x (implies y z . rest) #t))))
+
+(define-system prelude/equal (prelude/macros)
+  (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-system prelude/if (prelude/equal)
   (define-axiom if-nest (x y z)
     (if x
         (equal? (if x y z) y)
         (equal? (if x y z) z)))
-
   (define-axiom if-true (x y)
     (equal? (if '#t x y) x))
-
   (define-axiom if-false (x y)
     (equal? (if '#f x y) y))
-
   (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)))
-
-  (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 pair/cons (x y)
-    (equal? (pair? (cons x y)) '#t))
-
-  (define-axiom cons/car+cdr (x)
-    (implies (pair? x)
-             (equal? (cons (car x) (cdr x)) x)))
+            (if x z y))))
+
+(define-system prelude/number (prelude/if)
+  (define-core-function number? (x) number?)
+  (define-core-function rational? (x) rational?)
+  (define-core-function integer? (x) integer?)
+  (define-function zero? (x)
+    (equal? x 0))
+  (define-core-function < (x y)
+    (lambda (x y)
+      (if (rational? x)
+          (if (rational? y)
+              (< x y)
+              (< x 0))
+          (if (rational? y)
+              (< 0 y)
+              #f))))
+  (define-axiom axiom-< (x y)
+    (if (rational? x)
+        (if (rational? y)
+            #t
+            (equal? (< x y) (< x 0)))
+        (if (rational? y)
+            (equal? (< x y) (< 0 y))
+            (equal? (< x y) #f))))
+  (define-function natural? (x)
+    (if (integer? x)
+        (if (zero? x)
+            #t
+            (< 0 x))
+        #f))
+  (define-axiom rational-is-number (x y z)
+    (implies (rational? x) (equal? (if (number? x) y z) y)))
+  (define-axiom integer-is-rational (x y z)
+    (implies (integer? x) (equal? (if (rational? x) y z) y)))
+  (define-theorem integer-is-number (x y z)
+    (implies (integer? x) (equal? (if (number? x) y z) y)))
+  (define-theorem natural-is-integer (x y z)
+    (implies (natural? x) (equal? (if (integer? x) y z) y)))
+  (define-theorem natural-is-rational (x y z)
+    (implies (natural? x) (equal? (if (rational? x) y z) y)))
+  (define-theorem natural-is-number (x y z)
+    (implies (natural? x) (equal? (if (number? x) y z) y)))
+  (define-core-function + (x y)
+    (lambda (x y)
+      (if (number? x)
+          (if (number? y)
+              (+ x y)
+              (+ x 0))
+          (if (number? y)
+              (+ 0 y)
+              0)))))
 
-  (define-axiom car/cons (x y)
-    (equal? (car (cons x y)) x))
+(define-system prelude/measure (prelude/number)
+  (set-measure-predicate natural?)
+  (set-measure-less-than <))
 
-  (define-axiom cdr/cons (x y)
-    (equal? (cdr (cons x y)) y))
+(define-system prelude/pair (prelude/measure)
+  (define-core-function pair? (x) pair?)
+  (define-core-function cons (x y) cons)
+  (define-core-function car (x)
+    (lambda (x) (if (pair? x) (car x) '())))
+  (define-core-function cdr (x)
+    (lambda (x) (if (pair? x) (cdr x) '()))))
 
+(define-system prelude/tree (prelude/pair)
+  (define-trivial-total-function size (x)
+    (if (pair? x)
+        (+ 1
+           (+ (size (car x))
+              (size (cdr x))))
+        0))
   (define-axiom natural/size (x)
     (equal? (natural? (size x)) #t))
-
   (define-axiom size/car (x)
     (equal? (< (size (car x)) (size x)) #t))
-
   (define-axiom size/cdr (x)
     (equal? (< (size (cdr x)) (size x)) #t))
-
-  (define-axiom equal-car (x1 y1 x2 y2)
-    (implies (equal? (cons x1 y1) (cons x2 y2))
-             (equal? x1 x2)))
-
-  (define-theorem caar-cons2 (x y z)
-    (equal? (car (car (cons (cons x y) z))) x))
-  
-  (define-function app (x y)
+  (define-function tree-induction (x)
     (if (not (pair? x))
-        y
-        (cons (car x)
-              (app (cdr x) y))))
+        x
+        (cons (tree-induction (car x))
+              (tree-induction (cdr x))))))
+
+(define-system prelude/proofs (prelude/tree)
+  (define-proof/is integer-is-number
+    rational?
+    rational-is-number
+    integer-is-rational)
+
+  (define-proof natural-is-integer
+    ((() if-same (set x (integer? x)))
+     ((2 2 1) if-nest)
+     ((2 2) equal-same)
+     ((2) if-same)
+     ((3 1) natural?)
+     ((3 1) if-nest)
+     ((3) if-false)
+     (() if-same)))
+
+  (define-proof/is natural-is-rational
+    integer?
+    integer-is-rational
+    natural-is-integer)
+
+  (define-proof/is natural-is-number
+    rational?
+    rational-is-number
+    natural-is-rational)
   
-  (define-theorem assoc-app (x y z)
-    (equal? (app x (app y z))
-            (app (app x y) z)))
-
-  (define-proof caar-cons2
-    (((1 1)  car/cons)
-     ((1) car/cons)
-     (() equal-same)))
-
-  (define-proof app
+  (define-proof tree-induction
     (size x)
-    (((2 3) size/cdr)
+    (((2 3 1) size/car)
+     ((2 3 2) size/cdr)
+     ((2 3) if-true)
      ((2) if-same)
      ((1) natural/size)
-     (() if-true)))
-
-  (define-proof assoc-app
-    (list-induction x)
-    ()))
-
+     (() if-true))))
 
+(define-system prelude (prelude/proofs))
diff --git a/vikalpa/the-little-prover.scm b/vikalpa/the-little-prover.scm
index 338843b..fe7735e 100644
--- a/vikalpa/the-little-prover.scm
+++ b/vikalpa/the-little-prover.scm
@@ -17,24 +17,53 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa the-little-prover)
-  #:export (the-little-prover)
+  #:export (atom? nat? the-little-prover)
   #:use-module (vikalpa))
 
-(define (size x)
-  (if (pair? x)
-      (+ (size (car x))
-         (size (cdr x)))
-      0))
+(define (atom? x)
+  (not (pair? x)))
+
+(define (nat? x)
+  (and (integer? x)
+       (<= 0 x)))
 
 (define-system the-little-prover ()
-  (define-function atom? (x)
-    (not (pair? x)))
-  (define-builtin-function size (x))
-  (define-builtin-function + (x y))
-  (define-builtin-function natural? (x))
-  (define-builtin-function < (x y))
-  (define-totality-claim natural? natural? <)
-  
+  (define-core-function atom? (x) atom?)
+  (define-core-function nat? (x) nat?)
+  (define-core-function < (x y)
+    (lambda (x y)
+      (if (number? x)
+          (if (number? y)
+              (< x y)
+              (< x 0))
+          (if (number? y)
+              (< 0 y)
+              #f))))
+  (set-measure-predicate nat?)
+  (set-measure-less-than <)
+  (define-core-function + (x y)
+    (lambda (x y)
+      (if (number? x)
+          (if (number? y)
+              (+ x y)
+              x)
+          (if (number? y)
+              y
+              0))))
+  (define-core-function cons (x y) cons)
+  (define-core-function car (x)
+    (lambda (x)
+      (if (atom? x) '() (car x))))
+  (define-core-function cdr (x)
+    (lambda (x)
+      (if (atom? x) '() (cdr x))))
+  (define-trivial-total-function size (x)
+    (if (atom? x)
+        0
+        (+ 1
+           (+ (size (car x))
+              (size (cdr x))))))
+
   ;; Axioms of Equal
   (define-axiom equal-same (x)
     (equal? (equal? x x) #t))
@@ -68,8 +97,8 @@
     (if x #t (equal? (if x y z) z)))
 
   ;; Axioms of Size
-  (define-axiom natural?/size (x)
-    (equal? (natural? (size x)) #t))
+  (define-axiom nat/size (x)
+    (equal? (nat? (size x)) #t))
   (define-axiom size/car (x)
     (if (atom? x)
         #t
@@ -81,8 +110,8 @@
 
   ;; Axioms of `+` and `<`
   (define-axiom identity-+ (x)
-    (if (natural? x)
-        (equal? (+ (+ x y) z))
+    (if (nat? x)
+        (equal? (+ 0 x) x)
         #t))
   (define-axiom commute-+ (x y)
     (equal? (+ x y) (+ y x)))
@@ -94,23 +123,16 @@
             (equal? (< '0 (+ x y)) #t)
             #t)
         #t))
-  (define-axiom natural?/+ (x y)
-    (if (natural? x)
-        (if (natural? y)
-            (equal? (natural? (+ x y)) #t)
+  (define-axiom nat/+ (x y)
+    (if (nat? x)
+        (if (nat? y)
+            (equal? (nat? (+ x y)) #t)
             #t)
         #t))
   (define-axiom common-addends-< (x y z)
-    (equal? (< (+ x z) (+ y z) (< x y))))
-
-  ;; Axioms for Vikalpa
-  (define-axiom natural?/0 ()
-    (equal? (natural? '0) #t))
-  (define-axiom natural?/succ (x)
-    (if (natural? x)
-        (equal? (natural? (succ x)) #t)
-        #t))
-
+    (equal? (< (+ x z) (+ y z))
+            (< x y)))
+  
   ;; Prelude
   (define-function list-induction (x)
     (if (atom? x)
@@ -118,22 +140,24 @@
         (cons (car x)
               (list-induction (cdr x)))))
 
-  (define-proof list-induction
-    (natural? (size x))
-    (((2 3) size/cdr)
-     ((2) if-same)
-     (() if-same)))
-  
   (define-function star-induction (x)
     (if (atom? x)
         x
         (cons (star-induction (car x))
               (star-induction (cdr x)))))
 
+  (define-proof list-induction
+    (size x)
+    (((2 3) size/cdr)
+     ((2) if-same)
+     ((1) nat/size)
+     (() if-true)))
+
   (define-proof star-induction
-    (natural? (size x))
+    (size x)
     (((2 3 1) size/car)
      ((2 3 2) size/cdr)
      ((2 3) if-true)
      ((2) if-same)
-     (() if-same))))
+     ((1) nat/size)
+     (() if-true))))
-- 
cgit v1.2.3