Event: Start with the initial thm theory.

Definition: merge (l, m) = if l ≃ nil then m

elseif m ≃ nil then l

elseif car (l) < car (m) then cons (car (l), merge (cdr (l), m))

else cons (car (m), merge (l, cdr (m))) endif

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

elseif cdr (l) ≃ nil then nil

else cons (cadr (l), evens (cddr (l))) endif

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

else cons (car (l), odds (cddr (l))) endif

Theorem: evens-length ((l ≄ nil) ∧ (cdr (l) ≄ nil)) → (length (evens (l)) < length (l))

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

elseif cdr (l) ≃ nil then l

else merge (mergesort (evens (l)), mergesort (odds (l))) endif

; Interestingly, the prover can now prove (SORTEDP (MERGESORT L)) automatically,
; but we won't bother with that here.

Index

evens, 1 evens-length, 1 length, 1 merge, 1 mergesort, 1 odds, 1