Event: Start with the initial nqthm theory.

Definition: bubble1 (l) = if ¬ listp (l) then l

elseif ¬ listp (cdr (l)) then l

elseif car (l) < car (bubble1 (cdr (l))) then cons (car (l), bubble1 (cdr (l))) else cons (car (bubble1 (cdr (l))),

cons (car (l), cdr (bubble1 (cdr (l))))) endif

Definition: length (lst) = if listp (lst) then 1 + length (cdr (lst))

else 0 endif

Theorem: bubble1-preserves-length length (bubble1 (l)) = length (l)

Theorem: stupid-lemma-1 listp (l) → (length (cdr (bubble1 (l))) < length (l))

Definition: bubblesort (l) = if ¬ listp (l) then nil

else cons (car (bubble1 (l)), bubblesort (cdr (bubble1 (l)))) endif

Definition: sortedp (l) = if ¬ listp (l) then t

elseif ¬ listp (cdr (l)) then t

else (car (l) ≤ cadr (l)) ∧ sortedp (cdr (l)) endif

Theorem: member-cdr-bubble1-not-lessp (x ∈ cdr (bubble1 (l))) → ((x < car (bubble1 (l))) = f)

Theorem: bubblesort-is-sorted sortedp (bubblesort (l))

Theorem: bubblesort-is-sortedp sortedp (bubblesort (l))

; the last of these seems to be new
                                ; somehow, 2/20/88

Event: Introduce the function symbol amb of 2 arguments.

Axiom: amb-axiom (amb (x, y) = x) ∨ (amb (x, y) = y)

Definition: state (i) = if i ∈ N

then if i ≃ 0 then cons (0, 1) elseif car (state (i − 1)) ≃ 0 then amb (cons (1, cdr (state (i − 1))),

cons (0, 1 + cdr (state (i − 1)))) else cons (car (state (i − 1)), cdr (state (i − 1)) − 1) endif

else cons (0, 0) endif

Event: Introduce the function symbol constant of 0 arguments.

Axiom: constant-axiom ((constant ∈ N) ∧ (car (state (constant)) = 1)) ∨ (¬ ((x ∈ N) ∧ (car (state (x)) = 1)))

Definition: zz (x) = if x ≃ 0 then t

else zz (x − 1) endif

Theorem: car-of-state-is-numberp car (state (x)) ∈ N

Theorem: cdr-of-state-is-numberp cdr (state (x)) ∈ N

Definition: thm-ind (x, y) = if y ≃ 0 then t

else thm-ind (1 + x, y − 1) endif

Theorem: main-base t

Theorem: main-thm ((x ∈ N) ∧ (car (state (x)) = 1) ∧ (cdr (state (x)) = y)) → (state (x + y) = '(1 . 0))

Theorem: pnueli-1 ((constant ∈ N) ∧ (car (state (constant)) = 1)) → (cdr (state (constant + cdr (state (constant)))) = 0)

Theorem: car-of-state-is-zero-or-1 (car (state (x)) ≠ 1) → (car (state (x)) = 0)

Theorem: pnueli-2 (¬ ((x ∈ N) ∧ (car (state (x)) = 1))) → (car (state (x)) ≃ 0)

Theorem: pnueli-thm (cdr (state (constant + cdr (state (constant)))) = 0) ∨ (car (state (x)) ≃ 0)

; Begin commutativity of times

Definition: double-ind (x, y) = if (x ≃ 0) ∨ (y ≃ 0) then t

else double-ind (x, y − 1) ∧ double-ind (x − 1, y) ∧ double-ind (x − 1, y − 1) endif

; the following has USE-GOAL and hence is omitted, 2/88
#|
(PROVE-LEMMA TIMES-COMM
 (REWRITE)
 (EQUAL (TIMES X Y) (TIMES Y X))
 ((INSTRUCTIONS (INDUCT (DOUBLE-IND X Y))
S SPLIT SUBV S
(PUSH TIMES-0)
PROVE SUBV S USE-GOAL
(HIDE-HYPS 1 2 3)
(PUSH TIMES-NOT-NUMBERP)
PROVE USE-GOAL S DIVE PUSH DIVE
(DIVE 1)
X
(DIVE 2)
(= * (TIMES Y (SUB1 X)) T)
X UP NX X
(DIVE 2)
(= * (TIMES X (SUB1 Y)) T)
X UP UP
(DIVE 1 2 2)

    (= * (TIMES (SUB1 X) (SUB1 Y)) T)
    TOP
    (GENERALIZE (((TIMES (SUB1 X) (SUB1 Y)) ?)))
    PROVE)))
|#

Definition: flatten (x) = if x ≃ nil then list (x)

else append (flatten (car (x)), flatten (cdr (x))) endif

Definition: mcflatten (x, y) = if x ≃ nil then cons (x, y)

else mcflatten (car (x), mcflatten (cdr (x), y)) endif

Definition: fmfind (x, y) = if x ≃ nil then t

else fmfind (car (x), mcflatten (cdr (x), y)) ∧ fmfind (cdr (x), y) endif

Theorem: bookmark t

Theorem: assoc-of-append append (append (x, y), z) = append (x, append (y, z))

Theorem: flatten-mcflatten mcflatten (x, y) = append (flatten (x), y)

Theorem: plus-assoc (x + y + z) = ((x + y) + z)

Theorem: assoc-plus (x + y + z) = ((x + y) + z)

Definition: rev (l) = if l ≃ nil then nil

else append (rev (cdr (l)), list (car (l))) endif

Definition: plistp (l) = if l ≃ nil then l = nil

else plistp (cdr (l)) endif Theorem: rev-rev plistp (l) → (rev (rev (l)) = l)

Theorem: rev-plistp plistp (rev (l))

Theorem: rev-append-1 rev (y) = append (rev (y), nil)

Theorem: rev-append rev (append (x, y)) = append (rev (y), rev (x))

Index

amb, 2 amb-axiom, 2 assoc-of-append, 4 assoc-plus, 4

bookmark, 4 bubble1, 1 bubble1-preserves-length, 1 bubblesort, 1 bubblesort-is-sorted, 1 bubblesort-is-sortedp, 1

car-of-state-is-numberp, 2 car-of-state-is-zero-or-1, 3 cdr-of-state-is-numberp, 2 constant, 2, 3 constant-axiom, 2

double-ind, 3

flatten, 4 flatten-mcflatten, 4 fmfind, 4

length, 1

main-base, 2 main-thm, 2 mcflatten, 4 member-cdr-bubble1-not-lessp, 1

plistp, 4, 5 plus-assoc, 4 pnueli-1, 3 pnueli-2, 3 pnueli-thm, 3

rev, 4, 5 rev-append, 5 rev-append-1, 5 rev-plistp, 5 rev-rev, 5 sortedp, 1 state, 2, 3 stupid-lemma-1, 1

thm-ind, 2

zz, 2