
(define s.car car)
(define s.cdr cdr)
(define s.+ +)
(define s.< <)
(define (num x) (if (number? x) x 0))
(define (if/nil Q A E)
  (if (equal? Q 'nil) (E) (A)))

(define (atom x) (if (pair? x) 'nil 't))
(define (car x) (if (pair? x) (s.car x) '()))
(define (cdr x) (if (pair? x) (s.cdr x) '()))
(define (equal x y) (if (equal? x y) 't 'nil))
(define (natp x)
  (if (number? x) (if (s.< x 0) 'nil 't) 'nil))
(define (+ x y) (s.+ (num x) (num y)))
(define (< x y)
  (if (s.< (num x) (num y)) 't 'nil))

;(define-syntax if
;  (syntax-rules ()
;    ((_ Q A E)
;     (if/nil Q (lambda () A) (lambda () E)))))

(defmacro if
  (lambda (form)
    (let ((Q (cadr form))
	  (A (caddr form))
	  (E (cadddr form)))
      `(if/nil ,Q (lambda () ,A) (lambda () ,E)))))

;(define-syntax defun
;  (syntax-rules ()
;    ((_ name (arg ...) body)
;     (define (name arg ...) body))))

;(define-syntax dethm
;  (syntax-rules ()
;    ((_ name (arg ...) body)
;     (define (name arg ...) body))))

(defmacro defun
  (lambda (form)
    (let ((name (cadr form))
	  (args (caddr form))
	  (body (cdddr form)))
      `(define (,name . ,args) . ,body))))

(defmacro dethm
  (lambda (form)
    (let ((name (cadr form))
	  (args (caddr form))
	  (body (cdddr form)))
      `(define (,name . ,args) . ,body))))

(defun size (x)
  (if (atom x)
    '0
    (+ '1 (+ (size (car x)) (size (cdr x))))))

;;;;;;;;;;;;


(defun list0 () '())
(defun list0? (x) (equal x '()))

(defun list1 (x) (cons x (list0)))
(defun list1? (x)
  (if (atom x) 'nil (list0? (cdr x))))
(defun elem1 (xs) (car xs))

(defun list2 (x y) (cons x (list1 y)))
(defun list2? (x)
  (if (atom x) 'nil (list1? (cdr x))))
(defun elem2 (xs) (elem1 (cdr xs)))

(defun list3 (x y z) (cons x (list2 y z)))
(defun list3? (x)
  (if (atom x) 'nil (list2? (cdr x))))
(defun elem3 (xs) (elem2 (cdr xs)))

(defun tag (sym x) (cons sym x))
(defun tag? (sym x)
  (if (atom x) 'nil (equal (car x) sym)))
(defun untag (x) (cdr x))

(defun quote-c (value)
  (tag 'quote (list1 value)))
(defun quote? (x)
  (if (tag? 'quote x) (list1? (untag x)) 'nil))
(defun quote.value (e) (elem1 (untag e)))

(defun if-c (Q A E) (tag 'if (list3 Q A E)))
(defun if? (x)
  (if (tag? 'if x) (list3? (untag x)) 'nil))
(defun if.Q (e) (elem1 (untag e)))
(defun if.A (e) (elem2 (untag e)))
(defun if.E (e) (elem3 (untag e)))

(defun app-c (name args) (cons name args))
(defun app? (x)
  (if (atom x)
    'nil
    (if (quote? x)
      'nil
      (if (if? x)
        'nil
        't))))
(defun app.name (e) (car e))
(defun app.args (e) (cdr e))

(defun var? (x)
  (if (equal x 't)
    'nil
    (if (equal x 'nil)
      'nil
      (if (natp x)
        'nil
        (atom x)))))

(defun defun-c (name formals body)
  (tag 'defun (list3 name formals body)))
(defun defun? (x)
  (if (tag? 'defun x) (list3? (untag x)) 'nil))
(defun defun.name (def) (elem1 (untag def)))
(defun defun.formals (def) (elem2 (untag def)))
(defun defun.body (def) (elem3 (untag def)))

(defun dethm-c (name formals body)
  (tag 'dethm (list3 name formals body)))
(defun dethm? (x)
  (if (tag? 'dethm x) (list3? (untag x)) 'nil))
(defun dethm.name (def) (elem1 (untag def)))
(defun dethm.formals (def) (elem2 (untag def)))
(defun dethm.body (def) (elem3 (untag def)))

(defun if-QAE (e)
  (list3 (if.Q e) (if.A e) (if.E e)))
(defun QAE-if (es)
  (if-c (elem1 es) (elem2 es) (elem3 es)))

(defun member? (x ys)
  (if (atom ys)
    'nil
    (if (equal x (car ys))
      't
      (member? x (cdr ys)))))

(defun rator? (name)
  (member? name
    '(equal atom car cdr cons natp size + <)))

(defun rator.formals (rator)
  (if (member? rator '(atom car cdr natp size))
    '(x)
    (if (member? rator '(equal cons + <))
      '(x y)
      'nil)))

(defun def.name (def)
  (if (defun? def)
    (defun.name def)
    (if (dethm? def)
      (dethm.name def)
      def)))

(defun def.formals (def)
  (if (dethm? def)
    (dethm.formals def)
    (if (defun? def)
      (defun.formals def)
      '())))

(defun if-c-when-necessary (Q A E)
  (if (equal A E) A (if-c Q A E)))

(defun conjunction (es)
  (if (atom es)
    (quote-c 't)
    (if (atom (cdr es))
      (car es)
      (if-c (car es)
        (conjunction (cdr es))
        (quote-c 'nil)))))

(defun implication (es e)
  (if (atom es)
    e
    (if-c (car es)
      (implication (cdr es) e)
      (quote-c 't))))

(defun lookup (name defs)
  (if (atom defs)
    name
    (if (equal (def.name (car defs)) name)
      (car defs)
      (lookup name (cdr defs)))))

(defun undefined? (name defs)
  (if (var? name)
    (equal (lookup name defs) name)
    'nil))

(defun arity? (vars es)
  (if (atom vars)
    (atom es)
    (if (atom es)
      'nil
      (arity? (cdr vars) (cdr es)))))

(defun args-arity? (def args)
  (if (dethm? def)
    'nil
    (if (defun? def)
      (arity? (defun.formals def) args)
      (if (rator? def)
        (arity? (rator.formals def) args)
        'nil))))

(defun app-arity? (defs app)
  (args-arity? (lookup (app.name app) defs)
    (app.args app)))

(defun bound? (var vars)
  (if (equal vars 'any) 't (member? var vars)))

(defun exprs? (defs vars es)
  (if (atom es)
    't
    (if (var? (car es))
      (if (bound? (car es) vars)
        (exprs? defs vars (cdr es))
        'nil)
      (if (quote? (car es))
        (exprs? defs vars (cdr es))
        (if (if? (car es))
          (if (exprs? defs vars
                (if-QAE (car es)))
            (exprs? defs vars (cdr es))
            'nil)
          (if (app? (car es))
            (if (app-arity? defs (car es))
              (if (exprs? defs vars
                    (app.args (car es)))
                (exprs? defs vars (cdr es))
                'nil)
              'nil)
            'nil))))))
(defun expr? (defs vars e)
  (exprs? defs vars (list1 e)))

(defun get-arg-from (n args from)
  (if (atom args)
    'nil
    (if (equal n from)
      (car args)
      (get-arg-from n (cdr args) (+ from '1)))))
(defun get-arg (n args)
  (get-arg-from n args '1))

(defun set-arg-from (n args y from)
  (if (atom args)
    '()
    (if (equal n from)
      (cons y (cdr args))
      (cons (car args)
        (set-arg-from n (cdr args) y
          (+ from '1))))))
(defun set-arg (n args y)
  (set-arg-from n args y '1))

(defun <=len-from (n args from)
  (if (atom args)
    'nil
    (if (equal n from)
      't
      (<=len-from n (cdr args) (+ from '1)))))
(defun <=len (n args)
  (if (< '0 n) (<=len-from n args '1) 'nil))

(defun subset? (xs ys)
  (if (atom xs)
    't
    (if (member? (car xs) ys)
      (subset? (cdr xs) ys)
      'nil)))

(defun list-extend (xs x)
  (if (atom xs)
    (list1 x)
    (if (equal (car xs) x)
      xs
      (cons (car xs)
        (list-extend (cdr xs) x)))))

(defun list-union (xs ys)
  (if (atom ys)
    xs
    (list-union (list-extend xs (car ys))
      (cdr ys))))

(defun formals? (vars)
  (if (atom vars)
    't
    (if (var? (car vars))
      (if (member? (car vars) (cdr vars))
        'nil
        (formals? (cdr vars)))
      'nil)))

(defun direction? (dir)
  (if (natp dir)
    't
    (member? dir '(Q A E))))

(defun path? (path)
  (if (atom path)
    't
    (if (direction? (car path))
      (path? (cdr path))
      'nil)))

(defun quoted-exprs? (args)
  (if (atom args)
    't
    (if (quote? (car args))
      (quoted-exprs? (cdr args))
      'nil)))

(defun step-args? (defs def args)
  (if (dethm? def)
    (if (arity? (dethm.formals def) args)
      (exprs? defs 'any args)
      'nil)
    (if (defun? def)
      (if (arity? (defun.formals def) args)
        (exprs? defs 'any args)
        'nil)
      (if (rator? def)
        (if (arity? (rator.formals def) args)
          (quoted-exprs? args)
          'nil)
        'nil))))

(defun step-app? (defs app)
  (step-args? defs
    (lookup (app.name app) defs)
    (app.args app)))

(defun step? (defs step)
  (if (path? (elem1 step))
    (if (app? (elem2 step))
      (step-app? defs (elem2 step))
      'nil)
    'nil))

(defun steps? (defs steps)
  (if (atom steps)
    't
    (if (step? defs (car steps))
      (steps? defs (cdr steps))
      'nil)))

(defun induction-scheme-for? (def vars e)
  (if (defun? def)
    (if (arity? (defun.formals def) (app.args e))
      (if (formals? (app.args e))
        (subset? (app.args e) vars)
        'nil)
      'nil)
    'nil))

(defun induction-scheme? (defs vars e)
  (if (app? e)
    (induction-scheme-for?
      (lookup (app.name e) defs)
      vars
      e)
    'nil))

(defun seed? (defs def seed)
  (if (equal seed 'nil)
    't
    (if (defun? def)
      (expr? defs (defun.formals def) seed)
      (if (dethm? def)
        (induction-scheme? defs
          (dethm.formals def)
          seed)
        'nil))))

(defun extend-rec (defs def)
  (if (defun? def)
    (list-extend defs
      (defun-c
        (defun.name def)
        (defun.formals def)
        (app-c (defun.name def)
          (defun.formals def))))
    defs))

(defun def-contents? (known-defs formals body)
  (if (formals? formals)
    (expr? known-defs formals body)
    'nil))

(defun def? (known-defs def)
  (if (dethm? def)
    (if (undefined? (dethm.name def)
          known-defs)
      (def-contents? known-defs
        (dethm.formals def)
        (dethm.body def))
      'nil)
    (if (defun? def)
      (if (undefined? (defun.name def)
            known-defs)
        (def-contents?
          (extend-rec known-defs def)
          (defun.formals def)
          (defun.body def))
        'nil)
      'nil)))

(defun defs? (known-defs defs)
  (if (atom defs)
    't
    (if (def? known-defs (car defs))
      (defs? (list-extend known-defs (car defs))
        (cdr defs))
      'nil)))

(defun list2-or-more? (pf)
  (if (atom pf)
    'nil
    (if (atom (cdr pf))
      'nil
      't)))

(defun proof? (defs pf)
  (if (list2-or-more? pf)
    (if (def? defs (elem1 pf))
      (if (seed? defs (elem1 pf) (elem2 pf))
        (steps? (extend-rec defs (elem1 pf))
          (cdr (cdr pf)))
        'nil)
      'nil)
    'nil))

(defun proofs? (defs pfs)
  (if (atom pfs)
    't
    (if (proof? defs (car pfs))
      (proofs?
        (list-extend defs (elem1 (car pfs)))
        (cdr pfs))
      'nil)))

(defun sub-var (vars args var)
  (if (atom vars)
    var
    (if (equal (car vars) var)
      (car args)
      (sub-var (cdr vars) (cdr args) var))))

(defun sub-es (vars args es)
  (if (atom es)
    '()
    (if (var? (car es))
      (cons (sub-var vars args (car es))
        (sub-es vars args (cdr es)))
      (if (quote? (car es))
        (cons (car es)
          (sub-es vars args (cdr es)))
        (if (if? (car es))
          (cons
            (QAE-if
              (sub-es vars args
                (if-QAE (car es))))
            (sub-es vars args (cdr es)))
          (cons
            (app-c (app.name (car es))
              (sub-es vars args
                (app.args (car es))))
            (sub-es vars args (cdr es))))))))
(defun sub-e (vars args e)
  (elem1 (sub-es vars args (list1 e))))

(defun exprs-recs (f es)
  (if (atom es)
    '()
    (if (var? (car es))
      (exprs-recs f (cdr es))
      (if (quote? (car es))
        (exprs-recs f (cdr es))
        (if (if? (car es))
          (list-union
            (exprs-recs f (if-QAE (car es)))
            (exprs-recs f (cdr es)))
          (if (equal (app.name (car es)) f)
            (list-union
              (list1 (car es))
              (list-union
                (exprs-recs f
                  (app.args (car es)))
                (exprs-recs f (cdr es))))
            (list-union
              (exprs-recs f (app.args (car es)))
              (exprs-recs f
                (cdr es)))))))))
(defun expr-recs (f e)
  (exprs-recs f (list1 e)))

(defun totality/< (meas formals app)
  (app-c '<
    (list2 (sub-e formals (app.args app) meas)
      meas)))

(defun totality/meas (meas formals apps)
  (if (atom apps)
    '()
    (cons
      (totality/< meas formals (car apps))
      (totality/meas meas formals (cdr apps)))))

(defun totality/if (meas f formals e)
  (if (if? e)
    (conjunction
      (list-extend
        (totality/meas meas formals
          (expr-recs f (if.Q e)))
        (if-c-when-necessary (if.Q e)
          (totality/if meas f formals
            (if.A e))
          (totality/if meas f formals
            (if.E e)))))
    (conjunction
      (totality/meas meas formals
        (expr-recs f e)))))

(defun totality/claim (meas def)
  (if (equal meas 'nil)
    (if (equal (expr-recs (defun.name def)
                 (defun.body def))
               '())
      (quote-c 't)
      (quote-c 'nil))
    (if-c
      (app-c 'natp (list1 meas))
      (totality/if meas (defun.name def)
        (defun.formals def)
        (defun.body def))
      (quote-c 'nil))))

(defun induction/prems (vars claim apps)
  (if (atom apps)
    '()
    (cons
      (sub-e vars (app.args (car apps)) claim)
      (induction/prems vars claim (cdr apps)))))

(defun induction/if (vars claim f e)
  (if (if? e)
    (implication
      (induction/prems vars claim
        (expr-recs f (if.Q e)))
      (if-c-when-necessary (if.Q e)
        (induction/if vars claim f (if.A e))
        (induction/if vars claim f (if.E e))))
    (implication
      (induction/prems vars claim
        (expr-recs f e))
      claim)))

(defun induction/defun (vars claim def)
  (induction/if vars claim (defun.name def)
    (sub-e (defun.formals def) vars
      (defun.body def))))

(defun induction/claim (defs seed def)
  (if (equal seed 'nil)
    (dethm.body def)
    (induction/defun (app.args seed)
      (dethm.body def)
      (lookup (app.name seed) defs))))

(defun find-focus-at-direction (dir e)
  (if (equal dir 'Q)
    (if.Q e)
    (if (equal dir 'A)
      (if.A e)
      (if (equal dir 'E)
        (if.E e)
        (get-arg dir (app.args e))))))

(defun rewrite-focus-at-direction (dir e1 e2)
  (if (equal dir 'Q)
    (if-c e2 (if.A e1) (if.E e1))
    (if (equal dir 'A)
      (if-c (if.Q e1) e2 (if.E e1))
      (if (equal dir 'E)
        (if-c (if.Q e1) (if.A e1) e2)
        (app-c (app.name e1)
          (set-arg dir (app.args e1) e2))))))

(defun focus-is-at-direction? (dir e)
  (if (equal dir 'Q)
    (if? e)
    (if (equal dir 'A)
      (if? e)
      (if (equal dir 'E)
        (if? e)
        (if (app? e)
          (<=len dir (app.args e))
          'nil)))))

(defun focus-is-at-path? (path e)
  (if (atom path)
    't
    (if (focus-is-at-direction? (car path) e)
      (focus-is-at-path? (cdr path)
        (find-focus-at-direction (car path) e))
      'nil)))

(defun find-focus-at-path (path e)
  (if (atom path)
    e
    (find-focus-at-path (cdr path)
      (find-focus-at-direction (car path) e))))

(defun rewrite-focus-at-path (path e1 e2)
  (if (atom path)
    e2
    (rewrite-focus-at-direction (car path) e1
      (rewrite-focus-at-path (cdr path)
        (find-focus-at-direction (car path) e1)
        e2))))

(defun prem-A? (prem path e)
  (if (atom path)
    'nil
    (if (equal (car path) 'A)
      (if (equal (if.Q e) prem)
        't
        (prem-A? prem (cdr path)
          (find-focus-at-direction (car path)
            e)))
      (prem-A? prem (cdr path)
        (find-focus-at-direction (car path)
          e)))))

(defun prem-E? (prem path e)
  (if (atom path)
    'nil
    (if (equal (car path) 'E)
      (if (equal (if.Q e) prem)
        't
        (prem-E? prem (cdr path)
          (find-focus-at-direction (car path)
            e)))
      (prem-E? prem (cdr path)
        (find-focus-at-direction (car path)
          e)))))

(defun follow-prems (path e thm)
  (if (if? thm)
    (if (prem-A? (if.Q thm) path e)
      (follow-prems path e (if.A thm))
      (if (prem-E? (if.Q thm) path e)
        (follow-prems path e (if.E thm))
        thm))
    thm))

(defun unary-op (rator rand)
  (if (equal rator 'atom)
    (atom rand)
    (if (equal rator 'car)
      (car rand)
      (if (equal rator 'cdr)
        (cdr rand)
        (if (equal rator 'natp)
          (natp rand)
          (if (equal rator 'size)
            (size rand)
            'nil))))))

(defun binary-op (rator rand1 rand2)
  (if (equal rator 'equal)
    (equal rand1 rand2)
    (if (equal rator 'cons)
      (cons rand1 rand2)
      (if (equal rator '+)
        (+ rand1 rand2)
        (if (equal rator '<)
          (< rand1 rand2)
          'nil)))))

(defun apply-op (rator rands)
  (if (member? rator '(atom car cdr natp size))
    (unary-op rator (elem1 rands))
    (if (member? rator '(equal cons + <))
      (binary-op rator
        (elem1 rands)
        (elem2 rands))
      'nil)))

(defun rands (args)
  (if (atom args)
    '()
    (cons (quote.value (car args))
      (rands (cdr args)))))

(defun eval-op (app)
  (quote-c
    (apply-op (app.name app)
      (rands (app.args app)))))

(defun app-of-equal? (e)
  (if (app? e)
    (equal (app.name e) 'equal)
    'nil))

(defun equality (focus a b)
  (if (equal focus a)
    b
    (if (equal focus b)
      a
      focus)))

(defun equality/equation (focus concl-inst)
  (if (app-of-equal? concl-inst)
    (equality focus
      (elem1 (app.args concl-inst))
      (elem2 (app.args concl-inst)))
    focus))

(defun equality/path (e path thm)
  (if (focus-is-at-path? path e)
    (rewrite-focus-at-path path e
      (equality/equation
        (find-focus-at-path path e)
        (follow-prems path e thm)))
    e))

(defun equality/def (claim path app def)
  (if (rator? def)
    (equality/path claim path
      (app-c 'equal (list2 app (eval-op app))))
    (if (defun? def)
      (equality/path claim path
        (sub-e (defun.formals def)
          (app.args app)
          (app-c 'equal
            (list2
              (app-c (defun.name def)
                (defun.formals def))
              (defun.body def)))))
      (if (dethm? def)
        (equality/path claim path
          (sub-e (dethm.formals def)
            (app.args app)
            (dethm.body def)))
        claim))))

(defun rewrite/step (defs claim step)
  (equality/def claim (elem1 step) (elem2 step)
    (lookup (app.name (elem2 step)) defs)))

(defun rewrite/continue (defs steps old new)
  (if (equal new old)
    new
    (if (atom steps)
      new
      (rewrite/continue defs (cdr steps) new
        (rewrite/step defs new (car steps))))))

(defun rewrite/steps (defs claim steps)
  (if (atom steps)
    claim
    (rewrite/continue defs (cdr steps) claim
      (rewrite/step defs claim (car steps)))))

(defun rewrite/prove (defs def seed steps)
  (if (defun? def)
    (rewrite/steps defs
      (totality/claim seed def)
      steps)
    (if (dethm? def)
      (rewrite/steps defs
        (induction/claim defs seed def)
        steps)
      (quote-c 'nil))))

(defun rewrite/prove+1 (defs pf e)
  (if (equal e (quote-c 't))
    (rewrite/prove defs (elem1 pf) (elem2 pf)
      (cdr (cdr pf)))
    e))

(defun rewrite/prove+ (defs pfs)
  (if (atom pfs)
    (quote-c 't)
    (rewrite/prove+1 defs (car pfs)
      (rewrite/prove+
        (list-extend defs (elem1 (car pfs)))
        (cdr pfs)))))

(defun rewrite/define (defs def seed steps)
  (if (equal (rewrite/prove defs def seed steps)
             (quote-c 't))
    (list-extend defs def)
    defs))

(defun rewrite/define+1 (defs1 defs2 pfs)
  (if (equal defs1 defs2)
    defs1
    (if (atom pfs)
      defs2
      (rewrite/define+1 defs2
        (rewrite/define defs2
          (elem1 (car pfs))
          (elem2 (car pfs))
          (cdr (cdr (car pfs))))
        (cdr pfs)))))

(defun rewrite/define+ (defs pfs)
  (if (atom pfs)
    defs
    (rewrite/define+1 defs
      (rewrite/define defs
        (elem1 (car pfs))
        (elem2 (car pfs))
        (cdr (cdr (car pfs))))
      (cdr pfs))))

(defun J-Bob/step (defs e steps)
  (if (defs? '() defs)
    (if (expr? defs 'any e)
      (if (steps? defs steps)
        (rewrite/steps defs e steps)
        e)
      e)
    e))

(defun J-Bob/prove (defs pfs)
  (if (defs? '() defs)
    (if (proofs? defs pfs)
      (rewrite/prove+ defs pfs)
      (quote-c 'nil))
    (quote-c 'nil)))

(defun J-Bob/define (defs pfs)
  (if (defs? '() defs)
    (if (proofs? defs pfs)
      (rewrite/define+ defs pfs)
      defs)
    defs))

(defun axioms ()
  '((dethm atom/cons (x y)
      (equal (atom (cons x y)) 'nil))
    (dethm car/cons (x y)
      (equal (car (cons x y)) x))
    (dethm cdr/cons (x y)
      (equal (cdr (cons x y)) y))
    (dethm equal-same (x)
      (equal (equal x x) 't))
    (dethm equal-swap (x y)
      (equal (equal x y) (equal y x)))
    (dethm if-same (x y)
      (equal (if x y y) y))
    (dethm if-true (x y)
      (equal (if 't x y) x))
    (dethm if-false (x y)
      (equal (if 'nil x y) y))
    (dethm if-nest-E (x y z)
      (if x 't (equal (if x y z) z)))
    (dethm if-nest-A (x y z)
      (if x (equal (if x y z) y) 't))
    (dethm cons/car+cdr (x)
      (if (atom x)
        't
        (equal (cons (car x) (cdr x)) x)))
    (dethm equal-if (x y)
      (if (equal x y) (equal x y) 't))
    (dethm natp/size (x)
      (equal (natp (size x)) 't))
    (dethm size/car (x)
      (if (atom x)
        't
        (equal (< (size (car x)) (size x)) 't)))
    (dethm size/cdr (x)
      (if (atom x)
        't
        (equal (< (size (cdr x)) (size x)) 't)))
    (dethm associate-+ (a b c)
      (equal (+ (+ a b) c) (+ a (+ b c))))
    (dethm commute-+ (x y)
      (equal (+ x y) (+ y x)))
    (dethm natp/+ (x y)
      (if (natp x)
        (if (natp y)
          (equal (natp (+ x y)) 't)
          't)
        't))
    (dethm positives-+ (x y)
      (if (< '0 x)
        (if (< '0 y)
          (equal (< '0 (+ x y)) 't)
          't)
        't))
    (dethm common-addends-< (x y z)
      (equal (< (+ x z) (+ y z)) (< x y)))
    (dethm identity-+ (x)
      (if (natp x) (equal (+ '0 x) x) 't))))

(defun prelude ()
  (J-Bob/define (axioms)
    '(((defun list-induction (x)
         (if (atom x)
           '()
           (cons (car x)
             (list-induction (cdr x)))))
       (size x)
       ((A E) (size/cdr x))
       ((A) (if-same (atom x) 't))
       ((Q) (natp/size x))
       (() (if-true 't 'nil)))
      ((defun star-induction (x)
         (if (atom x)
           x
           (cons (star-induction (car x))
             (star-induction (cdr x)))))
       (size x)
       ((A E A) (size/cdr x))
       ((A E Q) (size/car x))
       ((A E) (if-true 't 'nil))
       ((A) (if-same (atom x) 't))
       ((Q) (natp/size x))
       (() (if-true 't 'nil))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;; Chapter 1

(defun chapter1.example1 ()
  (J-Bob/step (prelude)
    '(car (cons 'ham '(eggs)))
    '(((1) (cons 'ham '(eggs)))
      (() (car '(ham eggs))))))

(defun chapter1.example2 ()
  (J-Bob/step (prelude)
    '(atom '())
    '((() (atom '())))))

(defun chapter1.example3 ()
  (J-Bob/step (prelude)
    '(atom (cons 'ham '(eggs)))
    '(((1) (cons 'ham '(eggs)))
      (() (atom '(ham eggs))))))

(defun chapter1.example4 ()
  (J-Bob/step (prelude)
    '(atom (cons a b))
    '((() (atom/cons a b)))))

(defun chapter1.example5 ()
  (J-Bob/step (prelude)
    '(equal 'flapjack (atom (cons a b)))
    '(((2) (atom/cons a b))
      (() (equal 'flapjack 'nil)))))

(defun chapter1.example6 ()
  (J-Bob/step (prelude)
    '(atom (cdr (cons (car (cons p q)) '())))
    '(((1 1 1) (car/cons p q))
      ((1) (cdr/cons p '()))
      (() (atom '())))))

(defun chapter1.example7 ()
  (J-Bob/step (prelude)
    '(atom (cdr (cons (car (cons p q)) '())))
    '(((1) (cdr/cons (car (cons p q)) '()))
      (() (atom '())))))

(defun chapter1.example8 ()
  (J-Bob/step (prelude)
    '(car (cons (equal (cons x y) (cons x y)) '(and crumpets)))
    '(((1 1) (equal-same (cons x y)))
      ((1) (cons 't '(and crumpets)))
      (() (car '(t and crumpets))))))

(defun chapter1.example9 ()
  (J-Bob/step (prelude)
    '(equal (cons x y) (cons 'bagels '(and lox)))
    '((() (equal-swap (cons x y) (cons 'bagels '(and lox)))))))

(defun chapter1.example10 ()
  (J-Bob/step (prelude)
    '(cons y (equal (car (cons (cdr x) (car y))) (equal (atom x) 'nil)))
    '(((2 1) (car/cons (cdr x) (car y))))))

(defun chapter1.example11 ()
  (J-Bob/step (prelude)
    '(cons y (equal (car (cons (cdr x) (car y))) (equal (atom x) 'nil)))
    '(((2 1) (car/cons (car (cons (cdr x) (car y))) '(oats)))
      ((2 2 2) (atom/cons (atom (cdr (cons a b))) (equal (cons a b) c)))
      ((2 2 2 1 1 1) (cdr/cons a b))
      ((2 2 2 1 2) (equal-swap (cons a b) c)))))

(defun chapter1.example12 ()
  (J-Bob/step (prelude)
    '(atom (car (cons (car a) (cdr b))))
    '(((1) (car/cons (car a) (cdr b))))))

;; Chapter 2

(defun chapter2.example1 ()
  (J-Bob/step (prelude)
    '(if (car (cons a b)) c c)
    '(((Q) (car/cons a b))
      (() (if-same a c))
      (()
       (if-same
         (if (equal a 't) (if (equal 'nil 'nil) a b) (equal 'or (cons 'black '(coffee))))
         c))
      ((Q E 2) (cons 'black '(coffee)))
      ((Q A Q) (equal-same 'nil))
      ((Q A) (if-true a b))
      ((Q A) (equal-if a 't)))))

(defun chapter2.example2 ()
  (J-Bob/step (prelude)
    '(if (atom (car a))
         (if (equal (car a) (cdr a)) 'hominy 'grits)
         (if (equal (cdr (car a)) '(hash browns))
             (cons 'ketchup (car a))
             (cons 'mustard (car a))))
    '(((E A 2) (cons/car+cdr (car a)))
      ((E A 2 2) (equal-if (cdr (car a)) '(hash browns))))))

(defun chapter2.example3 ()
  (J-Bob/step (prelude)
    '(cons 'statement
       (cons (if (equal a 'question) (cons n '(answer)) (cons n '(else)))
         (if (equal a 'question) (cons n '(other answer)) (cons n '(other else)))))
    '(((2)
       (if-same (equal a 'question)
         (cons (if (equal a 'question) (cons n '(answer)) (cons n '(else)))
           (if (equal a 'question) (cons n '(other answer)) (cons n '(other else))))))
      ((2 A 1) (if-nest-A (equal a 'question) (cons n '(answer)) (cons n '(else))))
      ((2 E 1) (if-nest-E (equal a 'question) (cons n '(answer)) (cons n '(else))))
      ((2 A 2)
       (if-nest-A (equal a 'question) (cons n '(other answer)) (cons n '(other else))))
      ((2 E 2)
       (if-nest-E (equal a 'question)
         (cons n '(other answer))
         (cons n '(other else)))))))

;; Chapter 3

(defun defun.pair ()
  (J-Bob/define (prelude)
    '(((defun pair (x y)
         (cons x (cons y '())))
       nil))))

(defun defun.first-of ()
  (J-Bob/define (defun.pair)
    '(((defun first-of (x)
         (car x))
       nil))))

(defun defun.second-of ()
  (J-Bob/define (defun.first-of)
    '(((defun second-of (x)
         (car (cdr x)))
       nil))))

(defun dethm.first-of-pair ()
  (J-Bob/define (defun.second-of)
    '(((dethm first-of-pair (a b)
         (equal (first-of (pair a b)) a))
       nil
       ((1 1) (pair a b))
       ((1) (first-of (cons a (cons b '()))))
       ((1) (car/cons a (cons b '())))
       (() (equal-same a))))))

(defun dethm.second-of-pair ()
  (J-Bob/define (dethm.first-of-pair)
    '(((dethm second-of-pair (a b)
         (equal (second-of (pair a b)) b))
       nil
       ((1) (second-of (pair a b)))
       ((1 1 1) (pair a b))
       ((1 1) (cdr/cons a (cons b '())))
       ((1) (car/cons b '()))
       (() (equal-same b))))))

(defun defun.in-pair? ()
  (J-Bob/define (dethm.second-of-pair)
    '(((defun in-pair? (xs)
         (if (equal (first-of xs) '?) 't (equal (second-of xs) '?)))
       nil))))

(defun dethm.in-first-of-pair ()
  (J-Bob/define (defun.in-pair?)
    '(((dethm in-first-of-pair (b)
         (equal (in-pair? (pair '? b)) 't))
       nil
       ((1 1) (pair '? b))
       ((1) (in-pair? (cons '? (cons b '()))))
       ((1 Q 1) (first-of (cons '? (cons b '()))))
       ((1 Q 1) (car/cons '? (cons b '())))
       ((1 Q) (equal-same '?))
       ((1) (if-true 't (equal (second-of (cons '? (cons b '()))) '?)))
       (() (equal-same 't))))))

(defun dethm.in-second-of-pair ()
  (J-Bob/define (dethm.in-first-of-pair)
    '(((dethm in-second-of-pair (a)
         (equal (in-pair? (pair a '?)) 't))
       nil
       ((1 1) (pair a '?))
       ((1) (in-pair? (cons a (cons '? '()))))
       ((1 Q 1) (first-of (cons a (cons '? '()))))
       ((1 Q 1) (car/cons a (cons '? '())))
       ((1 E 1) (second-of (cons a (cons '? '()))))
       ((1 E 1 1) (cdr/cons a (cons '? '())))
       ((1 E 1) (car/cons '? '()))
       ((1 E) (equal-same '?))
       ((1) (if-same (equal a '?) 't))
       (() (equal-same 't))))))

;; Chapter 4

(defun defun.list0? ()
  (J-Bob/define (dethm.in-second-of-pair)
    '(((defun list0? (x)
         (equal x '()))
       nil))))

(defun defun.list1? ()
  (J-Bob/define (defun.list0?)
    '(((defun list1? (x)
         (if (atom x) 'nil (list0? (cdr x))))
       nil))))

(defun defun.list2? ()
  (J-Bob/define (defun.list1?)
    '(((defun list2? (x)
         (if (atom x) 'nil (list1? (cdr x))))
       nil))))

(defun dethm.contradiction ()
  (J-Bob/prove
    (list-extend (prelude)
      '(defun partial (x)
         (if (partial x) 'nil 't)))
    '(((dethm contradiction () 'nil)
       nil
       (() (if-same (partial x) 'nil))
       ((A) (if-nest-A (partial x) 'nil 't))
       ((E) (if-nest-E (partial x) 't 'nil))
       ((A Q) (partial x))
       ((E Q) (partial x))
       ((A Q) (if-nest-A (partial x) 'nil 't))
       ((E Q) (if-nest-E (partial x) 'nil 't))
       ((A) (if-false 'nil 't))
       ((E) (if-true 't 'nil))
       (() (if-same (partial x) 't))))))

(defun defun.list? ()
  (J-Bob/define (defun.list2?)
    '(((defun list? (x)
         (if (atom x) (equal x '()) (list? (cdr x))))
       (size x)
       ((Q) (natp/size x))
       (() (if-true (if (atom x) 't (< (size (cdr x)) (size x))) 'nil))
       ((E) (size/cdr x))
       (() (if-same (atom x) 't))))))

(defun defun.sub ()
  (J-Bob/define (defun.list?)
    '(((defun sub (x y)
         (if (atom y) (if (equal y '?) x y) (cons (sub x (car y)) (sub x (cdr y)))))
       (size y)
       ((Q) (natp/size y))
       (()
        (if-true
          (if (atom y)
              't
              (if (< (size (car y)) (size y)) (< (size (cdr y)) (size y)) 'nil))
          'nil))
       ((E Q) (size/car y))
       ((E A) (size/cdr y))
       ((E) (if-true 't 'nil))
       (() (if-same (atom y) 't))))))

;; Chapter 5

(defun defun.memb? ()
  (J-Bob/define (defun.sub)
    '(((defun memb? (xs)
         (if (atom xs) 'nil (if (equal (car xs) '?) 't (memb? (cdr xs)))))
       (size xs)
       ((Q) (natp/size xs))
       (()
        (if-true
          (if (atom xs) 't (if (equal (car xs) '?) 't (< (size (cdr xs)) (size xs))))
          'nil))
       ((E E) (size/cdr xs))
       ((E) (if-same (equal (car xs) '?) 't))
       (() (if-same (atom xs) 't))))))

(defun defun.remb ()
  (J-Bob/define (defun.memb?)
    '(((defun remb (xs)
         (if (atom xs)
             '()
             (if (equal (car xs) '?) (remb (cdr xs)) (cons (car xs) (remb (cdr xs))))))
       (size xs)
       ((Q) (natp/size xs))
       (() (if-true (if (atom xs) 't (< (size (cdr xs)) (size xs))) 'nil))
       ((E) (size/cdr xs))
       (() (if-same (atom xs) 't))))))

(defun dethm.memb?/remb0 ()
  (J-Bob/define (defun.remb)
    '(((dethm memb?/remb0 ()
         (equal (memb? (remb '())) 'nil))
       nil
       ((1 1) (remb '()))
       ((1 1 Q) (atom '()))
       ((1 1)
        (if-true '()
          (if (equal (car '()) '?) (remb (cdr '())) (cons (car '()) (remb (cdr '()))))))
       ((1) (memb? '()))
       ((1 Q) (atom '()))
       ((1) (if-true 'nil (if (equal (car '()) '?) 't (memb? (cdr '())))))
       (() (equal-same 'nil))))))

(defun dethm.memb?/remb1 ()
  (J-Bob/define (dethm.memb?/remb0)
    '(((dethm memb?/remb1 (x1)
         (equal (memb? (remb (cons x1 '()))) 'nil))
       nil
       ((1 1) (remb (cons x1 '())))
       ((1 1 Q) (atom/cons x1 '()))
       ((1 1)
        (if-false '()
          (if (equal (car (cons x1 '())) '?)
              (remb (cdr (cons x1 '())))
              (cons (car (cons x1 '())) (remb (cdr (cons x1 '())))))))
       ((1 1 Q 1) (car/cons x1 '()))
       ((1 1 A 1) (cdr/cons x1 '()))
       ((1 1 E 1) (car/cons x1 '()))
       ((1 1 E 2 1) (cdr/cons x1 '()))
       ((1)
        (if-same (equal x1 '?)
          (memb? (if (equal x1 '?) (remb '()) (cons x1 (remb '()))))))
       ((1 A 1) (if-nest-A (equal x1 '?) (remb '()) (cons x1 (remb '()))))
       ((1 E 1) (if-nest-E (equal x1 '?) (remb '()) (cons x1 (remb '()))))
       ((1 A) (memb?/remb0))
       ((1 E) (memb? (cons x1 (remb '()))))
       ((1 E Q) (atom/cons x1 (remb '())))
       ((1 E)
        (if-false 'nil
          (if (equal (car (cons x1 (remb '()))) '?)
              't
              (memb? (cdr (cons x1 (remb '())))))))
       ((1 E Q 1) (car/cons x1 (remb '())))
       ((1 E E 1) (cdr/cons x1 (remb '())))
       ((1 E) (if-nest-E (equal x1 '?) 't (memb? (remb '()))))
       ((1 E) (memb?/remb0))
       ((1) (if-same (equal x1 '?) 'nil))
       (() (equal-same 'nil))))))

(defun dethm.memb?/remb2 ()
  (J-Bob/define (dethm.memb?/remb1)
    '(((dethm memb?/remb2 (x1 x2)
         (equal (memb? (remb (cons x2 (cons x1 '())))) 'nil))
       nil
       ((1 1) (remb (cons x2 (cons x1 '()))))
       ((1 1 Q) (atom/cons x2 (cons x1 '())))
       ((1 1)
        (if-false '()
          (if (equal (car (cons x2 (cons x1 '()))) '?)
              (remb (cdr (cons x2 (cons x1 '()))))
              (cons (car (cons x2 (cons x1 '())))
                (remb (cdr (cons x2 (cons x1 '()))))))))
       ((1 1 Q 1) (car/cons x2 (cons x1 '())))
       ((1 1 A 1) (cdr/cons x2 (cons x1 '())))
       ((1 1 E 1) (car/cons x2 (cons x1 '())))
       ((1 1 E 2 1) (cdr/cons x2 (cons x1 '())))
       ((1)
        (if-same (equal x2 '?)
          (memb?
            (if (equal x2 '?) (remb (cons x1 '())) (cons x2 (remb (cons x1 '())))))))
       ((1 A 1)
        (if-nest-A (equal x2 '?) (remb (cons x1 '())) (cons x2 (remb (cons x1 '())))))
       ((1 E 1)
        (if-nest-E (equal x2 '?) (remb (cons x1 '())) (cons x2 (remb (cons x1 '())))))
       ((1 A) (memb?/remb1 x1))
       ((1 E) (memb? (cons x2 (remb (cons x1 '())))))
       ((1 E Q) (atom/cons x2 (remb (cons x1 '()))))
       ((1 E)
        (if-false 'nil
          (if (equal (car (cons x2 (remb (cons x1 '())))) '?)
              't
              (memb? (cdr (cons x2 (remb (cons x1 '()))))))))
       ((1 E Q 1) (car/cons x2 (remb (cons x1 '()))))
       ((1 E E 1) (cdr/cons x2 (remb (cons x1 '()))))
       ((1 E) (if-nest-E (equal x2 '?) 't (memb? (remb (cons x1 '())))))
       ((1 E) (memb?/remb1 x1))
       ((1) (if-same (equal x2 '?) 'nil))
       (() (equal-same 'nil))))))

;; Chapter 6

(defun dethm.memb?/remb ()
  (J-Bob/define (dethm.memb?/remb2)
    '(((dethm memb?/remb (xs)
         (equal (memb? (remb xs)) 'nil))
       (list-induction xs)
       ((A 1 1) (remb xs))
       ((A 1 1)
        (if-nest-A (atom xs)
          '()
          (if (equal (car xs) '?) (remb (cdr xs)) (cons (car xs) (remb (cdr xs))))))
       ((A 1) (memb? '()))
       ((A 1 Q) (atom '()))
       ((A 1) (if-true 'nil (if (equal (car '()) '?) 't  (memb? (cdr '())))))
       ((A) (equal-same 'nil))
       ((E A 1 1) (remb xs))
       ((E A 1 1)
        (if-nest-E (atom xs)
          '()
          (if (equal (car xs) '?) (remb (cdr xs)) (cons (car xs) (remb (cdr xs))))))
       ((E A 1)
        (if-same (equal (car xs) '?)
          (memb?
            (if (equal (car xs) '?) (remb (cdr xs)) (cons (car xs) (remb (cdr xs)))))))
       ((E A 1 A 1)
        (if-nest-A (equal (car xs) '?) (remb (cdr xs)) (cons (car xs) (remb (cdr xs)))))
       ((E A 1 E 1)
        (if-nest-E (equal (car xs) '?) (remb (cdr xs)) (cons (car xs) (remb (cdr xs)))))
       ((E A 1 A) (equal-if (memb? (remb (cdr xs))) 'nil))
       ((E A 1 E) (memb? (cons (car xs) (remb (cdr xs)))))
       ((E A 1 E Q) (atom/cons (car xs) (remb (cdr xs))))
       ((E A 1 E)
        (if-false 'nil
          (if (equal (car (cons (car xs) (remb (cdr xs)))) '?)
              't
              (memb? (cdr (cons (car xs) (remb (cdr xs))))))))
       ((E A 1 E Q 1) (car/cons (car xs) (remb (cdr xs))))
       ((E A 1 E E 1) (cdr/cons (car xs) (remb (cdr xs))))
       ((E A 1 E) (if-nest-E (equal (car xs) '?) 't (memb? (remb (cdr xs)))))
       ((E A 1 E) (equal-if (memb? (remb (cdr xs))) 'nil))
       ((E A 1) (if-same (equal (car xs) '?) 'nil))
       ((E A) (equal-same 'nil))
       ((E) (if-same (equal (memb? (remb (cdr xs))) 'nil) 't))
       (() (if-same (atom xs) 't))))))

;; Chapter 7

(defun defun.ctx? ()
  (J-Bob/define (dethm.memb?/remb)
    '(((defun ctx? (x)
         (if (atom x) (equal x '?) (if (ctx? (car x)) 't (ctx? (cdr x)))))
       (size x)
       ((Q) (natp/size x))
       (()
        (if-true
          (if (atom x)
              't
              (if (< (size (car x)) (size x))
                  (if (ctx? (car x)) 't (< (size (cdr x)) (size x)))
                  'nil))
          'nil))
       ((E Q) (size/car x))
       ((E A E) (size/cdr x))
       ((E A) (if-same (ctx? (car x)) 't))
       ((E) (if-true 't 'nil))
       (() (if-same (atom x) 't))))))

(defun dethm.ctx?/sub ()
  (J-Bob/define (defun.ctx?)
    '(((dethm ctx?/t (x)
         (if (ctx? x) (equal (ctx? x) 't) 't))
       (star-induction x)
       ((A A 1) (ctx? x))
       ((A A 1) (if-nest-A (atom x) (equal x '?) (if (ctx? (car x)) 't (ctx? (cdr x)))))
       ((A Q) (ctx? x))
       ((A Q) (if-nest-A (atom x) (equal x '?) (if (ctx? (car x)) 't (ctx? (cdr x)))))
       ((A A 1 1) (equal-if x '?))
       ((A A 1) (equal-same '?))
       ((A A) (equal-same 't))
       ((A) (if-same (equal x '?) 't))
       ((E A A A 1) (ctx? x))
       ((E A A A 1)
        (if-nest-E (atom x) (equal x '?) (if (ctx? (car x)) 't (ctx? (cdr x)))))
       ((E)
        (if-same (ctx? (car x))
          (if (if (ctx? (car x)) (equal (ctx? (car x)) 't) 't)
              (if (if (ctx? (cdr x)) (equal (ctx? (cdr x)) 't) 't)
                  (if (ctx? x) (equal (if (ctx? (car x)) 't (ctx? (cdr x))) 't) 't)
                  't)
              't)))
       ((E A Q)	(if-nest-A (ctx? (car x)) (equal (ctx? (car x)) 't) 't))
       ((E A A A A 1) (if-nest-A (ctx? (car x)) 't (ctx? (cdr x))))
       ((E E Q) (if-nest-E (ctx? (car x)) (equal (ctx? (car x)) 't) 't))
       ((E E A A A 1) (if-nest-E (ctx? (car x)) 't (ctx? (cdr x))))
       ((E A A A A) (equal-same 't))
       ((E E)
        (if-true
          (if (if (ctx? (cdr x)) (equal (ctx? (cdr x)) 't) 't)
              (if (ctx? x) (equal (ctx? (cdr x)) 't) 't)
              't)
          't))
       ((E A A A) (if-same (ctx? x) 't))
       ((E A A)	(if-same (if (ctx? (cdr x)) (equal (ctx? (cdr x)) 't) 't) 't))
       ((E A) (if-same (equal (ctx? (car x)) 't) 't))
       ((E E A Q) (ctx? x))
       ((E E A Q)
        (if-nest-E (atom x) (equal x '?) (if (ctx? (car x)) 't (ctx? (cdr x)))))
       ((E E A Q) (if-nest-E (ctx? (car x)) 't (ctx? (cdr x))))
       ((E E)
        (if-same (ctx? (cdr x))
          (if (if (ctx? (cdr x)) (equal (ctx? (cdr x)) 't) 't)
              (if (ctx? (cdr x)) (equal (ctx? (cdr x)) 't) 't)
              't)))
       ((E E A Q)(if-nest-A (ctx? (cdr x)) (equal (ctx? (cdr x)) 't) 't))
       ((E E A A)(if-nest-A (ctx? (cdr x)) (equal (ctx? (cdr x)) 't) 't))
       ((E E E Q)(if-nest-E (ctx? (cdr x)) (equal (ctx? (cdr x)) 't) 't))
       ((E E E A)(if-nest-E (ctx? (cdr x)) (equal (ctx? (cdr x)) 't) 't))
       ((E E E) (if-same 't 't))
       ((E E A A 1) (equal-if (ctx? (cdr x)) 't))
       ((E E A A) (equal-same 't))
       ((E E A) (if-same (equal (ctx? (cdr x)) 't) 't))
       ((E E) (if-same (ctx? (cdr x)) 't))
       ((E) (if-same (ctx? (car x)) 't))
       (() (if-same (atom x) 't)))
      ((dethm ctx?/sub (x y)
         (if (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) 't) 't) 't))
       (star-induction y)
       (()
        (if-same (ctx? x)
          (if (atom y)
              (if (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) 't) 't) 't)
              (if (if (ctx? x)
                      (if (ctx? (car y)) (equal (ctx? (sub x (car y))) 't) 't)
                      't)
                  (if (if (ctx? x)
                          (if (ctx? (cdr y)) (equal (ctx? (sub x (cdr y))) 't) 't)
                          't)
                      (if (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) 't) 't) 't)
                      't)
                  't))))
       ((A A) (if-nest-A (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) 't) 't) 't))
       ((A E Q)
        (if-nest-A (ctx? x) (if (ctx? (car y)) (equal (ctx? (sub x (car y))) 't) 't) 't))
       ((A E A Q)
        (if-nest-A (ctx? x) (if (ctx? (cdr y)) (equal (ctx? (sub x (cdr y))) 't) 't) 't))
       ((A E A A) (if-nest-A (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) 't) 't) 't))
       ((E A) (if-nest-E (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) 't) 't) 't))
       ((E E Q)
        (if-nest-E (ctx? x) (if (ctx? (car y)) (equal (ctx? (sub x (car y))) 't) 't) 't))
       ((E E A Q)
        (if-nest-E (ctx? x) (if (ctx? (cdr y)) (equal (ctx? (sub x (cdr y))) 't) 't) 't))
       ((E E A A) (if-nest-E (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) 't) 't) 't))
       ((E E A) (if-same 't 't))
       ((E E) (if-same 't 't))
       ((E) (if-same (atom y) 't))
       ((A A A 1 1) (sub x y))
       ((A A A 1 1)
        (if-nest-A (atom y)
          (if (equal y '?) x y)
          (cons (sub x (car y)) (sub x (cdr y)))))
       ((A A A)	(if-same (equal y '?) (equal (ctx? (if (equal y '?) x y)) 't)))
       ((A A A A 1 1) (if-nest-A (equal y '?) x y))
       ((A A A E 1 1) (if-nest-E (equal y '?) x y))
       ((A A A A 1) (ctx?/t x))
       ((A A A A) (equal-same 't))
       ((A A A E 1) (ctx?/t y))
       ((A A A E) (equal-same 't))
       ((A A A) (if-same (equal y '?) 't))
       ((A A) (if-same (ctx? y) 't))
       ((A E A A A 1 1) (sub x y))
       ((A E A A A 1 1)
        (if-nest-E (atom y)
          (if (equal y '?) x y)
          (cons (sub x (car y)) (sub x (cdr y)))))
       ((A E A A A 1) (ctx? (cons (sub x (car y)) (sub x (cdr y)))))
       ((A E A A A 1 Q) (atom/cons (sub x (car y)) (sub x (cdr y))))
       ((A E A A A 1 E Q 1) (car/cons (sub x (car y)) (sub x (cdr y))))
       ((A E A A A 1 E E 1) (cdr/cons (sub x (car y)) (sub x (cdr y))))
       ((A E A A A 1)
        (if-false (equal (cons (sub x (car y)) (sub x (cdr y))) '?)
          (if (ctx? (sub x (car y))) 't (ctx? (sub x (cdr y))))))
       ((A E A A Q) (ctx? y))
       ((A E A A Q)
        (if-nest-E (atom y) (equal y '?) (if (ctx? (car y)) 't (ctx? (cdr y)))))
       ((A E)
        (if-same (ctx? (car y))
          (if (if (ctx? (car y)) (equal (ctx? (sub x (car y))) 't) 't)
              (if (if (ctx? (cdr y)) (equal (ctx? (sub x (cdr y))) 't) 't)
                  (if (if (ctx? (car y)) 't (ctx? (cdr y)))
                      (equal (if (ctx? (sub x (car y))) 't (ctx? (sub x (cdr y)))) 't)
                      't)
                  't)
              't)))
       ((A E A Q) (if-nest-A (ctx? (car y)) (equal (ctx? (sub x (car y))) 't) 't))
       ((A E A A A Q) (if-nest-A (ctx? (car y)) 't (ctx? (cdr y))))
       ((A E E Q) (if-nest-E (ctx? (car y)) (equal (ctx? (sub x (car y))) 't) 't))
       ((A E E A A Q) (if-nest-E (ctx? (car y)) 't (ctx? (cdr y))))
       ((A E A A A)
        (if-true (equal (if (ctx? (sub x (car y))) 't (ctx? (sub x (cdr y)))) 't) 't))
       ((A E E)
        (if-true
          (if (if (ctx? (cdr y)) (equal (ctx? (sub x (cdr y))) 't) 't)
              (if (ctx? (cdr y))
                  (equal (if (ctx? (sub x (car y))) 't (ctx? (sub x (cdr y)))) 't)
                  't)
              't)
          't))
       ((A E A A A 1 Q) (equal-if (ctx? (sub x (car y))) 't))
       ((A E A A A 1) (if-true 't (ctx? (sub x (cdr y)))))
       ((A E A A A) (equal-same 't))
       ((A E A A) (if-same (if (ctx? (cdr y)) (equal (ctx? (sub x (cdr y))) 't) 't) 't))
       ((A E A) (if-same (equal (ctx? (sub x (car y))) 't) 't))
       ((A E E)
        (if-same (ctx? (cdr y))
          (if (if (ctx? (cdr y)) (equal (ctx? (sub x (cdr y))) 't) 't)
              (if (ctx? (cdr y))
                  (equal (if (ctx? (sub x (car y))) 't (ctx? (sub x (cdr y)))) 't)
                  't)
              't)))
       ((A E E A Q) (if-nest-A (ctx? (cdr y)) (equal (ctx? (sub x (cdr y))) 't) 't))
       ((A E E A A)
        (if-nest-A (ctx? (cdr y))
          (equal (if (ctx? (sub x (car y))) 't (ctx? (sub x (cdr y)))) 't)
          't))
       ((A E E E Q) (if-nest-E (ctx? (cdr y)) (equal (ctx? (sub x (cdr y))) 't) 't))
       ((A E E E A)
        (if-nest-E (ctx? (cdr y))
          (equal (if (ctx? (sub x (car y))) 't (ctx? (sub x (cdr y)))) 't)
          't))
       ((A E E E) (if-same 't 't))
       ((A E E A A 1 E) (equal-if (ctx? (sub x (cdr y))) 't))
       ((A E E A A 1) (if-same (ctx? (sub x (car y))) 't))
       ((A E E A A) (equal-same 't))
       ((A E E A) (if-same (equal (ctx? (sub x (cdr y))) 't) 't))
       ((A E E) (if-same (ctx? (cdr y)) 't))
       ((A E) (if-same (ctx? (car y)) 't))
       ((A) (if-same (atom y) 't))
       (() (if-same (ctx? x) 't))))))

;; Chapter 8

(defun defun.member? ()
  (J-Bob/define (dethm.ctx?/sub)
    '(((defun member? (x ys)
         (if (atom ys) 'nil (if (equal x (car ys)) 't (member? x (cdr ys)))))
       (size ys)
       ((Q) (natp/size ys))
       (()
        (if-true
          (if (atom ys) 't (if (equal x (car ys)) 't (< (size (cdr ys)) (size ys))))
          'nil))
       ((E E) (size/cdr ys))
       ((E) (if-same (equal x (car ys)) 't))
       (() (if-same (atom ys) 't))))))

(defun defun.set? ()
  (J-Bob/define (defun.member?)
    '(((defun set? (xs)
         (if (atom xs) 't (if (member? (car xs) (cdr xs)) 'nil (set? (cdr xs)))))
       (size xs)
       ((Q) (natp/size xs))
       (()
        (if-true
          (if (atom xs)
              't
              (if (member? (car xs) (cdr xs)) 't (< (size (cdr xs)) (size xs))))
          'nil))
       ((E E) (size/cdr xs))
       ((E) (if-same (member? (car xs) (cdr xs)) 't))
       (() (if-same (atom xs) 't))))))

(defun defun.add-atoms ()
  (J-Bob/define (defun.set?)
    '(((defun add-atoms (x ys)
         (if (atom x)
             (if (member? x ys) ys (cons x ys))
             (add-atoms (car x) (add-atoms (cdr x) ys))))
       (size x)
       ((Q) (natp/size x))
       (()
        (if-true
          (if (atom x)
              't
              (if (< (size (car x)) (size x)) (< (size (cdr x)) (size x)) 'nil))
          'nil))
       ((E Q) (size/car x))
       ((E A) (size/cdr x))
       ((E) (if-true 't 'nil))
       (() (if-same (atom x) 't))))))

(defun defun.atoms ()
  (J-Bob/define (defun.add-atoms)
    '(((defun atoms (x)
         (add-atoms x '()))
       nil))))

(defun dethm.set?/atoms.attempt ()
  (J-Bob/prove (defun.atoms)
    '(((dethm set?/add-atoms (a)
         (equal (set? (add-atoms a '())) 't))
       (star-induction a)
       ((E A A 1 1) (add-atoms a '())))
      ((dethm set?/atoms (a)
         (equal (set? (atoms a)) 't))
       nil
       ((1 1) (atoms a))
       ((1) (set?/add-atoms a))
       (() (equal-same 't))))))

(defun dethm.set?/atoms ()
  (J-Bob/define (defun.atoms)
    '(((dethm set?/t (xs)
         (if (set? xs) (equal (set? xs) 't) 't))
       (list-induction xs)
       ((A A 1) (set? xs))
       ((A A 1)
        (if-nest-A (atom xs) 't (if (member? (car xs) (cdr xs)) 'nil (set? (cdr xs)))))
       ((A A) (equal-same 't))
       ((A) (if-same (set? xs) 't))
       ((E A A 1) (set? xs))
       ((E A A 1)
        (if-nest-E (atom xs) 't (if (member? (car xs) (cdr xs)) 'nil (set? (cdr xs)))))
       ((E A Q) (set? xs))
       ((E A Q)
        (if-nest-E (atom xs) 't (if (member? (car xs) (cdr xs)) 'nil (set? (cdr xs)))))
       ((E A)
        (if-same (member? (car xs) (cdr xs))
          (if (if (member? (car xs) (cdr xs)) 'nil (set? (cdr xs)))
              (equal (if (member? (car xs) (cdr xs)) 'nil (set? (cdr xs))) 't)
              't)))
       ((E A A Q) (if-nest-A (member? (car xs) (cdr xs)) 'nil (set? (cdr xs))))
       ((E A A A 1) (if-nest-A (member? (car xs) (cdr xs)) 'nil (set? (cdr xs))))
       ((E A E Q) (if-nest-E (member? (car xs) (cdr xs)) 'nil (set? (cdr xs))))
       ((E A E A 1) (if-nest-E (member? (car xs) (cdr xs)) 'nil (set? (cdr xs))))
       ((E A A) (if-false (equal 'nil 't) 't))
       ((E)
        (if-same (set? (cdr xs))
          (if (if (set? (cdr xs)) (equal (set? (cdr xs)) 't) 't)
              (if (member? (car xs) (cdr xs))
                  't
                  (if (set? (cdr xs)) (equal (set? (cdr xs)) 't) 't))
              't)))
       ((E A Q) (if-nest-A (set? (cdr xs)) (equal (set? (cdr xs)) 't) 't))
       ((E A A E) (if-nest-A (set? (cdr xs)) (equal (set? (cdr xs)) 't) 't))
       ((E E Q) (if-nest-E (set? (cdr xs)) (equal (set? (cdr xs)) 't) 't))
       ((E E A E) (if-nest-E (set? (cdr xs)) (equal (set? (cdr xs)) 't) 't))
       ((E E A) (if-same (member? (car xs) (cdr xs)) 't))
       ((E E) (if-same 't 't))
       ((E A A E 1) (equal-if (set? (cdr xs)) 't))
       ((E A A E) (equal-same 't))
       ((E A A) (if-same (member? (car xs) (cdr xs)) 't))
       ((E A) (if-same (equal (set? (cdr xs)) 't) 't))
       ((E) (if-same (set? (cdr xs)) 't))
       (() (if-same (atom xs) 't)))
      ((dethm set?/nil (xs)
         (if (set? xs) 't (equal (set? xs) 'nil)))
       (list-induction xs)
       ((A Q) (set? xs))
       ((A Q)
        (if-nest-A (atom xs) 't (if (member? (car xs) (cdr xs)) 'nil (set? (cdr xs)))))
       ((A) (if-true 't (equal (set? xs) 'nil)))
       ((E A E 1) (set? xs))
       ((E A E 1)
        (if-nest-E (atom xs) 't (if (member? (car xs) (cdr xs)) 'nil (set? (cdr xs)))))
       ((E A Q) (set? xs))
       ((E A Q)
        (if-nest-E (atom xs) 't (if (member? (car xs) (cdr xs)) 'nil (set? (cdr xs)))))
       ((E A)
        (if-same (member? (car xs) (cdr xs))
          (if (if (member? (car xs) (cdr xs)) 'nil (set? (cdr xs)))
              't
              (equal (if (member? (car xs) (cdr xs)) 'nil (set? (cdr xs))) 'nil))))
       ((E A A Q) (if-nest-A (member? (car xs) (cdr xs)) 'nil (set? (cdr xs))))
       ((E A A E 1) (if-nest-A (member? (car xs) (cdr xs)) 'nil (set? (cdr xs))))
       ((E A E Q) (if-nest-E (member? (car xs) (cdr xs)) 'nil (set? (cdr xs))))
       ((E A E E 1) (if-nest-E (member? (car xs) (cdr xs)) 'nil (set? (cdr xs))))
       ((E A A E) (equal-same 'nil))
       ((E A A) (if-same 'nil 't))
       ((E)
        (if-same (set? (cdr xs))
          (if (if (set? (cdr xs)) 't (equal (set? (cdr xs)) 'nil))
              (if (member? (car xs) (cdr xs))
                  't
                  (if (set? (cdr xs)) 't (equal (set? (cdr xs)) 'nil)))
              't)))
       ((E A Q) (if-nest-A (set? (cdr xs)) 't (equal (set? (cdr xs)) 'nil)))
       ((E A A E) (if-nest-A (set? (cdr xs)) 't (equal (set? (cdr xs)) 'nil)))
       ((E E Q) (if-nest-E (set? (cdr xs)) 't (equal (set? (cdr xs)) 'nil)))
       ((E E A E) (if-nest-E (set? (cdr xs)) 't (equal (set? (cdr xs)) 'nil)))
       ((E A A) (if-same (member? (car xs) (cdr xs)) 't))
       ((E A) (if-same 't 't))
       ((E E A E 1) (equal-if (set? (cdr xs)) 'nil))
       ((E E A E) (equal-same 'nil))
       ((E E A) (if-same (member? (car xs) (cdr xs)) 't))
       ((E E) (if-same (equal (set? (cdr xs)) 'nil) 't))
       ((E) (if-same (set? (cdr xs)) 't))
       (() (if-same (atom xs) 't)))
      ((dethm set?/add-atoms (a bs)
         (if (set? bs) (equal (set? (add-atoms a bs)) 't) 't))
       (add-atoms a bs)
       ((A A 1 1) (add-atoms a bs))
       ((A A 1 1)
        (if-nest-A (atom a)
          (if (member? a bs) bs (cons a bs))
          (add-atoms (car a) (add-atoms (cdr a) bs))))
       ((A A 1) (if-same (member? a bs) (set? (if (member? a bs) bs (cons a bs)))))
       ((A A 1 A 1) (if-nest-A (member? a bs) bs (cons a bs)))
       ((A A 1 E 1) (if-nest-E (member? a bs) bs (cons a bs)))
       ((A A 1 A) (set?/t bs))
       ((A A 1 E) (set? (cons a bs)))
       ((A A 1 E Q) (atom/cons a bs))
       ((A A 1 E E Q 1) (car/cons a bs))
       ((A A 1 E E Q 2) (cdr/cons a bs))
       ((A A 1 E E E 1) (cdr/cons a bs))
       ((A A 1 E) (if-false 't (if (member? a bs) 'nil (set? bs))))
       ((A A 1 E) (if-nest-E (member? a bs) 'nil (set? bs)))
       ((A A 1 E) (set?/t bs))
       ((A A 1) (if-same (member? a bs) 't))
       ((A A) (equal-same 't))
       ((A) (if-same (set? bs) 't))
       ((E)
        (if-same (set? bs)
          (if (if (set? (add-atoms (cdr a) bs))
                  (equal (set? (add-atoms (car a) (add-atoms (cdr a) bs))) 't)
                  't)
              (if (if (set? bs) (equal (set? (add-atoms (cdr a) bs)) 't) 't)
                  (if (set? bs) (equal (set? (add-atoms a bs)) 't) 't)
                  't)
              't)))
       ((E A A Q) (if-nest-A (set? bs) (equal (set? (add-atoms (cdr a) bs)) 't) 't))
       ((E A A A) (if-nest-A (set? bs) (equal (set? (add-atoms a bs)) 't) 't))
       ((E E A Q) (if-nest-E (set? bs) (equal (set? (add-atoms (cdr a) bs)) 't) 't))
       ((E E A A) (if-nest-E (set? bs) (equal (set? (add-atoms a bs)) 't) 't))
       ((E E A) (if-same 't 't))
       ((E E)
        (if-same
          (if (set? (add-atoms (cdr a) bs))
              (equal (set? (add-atoms (car a) (add-atoms (cdr a) bs))) 't)
              't)
          't))
       ((E A)
        (if-same (set? (add-atoms (cdr a) bs))
          (if (if (set? (add-atoms (cdr a) bs))
                  (equal (set? (add-atoms (car a) (add-atoms (cdr a) bs))) 't)
                  't)
              (if (equal (set? (add-atoms (cdr a) bs)) 't)
                  (equal (set? (add-atoms a bs)) 't)
                  't)
              't)))
       ((E A A Q)
        (if-nest-A (set? (add-atoms (cdr a) bs))
          (equal (set? (add-atoms (car a) (add-atoms (cdr a) bs))) 't)
          't))
       ((E A E Q)
        (if-nest-E (set? (add-atoms (cdr a) bs))
          (equal (set? (add-atoms (car a) (add-atoms (cdr a) bs))) 't)
          't))
       ((E A E)
        (if-true
          (if (equal (set? (add-atoms (cdr a) bs)) 't)
              (equal (set? (add-atoms a bs)) 't)
              't)
          't))
       ((E A A A Q 1) (set?/t (add-atoms (cdr a) bs)))
       ((E A E Q 1) (set?/nil (add-atoms (cdr a) bs)))
       ((E A A A Q) (equal 't 't))
       ((E A E Q) (equal 'nil 't))
       ((E A A A) (if-true (equal (set? (add-atoms a bs)) 't) 't))
       ((E A E) (if-false (equal (set? (add-atoms a bs)) 't) 't))
       ((E A A A 1 1) (add-atoms a bs))
       ((E A A A 1 1)
        (if-nest-E (atom a)
          (if (member? a bs) bs (cons a bs))
          (add-atoms (car a) (add-atoms (cdr a) bs))))
       ((E A A A 1) (equal-if (set? (add-atoms (car a) (add-atoms (cdr a) bs))) 't))
       ((E A A A) (equal-same 't))
       ((E A A)
        (if-same (equal (set? (add-atoms (car a) (add-atoms (cdr a) bs))) 't) 't))
       ((E A) (if-same (set? (add-atoms (cdr a) bs)) 't))
       ((E) (if-same (set? bs) 't))
       (() (if-same (atom a) 't)))
      ((dethm set?/atoms (a)
         (equal (set? (atoms a)) 't))
       nil
       ((1 1) (atoms a))
       (() (if-true (equal (set? (add-atoms a '())) 't) 't))
       ((Q) (if-true 't (if (member? (car '()) (cdr '())) 'nil (set? (cdr '())))))
       ((Q Q) (atom '()))
       ((Q) (set? '()))
       ((A 1) (set?/add-atoms a '()))
       ((A) (equal-same 't))
       (() (if-same (set? '()) 't))))))

;; Chapter 9

(defun defun.rotate ()
  (J-Bob/define (dethm.set?/atoms)
    '(((defun rotate (x)
         (cons (car (car x)) (cons (cdr (car x)) (cdr x))))
       nil))))

(defun dethm.rotate/cons ()
  (J-Bob/define (defun.rotate)
    '(((dethm rotate/cons (x y z)
         (equal (rotate (cons (cons x y) z)) (cons x (cons y z))))
       nil
       ((1) (rotate (cons (cons x y) z)))
       ((1 1 1) (car/cons (cons x y) z))
       ((1 1) (car/cons x y))
       ((1 2 1 1) (car/cons (cons x y) z))
       ((1 2 1) (cdr/cons x y))
       ((1 2 2) (cdr/cons (cons x y) z))
       (() (equal-same (cons x (cons y z))))))))

(defun defun.align.attempt ()
  (J-Bob/prove (dethm.rotate/cons)
    '(((defun align (x)
         (if (atom x)
             x
             (if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
       (size x)
       ((Q) (natp/size x))
       (()
        (if-true
          (if (atom x)
              't
              (if (atom (car x))
                  (< (size (cdr x)) (size x))
                  (< (size (rotate x)) (size x))))
          'nil))
       ((E A) (size/cdr x))
       ((E E 1 1 1) (cons/car+cdr x))
       ((E E 2 1) (cons/car+cdr x))
       ((E E 1 1 1 1) (cons/car+cdr (car x)))
       ((E E 2 1 1) (cons/car+cdr (car x)))
       ((E E 1 1) (rotate/cons (car (car x)) (cdr (car x)) (cdr x)))))))

(defun defun.wt ()
  (J-Bob/define (dethm.rotate/cons)
    '(((defun wt (x)
         (if (atom x) '1 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))))
       (size x)
       ((Q) (natp/size x))
       (()
        (if-true
          (if (atom x)
              't
              (if (< (size (car x)) (size x)) (< (size (cdr x)) (size x)) 'nil))
          'nil))
       ((E Q) (size/car x))
       ((E A) (size/cdr x))
       ((E) (if-true 't 'nil))
       (() (if-same (atom x) 't))))))

(defun defun.align ()
  (J-Bob/define (defun.wt)
    '(((dethm natp/wt (x)
         (equal (natp (wt x)) 't))
       (star-induction x)
       ((A 1 1) (wt x))
       ((A 1 1) (if-nest-A (atom x) '1 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))))
       ((A 1) (natp '1))
       ((A) (equal-same 't))
       ((E A A 1 1) (wt x))
       ((E A A 1 1)
        (if-nest-E (atom x) '1 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))))
       ((E A A)
        (if-true (equal (natp (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))) 't) 't))
       ((E A A Q) (equal-if (natp (wt (car x))) 't))
       ((E A A A)
        (if-true (equal (natp (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))) 't) 't))
       ((E A A A Q) (natp/+ (wt (car x)) (wt (car x))))
       ((E A A Q) (equal-if (natp (wt (car x))) 't))
       ((E A A Q) (equal-if (natp (wt (cdr x))) 't))
       ((E A A A A 1) (natp/+ (+ (wt (car x)) (wt (car x))) (wt (cdr x))))
       ((E A A A A) (equal-same 't))
       ((E A A A) (if-same (natp (+ (wt (car x)) (wt (car x)))) 't))
       ((E A A) (if-same (natp (wt (cdr x))) 't))
       ((E A) (if-same (equal (natp (wt (cdr x))) 't) 't))
       ((E) (if-same (equal (natp (wt (car x))) 't) 't))
       (() (if-same (atom x) 't)))
      ((dethm positive/wt (x)
         (equal (< '0 (wt x)) 't))
       (star-induction x)
       ((A 1 2) (wt x))
       ((A 1 2) (if-nest-A (atom x) '1 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))))
       ((A 1) (< '0 '1))
       ((A) (equal-same 't))
       ((E A A 1 2) (wt x))
       ((E A A 1 2)
        (if-nest-E (atom x) '1 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))))
       ((E A A)
        (if-true (equal (< '0 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))) 't) 't))
       ((E A A Q) (equal-if (< '0 (wt (car x))) 't))
       ((E A A A)
        (if-true (equal (< '0 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))) 't) 't))
       ((E A A A Q) (positives-+ (wt (car x)) (wt (car x))))
       ((E A A Q) (equal-if (< '0 (wt (car x))) 't))
       ((E A A Q) (equal-if (< '0 (wt (cdr x))) 't))
       ((E A A A A 1) (positives-+ (+ (wt (car x)) (wt (car x))) (wt (cdr x))))
       ((E A A A A) (equal-same 't))
       ((E A A A) (if-same (< '0 (+ (wt (car x)) (wt (car x)))) 't))
       ((E A A) (if-same (< '0 (wt (cdr x))) 't))
       ((E A) (if-same (equal (< '0 (wt (cdr x))) 't) 't))
       ((E) (if-same (equal (< '0 (wt (car x))) 't) 't))
       (() (if-same (atom x) 't)))
      ((defun align (x)
         (if (atom x)
             x
             (if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
       (wt x)
       ((Q) (natp/wt x))
       (()
        (if-true
          (if (atom x)
              't
              (if (atom (car x)) (< (wt (cdr x)) (wt x)) (< (wt (rotate x)) (wt x))))
          'nil))
       ((E A 2) (wt x))
       ((E A 2) (if-nest-E (atom x) '1 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))))
       ((E A)
        (if-true (< (wt (cdr x)) (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))) 't))
       ((E A Q) (natp/wt (cdr x)))
       ((E A A 1) (identity-+ (wt (cdr x))))
       ((E A A) (common-addends-< '0 (+ (wt (car x)) (wt (car x))) (wt (cdr x))))
       ((E A Q) (natp/wt (cdr x)))
       ((E A Q) (positive/wt (car x)))
       ((E A A) (positives-+ (wt (car x)) (wt (car x))))
       ((E A) (if-same (< '0 (wt (car x))) 't))
       ((E E 1 1) (rotate x))
       ((E E 1) (wt (cons (car (car x)) (cons (cdr (car x)) (cdr x)))))
       ((E E 1 Q) (atom/cons (car (car x)) (cons (cdr (car x)) (cdr x))))
       ((E E 1)
        (if-false '1
          (+ (+ (wt (car (cons (car (car x)) (cons (cdr (car x)) (cdr x)))))
                (wt (car (cons (car (car x)) (cons (cdr (car x)) (cdr x))))))
             (wt (cdr (cons (car (car x)) (cons (cdr (car x)) (cdr x))))))))
       ((E E 1 1 1 1) (car/cons (car (car x)) (cons (cdr (car x)) (cdr x))))
       ((E E 1 1 2 1) (car/cons (car (car x)) (cons (cdr (car x)) (cdr x))))
       ((E E 1 2 1) (cdr/cons (car (car x)) (cons (cdr (car x)) (cdr x))))
       ((E E 1 2) (wt (cons (cdr (car x)) (cdr x))))
       ((E E 1 2 Q) (atom/cons (cdr (car x)) (cdr x)))
       ((E E 1 2)
        (if-false '1
          (+ (+ (wt (car (cons (cdr (car x)) (cdr x))))
                (wt (car (cons (cdr (car x)) (cdr x)))))
             (wt (cdr (cons (cdr (car x)) (cdr x)))))))
       ((E E 1 2 1 1 1) (car/cons (cdr (car x)) (cdr x)))
       ((E E 1 2 1 2 1) (car/cons (cdr (car x)) (cdr x)))
       ((E E 1 2 2 1) (cdr/cons (cdr (car x)) (cdr x)))
       ((E E 2) (wt x))
       ((E E 2) (if-nest-E (atom x) '1 (+ (+ (wt (car x)) (wt (car x))) (wt (cdr x)))))
       ((E E 2 1 1) (wt (car x)))
       ((E E 2 1 1)
        (if-nest-E (atom (car x))
          '1
          (+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x))))))
       ((E E 2 1 2) (wt (car x)))
       ((E E 2 1 2)
        (if-nest-E (atom (car x))
          '1
          (+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x))))))
       ((E E 1)
        (associate-+
          (+ (wt (car (car x))) (wt (car (car x))))
          (+ (wt (cdr (car x))) (wt (cdr (car x))))
          (wt (cdr x))))
       ((E E)
        (common-addends-<
          (+ (+ (wt (car (car x))) (wt (car (car x))))
             (+ (wt (cdr (car x))) (wt (cdr (car x)))))
          (+ (+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x))))
             (+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x)))))
          (wt (cdr x))))
       ((E E 1)
        (associate-+
          (+ (wt (car (car x))) (wt (car (car x))))
          (wt (cdr (car x)))
          (wt (cdr (car x)))))
       ((E E 1)
        (commute-+
          (+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x))))
          (wt (cdr (car x)))))
       ((E E)
        (common-addends-<
          (wt (cdr (car x)))
          (+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x))))
          (+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x))))))
       ((E E)
        (if-true
          (< (wt (cdr (car x)))
             (+ (+ (wt (car (car x))) (wt (car (car x)))) (wt (cdr (car x)))))
          't))
       ((E E Q) (natp/wt (cdr (car x))))
       ((E E A 1) (identity-+ (wt (cdr (car x)))))
       ((E E A)
        (common-addends-<
          '0
          (+ (wt (car (car x))) (wt (car (car x))))
          (wt (cdr (car x)))))
       ((E E Q) (natp/wt (cdr (car x))))
       ((E E Q) (positive/wt (car (car x))))
       ((E E A) (positives-+ (wt (car (car x))) (wt (car (car x)))))
       ((E E) (if-same (< '0 (wt (car (car x)))) 't))
       ((E) (if-same (atom (car x)) 't))
       (() (if-same (atom x) 't))))))

(defun dethm.align/align ()
  (J-Bob/define (defun.align)
    '(((dethm align/align (x)
         (equal (align (align x)) (align x)))
       (align x)
       ((A 1 1) (align x))
       ((A 1 1)
        (if-nest-A (atom x)
          x
          (if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
       ((A 2) (align x))
       ((A 2)
        (if-nest-A (atom x)
          x
          (if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
       ((A 1) (align x))
       ((A 1)
        (if-nest-A (atom x)
          x
          (if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
       ((A) (equal-same x))
       ((E A A 1 1) (align x))
       ((E A A 1 1)
        (if-nest-E (atom x)
          x
          (if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
       ((E A A 1 1)
        (if-nest-A (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x))))
       ((E A A 2) (align x))
       ((E A A 2)
        (if-nest-E (atom x)
          x
          (if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
       ((E A A 2)
        (if-nest-A (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x))))
       ((E A A 1) (align (cons (car x) (align (cdr x)))))
       ((E A A 1 Q) (atom/cons (car x) (align (cdr x))))
       ((E A A 1 E Q 1) (car/cons (car x) (align (cdr x))))
       ((E A A 1 E A 1) (car/cons (car x) (align (cdr x))))
       ((E A A 1 E A 2 1) (cdr/cons (car x) (align (cdr x))))
       ((E A A 1)
        (if-false (cons (car x) (align (cdr x)))
          (if (atom (car x))
              (cons (car x) (align (align (cdr x))))
              (align (rotate (cons (car x) (align (cdr x))))))))
       ((E A A 1)
        (if-nest-A (atom (car x))
          (cons (car x) (align (align (cdr x))))
          (align (rotate (cons (car x) (align (cdr x)))))))
       ((E A A 1 2) (equal-if (align (align (cdr x))) (align (cdr x))))
       ((E A A)	(equal-same (cons (car x) (align (cdr x)))))
       ((E A) (if-same (equal (align (align (cdr x))) (align (cdr x))) 't))
       ((E E A 1 1) (align x))
       ((E E A 1 1)
        (if-nest-E (atom x)
          x
          (if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
       ((E E A 1 1)
        (if-nest-E (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x))))
       ((E E A 2) (align x))
       ((E E A 2)
        (if-nest-E (atom x)
          x
          (if (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x)))))
       ((E E A 2)
        (if-nest-E (atom (car x)) (cons (car x) (align (cdr x))) (align (rotate x))))
       ((E E A 1) (equal-if (align (align (rotate x))) (align (rotate x))))
       ((E E A) (equal-same (align (rotate x))))
       ((E E) (if-same (equal (align (align (rotate x))) (align (rotate x))) 't))
       ((E) (if-same (atom (car x)) 't))
       (() (if-same (atom x) 't))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(dethm.align/align)
