Event: Start with the initial nqthm theory.

Definition: h (n, from, to, temp) = if n ≃ 0 then nil

else append (h (n − 1, from, temp, to), cons (cons (from, to), h (n − 1, temp, to, from))) endif

Definition: hanoi (n) = h (n, 0, 1, 2)

Definition: nth (i, l) = if i ≃ 0 then car (l)

else nth (i − 1, cdr (l)) endif

Definition: set-nth (i, l, v) = if i ≃ 0 then cons (v, cdr (l))

else cons (car (l), set-nth (i − 1, cdr (l), v)) endif

Definition: legal (move, st) = (listp (move)

∧ (car (move) ∈ '(0 1 2)) ∧ (cdr (move) ∈ '(0 1 2)) ∧ listp (nth (car (move), st)) ∧ ((nth (cdr (move), st) ≃ nil)

∨ (car (nth (car (move), st)) < car (nth (cdr (move), st)))))

Definition: step (move, st) = set-nth (car (move),

set-nth (cdr (move), st, cons (car (nth (car (move), st)), nth (cdr (move), st))),

cdr (nth (car (move), st)))

Event: Disable legal.

Definition: play (moves, st) = if listp (moves)

then if legal (car (moves), st)

then play (cdr (moves), step (car (moves), st))

else f endif else st endif Event: Enable legal.

Definition: tower (n) = if n ≃ 0 then nil

else append (tower (n − 1), list (n)) endif

Definition: permp (i, j , k)

= ((i ∈ '(0 1 2))
    ∧ (j ∈ '(0 1 2))

    ∧ (k ∈ '(0 1 2))

∧ (i ≠ j )
∧ (i ≠ k)
∧ (j ≠ k))

Definition: statep (s) = (listp (s) ∧ listp (cdr (s)) ∧ listp (cddr (s)))

Definition: slessp (n, s) = (if nth (0, s) ≃ nil then t

else n < car (nth (0, s)) endif ∧ if nth (1, s) ≃ nil then t

else n < car (nth (1, s)) endif ∧ if nth (2, s) ≃ nil then t

else n < car (nth (2, s)) endif)

; We wish to prove:
;(equal (play (hanoi n) (list (tower n) nil nil))
;       (list nil (tower n) nil))
; i.e.
;(equal (play (h n 0 1 2) (list (tower n) nil nil))
;       (list nil (tower n) nil))
; But to do so we go for a more general fact:
; (implies
;   (and (statep s)
;        (slessp n s)
;        (permp i j k))

;   (and (play (h n i j k)
;              (set-nth i s
;                       (append (tower n) (nth i s))))
;        (equal (play (h n i j k)
;                     (set-nth i s
;                              (append (tower n) (nth i s))))
;               (set-nth j s
;                        (append (tower n) (nth j s))))))
; The proof should go roughly by induction along the definition of
; h, but with s instantiated appropriately.

Definition: main-ind (i, j , k, n, s) = if n ≃ 0 then nil

else main-ind (i, k, j , n − 1, set-nth (i, s, cons (n, nth (i, s)))) ∧ main-ind (k, j , i, n − 1, set-nth (j , s, cons (n, nth (j , s)))) endif

; The following is used to conclude the proof of the base case.

Theorem: set-nth-nth ((i ∈ '(0 1 2)) ∧ statep (s)) → (set-nth (i, s, nth (i, s)) = s)

Definition: hyps (i, j , k, n, s) = (statep (s) ∧ slessp (n, s) ∧ permp (i, j , k))

Definition: conc (i, j , k, n, s) = (play (h (n, i, j , k), set-nth (i, s, append (tower (n), nth (i, s))))

∧ (play (h (n, i, j , k), set-nth (i, s, append (tower (n), nth (i, s)))) = set-nth (j , s, append (tower (n), nth (j , s)))))

Definition: main-thm (i, j , k, n, s) = (hyps (i, j , k, n, s) → conc (i, j , k, n, s))

Theorem: base-case (n ≃ 0) → main-thm (i, j , k, n, s)

Theorem: nth-of-nlistp (¬ listp (x)) → (nth (n, x) = 0)

Theorem: play-append play (append (x, y), s) = play (y, play (x, s))

Theorem: statep-set-nth statep (s) → statep (set-nth (i, s, cons (n, nth (i, s))))

; Got to here, and then aborted out as follows:

Theorem: nth-of-set-nth (statep (s) ∧ (i ∈ '(0 1 2)) ∧ (j ∈ '(0 1 2))) → (nth (i, set-nth (j , s, v))

= if i = j then v else nth (i, s) endif)

Definition: statep-tower-ind (i, n, s) = if n ≃ 0 then t

else statep-tower-ind (i, n − 1, set-nth (i, s, cons (n, nth (i, s)))) endif

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

Theorem: set-nth-twice set-nth (i, set-nth (i, s, v1 ), v2 ) = set-nth (i, s, v2 )

Theorem: slessp-preserved ((n ∈ N) ∧ (n ≠ 0) ∧ statep (s) ∧ (i ∈ '(0 1 2)) ∧ slessp (n, s)) → slessp (n − 1, set-nth (i, s, cons (n, nth (i, s))))

Theorem: statep-tower ((n ∈ N) ∧ (n ≠ 0) ∧ statep (s) ∧ slessp (n, s) ∧ (i ∈ '(0 1 2))) → statep (set-nth (i, s, append (tower (n), nth (i, s))))

Theorem: play-is-non-f-bookmark t

Theorem: permp-preserved-1 permp (i, j , k) → permp (i, k, j )

Event: Disable permp-preserved-1.

Theorem: used-first-ind-hyp t

Theorem: set-nth-different-twice ((i ∈ '(0 1 2)) ∧ (j ∈ '(0 1 2)) ∧ (i ≠ j ) ∧ statep (s)) → (set-nth (i, set-nth (j , s, v), w) = set-nth (j , set-nth (i, s, w), v))

Theorem: slessp-sub1 slessp (n, s) → slessp (n − 1, s)

Theorem: permp-preserved-2 permp (i, j , k) → permp (k, j , i)

Event: Disable permp-preserved-2.

Theorem: statep-preserved-by-set-nth (statep (s) ∧ (i ∈ '(0 1 2))) → statep (set-nth (i, s, v))

Theorem: all-but-legal t

Theorem: ind-step ((n ≄ 0) ∧ main-thm (i, k, j , n − 1, set-nth (i, s, cons (n, nth (i, s)))) ∧ main-thm (k, j , i, n − 1, set-nth (j , s, cons (n, nth (j , s))))) → main-thm (i, j , k, n, s)

Theorem: main-theorem-abbreviated main-thm (i, j , k, n, s)

Theorem: main-theorem (statep (s) ∧ slessp (n, s) ∧ permp (i, j , k)) → (play (h (n, i, j , k), set-nth (i, s, append (tower (n), nth (i, s))))

= set-nth (j , s, append (tower (n), nth (j , s))))

Theorem: correctness-of-hanoi play (hanoi (n), cons (tower (n), '(nil nil))) = cons (nil, cons (tower (n), '(nil)))

Index

all-but-legal, 5 append-assoc, 4

base-case, 3

conc, 3 correctness-of-hanoi, 5

h, 1, 3, 5 hanoi, 1, 5 hyps, 3

ind-step, 5

legal, 1

main-ind, 3 main-theorem, 5 main-theorem-abbreviated, 5 main-thm, 3, 5

nth, 1–5 nth-of-nlistp, 3 nth-of-set-nth, 4

permp, 2–5 permp-preserved-1, 4 permp-preserved-2, 5 play, 1, 3, 5 play-append, 3 play-is-non-f-bookmark, 4

set-nth, 1, 3–5 set-nth-different-twice, 4 set-nth-nth, 3 set-nth-twice, 4 slessp, 2–5 slessp-preserved, 4 slessp-sub1, 5 statep, 2–5 statep-preserved-by-set-nth, 5 statep-set-nth, 4 statep-tower, 4 statep-tower-ind, 4 step, 1

tower, 2–5

used-first-ind-hyp, 4