((dethm atom/cons (x y) (equal (atom (cons x y)) (quote 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) (quote 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 (quote t) x y) x)) (dethm if-false (x y) (equal (if (quote nil) x y) y)) (dethm if-nest-E (x y z) (if x (quote t) (equal (if x y z) z))) (dethm if-nest-A (x y z) (if x (equal (if x y z) y) (quote t))) (dethm cons/car+cdr (x) (if (atom x) (quote t) (equal (cons (car x) (cdr x)) x))) (dethm equal-if (x y) (if (equal x y) (equal x y) (quote t))) (dethm natp/size (x) (equal (natp (size x)) (quote t))) (dethm size/car (x) (if (atom x) (quote t) (equal (< (size (car x)) (size x)) (quote t)))) (dethm size/cdr (x) (if (atom x) (quote t) (equal (< (size (cdr x)) (size x)) (quote 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)) (quote t)) (quote t)) (quote t))) (dethm positives-+ (x y) (if (< (quote 0) x) (if (< (quote 0) y) (equal (< (quote 0) (+ x y)) (quote t)) (quote t)) (quote t))) (dethm common-addends-< (x y z) (equal (< (+ x z) (+ y z)) (< x y))) (dethm identity-+ (x) (if (natp x) (equal (+ (quote 0) x) x) (quote t))) (defun list-induction (x) (if (atom x) (quote ()) (cons (car x) (list-induction (cdr x))))) (defun star-induction (x) (if (atom x) x (cons (star-induction (car x)) (star-induction (cdr x))))) (defun pair (x y) (cons x (cons y (quote ())))) (defun first-of (x) (car x)) (defun second-of (x) (car (cdr x))) (dethm first-of-pair (a b) (equal (first-of (pair a b)) a)) (dethm second-of-pair (a b) (equal (second-of (pair a b)) b)) (defun in-pair? (xs) (if (equal (first-of xs) (quote ?)) (quote t) (equal (second-of xs) (quote ?)))) (dethm in-first-of-pair (b) (equal (in-pair? (pair (quote ?) b)) (quote t))) (dethm in-second-of-pair (a) (equal (in-pair? (pair a (quote ?))) (quote t))) (defun list0? (x) (equal x (quote ()))) (defun list1? (x) (if (atom x) (quote nil) (list0? (cdr x)))) (defun list2? (x) (if (atom x) (quote nil) (list1? (cdr x)))) (defun list? (x) (if (atom x) (equal x (quote ())) (list? (cdr x)))) (defun sub (x y) (if (atom y) (if (equal y (quote ?)) x y) (cons (sub x (car y)) (sub x (cdr y))))) (defun memb? (xs) (if (atom xs) (quote nil) (if (equal (car xs) (quote ?)) (quote t) (memb? (cdr xs))))) (defun remb (xs) (if (atom xs) (quote ()) (if (equal (car xs) (quote ?)) (remb (cdr xs)) (cons (car xs) (remb (cdr xs)))))) (dethm memb?/remb0 () (equal (memb? (remb (quote ()))) (quote nil))) (dethm memb?/remb1 (x1) (equal (memb? (remb (cons x1 (quote ())))) (quote nil))) (dethm memb?/remb2 (x1 x2) (equal (memb? (remb (cons x2 (cons x1 (quote ()))))) (quote nil))) (dethm memb?/remb (xs) (equal (memb? (remb xs)) (quote nil))) (defun ctx? (x) (if (atom x) (equal x (quote ?)) (if (ctx? (car x)) (quote t) (ctx? (cdr x))))) (dethm ctx?/t (x) (if (ctx? x) (equal (ctx? x) (quote t)) (quote t))) (dethm ctx?/sub (x y) (if (ctx? x) (if (ctx? y) (equal (ctx? (sub x y)) (quote t)) (quote t)) (quote t))) (defun member? (x ys) (if (atom ys) (quote nil) (if (equal x (car ys)) (quote t) (member? x (cdr ys))))) (defun set? (xs) (if (atom xs) (quote t) (if (member? (car xs) (cdr xs)) (quote nil) (set? (cdr xs))))) (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)))) (defun atoms (x) (add-atoms x (quote ()))) (dethm set?/t (xs) (if (set? xs) (equal (set? xs) (quote t)) (quote t))) (dethm set?/nil (xs) (if (set? xs) (quote t) (equal (set? xs) (quote nil)))) (dethm set?/add-atoms (a bs) (if (set? bs) (equal (set? (add-atoms a bs)) (quote t)) (quote t))) (dethm set?/atoms (a) (equal (set? (atoms a)) (quote t))) (defun rotate (x) (cons (car (car x)) (cons (cdr (car x)) (cdr x)))) (dethm rotate/cons (x y z) (equal (rotate (cons (cons x y) z)) (cons x (cons y z)))) (defun wt (x) (if (atom x) (
