#|
Copyright (C) 1994 by Computational Logic, Inc.  All Rights Reserved.
This script is hereby placed in the public domain, and therefore unlimited
editing and redistribution is permitted.
NO WARRANTY
Computational Logic, Inc. PROVIDES ABSOLUTELY NO WARRANTY.  THE EVENT SCRIPT
IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESS OR IMPLIED,
INCLUDING, BUT NOT LIMITED TO, ANY IMPLIED WARRANTIES OF MERCHANTABILITY AND
FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND
PERFORMANCE OF THE SCRIPT IS WITH YOU.  SHOULD THE SCRIPT PROVE DEFECTIVE, YOU
ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
IN NO EVENT WILL Computational Logic, Inc. BE LIABLE TO YOU FOR ANY DAMAGES,
ANY LOST PROFITS, LOST MONIES, OR OTHER SPECIAL, INCIDENTAL OR CONSEQUENTIAL
DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THIS SCRIPT (INCLUDING BUT
NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES
SUSTAINED BY THIRD PARTIES), EVEN IF YOU HAVE ADVISED US OF THE POSSIBILITY OF
SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY.
|#
;; See CLI Internal Note 185 for a tutorial introduction to the
;; Boyer-Moore prove based on this example.

Event: Start with the initial nqthm theory.

Definition: rotate (n, lst) = if n ≃ 0 then lst

else rotate (n − 1, append (cdr (lst), list (car (lst)))) endif

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

else 0 endif

Definition: properp (x) = if listp (x) then properp (cdr (x))

else x = nil endif Definition: firstn (n, lst) = if n ≃ 0 then nil

else cons (car (lst), firstn (n − 1, cdr (lst))) endif

Definition: nthcdr (n, lst) = if n ≃ 0 then lst

else nthcdr (n − 1, cdr (lst)) endif

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

Theorem: append-nil properp (x) → (append (x, nil) = x)

Definition: rotate-append-induction (n, lst, extra) = if (n = 0) ∨ (n ∉ N) then t

elseif lst ≃ nil then t

else rotate-append-induction (n − 1, cdr (lst), append (extra, list (car (lst)))) endif

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

Theorem: rotate-append (properp (extra) ∧ (length (lst) ≮ n)) → (rotate (n, append (lst, extra))

= append (nthcdr (n, lst), append (extra, firstn (n, lst))))

Theorem: nthcdr-length properp (lst) → (nthcdr (length (lst), lst) = nil)

Theorem: firstn-length properp (lst) → (firstn (length (lst), lst) = lst)

Theorem: rotate-length properp (lst) → (rotate (length (lst), lst) = lst)

Index

append-nil, 2 associativity-of-append, 2

firstn, 2 firstn-length, 2

length, 1, 2

nthcdr, 2 nthcdr-length, 2

properp, 1, 2 properp-append, 2

rotate, 1, 2 rotate-append, 2 rotate-append-induction, 2 rotate-length, 2