wip80

3 files changed, 329 insertions, 263 deletions

diff --git a/vikalpa/prelude.scm b/examples/prelude.scm
index 824b5c5..f171b6e 100644
--- a/vikalpa/prelude.scm
+++ b/examples/prelude.scm
@@ -17,16 +17,14 @@
 ;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
 
 (define-module (vikalpa prelude)
-  #:export (prelude)
+  #:export (size prelude)
   #:use-module (vikalpa))
 
-(define (exact-positive-integer? x)
-  (and (exact-integer? x)
-       (positive? x)))
-
-(define (exact-negative-integer? x)
-  (and (exact-integer? x)
-       (negative? x)))
+(define (size x)
+  (if (pair? x)
+      (+ (size (car x))
+         (size (cdr x)))
+      1))
 
 (define-syntax-rule (define-axiom/is p1 p2)
   (define-axiom (is p1 p2) (x) (is (p1 x) (p2 x))))
@@ -64,7 +62,8 @@
   (define-syntax-rules predicate ()
     ((predicate x) (implies x (equal? x #t))))
   (define-syntax-rules is ()
-    ((is x y) (implies x (equal? y #t)))))
+    ((is x y) (implies x (equal? y #t)))
+    ((is x y . ys) (implies x (is y . ys)))))
 
 (define-system prelude/axiom/equal (prelude/macro)
   (define-axiom equal-same (x)
@@ -122,7 +121,7 @@
   (define-proof/is exact-integer? number? real?)
   (define-core-function/guard < (x y) (and (real? x) (real? y)) <)
   (define-axiom (predicate <) (x y) (predicate (< x y)))
-
+  
   (define-function/guard positive? (x)
     (real? x)
     (< 0 x))
@@ -131,26 +130,127 @@
     (real? x)
     (< x 0))
   (define-theorem (predicate negative?) (x) (predicate (negative? x)))
-
   (define-function exact-positive-integer? (x)
     (and (exact-integer? x)
          (positive? x)))
   (define-theorem (predicate exact-positive-integer?) (x)
     (predicate (exact-positive-integer? x)))
   (define-theorem/is exact-positive-integer? exact-integer?)
-
+  (define-theorem/is exact-positive-integer? exact?)
+  (define-proof/is exact-positive-integer? exact? exact-integer?)
+  (define-theorem/is exact-positive-integer? integer?)
+  (define-proof/is exact-positive-integer? integer? exact-integer?)
+  (define-theorem/is exact-positive-integer? real?)
+  (define-proof/is exact-positive-integer? real? exact-integer?)
+  (define-theorem/is exact-positive-integer? number?)
+  (define-proof/is exact-positive-integer? number? exact-integer?)
+  
   (define-function exact-zero? (x) (equal? x 0))
   (define-theorem (predicate exact-zero?) (x)
     (predicate (exact-zero? x)))
   (define-theorem/is exact-zero? exact-integer?)
+  (define-theorem/is exact-zero? integer?)
+  (define-proof/is exact-zero? integer? exact-integer?)
+  (define-theorem/is exact-zero? exact?)
+  (define-proof/is exact-zero? exact? exact-integer?)
+  (define-theorem/is exact-zero? real?)
+  (define-proof/is exact-zero? real? exact-integer?)
+  (define-theorem/is exact-zero? number?)
+  (define-proof/is exact-zero? number? real?)
 
   (define-function natural? (x)
     (if (exact-zero? x)
         #t
         (exact-positive-integer? x)))
+
   (define-theorem (predicate natural?) (x)
     (predicate (natural? x)))
-  (define-theorem/is natural? exact-integer?))
+  (define-theorem/is natural? exact-integer?)
+  (define-theorem/is natural? integer?)
+  (define-proof/is natural? integer? exact-integer?)
+  (define-theorem/is natural? exact?)
+  (define-proof/is natural? exact? exact-integer?)
+  (define-theorem/is natural? real?)
+  (define-proof/is natural? real? exact-integer?)
+  (define-theorem/is natural? number?)
+  (define-proof/is natural? number? real?)
+
+  (define-theorem/is exact-zero? natural?)
+  (define-theorem/is exact-positive-integer? natural?)
+
+  (set-measure-predicate natural?)
+  (set-measure-less-than <)
+
+(define-core-function/guard + (x y) (and (number? x) (number? y)) +)
+  (define-core-function/guard - (x y) (and (number? x) (number? y)) -)
+  (define-function/guard succ (x) (natural? x) (+ x 1))
+  (define-function/guard pred (x) (exact-positive-integer? x) (- x 1))
+  (define-function/guard natural-induction (x)
+    (natural? x)
+    (if (exact-zero? x)
+        #t
+        (succ (natural-induction (pred x)))))
+  (admit natural-induction)
+
+  (define-axiom (+ natural? natural?) (x y)
+    (implies (natural? x)
+             (natural? y)
+             (equal? (+ x y)
+                     (if (exact-zero? x)
+                         y
+                         (succ (+ (pred x) y))))))
+  (define-axiom pred/succ (x)
+    (implies (natural? x)
+             (equal? (pred (succ x)) x)))
+  (define-theorem succ/pred (x)
+    (implies (exact-positive-integer? x)
+             (equal? (succ (pred x)) x)))
+  (define-theorem (is natural? (o natural? succ)) (x)
+    (is (natural? x) (natural? (succ x))))
+
+  (define-theorem (is (o natural? pred) natural?) (x)
+    (is (natural? (pred x))
+        (natural? x)))
+
+  (define-axiom pred/zero (x)
+    (equal? (natural? (pred 0)) #f))
+
+  (define-theorem (is (o not natural?) (o not natural? pred)) (x)
+    (is (not (natural? x))
+        (not (natural? (pred x)))))
+  
+  (define-theorem (is (o natural?)
+                      (o not exact-zero?)
+                      exact-positive-integer?)
+    (x)
+    (is (not (natural? x))
+        (not (exact-zero? x))
+        (exact-positive-integer? x)))
+
+  (define-function/guard natural-induction-+ (x y)
+    (and (natural? x) (natural? y))
+    (if (exact-zero? x)
+        y
+        (succ (natural-induction-+ (pred x) y))))
+  (admit natural-induction-+)
+
+  (define-theorem (is natural? (o not exact-zero?) exact-positive-integer?) (x)
+    (is (natural? x)
+        (not (exact-zero? x))
+        (exact-positive-integer? x)))
+  
+  (define-theorem (implies natural?
+                           (equal? (o natural? pred)
+                                   exact-positive-integer?))
+    (x)
+    (implies (natural? x)
+             (equal? (natural? (pred x))
+                     (exact-positive-integer? x))))
+  
+  (define-theorem (+ (-> natural? natural? natural?)) (x y)
+    (implies (natural? x)
+             (natural? y)
+             (natural? (+ x y)))))
 
 (define-system prelude/measure/natural (prelude/number)
   (set-measure-predicate natural?)
@@ -160,7 +260,8 @@
   (define-core-function pair? (x) pair?)
   (define-core-function cons (x y) cons)
   (define-core-function/guard car (x) (pair? x) car)
-  (define-core-function/guard cdr (x) (pair? x) cdr))
+  (define-core-function/guard cdr (x) (pair? x) cdr)
+  (define-core-function size (x) size))
 
 (define-system prelude (prelude/pair)
   (define-proof inexact?
@@ -232,4 +333,94 @@
      (eval (3 2))
      (rewrite (3) if-same)
      (rewrite () if-same)))
-  )
+  (define-proof (is exact-positive-integer? exact-integer?)
+    ((rewrite (1) exact-positive-integer?)
+     (rewrite () if-same (set x (exact-integer? x)))
+     (rewrite (3 1) if-nest)
+     (rewrite (2 1) if-nest)
+     (rewrite (2 2 1) (predicate exact-integer?))
+     (eval (2 2))
+     (rewrite (2) if-same)
+     (rewrite (3) if-false)
+     (rewrite ()  if-same)))
+  (define-proof (is exact-zero? exact-integer?)
+    ((rewrite (1) exact-zero?)
+     (rewrite (2 1 1) equal-if)
+     (eval (2))
+     (rewrite () if-same)))
+  (define-proof (is natural? exact-integer?)
+    ((rewrite (1) natural?)
+     (rewrite () if-same (set x (exact-zero? x)))
+     (rewrite (2 1) if-nest)
+     (rewrite (2) if-true)
+     (rewrite (2 1) (is exact-zero? exact-integer?))
+     (eval (2))
+     (rewrite (3 1) if-nest)
+     (rewrite (3 2 1) (is exact-positive-integer? exact-integer?))
+     (eval (3 2))
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+  (define-proof succ
+    ((rewrite (2 1 1) (is natural? number?))
+     (eval (2))
+     (rewrite ()  if-same)))
+  (define-proof pred
+    ((rewrite (2 1 1) (is exact-positive-integer? number?))
+     (eval (2))
+     (rewrite () if-same)))
+
+  #;
+  (define-proof (natural? and not exact-zero? implies exact-positive-integer?)
+    ((rewrite (1) natural?)
+     (rewrite () if-same (set x (exact-zero? x)))
+     (rewrite (2 1) if-nest)
+     (rewrite (2) if-true)
+     (rewrite (2) if-not)
+     (rewrite (2) if-nest)
+     (rewrite (3 1) if-nest)
+     (rewrite (3 2) if-not)
+     (rewrite (3 2) if-nest)
+     (rewrite (3 2) (predicate exact-positive-integer?))
+     (rewrite (3) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (+ (-> natural? natural? natural?))
+    ((induction (2 2) (natural-induction-+ x y))
+     (rewrite (2 2 2 1) (+ natural? natural?))
+     (rewrite (2 2 2 1) if-nest)
+     (rewrite (2 2 2) (predicate natural?))
+     (rewrite (2 2 3 2) if-same (set x (natural? (pred x))))
+     (rewrite (2 2 3 2 2 1) (+ natural? natural?))
+     (rewrite (2 2 3 2 2 1) if-nest)
+     (rewrite (2 2 3 2 2) (is natural? (o natural? succ)))
+     (rewrite (2 2 3 2 1) (implies natural?
+                                   (equal? (o natural? pred)
+                                           exact-positive-integer?)))
+     (rewrite (2 2 3 2 1) (is natural? (o not exact-zero?)
+                              exact-positive-integer?))
+     (rewrite (2 2 3 2) if-true)
+     (rewrite (2 2 3) if-same)
+     (rewrite (2 2) if-same)
+     (rewrite (2) if-same)
+     (rewrite () if-same)))
+
+  (define-proof (is exact-zero? natural?)
+    ((rewrite (1) exact-zero?)
+     (rewrite (2 1 1) equal-if)
+     (eval (2))
+     (rewrite ()  if-same)))
+
+  (define-proof (is exact-positive-integer? natural?)
+    ((rewrite (2 1) natural?)
+     (rewrite (2 1 3) (predicate exact-positive-integer?))
+     (rewrite (2 1) if-same)
+     (eval (2))
+     (rewrite () if-same)))
+
+  (define-proof (is (o natural? pred) natural?)
+    ((rewrite () if-same (set x (natural? x)))
+     (rewrite (2 2 1) (predicate natural?))
+     (eval (2 2))
+     (rewrite (3 2 1) equal-if-false)
+     (eval (3 2))
+     (rewrite (2) if-same))))
diff --git a/vikalpa.scm b/vikalpa.scm
index 79f6fb1..3d5e3e5 100644
--- a/vikalpa.scm
+++ b/vikalpa.scm
@@ -30,10 +30,14 @@
             define-core-function
             define-core-function/guard
             define-function
+            define-function
             define-function/guard
+            define-axiom-function
+            define-axiom-function/guard
             define-syntax-rules
             define-axiom
-            define-theorem)
+            define-theorem
+            admit)
   #:use-module (ice-9 match)
   #:use-module (ice-9 format)
   #:use-module (ice-9 control)
@@ -69,6 +73,7 @@
 (define-class <proved> (<provable>)
   (claim #:getter get-claim #:init-keyword #:claim)
   (proof #:getter get-proof #:init-keyword #:proof))
+(define-class <admitted> ())
 
 (define-class <theorem*> (<definition>)
   (expression #:getter get-expression #:init-keyword #:expression))
@@ -86,6 +91,7 @@
   (code #:getter get-code #:init-keyword #:code))
 (define-class <function> (<expandable-function> <provable>))
 (define-class <total-function> (<expandable-function> <proved>))
+(define-class <admitted-function> (<expandable-function> <proved> <admitted>))
 
 (define-class <macro> (<definition>)
   (mrules #:getter macro-mrules #:init-keyword #:mrules)
@@ -719,6 +725,10 @@
           (command-name? command-name)
           (every command-option? command-ops)))
     (('eval path) (path? path))
+    (('induction path (fname vars ...))
+     (and (path? path)
+          (symbol? fname)
+          (every variable? vars)))
     (else #f)))
 
 ;; (sequence? x) -> boolean?
@@ -835,12 +845,6 @@
         (else
          (result/error 'apply-theorem cmd-name expr)))))))
 
-(define (rewrite/induction sys fname vars expr fail)
-  (cond
-   ((lookup fname sys)
-    => (cut make-induction-claim <> vars expr))
-   (else (fail 'induction 'not-found fname))))
-
 (define (rewrite/core-function sys f expr)
   (if (and (app-form? expr)
            (eq? (get-name f) (app-form-name expr))
@@ -851,6 +855,30 @@
                           (map expr-unquote (app-form-args expr)))))
       (result/error 'apply-core-function (get-name f) expr)))
 
+(define (rewrite/function sys fname f expr)
+  (cond
+   ((any (cut apply-rule '() <> expr '())
+         (function->rules f))
+    => result/expr)
+   (else
+    (result/error 'apply-function fname expr))))
+
+(define (rewrite/induction sys fname vars ps expr)
+  (cond
+   ((lookup fname sys)
+    => (lambda (f)
+         (cond
+          ((not (is-a? f <expandable-function>))
+           (result/error 'induction 'not-expandable-function fname expr))
+          ((apply-rule ps
+                       (make-induction-rule f vars expr)
+                       expr
+                       '())
+           => result/expr)
+          (else
+           (result/error 'induction 'error fname expr)))))
+   (else (result/error 'induction 'not-found fname expr))))
+
 (define (rewrite1 sys expr r)
   (call/cc
    (lambda (k)
@@ -868,6 +896,13 @@
           (result/expr
            (builder
             (result->expr (rewrite/eval extracted-expr sys))))))
+       (('induction path (fname vars ...))
+        (receive (extracted-expr preconds builder)
+            (extract path expr fail)
+          (result/expr
+           (builder
+            (result->expr
+             (rewrite/induction sys fname vars preconds extracted-expr))))))
        (('rewrite path cmd-name cmd-ops ...)
         (receive (extracted-expr preconds builder)
             (extract path expr fail)
@@ -883,13 +918,7 @@
                      ((is-a? x <theorem*>)
                       (rewrite/theorem cmd-name cmd-ops sys x preconds extracted-expr))
                      ((is-a? x <expandable-function>)
-                      (cond
-                       ((any (cut apply-rule '() <> extracted-expr '())
-                             (function->rules x))
-                        => result/expr)
-                       (else
-                        (result/error 'apply-function cmd-name extracted-expr))))
-                     
+                      (rewrite/function sys cmd-name x extracted-expr))
                      (else
                       (result/error 'invalid-command cmd-name extracted-expr)))))
               (else (result/error 'command-not-found cmd-name extracted-expr))))))))))))
@@ -1058,6 +1087,35 @@
        (current-system (add-definition m (current-system)))
        m))))
 
+(define-syntax admit
+  (syntax-rules (and)
+    ((_ name)
+     (cond
+      ((lookup 'name (current-system))
+       => (lambda (f)
+            (unless (is-a? f <function>)
+              (raise-exception
+               (make-exception
+                (make-exception-with-origin 'name)
+                (make-exception-with-message "not provable definition")
+                (make-exception-with-irritants 'name))))
+            (let ((g (make <admitted-function>
+                       #:name (get-name f)
+                       #:variables (get-variables f)
+                       #:guards (get-guards f)
+                       #:expression (get-expression f)
+                       #:code (get-code f)
+                       #:claim ''#t
+                       #:proof '())))
+              (validate g)
+              (current-system (update-definition g (current-system))))))
+      (else
+       (raise-exception
+        (make-exception
+         (make-exception-with-origin 'name)
+         (make-exception-with-message "not found")
+         (make-exception-with-irritants 'name))))))))
+
 (define* (core-system #:optional (parent (make <system>)))
   (parameterize ((current-system parent))
     (define-syntax-rules and ()
@@ -1148,16 +1206,6 @@
     (smart-if x y ''#t))))
 
 (define (make-totality-claim* sys m-expr f)
-  (unless (get-measure-predicate sys)
-    (raise-exception
-     (make-exception
-      (make-exception-with-origin `(define-proof ,(get-name f)))
-      (make-exception-with-message "measure-predicate is not found"))))
-  (unless (get-measure-less-than sys)
-    (raise-exception
-     (make-exception
-      (make-exception-with-origin `(define-proof ,(get-name f)))
-      (make-exception-with-message "measure-less-than is not found"))))
   (let* ((name (get-name f)))
     (define (convert app-form)
       (cond
@@ -1249,7 +1297,14 @@
             ''#t
             ''#f))
 
-(define (make-induction-claim f vars c)
+(define (make-induction-rule f vars c)
+  (unless (is-a? f <proved>)
+    (raise-exception
+     (make-exception
+      (make-exception-with-origin 'define-proof)
+      (make-exception-with-message
+       "measure function must be proved function")
+      (make-exception-with-irritants (get-name f)))))
   (define (find-app-forms expr)
     (cond
      ((app-form? expr)
@@ -1273,24 +1328,28 @@
       => identity)
      (else
       (error "make-induction-claim: fail" app-form))))
-  (cond
-   ((apply-function f vars)
-    => (lambda (expr)
-         (let build ((expr expr))
-           (cond
-            ((if-form? expr)
-             (let ((app-forms (find-app-forms (if-form-test expr))))
-               (smart-implies (if (null? app-forms)
-                                  ''#t
-                                  (fold smart-implies c (map prop app-forms)))
-                              (smart-if (if-form-test expr)
-                                        (build (if-form-then expr))
-                                        (build (if-form-else expr))))))
-            (else
-             (let ((app-forms (find-app-forms expr)))
-               (fold smart-implies c (map prop app-forms))))))))
-   (else (error "make-induction-claim: invalid"
-                f vars c))))
+  (define rhs
+    (cond
+     ((apply-function f vars)
+      => (lambda (expr)
+           (let build ((expr expr))
+             (cond
+              ((if-form? expr)
+               (let ((app-forms (find-app-forms (if-form-test expr))))
+                 (smart-implies (if (null? app-forms)
+                                    ''#t
+                                    (fold smart-implies
+                                          c
+                                          (map prop app-forms)))
+                                (smart-if (if-form-test expr)
+                                          (build (if-form-then expr))
+                                          (build (if-form-else expr))))))
+              (else
+               (let ((app-forms (find-app-forms expr)))
+                 (fold smart-implies c (map prop app-forms))))))))
+     (else (error "make-induction-claim: invalid"
+                  f vars c))))
+  (rule vars (get-guards f) c rhs))
 
 (define (validate-sequence sys d seq)
   (for-each (lambda (r)
@@ -1345,38 +1404,13 @@
 
 (define (add-proof/theorem sys t seed seq)
   (validate-sequence sys t seq)
-  (let ((claim
-         (if seed
-             (begin
-               (validate-expression sys
-                                    `(define-proof ,(get-name t))
-                                    (get-variables t)
-                                    seed)
-               (match seed
-                 ((fname . vars)
-                  (cond
-                   ((lookup fname sys)
-                    => (cut make-induction-claim <> vars (get-expression t)))
-                   (else
-                    (raise-exception
-                     (make-exception
-                      (make-exception-with-origin 'add-proof/theorem)
-                      (make-exception-with-message "error")
-                      (make-exception-with-irritants seed))))))
-                 (else
-                  (raise-exception
-                   (make-exception
-                    (make-exception-with-origin `(define-proof ,(get-name t)))
-                    (make-exception-with-message "invalid induction form")
-                    (make-exception-with-irritants seed))))))
-             (get-expression t))))
-    (update-definition (make <theorem>
-                         #:name (get-name t)
-                         #:variables (get-variables t)
-                         #:expression (get-expression t)
-                         #:claim claim
-                         #:proof seq)
-                       sys)))
+  (update-definition (make <theorem>
+                       #:name (get-name t)
+                       #:variables (get-variables t)
+                       #:expression (get-expression t)
+                       #:claim (get-expression t)
+                       #:proof seq)
+                     sys))
 
 (define (add-proof sys name seed seq)
   (cond
@@ -1498,6 +1532,7 @@
 (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 <admitted-function>)) 'admitted-function)
 (define-method (get-type (s <macro>)) 'macro)
 
 (define-method (show (d <macro>))
@@ -1513,21 +1548,24 @@
   (list (get-type d)
         (get-variables d)
         (get-expression d)))
+(define-method (show (d <admitted-function>))
+  (list (get-type d)
+        (get-variables d)
+        (get-expression d)))
 
 (define* (system-apropos sys
                          str
                          #:key all?)
   (filter-map (lambda (d)
-                (if (and (or all?
-                             (not (string-match "^%"
-                                                (symbol->string
-                                                 (get-name d)))))
-                         (string-match (string-append ".*"
-                                                      (regexp-quote str)
-                                                      ".*")
-                                       (symbol->string (get-name d))))
-                    (list (get-name d) (show d))
-                    #f))
+                (let ((name (format #f "~a" (get-name d))))
+                  (if (and (or all?
+                               (not (string-match "^%" name)))
+                           (string-match (string-append ".*"
+                                                        (regexp-quote str)
+                                                        ".*")
+                                         name))
+                      (list (get-name d) (show d))
+                      #f)))
               (get-definitions sys)))
 
 (define (system-check sys)
diff --git a/vikalpa/the-little-prover.scm b/vikalpa/the-little-prover.scm
deleted file mode 100644
index fe7735e..0000000
--- a/vikalpa/the-little-prover.scm
+++ /dev/null
@@ -1,163 +0,0 @@
-;;; Vikalpa --- Proof Assistant
-;;; Copyright © 2020 Masaya Tojo <masaya@tojo.tokyo>
-;;;
-;;; This file is part of Vikalpa.
-;;;
-;;; Vikalpa is free software; you can redistribute it and/or modify it
-;;; under the terms of the GNU General Public License as published by
-;;; the Free Software Foundation; either version 3 of the License, or
-;;; (at your option) any later version.
-;;;
-;;; Vikalpa is distributed in the hope that it will be useful, but
-;;; WITHOUT ANY WARRANTY; without even the implied warranty of
-;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
-;;; General Public License for more details.
-;;;
-;;; You should have received a copy of the GNU General Public License
-;;; along with Vikalpa.  If not, see <http://www.gnu.org/licenses/>.
-
-(define-module (vikalpa the-little-prover)
-  #:export (atom? nat? the-little-prover)
-  #:use-module (vikalpa))
-
-(define (atom? x)
-  (not (pair? x)))
-
-(define (nat? x)
-  (and (integer? x)
-       (<= 0 x)))
-
-(define-system the-little-prover ()
-  (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))
-  (define-axiom equal-swap (x y)
-    (equal? (equal? x y) (equal? y x)))
-  (define-axiom equal-if (x y)
-    (if (equal? x y) (equal? x y) #t))
-
-  ;; Axioms of Cons
-  (define-axiom atom/cons (x y)
-    (equal? (atom? (cons x y)) #f))
-  (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)))
-
-  ;; Axioms of If
-  (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-nest-A (x y z)
-    (if x (equal? (if x y z) y) #t))
-  (define-axiom if-nest-E (x y z)
-    (if x #t (equal? (if x y z) z)))
-
-  ;; Axioms of Size
-  (define-axiom nat/size (x)
-    (equal? (nat? (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)))
-
-  ;; Axioms of `+` and `<`
-  (define-axiom identity-+ (x)
-    (if (nat? x)
-        (equal? (+ 0 x) x)
-        #t))
-  (define-axiom commute-+ (x y)
-    (equal? (+ x y) (+ y x)))
-  (define-axiom associate-+ (x y z)
-    (equal? (+ (+ x y) z) (+ x (+ y z))))
-  (define-axiom positive-+ (x y)
-    (if (< '0 x)
-        (if (< '0 y)
-            (equal? (< '0 (+ x y)) #t)
-            #t)
-        #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)))
-  
-  ;; Prelude
-  (define-function list-induction (x)
-    (if (atom? x)
-        x
-        (cons (car x)
-              (list-induction (cdr x)))))
-
-  (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
-    (size x)
-    (((2 3 1) size/car)
-     ((2 3 2) size/cdr)
-     ((2 3) if-true)
-     ((2) if-same)
-     ((1) nat/size)
-     (() if-true))))