#|
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.
|#
;; Matt Kaufmann

Event: Start with the initial nqthm theory.

;; These are events in support of the paper ``A Mechanically-Checked
;; Correctness Proof for Generalization in the Presence of Free
;; Variables,'' Journal of Automated Reasoning, Vol. 7, 1991.
;; This events file contains no DEFN-SK events, but instead contains two
;; DCLs and two ADD-AXIOMs from a DEFN-SK event that I commented out.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; sets.events file
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Requires deftheory enhancement.
;; Requires only ground-zero theory, nqthm mode.
;; Sets; Matt Kaufmann, Dec. 1989, revised March 1990.  The first few events

;; are some basic events about lists.  I'll take the approach that all these
;; basic functions will be disabled once enough algebraic properties have
;; been proved.
;; Theories:
;; (deftheory set-defns
;;  (length properp fix-properp member append subsetp delete
;;          disjoint intersection set-diff setp))

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

else 0 endif

Theorem: length-nlistp (x ≃ nil) → (length (x) = 0)

Theorem: length-cons length (cons (a, x)) = (1 + length (x))

Theorem: length-append length (append (x, y)) = (length (x) + length (y))

Event: Disable length.

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

Theorem: member-cons (a ∈ cons (x, l)) = ((a = x) ∨ (a ∈ l))

Theorem: member-nlistp (l ≃ nil) → (a ∉ l)

Event: Disable member.

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

else (car (x) ∈ y) ∧ subsetp (cdr (x), y) endif Definition: subsetp-wit (x, y) = if x ≃ nil then t

elseif car (x) ∈ y then subsetp-wit (cdr (x), y)

else car (x) endif

Theorem: subsetp-wit-witnesses subsetp (x, y) = (¬ ((subsetp-wit (x, y) ∈ x) ∧ (subsetp-wit (x, y) ∉ y)))

Theorem: subsetp-wit-witnesses-general-1 ((subsetp-wit (x, y) ∉ x) ∧ (a ∈ x)) → (a ∈ y)

Theorem: subsetp-wit-witnesses-general-2 ((subsetp-wit (x, y) ∈ y) ∧ (a ∈ x)) → (a ∈ y)

Event: Disable subsetp-wit-witnesses.

Event: Disable subsetp-wit-witnesses-general-1.

Event: Disable subsetp-wit-witnesses-general-2.

Theorem: subsetp-cons-1 subsetp (cons (a, x), y) = ((a ∈ y) ∧ subsetp (x, y))

Theorem: subsetp-cons-2 subsetp (l, m) → subsetp (l, cons (a, m))

Theorem: subsetp-reflexivity subsetp (x, x)

Theorem: cdr-subsetp subsetp (cdr (x), x)

Theorem: member-subsetp ((x ∈ y) ∧ subsetp (y, z)) → (x ∈ z)

Theorem: subsetp-is-transitive (subsetp (x, y) ∧ subsetp (y, z)) → subsetp (x, z)

Theorem: member-append (a ∈ append (x, y)) = ((a ∈ x) ∨ (a ∈ y))

Theorem: subsetp-append subsetp (append (x, y), z) = (subsetp (x, z) ∧ subsetp (y, z))

Theorem: subsetp-of-append-sufficiency (subsetp (a, b) ∨ subsetp (a, c)) → subsetp (a, append (b, c))

Theorem: subsetp-nlistp (x ≃ nil) → (subsetp (x, y) ∧ (subsetp (y, x) = (y ≃ nil)))

Theorem: subsetp-cons-not-member (z ∉ x) → (subsetp (x, cons (z, v)) = subsetp (x, v))

Event: Disable subsetp.

;;;;; Other set-theoretic and list-theoretic definitions, and properp observations.

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

else x = nil endif

Definition: fix-properp (x) = if listp (x) then cons (car (x), fix-properp (cdr (x)))

else nil endif

Theorem: properp-fix-properp properp (fix-properp (x))

Theorem: fix-properp-properp properp (x) → (fix-properp (x) = x)

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

Theorem: properp-nlistp (x ≃ nil) → (properp (x) = (x = nil))

Theorem: fix-properp-cons fix-properp (cons (x, y)) = cons (x, fix-properp (y))

Theorem: fix-properp-nlistp (x ≃ nil) → (fix-properp (x) = nil)

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

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

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

Definition: delete (x, l) = if listp (l)

then if x = car (l) then cdr (l)

else cons (car (l), delete (x, cdr (l))) endif else l endif

Theorem: properp-delete properp (delete (x, l)) = properp (l)

Definition: disjoint (x, y) = if listp (x) then (car (x) ∉ y) ∧ disjoint (cdr (x), y)

else t endif

Definition: disjoint-wit (x, y) = if listp (x)

then if car (x) ∈ y then car (x)

else disjoint-wit (cdr (x), y) endif else t endif

Theorem: disjoint-wit-witnesses disjoint (x, y) = (¬ ((disjoint-wit (x, y) ∈ x) ∧ (disjoint-wit (x, y) ∈ y)))

Event: Disable disjoint-wit.

Event: Disable disjoint-wit-witnesses.

Definition: intersection (x, y) = if listp (x)

then if car (x) ∈ y then cons (car (x), intersection (cdr (x), y))

else intersection (cdr (x), y) endif else nil endif

Theorem: properp-intersection properp (intersection (x, y))

Definition: set-diff (x, y) = if listp (x)

then if car (x) ∈ y then set-diff (cdr (x), y)

else cons (car (x), set-diff (cdr (x), y)) endif else nil endif

Theorem: properp-set-diff properp (set-diff (x, y))

Definition: setp (x) = if ¬ listp (x) then x = nil

else (car (x) ∉ cdr (x)) ∧ setp (cdr (x)) endif

Theorem: setp-implies-properp setp (x) → properp (x)

Event: Disable properp.

Event: Let us define the theory set-defns to consist of the following events: length, properp, fix-properp, member, append, subsetp, delete, disjoint, intersection, set-diff, setp, properp.

;; Set theory lemmas

Theorem: delete-cons delete (a, cons (b, x)) = if a = b then x

else cons (b, delete (a, x)) endif

Theorem: delete-nlistp (x ≃ nil) → (delete (a, x) = x)

Theorem: listp-delete listp (delete (x, l)) = if listp (l) then (x ≠ car (l)) ∨ listp (cdr (l))

else f endif

Theorem: delete-non-member (x ∉ y) → (delete (x, y) = y)

Theorem: delete-delete delete (y, delete (x, z)) = delete (x, delete (y, z))

Theorem: member-delete setp (x) → ((a ∈ delete (b, x)) = ((a ≠ b) ∧ (a ∈ x)))

Theorem: setp-delete setp (x) → setp (delete (a, x))

Event: Disable delete.

Theorem: disjoint-cons-1 disjoint (cons (a, x), y) = ((a ∉ y) ∧ disjoint (x, y))

Theorem: disjoint-cons-2 disjoint (x, cons (a, y)) = ((a ∉ x) ∧ disjoint (x, y))

Theorem: disjoint-nlistp ((x ≃ nil) ∨ (y ≃ nil)) → disjoint (x, y)

Theorem: disjoint-symmetry disjoint (x, y) = disjoint (y, x)

Theorem: disjoint-append-right disjoint (u, append (y, z)) = (disjoint (u, y) ∧ disjoint (u, z))

Theorem: disjoint-append-left disjoint (append (y, z), u) = (disjoint (y, u) ∧ disjoint (z, u))

Theorem: disjoint-non-member ((a ∈ x) ∧ (a ∈ y)) → (¬ disjoint (x, y))

Theorem: disjoint-subsetp-monotone-second (subsetp (y, z) ∧ disjoint (x, z)) → disjoint (x, y)

Theorem: subsetp-disjoint-2 (subsetp (x, y) ∧ disjoint (y, z)) → disjoint (z, x)

Theorem: subsetp-disjoint-1 (subsetp (x, y) ∧ disjoint (y, z)) → disjoint (x, z)

Theorem: subsetp-disjoint-3 (subsetp (x, y) ∧ disjoint (z, y)) → disjoint (x, z)

Event: Disable disjoint.

Theorem: intersection-disjoint (intersection (x, y) = nil) = disjoint (x, y)

Theorem: intersection-nlistp ((x ≃ nil) ∨ (y ≃ nil)) → (intersection (x, y) = nil)

Theorem: member-intersection (a ∈ intersection (x, y)) = ((a ∈ x) ∧ (a ∈ y))

Theorem: subsetp-intersection subsetp (x, intersection (y, z)) = (subsetp (x, y) ∧ subsetp (x, z))

Theorem: intersection-symmetry subsetp (intersection (x, y), intersection (y, x))

Theorem: intersection-cons-1 intersection (cons (a, x), y) = if a ∈ y then cons (a, intersection (x, y))

else intersection (x, y) endif

Theorem: intersection-cons-2 (a ∉ y) → (intersection (y, cons (a, x)) = intersection (y, x))

;; The following is needed because DISJOINT-INTERSECTION-COMMUTER,
;; added during polishing, caused the proof of
;; DISJOINT-DOMAIN-CO-RESTRICT (in "alists.events") to fail.

Theorem: intersection-cons-3 (w ∈ x) → (subsetp (intersection (y, cons (w, z)), x)

= subsetp (intersection (y, z), x))

Theorem: intersection-cons-subsetp subsetp (intersection (x, y), intersection (x, cons (a, y)))

Theorem: subsetp-intersection-left-1 subsetp (intersection (x, y), x)

Theorem: subsetp-intersection-left-2 subsetp (intersection (x, y), y)

Theorem: subsetp-intersection-sufficiency-1 subsetp (y, z) → subsetp (intersection (x, y), z)

Theorem: subsetp-intersection-sufficiency-2 subsetp (y, z) → subsetp (intersection (y, x), z)

Theorem: intersection-associative intersection (intersection (x, y), z) = intersection (x, intersection (y, z))

Theorem: intersection-elimination subsetp (x, y) → (intersection (x, y) = fix-properp (x))

Theorem: length-intersection length (x) ≮ length (intersection (x, y))

Theorem: subsetp-intersection-member (subsetp (intersection (x, y), z) ∧ (a ∉ z)) → (((a ∈ x) → (a ∉ y)) ∧ ((a ∈ y) → (a ∉ x)))

;; The following wasn't needed in the proof about generalization, but it's a nice rule.

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

;; I'd rather just prove that intersection distributes over append on
;; the right but that isn't true.  Congruence relations would probably
;; help a lot with that problem.  In the meantime, I content myself
;; with the following.

Theorem: disjoint-intersection-append disjoint (x, intersection (y, append (z1 , z2 ))) = (disjoint (x, intersection (y, z1 )) ∧ disjoint (x, intersection (y, z2 )))

;; See comment just above DISJOINT-INTERSECTION-APPEND

Theorem: subsetp-intersection-append subsetp (intersection (u, append (x, y)), z) = (subsetp (intersection (u, x), z) ∧ subsetp (intersection (u, y), z))

Theorem: subsetp-intersection-elimination-lemma (subsetp (y, x) ∧ (¬ subsetp (y, z))) → (¬ subsetp (intersection (x, y), z))

Theorem: subsetp-intersection-elimination subsetp (y, x) → (subsetp (intersection (x, y), z) ↔ subsetp (y, z))

Theorem: disjoint-intersection disjoint (intersection (x, y), z) = disjoint (x, intersection (y, z))

Theorem: subsetp-intersection-monotone-1 (subsetp (intersection (x, y), z) ∧ subsetp (x1 , x)) → subsetp (intersection (x1 , y), z)

;; The lemma SUBSETP-INTERSECTION-MONOTONE-2 below was added during
;; polishing of the final proof in "generalize.events", since the
;; lemma immediately above wasn't enough at that point.  Actually
;; I realized at this point that intersection commutes from the point
;; of view of subsetp:

Theorem: subsetp-intersection-commuter subsetp (intersection (x, y), z) = subsetp (intersection (y, x), z)

Theorem: subsetp-intersection-monotone-2 (subsetp (intersection (y, x), z) ∧ subsetp (x1 , x)) → subsetp (intersection (x1 , y), z)

Theorem: disjoint-intersection-commuter disjoint (x, intersection (y, z)) = disjoint (x, intersection (z, y))

Theorem: disjoint-intersection3 disjoint (free, intersection (vars, x)) → (intersection (x, intersection (vars, free)) = nil)

Event: Disable intersection.

Theorem: member-set-diff (a ∈ set-diff (y, z)) = ((a ∈ y) ∧ (a ∉ z))

Theorem: subsetp-set-diff-1 subsetp (set-diff (x, y), x)

Theorem: disjointp-set-diff disjoint (set-diff (x, y), y)

Theorem: subsetp-set-diff-2 subsetp (x, set-diff (y, z)) = (subsetp (x, y) ∧ disjoint (x, z))

Theorem: set-diff-cons set-diff (cons (a, x), y) = if a ∈ y then set-diff (x, y)

else cons (a, set-diff (x, y)) endif

Theorem: set-diff-nlistp (x ≃ nil) → (set-diff (x, y) = nil)

;; The following was discovered during final polishing, for the
;; proof of MAIN-HYPS-RELIEVED-6-FIRST.

Theorem: disjoint-set-diff-general disjoint (x, set-diff (y, z)) = subsetp (intersection (x, y), z)

;; No longer relevant:
;(prove-lemma disjoint-set-diff-subsetp (rewrite)
;  (implies (and (disjoint x (set-diff y z))
;               (subsetp z z1))
;          (disjoint x (set-diff y z1)))
;  ((use (disjoint-wit-witnesses (y (set-diff y z1))))
;   (disable member-set-diff set-diff)))
;; Instead of the following I'll prove the corresponding (in light of
;; DISJOINT-SET-DIFF-GENERAL) fact INTERSECTION-X-X about intersection.
;(prove-lemma disjoint-set-diff (rewrite)
;  (disjoint x (set-diff y x)))

Theorem: intersection-subsetp-identity (properp (x) ∧ subsetp (x, y)) → (intersection (x, y) = x)

Theorem: intersection-x-x properp (x) → (intersection (x, x) = x)

Theorem: subsetp-set-diff-mononone-2 subsetp (set-diff (x, append (y, z)), set-diff (x, z))

Theorem: subsetp-set-diff-monotone-second subsetp (set-diff (x, y), set-diff (x, z)) = subsetp (intersection (x, z), y)

Theorem: set-diff-nil set-diff (x, nil) = fix-properp (x)

Theorem: set-diff-cons-non-member-1 (a ∉ x) → (set-diff (x, cons (a, y)) = set-diff (x, y))

Theorem: length-intersection-set-diff length (x) = (length (set-diff (x, y)) + length (intersection (x, y)))

Theorem: length-set-diff-opener length (set-diff (x, y)) = (length (x) − length (intersection (x, y)))

Theorem: listp-set-diff listp (set-diff (x, y)) = (¬ subsetp (x, y))

;; Here is a messy lemma about disjoint and such

Theorem: disjoint-intersection-set-diff-intersection disjoint (x, intersection (y, set-diff (z, intersection (y, x))))

Event: Disable set-diff.

Theorem: member-fix-properp (a ∈ fix-properp (x)) = (a ∈ x)

Theorem: setp-append setp (append (x, y)) = (disjoint (x, y) ∧ setp (fix-properp (x)) ∧ setp (y))

Theorem: setp-cons setp (cons (a, x)) = ((a ∉ x) ∧ setp (x))

Theorem: setp-nlistp (x ≃ nil) → (setp (x) = (x = nil))

Definition: make-set (l) = if ¬ listp (l) then nil

elseif car (l) ∈ cdr (l) then make-set (cdr (l)) else cons (car (l), make-set (cdr (l))) endif

Theorem: make-set-preserves-member (x ∈ make-set (l)) = (x ∈ l)

Theorem: make-set-preserves-subsetp-1 subsetp (make-set (x), make-set (y)) = subsetp (x, y)

Theorem: make-set-preserves-subsetp-2 subsetp (x, make-set (y)) = subsetp (x, y)

Theorem: make-set-preserves-subsetp-3 subsetp (make-set (x), y) = subsetp (x, y)

Theorem: make-set-gives-setp setp (make-set (x))

Theorem: make-set-set-diff make-set (set-diff (x, y)) = set-diff (make-set (x), make-set (y))

Theorem: set-diff-make-set set-diff (x, make-set (y)) = set-diff (x, y)

Theorem: listp-make-set listp (make-set (x)) = listp (x)

Event: Disable setp.

;;;;;; The following were proved in the course of the final run
;;;;;; through the generalization proof.  There are a couple or
;;;;;; so noted above here, too.

Theorem: set-diff-append set-diff (x, append (y, z)) = set-diff (set-diff (x, z), y)

Theorem: length-set-diff-leq length (x) ≮ length (set-diff (x, y))

Theorem: lessp-length listp (x) → (0 < length (x))

Theorem: listp-intersection listp (intersection (x, y)) = (¬ disjoint (x, y))

Theorem: length-set-diff-lessp (¬ disjoint (x, new)) → (length (set-diff (x, new)) < length (x))

Theorem: disjoint-implies-empty-intersection disjoint (x, y) → (intersection (x, y) = nil)

;; The following lemma DISJOINT-INTERSECTION3-MIDDLE is needed for the
;; proof of ALL-VARS-DISJOINT-OR-SUBSETP-GEN-CLOSURE in
;; generalize.events.  I think I could avoid lemmas like this one
;; INTERSECTION were actually commutative-associative (in which case
;; I'd get rid of disjoint and rely on normalization).

Theorem: disjoint-intersection3-middle disjoint (y, intersection (x, z)) → (intersection (x, intersection (y, z)) = nil)

;; Maybe I should redo the notion of disjoint sometime, perhaps using
;; the fact that intersection is commutative and associative when it's
;; equated with nil.

Theorem: disjoint-subsetp-hack (disjoint (x, intersection (u, v)) ∧ subsetp (w, x)) → disjoint (u, intersection (w, v))

Theorem: subsetp-set-diff-sufficiency subsetp (x, y) → subsetp (set-diff (x, z), y)

;; The following lemma SETP-INTERSECTION-SUFFICIENCY is needed for
;; MAPPING-RESTRICT from "alists.events", because (I believe)
;; DOMAIN-RESTRICT, which was added during polishing, changed the
;; course of the previous proof.  Similarly for
;; SETP-SET-DIFF-SUFFICIENCY and the lemma MAPPING-CO-RESTRICT.

Theorem: setp-intersection-sufficiency setp (x) → setp (intersection (x, y))

Theorem: setp-set-diff-sufficiency setp (x) → setp (set-diff (x, y))

;; The definition of FIX-PROPERP was also added in polishing because
;; of a problem with the proof of GEN-CLOSURE-ACCEPT in
;; "generalize.events".  Here are a couple of lemmas about it that
;; might or might not be useful; all other lemmas about it above, and
;; the definition, were added during polishing.

Event: Disable fix-properp.

Theorem: subsetp-fix-properp-1 subsetp (fix-properp (x), y) = subsetp (x, y)

Theorem: subsetp-fix-properp-2 subsetp (x, fix-properp (y)) = subsetp (x, y)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; alists.events file
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Requires deftheory enhancement.
;; Requires sets.
;; Alists, March 1990.  Most of the definitions and some of the lemmas
;; were contributed by Bill Bevier; the rest are by Matt Kaufmann.
;; Functions defined here:
;; (deftheory alist-defns
;;   (alistp domain range value bind rembind invert mapping
;;           restrict co-restrict))

Definition: alistp (x) = if listp (x) then listp (car (x)) ∧ alistp (cdr (x))

else x = nil endif

Theorem: alistp-implies-properp alistp (x) → properp (x)

Theorem: alistp-nlistp (x ≃ nil) → (alistp (x) = (x = nil))

Theorem: alistp-cons alistp (cons (a, x)) = (listp (a) ∧ alistp (x))

Event: Disable alistp.

Theorem: alistp-append alistp (append (x, y)) = (alistp (fix-properp (x)) ∧ alistp (y))

Definition: domain (map) = if listp (map)

then if listp (car (map)) then cons (car (car (map)), domain (cdr (map)))

else domain (cdr (map)) endif else nil endif

Theorem: properp-domain properp (domain (map))

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

Theorem: domain-nlistp (map ≃ nil) → (domain (map) = nil)

Theorem: domain-cons domain (cons (a, map)) = if listp (a) then cons (car (a), domain (map))

else domain (map) endif

Theorem: member-domain-sufficiency (cons (a, x) ∈ y) → (a ∈ domain (y))

Theorem: subsetp-domain subsetp (x, y) → subsetp (domain (x), domain (y))

Event: Disable domain.

Definition: range (map) = if listp (map)

then if listp (car (map)) then cons (cdr (car (map)), range (cdr (map)))

else range (cdr (map)) endif else nil endif

Theorem: properp-range properp (range (map))

Theorem: range-append range (append (s1 , s2 )) = append (range (s1 ), range (s2 ))

Theorem: range-nlistp (map ≃ nil) → (range (map) = nil)

Theorem: range-cons range (cons (a, map)) = if listp (a) then cons (cdr (a), range (map))

else range (map) endif

Event: Disable range.

;; BOUNDP has been eliminated in favor of membership in domain.
;; Notice that I have to talk about things like disjointness of
;; domains anyhow.  New definition body would be (member x (domain map)).
;(defn boundp (x map)
;  (if (listp map)
;      (if (listp (car map))
;          (if (equal x (caar map))
;              t
;            (boundp x (cdr map)))
;        (boundp x (cdr map)))
;    f))

Definition: value (x, map) = if listp (map)

then if listp (car (map)) ∧ (x = caar (map)) then cdar (map)

else value (x, cdr (map)) endif else 0 endif Theorem: value-nlistp (map ≃ nil) → (value (x, map) = 0)

Theorem: value-cons value (x, cons (pair, map)) = if listp (pair) ∧ (x = car (pair)) then cdr (pair)

else value (x, map) endif

Event: Disable value.

Definition: bind (x, v, map) = if listp (map)

then if listp (car (map))

then if x = caar (map) then cons (cons (x, v), cdr (map)) else cons (car (map), bind (x, v, cdr (map))) endif

else cons (car (map), bind (x, v, cdr (map))) endif else cons (cons (x, v), nil) endif

Definition: rembind (x, map) = if listp (map)

then if listp (car (map))

then if x = caar (map) then cdr (map)

else cons (car (map), rembind (x, cdr (map))) endif else cons (car (map), rembind (x, cdr (map))) endif

else nil endif

Definition: invert (map) = if listp (map)

then if listp (car (map))

then cons (cons (cdr (car (map)), car (car (map))), invert (cdr (map))) else invert (cdr (map)) endif

else nil endif

Theorem: properp-invert properp (invert (map))

Theorem: invert-nlistp (map ≃ nil) → (invert (map) = nil)

Theorem: invert-cons invert (cons (pair, map)) = if listp (pair) then cons (cons (cdr (pair), car (pair)), invert (map))

else invert (map) endif Theorem: value-invert-not-member-of-domain ((g ∈ range (sg)) ∧ disjoint (domain (s), domain (sg))) → (value (g, invert (sg)) ∉ domain (s))

Event: Disable invert.

Definition: mapping (map) = (alistp (map) ∧ setp (domain (map)))

;; For when we disable mapping:

Theorem: mapping-implies-alistp mapping (map) → alistp (map)

Theorem: mapping-implies-setp-domain mapping (map) → setp (domain (map))

Definition: restrict (s, new-domain) = if listp (s)

then if listp (car (s)) ∧ (caar (s) ∈ new-domain) then cons (car (s), restrict (cdr (s), new-domain)) else restrict (cdr (s), new-domain) endif

else nil endif

Definition: co-restrict (s, new-domain) = if listp (s)

then if listp (car (s)) ∧ (caar (s) ∉ new-domain) then cons (car (s), co-restrict (cdr (s), new-domain)) else co-restrict (cdr (s), new-domain) endif

else nil endif

Event: Let us define the theory alist-defns to consist of the following events: alistp, domain, range, value, bind, rembind, invert, mapping, restrict, co-restrict.

;;;;; alist lemmas
; DOMAIN
;; The following was proved in the course of the final run through
;; the generalization proof.  The one after it isn't needed but
;; seems like it's worth proving too.  Actually now I see that
;; some other lemmas are now obsolete, so I'll put these both
;; early in the file and delete the others.

Theorem: domain-restrict domain (restrict (s, dom)) = intersection (domain (s), dom)

Theorem: domain-co-restrict domain (co-restrict (s, dom)) = set-diff (domain (s), dom)

Theorem: domain-bind domain (bind (x, v, map)) = if x ∈ domain (map) then domain (map)

else append (domain (map), list (x)) endif

Theorem: domain-rembind domain (rembind (x, map)) = delete (x, domain (map))

Theorem: domain-invert domain (invert (map)) = range (map)

; RANGE

Theorem: range-invert range (invert (map)) = domain (map)

; BOUNDP

Theorem: boundp-bind (x ∈ domain (bind (y, v, map))) = ((x = y) ∨ (x ∈ domain (map)))

Theorem: boundp-rembind mapping (map) → ((x ∈ domain (rembind (y, map)))

= if x = y then f else x ∈ domain (map) endif)

Theorem: boundp-subsetp (subsetp (map1 , map2 ) ∧ (name ∈ domain (map1 ))) → (name ∈ domain (map2 ))

Theorem: disjoint-domain-singleton (disjoint (domain (s), list (x)) = (x ∉ domain (s))) ∧ (disjoint (list (x), domain (s)) = (x ∉ domain (s)))

Theorem: boundp-value-invert (x ∈ range (map)) → (value (x, invert (map)) ∈ domain (map))

; VALUE

Theorem: value-when-not-bound (name ∉ domain (map)) → (value (name, map) = 0)

Theorem: value-bind value (x, bind (y, v, map)) = if x = y then v

else value (x, map) endif

Theorem: value-rembind mapping (map) → (value (x, rembind (y, map))

= if x = y then 0 else value (x, map) endif)

Theorem: value-append value (x, append (s1 , s2 )) = if x ∈ domain (s1 ) then value (x, s1 )

else value (x, s2 ) endif

Theorem: value-value-invert ((x ∈ range (s)) ∧ mapping (s)) → (value (value (x, invert (s)), s) = x)

; MAPPING

Theorem: mapping-append mapping (append (s1 , s2 )) = (disjoint (domain (s1 ), domain (s2 ))

∧ mapping (fix-properp (s1 )) ∧ mapping (s2 ))

Event: Disable mapping.

;; RESTRICT and CO-RESTRICT

Theorem: alistp-restrict alistp (restrict (s, r))

Theorem: alistp-co-restrict alistp (co-restrict (s, r))

Theorem: value-restrict ((a ∈ r) ∧ (a ∈ domain (s))) → (value (a, restrict (s, r)) = value (a, s))

Theorem: value-co-restrict ((a ∉ r) ∧ (a ∈ domain (s))) → (value (a, co-restrict (s, r)) = value (a, s))

Theorem: mapping-restrict mapping (s) → mapping (restrict (s, x))

Theorem: mapping-co-restrict mapping (s) → mapping (co-restrict (s, x))

Event: Disable restrict.

Event: Disable co-restrict.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; terms.events file
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Requires deftheory and constrain enhancments.
;; Requires sets and alists libraries.
;; This is a library of events about terms, including substitutions.
;; A TERMP is either a variable or the application of a function
;; symbol to a "proper list" of terms.  Variables and function symbols
;; are introduced with CONSTRAIN.
;; NOTE:  In functions like TERMP that have a flag, it seems to be
;; important to use T and F rather than, say, T and 'LIST.  That's
;; because otherwise, the "worse-than" heuristic will otherwise
;; prevent some necessary backchaining in cases where the hypothesis
;; to be relieved is of the form (TERMP 'LIST ...) and an "ancestor"
;; is of the form (TERMP T ...).
;; Definitions:
;; (deftheory term-defns
;;  (variablep-intro variable-listp termp function-symbol-intro all-vars))
;; (deftheory substitution-defns
;;   (instance var-substp compose apply-to-subst subst

;;    nullify-subst ;; returns a substitution whose range has no variables
;;    ))

Conservative Axiom: variablep-intro (listp (x) → (¬ variablep (x))) ∧ (truep (variablep (x)) ∨ falsep (variablep (x)))

Simultaneously, we introduce the new function symbol variablep.

Definition: variable-listp (x) = if listp (x) then variablep (car (x)) ∧ variable-listp (cdr (x))

else x = nil endif

Theorem: variable-listp-implies-properp variable-listp (x) → properp (x)

Theorem: variable-listp-cons variable-listp (cons (a, x)) = (variablep (a) ∧ variable-listp (x))

Theorem: variable-nlistp (x ≃ nil) → (variable-listp (x) = (x = nil))

Event: Disable variable-listp.

Conservative Axiom: function-symbol-intro function-symbol-p (fn)

Simultaneously, we introduce the new function symbols function-symbol-p and fn.

Definition: termp (flg, x) = if flg

then if variablep (x) then t elseif listp (x) then function-symbol-p (car (x)) ∧ termp (f, cdr (x)) else f endif

elseif listp (x) then termp (t, car (x)) ∧ termp (f, cdr (x))

else x = nil endif

Theorem: termp-list-cons termp (f, cons (a, x)) = (termp (t, a) ∧ termp (f, x))

Theorem: termp-list-nlistp (x ≃ nil) → (termp (f, x) = (x = nil))

Theorem: termp-t-cons flg → (termp (flg, cons (a, x)) = (function-symbol-p (a) ∧ termp (f, x)))

Theorem: termp-t-nlistp (flg ∧ (¬ listp (x))) → (termp (flg, x) = variablep (x))

Event: Disable termp.

Theorem: termp-list-implies-properp termp (f, x) → properp (x)

Definition: all-vars (flg, x) = if flg

then if variablep (x) then list (x)

elseif listp (x) then all-vars (f, cdr (x))

else nil endif elseif listp (x) then append (all-vars (t, car (x)), all-vars (f, cdr (x))) else nil endif

Theorem: properp-all-vars properp (all-vars (flg, x))

Theorem: all-vars-list-cons all-vars (f, cons (a, x)) = append (all-vars (t, a), all-vars (f, x))

Theorem: all-vars-t-cons flg → (all-vars (flg, cons (a, x)) = all-vars (f, x))

;; Here is a hack to deal with the flags.

Theorem: all-vars-subsetp-append-hack (flg1 ∧ flg2 ) → (subsetp (all-vars (flg1 , x), append (all-vars (flg2 , x), y))

∧ subsetp (all-vars (flg1 , x), append (y, all-vars (flg2 , x))))

;; The following is used later in the proof of MEMBER-PRESERVES-DISJOINT-ALL-VARS
;; and could conceivably be of use elsewhere.

Theorem: all-vars-flg-boolean flg → (all-vars (flg, x) = all-vars (t, x))

Event: Disable all-vars.

Event: Let us define the theory term-defns to consist of the following events: variablep-intro, variable-listp, termp, function-symbol-intro, all-vars.

;;;;; lemmas about termps

Theorem: variable-listp-set-diff variable-listp (x) → variable-listp (set-diff (x, y))

Theorem: all-vars-variablep (flg ∧ variablep (x)) → (all-vars (flg, x) = list (x))

Theorem: member-variable-listp-implies-variablep ((a ∈ x) ∧ variable-listp (x)) → variablep (a)

;; The following was proved in the course of the final run through the
;; generalization proof.  But in fact it's useful for the next result,
;; especially in the presence of domain-restrict -- so I don't need to
;; enable restrict there any longer.  Similarly for the lemma after
;; that.

Theorem: variable-listp-intersection (variable-listp (x) ∨ variable-listp (y)) → variable-listp (intersection (x, y))

Theorem: variable-listp-domain-restrict variable-listp (domain (s)) → variable-listp (domain (restrict (s, x)))

Theorem: variable-listp-domain-co-restrict variable-listp (domain (s)) → variable-listp (domain (co-restrict (s, x)))

Theorem: termp-range-restrict termp (f, range (s)) → termp (f, range (restrict (s, x)))

Theorem: termp-range-co-restrict termp (f, range (s)) → termp (f, range (co-restrict (s, x)))

Theorem: member-preserves-disjoint-all-vars-lemma (disjoint (y, all-vars (f, x)) ∧ (g ∈ x)) → disjoint (y, all-vars (t, g))

Theorem: member-preserves-disjoint-all-vars (flg ∧ disjoint (y, all-vars (f, x)) ∧ (g ∈ x)) → disjoint (y, all-vars (flg, g))

Theorem: member-all-vars-subsetp (flg ∧ (a ∈ x)) → subsetp (all-vars (flg, a), all-vars (f, x))

Theorem: all-vars-f-monotone subsetp (x, y) → subsetp (all-vars (f, x), all-vars (f, y))

;;;;; substitutions:  definitions

Definition: var-substp (s) = (mapping (s) ∧ variable-listp (domain (s)) ∧ termp (f, range (s)))

Definition: subst (flg, s, x) = if flg

then if x ∈ domain (s) then value (x, s) elseif variablep (x) then x elseif listp (x) then cons (car (x), subst (f, s, cdr (x))) else f endif

elseif listp (x) then cons (subst (t, s, car (x)), subst (f, s, cdr (x)))

else nil endif

Definition: apply-to-subst (s1 , s2 ) = if listp (s2 )

then if listp (car (s2 ))

then cons (cons (caar (s2 ), subst (t, s1 , cdar (s2 ))), apply-to-subst (s1 , cdr (s2 )))

else apply-to-subst (s1 , cdr (s2 )) endif else nil endif

Definition: compose (s1 , s2 ) = append (apply-to-subst (s2 , s1 ), s2 )

;; The following was in the original version, but isn't needed.
;;;  (defn-sk instance (flg term1 term2)
;;;    ;; term1 is an instance of term2
;;;    (exists one-way-unifier
;;;            (and (var-substp one-way-unifier)
;;;                 (equal term1 (subst flg one-way-unifier term2)))))
;;;;; substitution lemmas

Theorem: subst-list-cons subst (f, s, cons (a, x)) = cons (subst (t, s, a), subst (f, s, x))

Theorem: subst-list-nlistp (x ≃ nil) → (subst (f, s, x) = nil)

Theorem: subst-t-variablep (flg ∧ variablep (x)) → (subst (flg, s, x)

= if x ∈ domain (s) then value (x, s) else x endif)

Theorem: subst-t-non-variablep flg → (subst (flg, s, cons (fn, x))

= if cons (fn, x) ∈ domain (s) then value (cons (fn, x), s) else cons (fn, subst (f, s, x)) endif)

Theorem: all-vars-subst-lemma (flg ∧ (x ∈ domain (s))) → subsetp (all-vars (flg, value (x, s)), all-vars (f, range (s)))

Theorem: all-vars-subst termp (flg, x) → subsetp (all-vars (flg, subst (flg, s, x)),

append (all-vars (flg, x), all-vars (f, range (s))))

Theorem: subst-occur (flg ∧ (x ∈ domain (s))) → (subst (flg, s, x) = value (x, s))

Theorem: boundp-in-var-substp-implies-variablep (variable-listp (domain (s)) ∧ (¬ variablep (a))) → (a ∉ domain (s))

Theorem: variablep-value-invert (variable-listp (domain (s)) ∧ (x ∈ range (s))) → variablep (value (x, invert (s)))

Theorem: subst-invert (termp (flg, x) ∧ disjoint (domain (s), all-vars (flg, x)) ∧ var-substp (s)) → (subst (flg, s, subst (flg, invert (s), x)) = x)

Theorem: boundp-apply-to-subst (x ∈ domain (apply-to-subst (s1 , s2 ))) = (x ∈ domain (s2 ))

Theorem: mapping-apply-to-subst mapping (s) → mapping (apply-to-subst (s1 , s))

Theorem: alistp-apply-to-subst alistp (apply-to-subst (s1 , s2 ))

Theorem: subst-flg-not-list flg → (((subst (flg, s, x) = subst (t, s, x)) = t)

∧ ((subst (t, s, x) = subst (flg, s, x)) = t))

Theorem: subst-co-restrict (disjoint (x, intersection (domain (s), all-vars (flg, term))) ∧ variable-listp (domain (s)) ∧ termp (flg, term)) → (subst (flg, co-restrict (s, x), term) = subst (flg, s, term))

Theorem: subst-restrict (subsetp (intersection (domain (s), all-vars (flg, term)), x) ∧ variable-listp (domain (s)) ∧ termp (flg, term)) → (subst (flg, restrict (s, x), term) = subst (flg, s, term))

Theorem: termp-value (flg ∧ (x ∈ domain (s)) ∧ termp (f, range (s))) → termp (flg, value (x, s))

Theorem: termp-subst (termp (flg, x) ∧ termp (f, range (s))) → termp (flg, subst (flg, s, x))

Theorem: termp-domain variable-listp (domain (s)) → termp (f, domain (s))

Theorem: domain-apply-to-subst domain (apply-to-subst (s1 , s2 )) = domain (s2 )

Theorem: var-substp-apply-to-subst (termp (f, range (s)) ∧ termp (f, range (sg))) → termp (f, range (apply-to-subst (sg, s)))

Theorem: value-apply-to-subst (g ∈ domain (s)) → (value (g, apply-to-subst (sg, s)) = subst (t, sg, value (g, s)))

Theorem: non-variablep-not-member-of-variable-listp (variable-listp (d) ∧ (¬ variablep (term))) → (term ∉ d)

Theorem: compose-property (variable-listp (domain (s2 )) ∧ termp (flg, x)) → (subst (flg, compose (s1 , s2 ), x) = subst (flg, s2 , subst (flg, s1 , x)))

Theorem: compose-property-reversed (variable-listp (domain (s2 )) ∧ termp (flg, x)) → (subst (flg, s2 , subst (flg, s1 , x)) = subst (flg, compose (s1 , s2 ), x))

Event: Disable compose-property.

Theorem: subst-not-occur (termp (flg, x) ∧ variable-listp (domain (s)) ∧ disjoint (domain (s), all-vars (flg, x))) → (subst (flg, s, x) = x)

Theorem: disjoint-range-implies-disjoint-value ((x ∈ domain (s)) ∧ flg ∧ disjoint (z, all-vars (f, range (s)))) → disjoint (z, all-vars (flg, value (x, s)))

Theorem: disjoint-all-vars-subst (termp (flg, x) ∧ disjoint (z, all-vars (flg, x)) ∧ disjoint (z, all-vars (f, range (s)))) → disjoint (z, all-vars (flg, subst (flg, s, x)))

Theorem: all-vars-variable-listp variable-listp (x) → (all-vars (f, x) = x)

Theorem: variable-listp-append variable-listp (append (x, y)) = (variable-listp (fix-properp (x)) ∧ variable-listp (y))

Theorem: termp-list-append termp (f, append (x, y)) = (termp (f, fix-properp (x)) ∧ termp (f, y))

Theorem: apply-to-subst-append apply-to-subst (sg, append (s1 , s2 )) = append (apply-to-subst (sg, s1 ), apply-to-subst (sg, s2 ))

Theorem: subst-apply-to-subst (flg ∧ (g ∈ domain (s))) → (subst (flg, apply-to-subst (sg, s), g) = subst (flg, sg, value (g, s)))

Theorem: subst-append-not-occur-1 (termp (flg, x) ∧ variable-listp (domain (s1 )) ∧ disjoint (all-vars (f, domain (s1 )), all-vars (flg, x))) → (subst (flg, append (s1 , s2 ), x) = subst (flg, s2 , x))

Theorem: subst-append-not-occur-2 (termp (flg, x) ∧ variable-listp (domain (s2 )) ∧ disjoint (all-vars (f, domain (s2 )), all-vars (flg, x))) → (subst (flg, append (s1 , s2 ), x) = subst (flg, s1 , x))

Theorem: apply-to-subst-is-no-op-for-disjoint-domain (variable-listp (domain (s1 )) ∧ alistp (s2 ) ∧ termp (f, range (s2 )) ∧ disjoint (domain (s1 ), all-vars (f, range (s2 )))) → (apply-to-subst (s1 , s2 ) = s2 )

Theorem: member-subst (flg ∧ (a ∈ x)) → (subst (flg, s, a) ∈ subst (f, s, x))

Theorem: subsetp-subst subsetp (x, y) → subsetp (subst (f, s, x), subst (f, s, y))

;;; (disable instance) -- not included in this version
;;;(disable compose) -- COMPOSE is left enabled for use with COMPOSE-PROPERTY-REVERSED

Event: Disable apply-to-subst.

Event: Disable subst.

Event: Disable rembind.

Event: Disable bind.

;;;;; nullify-subst:  a substitution that has a range containing
;;                    no variables

Definition: nullify-subst (s) = if listp (s)

then if listp (car (s)) then cons (cons (caar (s), list (fn)), nullify-subst (cdr (s))) else nullify-subst (cdr (s)) endif

else nil endif

Theorem: properp-nullify-subst properp (nullify-subst (s))

Theorem: all-vars-f-range-nullify-subst all-vars (f, range (nullify-subst (s))) = nil

Theorem: termp-range-nullify-subst termp (f, range (nullify-subst (s)))

Theorem: domain-nullify-subst domain (nullify-subst (s)) = domain (s)

Theorem: mapping-nullify-subst alistp (s) → (mapping (nullify-subst (s)) = mapping (s))

Theorem: disjoint-all-vars-subst-nullify-subst termp (flg, term) → disjoint (domain (sg), all-vars (flg, subst (flg, nullify-subst (sg), term)))

Theorem: disjoint-all-vars-range-apply-subst-nullify-subst termp (f, range (s)) → disjoint (domain (sg),

all-vars (f, range (apply-to-subst (nullify-subst (sg), s))))

Event: Disable nullify-subst.

Event: Let us define the theory substitution-defns to consist of the following events: var-substp, compose, apply-to-subst, subst, nullify-subst.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; generalize.events file
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Requires sets, alists, and terms, which currently contain a number
;; of rules that aren't really needed here, even indirectly.
;; This is a proof soundness of a slight abstraction of the GENERALIZE
;; command of PC-NQTHM.
#| Here's what I want to prove.
(implies (and (generalize-okp sg state)
              (valid-state (generalize sg state)))
         (valid-state state))
I also prove the much simpler fact, GENERALIZE-STATEP:
(implies (generalize-okp sg state)
         (statep (generalize sg state)))
|#
;; << 1 >>

Conservative Axiom: theorem-intro ((theorem (x) ∧ flg) → termp (flg, x)) ∧ ((theorem (x) ∧ flg ∧ var-substp (s)) → theorem (subst (flg, s, x)))

Simultaneously, we introduce the new function symbol theorem.

;; << 2 >>

Definition: theorem-list (x) = if listp (x) then theorem (car (x)) ∧ theorem-list (cdr (x))

else x = nil endif

;; << 3 >>

Theorem: theorem-list-properties (theorem-list (x) → termp (f, x)) ∧ ((theorem-list (x) ∧ var-substp (s)) → theorem-list (subst (f, s, x)))

;; << 4 >>

Definition: statep (state) = (listp (state) ∧ termp (f, car (state)) ∧ variable-listp (cdr (state)))

;; << 5 >>
#|
(DEFN-SK VALID-STATE
         (STATE)
         (AND (STATEP STATE)
              (EXISTS WITNESSING-INSTANTIATION
                      (AND (VAR-SUBSTP WITNESSING-INSTANTIATION)
                           (SUBSETP (DOMAIN WITNESSING-INSTANTIATION)
                                    (CDR STATE))
                           (THEOREM-LIST (SUBST F WITNESSING-INSTANTIATION
                                                (CAR STATE)))))))

Adding the Skolem axiom:
      (AND
       (IMPLIES (AND (STATEP STATE)
                     (VAR-SUBSTP WITNESSING-INSTANTIATION)
                     (SUBSETP (DOMAIN WITNESSING-INSTANTIATION)
                              (CDR STATE))
                     (THEOREM-LIST (SUBST F WITNESSING-INSTANTIATION

                                          (CAR STATE))))
                (VALID-STATE STATE))
       (IMPLIES (NOT (AND (STATEP STATE)
                          (VAR-SUBSTP (WITNESSING-INSTANTIATION STATE))
                          (SUBSETP (DOMAIN (WITNESSING-INSTANTIATION STATE))
                                   (CDR STATE))
                          (THEOREM-LIST (SUBST F
                                               (WITNESSING-INSTANTIATION STATE)
                                               (CAR STATE)))))
                (NOT (VALID-STATE STATE)))).

     As this is a DEFN-SK we can conclude that:
      (OR (TRUEP (VALID-STATE STATE))
          (FALSEP (VALID-STATE STATE)))
is a theorem.

|#

Event: Introduce the function symbol witnessing-instantiation of one argument.

Event: Introduce the function symbol valid-state of one argument.

Axiom: valid-state-intro ((statep (state) ∧ var-substp (witnessing-instantiation) ∧ subsetp (domain (witnessing-instantiation), cdr (state)) ∧ theorem-list (subst (f, witnessing-instantiation, car (state)))) → valid-state (state)) ∧ ((¬ (statep (state)

∧ var-substp (witnessing-instantiation (state))

∧ subsetp (domain (witnessing-instantiation (state)),

cdr (state))

∧ theorem-list (subst (f, witnessing-instantiation (state), car (state)))))

→ (¬ valid-state (state)))

Axiom: valid-state-type truep (valid-state (state)) ∨ falsep (valid-state (state))

;; << 6 >>

Definition: new-gen-vars (goals, free, vars) = if listp (goals)

then let current-free-vars be intersection (free,

all-vars (t, car (goals)))

in

if disjoint (current-free-vars, vars)

then new-gen-vars (cdr (goals), free, vars)

else append (current-free-vars,

new-gen-vars (cdr (goals), free, vars)) endif endlet

else nil endif

;; << 7 >>

Definition: cardinality (x) = length (make-set (x))

;; Next goal:  get the definition of GEN-CLOSURE accepted.  In fact,
;; the lemma GEN-CLOSURE-ACCEPT below suffices, taking NEW to be
;; (NEW-GEN-VARS GOALS FREE FREE-VARS-SO-FAR), as long as we prove the
;; following lemma, NEW-GEN-VARS-SUBSET.
;; << 8 >>

Theorem: new-gen-vars-subset subsetp (new-gen-vars (goals, free, vars), free)

;; It is interesting to note that the exact form of the following
;; lemma changed while polishing the proof, since rewrite rules
;; applied to the old version so as to make it irrelevant.
;; << 9 >>

Theorem: gen-closure-accept ((¬ subsetp (new, free-vars-so-far)) ∧ subsetp (new, free)) → (((length (make-set (free))

− length (intersection (make-set (free), free-vars-so-far))) − length (intersection (set-diff (make-set (free), free-vars-so-far),

new)))

< (length (make-set (free)) − length (intersection (make-set (free), free-vars-so-far))))

;; Here I have a choice:  I could intersect the accumulator with free
;; at the end, or I could assume that it's intersected with free

;; before it's input.  I'll choose the former approach, so that I'll
;; have a simpler rewrite rule and so that I can call gen-closure more
;; simply.  I may wish to commute the arguments to intersection in the
;; exit below, but probably that won't matter because I'll only be
;; talking about membership.
;; << 10 >>

Definition: gen-closure (goals, free, free-vars-so-far) = let new-free-vars be new-gen-vars (goals, free, free-vars-so-far)

in

if subsetp (new-free-vars, free-vars-so-far) then intersection (free-vars-so-far, free) else gen-closure (goals,

free,

append (new-free-vars, free-vars-so-far)) endif endlet

;; << 11 >>

Definition: generalize-okp (sg, state) = (var-substp (sg)

∧ statep (state)

∧ disjoint (domain (sg), all-vars (f, car (state))) ∧ listp (car (state)) ∧ disjoint (domain (sg), cdr (state)))

;; << 12 >>

Definition: generalize (sg, state) = let g be caar (state),

p be cdar (state), free be cdr (state), sg-vars be all-vars (f, range (sg))

in

let new-g be subst (t, invert (sg), g)

in

let new-free be set-diff (free,

intersection (gen-closure (cons (new-g,

p), free, all-vars (t,

new-g)), all-vars (f,

range (sg))))

in

cons (cons (new-g, p), new-free) endlet endlet endlet

;; Here is a fact, not needed elsewhere, that is worth noticing, in
;; case we wish to extend the current theorem to a sequence of commands.
;; << 13 >>

Theorem: generalize-statep generalize-okp (sg, state) → statep (generalize (sg, state))

;; << 14 >>

Definition: gen-inst (sg, state) = let s be witnessing-instantiation (generalize (sg, state)),

domain-1 be gen-closure (cons (subst (t, invert (sg), caar (state)),

cdar (state)), cdr (state), all-vars (t,

subst (t, invert (sg), caar (state))))

in

let s1 be restrict (s, domain-1 ),

s2 be apply-to-subst (nullify-subst (sg),

co-restrict (s, domain-1 ))

in

apply-to-subst (apply-to-subst (s2 , sg), append (s1 , s2 )) endlet endlet

;; Let's see that it suffices to prove the result of opening up the
;; conclusion of the main theorem with a particular witness.
#|
(add-axiom main-theorem-1 (rewrite)
  (let ((wit (gen-inst sg state)))
    (implies (and (generalize-okp sg state)
                  (valid-state (generalize sg state)))
             (and (statep state)
                  (var-substp wit)
                  (subsetp (domain wit) (cdr state))
                  (theorem-list (subst f wit (car state)))))))

(prove-lemma generalize-is-correct (rewrite)
  (implies (and (generalize-okp sg state)
                (valid-state (generalize sg state)))
           (valid-state state))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable main-theorem-1)
   (use (valid-state-intro
         (witnessing-instantiation (gen-inst sg state))))))
|#
;; So, it suffices to prove main-theorem-1.  The first three conjuncts
;; of the conclusion are quite trivial.
;; << 15 >>

Theorem: main-theorem-1-case-1 generalize-okp (sg, state) → statep (state)

;; We put one direction of the definition of valid-state here, for
;; efficiency in proofs.
;; << 16 >>

Theorem: valid-state-opener valid-state (state) = (statep (state)

∧ let witnessing-instantiation be witnessing-instantiation (state) in var-substp (witnessing-instantiation) ∧ subsetp (domain (witnessing-instantiation),

cdr (state))

∧ theorem-list (subst (f, witnessing-instantiation, car (state))) endlet)

;; << 17 >>

Theorem: main-theorem-1-case-2 let wit be gen-inst (sg, state) in (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → var-substp (wit) endlet Theorem: subsetp-cdr-generalize subsetp (cdr (generalize (sg, state)), cdr (state))

;; At this point I had to prove SUBSETP-SET-DIFF-SUFFICIENCY because
;; of some lemma that was created during the polishing process
;; (perhaps DOMAIN-RESTRICT).
;; << 19 >>

Theorem: main-theorem-1-case-3 let wit be gen-inst (sg, state) in valid-state (generalize (sg, state)) → subsetp (domain (wit), cdr (state)) endlet

;; So now we only have to prove MAIN-THEOREM-1-CASE-4 (written here
;; without use of LET):
#|
(add-axiom main-theorem-1-case-4 (rewrite)
  (implies (and (generalize-okp sg state)
                (valid-state (generalize sg state)))
           (theorem-list (subst f (gen-inst sg state) (car state)))))
(prove-lemma main-theorem-1 (rewrite)
  (let ((wit (gen-inst sg state)))
    (implies (and (generalize-okp sg state)
                  (valid-state (generalize sg state)))
             (and (statep state)
                  (var-substp wit)
                  (subsetp (domain wit) (cdr state))
                  (theorem-list (subst f wit (car state))))))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable main-theorem-1-case-1 main-theorem-1-case-2
           main-theorem-1-case-3 main-theorem-1-case-4)))
|#
;; << 20 >>

Definition: gen-setting-substitutions (s1 , s2 , sg) = (var-substp (s1 )

∧ var-substp (s2 ) ∧ var-substp (sg) ∧ disjoint (domain (s1 ), domain (s2 )) ∧ disjoint (domain (s1 ), domain (sg)) ∧ disjoint (domain (s2 ), domain (sg)) ∧ disjoint (all-vars (f, range (sg)), domain (s1 )) ∧ disjoint (all-vars (f, range (s2 )), domain (sg)))

;; << 21 >>

Definition: main-hyps (s1 , s2 , sg, g, p) = (termp (t, g)

∧ disjoint (all-vars (t, g), domain (sg)) ∧ termp (f, p) ∧ disjoint (all-vars (f, p), domain (sg)) ∧ gen-setting-substitutions (s1 , s2 , sg) ∧ theorem-list (subst (f,

append (s1 , s2 ),

cons (subst (t, invert (sg), g), p))))

;; The goal above, MAIN-THEOREM-1-CASE-4, should follow from the
;; following two lemmas.
#|
(add-axiom main-hyps-suffice (rewrite)
(implies (and (listp goals)
            (main-hyps s1 s2 sg (car goals) (cdr goals)))
       (theorem-list (subst f
                            (apply-to-subst (apply-to-subst s2 sg)
                                            (append s1 s2))
                            goals))))
(add-axiom main-hyps-relieved (rewrite)
(let ((g (caar state))
    (p (cdar state))
    (free (cdr state))
    (s (witnessing-instantiation (generalize sg state))))
(let ((new-g (subst t (invert sg) g)))
  (let ((domain-1
         (gen-closure (cons new-g p) free (all-vars t new-g))))
    (let ((s1 (restrict s domain-1))

              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (main-hyps s1 s2 sg g p)))))))
(prove-lemma main-theorem-1-case-4 (rewrite)
  (implies (and (generalize-okp sg state)
                (valid-state (generalize sg state)))
           (theorem-list (subst f (gen-inst sg state) (car state))))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable gen-inst main-hyps-suffice generalize-okp main-hyps-relieved)))
|#
;; So, now let us start with MAIN-HYPS-SUFFICE.  It should follow from
;; two subgoals, as shown:
#|
(add-axiom main-hyps-suffice-first (rewrite)
  (implies (main-hyps s1 s2 sg g p)
           (theorem (subst t
                           (apply-to-subst (apply-to-subst s2 sg)
                                           (append s1 s2))
                           g))))
(add-axiom main-hyps-suffice-rest (rewrite)
  (implies (main-hyps s1 s2 sg g p)
           (theorem-list (subst f
                                (apply-to-subst (apply-to-subst s2 sg)
                                                (append s1 s2))
                                p))))
(prove-lemma main-hyps-suffice (rewrite)
  (implies (and (listp goals)
                (main-hyps s1 s2 sg (car goals) (cdr goals)))
           (theorem-list (subst f
                                (apply-to-subst (apply-to-subst s2 sg)
                                                (append s1 s2))
                                goals)))
  ((disable-theory t)
   (enable-theory ground-zero)

   (enable theorem-list subst main-hyps-suffice-first main-hyps-suffice-rest)))
|#
;; Consider the first of these.  Although COMPOSE-PROPERTY-REVERSED is
;; used in the proof (because it's enabled), it's actually not
;; necessary.  A proof took slightly over 10 minutes with the rule
;; enabled, and roughly 9 minutes without.
;; << 22 >>

Theorem: main-hyps-suffice-first-lemma-general (termp (flg, g) ∧ disjoint (all-vars (flg, g), domain (sg)) ∧ gen-setting-substitutions (s1 , s2 , sg) ∧ (sg-1 = invert (sg))) → (subst (flg, apply-to-subst (apply-to-subst (s2 , sg), append (s1 , s2 )), g)

= subst (flg, apply-to-subst (s2 , sg), subst (flg, append (s1 , s2 ), subst (flg, sg-1 , g))))

;; << 23 >>

Theorem: main-hyps-suffice-first-lemma (termp (t, g) ∧ disjoint (all-vars (t, g), domain (sg)) ∧ gen-setting-substitutions (s1 , s2 , sg)) → (subst (t, apply-to-subst (apply-to-subst (s2 , sg), append (s1 , s2 )), g)

= subst (t, apply-to-subst (s2 , sg), subst (t, append (s1 , s2 ), subst (t, invert (sg), g))))

;; << 24 >>

Theorem: main-hyps-suffice-first main-hyps (s1 , s2 , sg, g, p) → theorem (subst (t, apply-to-subst (apply-to-subst (s2 , sg), append (s1 , s2 )), g))

;; The following is useful with s = (append s1 s2).
;; << 25 >>

Theorem: main-hyps-suffice-rest-lemma (termp (flg, p) ∧ variable-listp (domain (sg))

∧ disjoint (all-vars (flg, p), domain (sg))) → (subst (flg, apply-to-subst (apply-to-subst (s2 , sg), s), p)

= subst (flg, apply-to-subst (s2 , sg), subst (flg, s, p)))

;; << 26 >>

Theorem: main-hyps-suffice-rest main-hyps (s1 , s2 , sg, g, p) → theorem-list (subst (f,

apply-to-subst (apply-to-subst (s2 , sg), append (s1 , s2 )), p))

;; << 27 >>

Theorem: main-hyps-suffice (listp (goals) ∧ main-hyps (s1 , s2 , sg, car (goals), cdr (goals))) → theorem-list (subst (f,

apply-to-subst (apply-to-subst (s2 , sg), append (s1 , s2 )), goals))

;; I'll disable the two lemmas used above so that I avoid the possibility
;; of looping with COMPOSE-PROPERTY-REVERSED.
;; << 28 >>

Event: Disable main-hyps-suffice-first-lemma.

;; << 29 >>

Event: Disable main-hyps-suffice-rest-lemma.

;; All that remains now is to prove MAIN-HYPS-RELIEVED.  If we open up
;; MAIN-HYPS we see what the necessary subgoals are.  Recall the
;; definition of MAIN-HYPS:
#|
(defn main-hyps (s1 s2 sg g p)
  (and (termp t g)
       (disjoint (all-vars t g) (domain sg))
       (termp f p)
       (disjoint (all-vars f p) (domain sg))
       (gen-setting-substitutions s1 s2 sg)
       (theorem-list (subst f (append s1 s2)
                            (cons (subst t (invert sg) g) p)))))

|#
;; << 30 >>

Theorem: main-hyps-relieved-1 let g be caar (state) in generalize-okp (sg, state) → termp (t, g) endlet

;; << 31 >>

Theorem: main-hyps-relieved-2 let g be caar (state) in generalize-okp (sg, state) → disjoint (all-vars (t, g), domain (sg)) endlet

;; << 32 >>

Theorem: main-hyps-relieved-3 let p be cdar (state) in generalize-okp (sg, state) → termp (f, p) endlet

;; << 33 >>

Theorem: main-hyps-relieved-4 let p be cdar (state) in generalize-okp (sg, state) → disjoint (all-vars (f, p), domain (sg)) endlet

#|
(add-axiom main-hyps-relieved-5 (rewrite)
 (let ((g (caar state))
       (p (cdar state))
       (free (cdr state))
       (s (witnessing-instantiation (generalize sg state))))
   (let ((new-g (subst t (invert sg) g)))
     (let ((domain-1
            (gen-closure (cons new-g p) free (all-vars t new-g))))
       (let ((s1 (restrict s domain-1))
             (s2 (apply-to-subst (nullify-subst sg)
                                 (co-restrict s domain-1))))
         (implies (and (generalize-okp sg state)
                       (valid-state (generalize sg state)))

           (gen-setting-substitutions s1 s2 sg)))))))
(add-axiom main-hyps-relieved-6 (rewrite)
(let ((g (caar state))
(p (cdar state))
(free (cdr state))
(s (witnessing-instantiation (generalize sg state))))
(let ((new-g (subst t (invert sg) g)))
(let ((domain-1
     (gen-closure (cons new-g p) free (all-vars t new-g))))
(let ((s1 (restrict s domain-1))
      (s2 (apply-to-subst (nullify-subst sg)
                          (co-restrict s domain-1))))
  (implies (and (generalize-okp sg state)
                (valid-state (generalize sg state)))
           (theorem-list (subst f (append s1 s2)
                                (cons (subst t (invert sg) g) p)))))))))
(prove-lemma main-hyps-relieved (rewrite)
(let ((g (caar state))
(p (cdar state))
(free (cdr state))
(s (witnessing-instantiation (generalize sg state))))
(let ((new-g (subst t (invert sg) g)))
(let ((domain-1
     (gen-closure (cons new-g p) free (all-vars t new-g))))
(let ((s1 (restrict s domain-1))
      (s2 (apply-to-subst (nullify-subst sg)
                          (co-restrict s domain-1))))
  (implies (and (generalize-okp sg state)
                (valid-state (generalize sg state)))
           (main-hyps s1 s2 sg g p))))))
((disable-theory t)
(enable-theory ground-zero)
(enable main-hyps main-hyps-relieved-1 main-hyps-relieved-2 main-hyps-relieved-3
   main-hyps-relieved-4 main-hyps-relieved-5 main-hyps-relieved-6)))
|#
;; So, we have left the goals MAIN-HYPS-RELIEVED-5 and
;; MAIN-HYPS-RELIEVED-6.  Let us start with the first.  Opening up
;; GEN-SETTING-SUBSTITUTIONS gives us a number of subgoals.
;; The first two cases below do not require knowledge about DOMAIN-1

;; (or G, P, FREE, or NEW-G), but simply following from the validity
;; of the state (GENERALIZE SG STATE).  Disabling GENERALIZE is very
;; useful (probably not necessary, though I didn't let the prover run
;; long enough to find out).
;; << 34 >>

Theorem: main-hyps-relieved-5-lemma-1 let s be witnessing-instantiation (generalize (sg, state)) in let s1 be restrict (s, domain-1 ),

s2 be apply-to-subst (nullify-subst (sg), co-restrict (s, domain-1 )) in valid-state (generalize (sg, state)) → (var-substp (s1 ) ∧ var-substp (s2 )) endlet endlet

;; The next case is trivial.
;; << 35 >>

Theorem: main-hyps-relieved-5-lemma-2 generalize-okp (sg, state) → var-substp (sg)

;; The next case is also quite trivial; notice how abstracted it is.
;; << 36 >>

Theorem: main-hyps-relieved-5-lemma-3 let s1 be restrict (s, domain-1 ),

s2 be apply-to-subst (nullify-subst (sg), co-restrict (s, domain-1 )) in disjoint (domain (s1 ), domain (s2 )) endlet

;; For the next two cases we first observe that (DOMAIN S) is disjoint
;; from (DOMAIN SG), and then we use SUBSETP-DISJOINT-1 where X is the
;; domain of S1 or S2, Y is the domain of S, and Z is the domain of
;; SG:
;;             (IMPLIES (AND (SUBSETP X Y) (DISJOINT Y Z))
;;                      (DISJOINT X Z))
;; << 37 >>

Theorem: witnessing-instantiation-is-disjoint-from-generalizing-substitution let s be witnessing-instantiation (generalize (sg, state)) in (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → disjoint (domain (s), domain (sg)) endlet

;; In the next case we abstract away DOMAIN-1 (and hence G, P, FREE,
;; and NEW-G).  Incidentally, a similar phenomenon occurred here to
;; the one reported just above the statement above of MAIN-THEOREM-1-CASE-3:
;; final polishing resulted in the need for another lemma.  That extra
;; lemma is DISJOINT-SET-DIFF-SUFFICIENCY in this case, to be found
;; in "sets.events".
;; << 38 >>

Theorem: main-hyps-relieved-5-lemma-4 let s be witnessing-instantiation (generalize (sg, state)) in let s1 be restrict (s, domain-1 ),

s2 be apply-to-subst (nullify-subst (sg), co-restrict (s, domain-1 )) in (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → (disjoint (domain (s1 ), domain (sg))

∧ disjoint (domain (s2 ), domain (sg))) endlet endlet

;; The lemma MAIN-HYPS-RELIEVED-5-LEMMA-5-WIT is true because the
;; domain of s is contained in the free variables of the generalized
;; state (by choice, i.e. definition, of witnessing-instantiation),
;; which is disjoint from the intersection of the indicated
;; GEN-CLOSURE with the variables in the range of sg.  I'll use a
;; trick that I learned from Ken Kunen (definable Skolem function is
;; all, really) to reduce disjointness considerations to membership
;; considerations.
;; << 39 >>

Theorem: main-hyps-relieved-5-lemma-5-wit let g be caar (state),

p be cdar (state), free be cdr (state), s be witnessing-instantiation (generalize (sg, state))

in let new-g be subst (t, invert (sg), g) in let domain-1 be gen-closure (cons (new-g, p),

free,

all-vars (t, new-g))

in let s1 be restrict (s, domain-1 ) in (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state)) ∧ (wit ∈ all-vars (f, range (sg))) ∧ (wit ∈ domain (s))) → (wit ∉ domain-1 ) endlet endlet endlet endlet

;; << 40 >>

Theorem: main-hyps-relieved-5-lemma-5 let g be caar (state),

p be cdar (state), free be cdr (state), s be witnessing-instantiation (generalize (sg, state))

in let new-g be subst (t, invert (sg), g) in let domain-1 be gen-closure (cons (new-g, p),

free,

all-vars (t, new-g))

in let s1 be restrict (s, domain-1 ) in (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → disjoint (all-vars (f, range (sg)), domain (s1 )) endlet endlet endlet endlet

;; << 41 >>

Theorem: main-hyps-relieved-5-lemma-6 let g be caar (state),

p be cdar (state), free be cdr (state), s be witnessing-instantiation (generalize (sg, state))

in let new-g be subst (t, invert (sg), g) in let domain-1 be gen-closure (cons (new-g, p),

free,

all-vars (t, new-g))

in let s2 be apply-to-subst (nullify-subst (sg),

co-restrict (s, domain-1 ))

in (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → disjoint (all-vars (f, range (s2 )), domain (sg)) endlet endlet endlet endlet Theorem: main-hyps-relieved-5 let g be caar (state),

p be cdar (state), free be cdr (state), s be witnessing-instantiation (generalize (sg, state))

in let new-g be subst (t, invert (sg), g) in let domain-1 be gen-closure (cons (new-g, p),

free,

all-vars (t, new-g))

in let s1 be restrict (s, domain-1 ),

s2 be apply-to-subst (nullify-subst (sg),

co-restrict (s, domain-1 ))

in (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → gen-setting-substitutions (s1 , s2 , sg) endlet endlet endlet endlet

;; Now all that is left is MAIN-HYPS-RELIEVED-6.  Actually, this lemma
;; doesn't have anything to do with inverse substitutions or even with
;; generalization, really.  The idea is simply that one takes a valid
;; state and wishes to split its witnessing substitution into two
;; parts.  The parts are the respective restriction and co-restriction
;; of the original substitution to some set that is ``closed'' in the
;; appropriate sense.  Actually, the co-restriction is allowed to have
;; a substitution applied to it, whose domain is disjoint from the
;; goals ``outside'' that closure.  Below we give the lemmas and the
;; proof of MAIN-HYPS-RELIEVED-6 from those lemmas.  But first let us
;; introduce the necessary notions.
;; << 43 >>

Definition: all-vars-disjoint-or-subsetp (goals, free, x) = if listp (goals)

then (subsetp (intersection (free, all-vars (t, car (goals))), x) ∨ disjoint (intersection (free, all-vars (t, car (goals))), x)) ∧ all-vars-disjoint-or-subsetp (cdr (goals), free, x)

else t endif

;; Our plan will be to show that (CDR STATE) has the above property

;; with respect to the free variables of the generalized state and the
;; appropriate gen-closure.  In cases where one applies a substitution
;; of the form (append s1 s2) to such a list of goals, where the
;; domain of s1 is contained in the intersection of those free
;; variables with that closure and the domain of s2 is disjoint from
;; that intersection, we'll show that the result is a theorem-list iff
;; each of the following are theorem-lists:  apply s1 to the goals
;; whose vars intersect its domain, and apply s2 to the rest.
;; Reduction rules about applying restrictions etc. will then finish
;; the job.
;; Notice the similarity of the following definition with new-gen-vars.
;; Think of vars as the closure variables, and free as the free variable
;; set within which this all "takes place".
;; << 44 >>

Definition: goals-intersecting-vars (goals, free, vars) = if listp (goals)

then let current-free-vars be intersection (free,

all-vars (t, car (goals)))

in

if disjoint (current-free-vars, vars)

then goals-intersecting-vars (cdr (goals), free, vars)

else cons (car (goals),

goals-intersecting-vars (cdr (goals), free, vars)) endif endlet

else nil endif

;; << 45 >>

Definition: goals-disjoint-from-vars (goals, free, vars) = if listp (goals)

then let current-free-vars be intersection (free,

all-vars (t, car (goals)))

in

if disjoint (current-free-vars, vars)

then cons (car (goals),

goals-disjoint-from-vars (cdr (goals), free, vars)) else goals-disjoint-from-vars (cdr (goals), free, vars) endif endlet

else nil endif

;; Now we begin the remaining goal, MAIN-HYPS-RELIEVED-6.  The idea is
;; to show that the appropriate goal list is a theorem-list by showing
;; separately that the first and the rest are theorems, since the
;; reasons are slightly different.  The first is a theorem because its
;; free vars are all in domain-1, hence in the domain of s1; so, s2
;; can be dropped from the APPEND.  The rest all have the property
;; that their free vars are contained in or disjoint from domain-1,
;; and for those disjoint from it, they do not contain variables from
;; the domain of sg.  Notice that the new current goal may violate the
;; latter requirement, since it may have no free vars at all but
;; contain vars from the domain of sg, and that's why we have to make
;; a special case out of it.
#|
(add-axiom main-hyps-relieved-6-first (rewrite)
  (let ((g (caar state))
        (p (cdar state))
        (free (cdr state))
        (s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (theorem (subst t (append s1 s2)
                                   (subst t (invert sg) g)))))))))
(add-axiom main-hyps-relieved-6-rest (rewrite)
  (let ((g (caar state))
        (p (cdar state))
        (free (cdr state))
        (s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))

                   (theorem-list (subst f (append s1 s2) p))))))))
(prove-lemma main-hyps-relieved-6 (rewrite)
  (let ((g (caar state))
        (p (cdar state))
        (free (cdr state))
        (s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (theorem-list (subst f (append s1 s2)
                                        (cons (subst t (invert sg) g) p))))))))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable main-hyps-relieved-6-first main-hyps-relieved-6-rest subst theorem-list)))
|#
;; The first is true because the free vars in new-g are all in the
;; domain of s1, since they are all in domain-1.  By the way, the
;; proof-checker was useful here; I dove to the subst term (after
;; adding abbreviations and promoting hypotheses) and saw that I
;; wanted to rewrite with SUBST-APPEND-NOT-OCCUR-2.  I also notice the
;; need for GEN-CLOSURE-CONTAINS-THIRD-ARG during the attempt to prove
;; a goal.
;; First, we only want to open up GENERALIZE when we are looking at
;; goals, not when we are simply asking about the witnessing
;; substitution.
;; << 46 >>

Theorem: car-generalize car (generalize (sg, state)) = cons (subst (t, invert (sg), caar (state)), cdar (state))

;; << 47 >>

Event: Disable generalize.

;; Inspection of the proof of a subgoal of MAIN-HYPS-RELIEVED-6-FIRST
;; suggests that we need the following lemma.  Actually, before the
;; final polishing it was the case that the following version sufficed.
;; But final polishing led me to prove a "better" version, as well
;; as the lemma DISJOINT-SET-DIFF-GENERAL in "sets.events".
#|
(prove-lemma gen-closure-contains-third-arg (rewrite)
  (implies (subsetp domain free)
           (subsetp (intersection domain free-vars-so-far)
                    (gen-closure goals free free-vars-so-far))))
|#
;; << 48 >>

Theorem: gen-closure-contains-third-arg subsetp (x, intersection (free, free-vars-so-far)) → subsetp (x, gen-closure (goals, free, free-vars-so-far))

;; << 49 >>

Theorem: main-hyps-relieved-6-first let g be caar (state),

p be cdar (state), free be cdr (state), s be witnessing-instantiation (generalize (sg, state))

in let new-g be subst (t, invert (sg), g) in let domain-1 be gen-closure (cons (new-g, p),

free,

all-vars (t, new-g))

in let s1 be restrict (s, domain-1 ),

s2 be apply-to-subst (nullify-subst (sg),

co-restrict (s, domain-1 ))

in (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → theorem (subst (t, append (s1 , s2 ), new-g)) endlet endlet endlet endlet

;; Now all that remains is MAIN-HYPS-RELIEVED-6-REST.
#|

;; I originally forgot the (TERMP F P) hypothesis below, but it wasn't
;; very hard to back up and fix this.
(add-axiom main-hyps-relieved-6-rest-generalization (rewrite)
(let ((s1 (restrict s domain-1))
(s2 (apply-to-subst (nullify-subst sg)
                    (co-restrict s domain-1))))
(implies (and (var-substp sg)
          (var-substp s)
          (subsetp (domain s) new-free)
          (termp f p)
          (theorem-list (subst f s p))
          (disjoint (domain sg)
                    (all-vars f (goals-disjoint-from-vars
                                 p new-free domain-1)))
          (all-vars-disjoint-or-subsetp p new-free domain-1))
     (theorem-list (subst f (append s1 s2) p)))))
(add-axiom main-hyps-relieved-6-rest-lemma-1 (rewrite)
(let ((g (caar state))
(p (cdar state))
(free (cdr state))
(s (witnessing-instantiation (generalize sg state))))
(let ((new-g (subst t (invert sg) g)))
(let ((domain-1
     (gen-closure (cons new-g p) free (all-vars t new-g))))
(let ((s1 (restrict s domain-1))
      (s2 (apply-to-subst (nullify-subst sg)
                          (co-restrict s domain-1))))
  (implies (and (generalize-okp sg state)
                (valid-state (generalize sg state)))
           (disjoint (domain sg)
                     (all-vars f (goals-disjoint-from-vars
                                  p (cdr (generalize sg state)) domain-1)))))))))
;; Minor note:  I used the BREAK-LEMMA feature of NQTHM to realize
;; that I needed the following lemma.
(add-axiom main-hyps-relieved-6-rest-lemma-2 (rewrite)
(let ((g (caar state))
(p (cdar state))
(free (cdr state))
(s (witnessing-instantiation (generalize sg state))))
(let ((new-g (subst t (invert sg) g)))

      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (all-vars-disjoint-or-subsetp p (cdr (generalize sg state)) domain-1)))))))
(prove-lemma main-hyps-relieved-6-rest (rewrite)
  (let ((g (caar state))
        (p (cdar state))
        (free (cdr state))
        (s (witnessing-instantiation (generalize sg state))))
    (let ((new-g (subst t (invert sg) g)))
      (let ((domain-1
             (gen-closure (cons new-g p) free (all-vars t new-g))))
        (let ((s1 (restrict s domain-1))
              (s2 (apply-to-subst (nullify-subst sg)
                                  (co-restrict s domain-1))))
          (implies (and (generalize-okp sg state)
                        (valid-state (generalize sg state)))
                   (theorem-list (subst f (append s1 s2) p)))))))
  ((disable-theory t)
   (enable-theory ground-zero)
   (enable theorem-list subst car-generalize ;; so that we can get at p from (car state)
           ;; relieving hyps of main-hyps-relieved-6-rest-generalization:
           main-hyps-relieved-6-rest-lemma-1 main-hyps-relieved-6-rest-lemma-2
           ;; to relieve the (termp f p) hypothesis in main-hyps-relieved-6-rest-generalization:
           statep termp-list-cons
           generalize-okp valid-state-opener main-hyps-relieved-6-rest-generalization)))
;; At this point I did a sanity check and sure enough, the pushed
;; lemmas all go through at this point:  main-hyps-relieved-6,
;; main-hyps-relieved, main-theorem-1-case-4, main-theorem-1, and
;; generalize-is-correct.
|#
;; It remains to prove MAIN-HYPS-RELIEVED-6-REST-LEMMA-1,
;; MAIN-HYPS-RELIEVED-6-REST-LEMMA-2, and
;; MAIN-HYPS-RELIEVED-6-REST-GENERALIZATION.
;; For the first of these we need the following trivial observation.

Theorem: goals-disjoint-from-vars-subsetp subsetp (goals-disjoint-from-vars (goals, free, vars), goals)

;; Unfortunately the observation above doesn't quite suffice, because
;; of a technical problem with free variables in hypotheses.  The
;; following consequence does, though.
;; << 51 >>

Theorem: disjoint-all-vars-goals-disjoint-from-vars disjoint (x, all-vars (f, goals)) → disjoint (x, all-vars (f, goals-disjoint-from-vars (goals, free, vars)))

;; << 52 >>

Theorem: main-hyps-relieved-6-rest-lemma-1 let g be caar (state),

p be cdar (state), free be cdr (state), s be witnessing-instantiation (generalize (sg, state))

in let new-g be subst (t, invert (sg), g) in let domain-1 be gen-closure (cons (new-g, p),

free,

all-vars (t, new-g))

in let s1 be restrict (s, domain-1 ),

s2 be apply-to-subst (nullify-subst (sg),

co-restrict (s, domain-1 ))

in (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → disjoint (domain (sg),

all-vars (f,

goals-disjoint-from-vars (p,

cdr (generalize (sg,

state)), domain-1 ))) endlet endlet endlet endlet

;; The next goal, MAIN-HYPS-RELIEVED-6-REST-LEMMA-2, needs the lemma
;; ALL-VARS-DISJOINT-OR-SUBSETP-GEN-CLOSURE below.  That lemma's

;; mechanical proof depends on the trivial observation
;; DISJOINT-INTERSECTION3-MIDDLE in file sets.events.
;; << 53 >>

Theorem: all-vars-disjoint-or-subsetp-gen-closure subsetp (domain, free) → all-vars-disjoint-or-subsetp (goals,

domain,

gen-closure (cons (g, goals), free, vars))

;; << 54 >>

Theorem: main-hyps-relieved-6-rest-lemma-2 let g be caar (state),

p be cdar (state), free be cdr (state), s be witnessing-instantiation (generalize (sg, state))

in let new-g be subst (t, invert (sg), g) in let domain-1 be gen-closure (cons (new-g, p),

free,

all-vars (t, new-g))

in let s1 be restrict (s, domain-1 ),

s2 be apply-to-subst (nullify-subst (sg),

co-restrict (s, domain-1 ))

in (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → all-vars-disjoint-or-subsetp (p,

cdr (generalize (sg,

state)), domain-1 ) endlet endlet endlet endlet

;; Finally, all that's left is
;; MAIN-HYPS-RELIEVED-6-REST-GENERALIZATION.  An attempted proof by
;; induction of that theorem results in 11 goals, all but one of which
;; goes through automatically.  The remaining one is as follows.
#|
(IMPLIES
 (AND

(DISJOINT NEW-FREE
          (INTERSECTION DOMAIN-1
                        (ALL-VARS T X)))
(THEOREM-LIST
 (SUBST F
        (APPEND (RESTRICT S DOMAIN-1)
                (APPLY-TO-SUBST (NULLIFY-SUBST SG)
                                (CO-RESTRICT S DOMAIN-1)))
        Z))
(MAPPING SG)
(VARIABLE-LISTP (DOMAIN SG))
(TERMP F (RANGE SG))
(MAPPING S)
(VARIABLE-LISTP (DOMAIN S))
(TERMP F (RANGE S))
(SUBSETP (DOMAIN S) NEW-FREE)
(TERMP T X)
(TERMP F Z)
(THEOREM (SUBST T S X))
(THEOREM-LIST (SUBST F S Z))
(DISJOINT (DOMAIN SG) (ALL-VARS T X))
(DISJOINT (DOMAIN SG)
          (ALL-VARS F
                    (GOALS-DISJOINT-FROM-VARS Z NEW-FREE DOMAIN-1)))
(ALL-VARS-DISJOINT-OR-SUBSETP Z NEW-FREE DOMAIN-1))
(THEOREM (SUBST T
               (APPEND (RESTRICT S DOMAIN-1)
                       (APPLY-TO-SUBST (NULLIFY-SUBST SG)
                                       (CO-RESTRICT S DOMAIN-1)))
               X)))
|#
;; Let us attempt to prove this goal with the proof-checker, thus
;; seeing why the rewriter can't handle it automatically.  We would
;; like to rewrite with SUBST-APPEND-NOT-OCCUR-1 to replace the
;; conclusion with:
#|
(THEOREM (SUBST T
              (APPLY-TO-SUBST (NULLIFY-SUBST SG)
                              (CO-RESTRICT S DOMAIN-1))
              X))
|#

;; However, in order to do that we need to observe that under the
;; hypotheses, the following holds.
#|
(DISJOINT (ALL-VARS F
                    (DOMAIN (RESTRICT S DOMAIN-1)))
          (ALL-VARS T X))
|#
;; This is one of those cases of a problem with free variables in
;; hypotheses that are so annoying.  The lemma DOMAIN-RESTRICT has
;; been put in alists.events to help with this.  But then we lose the
;; fact that the first ALL-VARS in the goal above may be removed.  The
;; lemma VARIABLE-LISTP-INTERSECTION has been added to terms.events to
;; take care of that.
;; Now it looks like the rewrite using SUBST-APPEND-NOT-OCCUR-1 should
;; succeed, since all hypotheses are relieved by rewriting alone.
;; Just to make sure, we back up in the proof checker and see if BASH
;; uses this rule on our original goal.  Sure enough, it does.
;; Now our conclusion is the one displayed above, i.e.
#|
(THEOREM (SUBST T
                (APPLY-TO-SUBST (NULLIFY-SUBST SG)
                                (CO-RESTRICT S DOMAIN-1))
                X))
|#
;; Since (as we already know) (NULLIFY-SUBST SG) has the same domain
;; as does SG, and since the hypotheses imply that (DOMAIN SG) is
;; disjoint from the variables of X, the SUBST expression in this
;; conclusion should simplify to:
#|
(SUBST T (NULLIFY-SUBST SG)
       (SUBST T (CO-RESTRICT S DOMAIN-1)
              X))
|#
;; We therefore need the lemma SUBST-APPLY-TO-SUBST-ELIMINATOR below
;; (which is used under the substitution where S gets (CO-RESTRICT S

;; DOMAIN-1) and SG gets (NULLIFY-SUBST SG)).  However, we'll
;; immediately derive the desired consequence and then disable this
;; lemma, since it appears that it would loop with
;; COMPOSE-PROPERTY-REVERSED.
;; << 55 >>

Theorem: subst-apply-to-subst-eliminator (variable-listp (domain (sg)) ∧ variable-listp (domain (s)) ∧ termp (t, x) ∧ disjoint (domain (sg), all-vars (t, x))) → (subst (t, apply-to-subst (sg, s), x) = subst (t, sg, subst (t, s, x)))

;; << 56 >>

Theorem: theorem-subst-apply-to-subst-with-disjoint-domain (var-substp (sg) ∧ var-substp (s) ∧ termp (t, x) ∧ disjoint (domain (sg), all-vars (t, x)) ∧ theorem (subst (t, s, x))) → theorem (subst (t, apply-to-subst (sg, s), x))

;; << 57 >>

Event: Disable subst-apply-to-subst-eliminator.

;; The proof of the remaining goal should go through now, one might
;; think.  However, we need one more observation first, because we
;; need to apply the following lemma.
#|
(PROVE-LEMMA SUBST-CO-RESTRICT
             (REWRITE)
             (IMPLIES (AND (DISJOINT X
                                     (INTERSECTION (DOMAIN S)
                                                   (ALL-VARS FLG TERM)))
                           (VARIABLE-LISTP (DOMAIN S))
                           (TERMP FLG TERM))
                      (EQUAL (SUBST FLG (CO-RESTRICT S X) TERM)
                             (SUBST FLG S TERM))))
|#

;; but the first hypothesis of this lemma needs special handling because of
;; free variables.  The lemma DISJOINT-SUBSETP-HACK was proved at this point,
;; and appears now in sets.events.
;; And finally, we finish.  During polishing I suddenly needed the
;; lemma SUBSETP-INTERSECTION-MONOTONE-2, which is now included in
;; "sets.events", and which in turn suggested
;; SUBSETP-INTERSECTION-COMMUTER there.
;; << 58 >>

Theorem: main-hyps-relieved-6-rest-generalization let s1 be restrict (s, domain-1 ),

s2 be apply-to-subst (nullify-subst (sg), co-restrict (s, domain-1 )) in (var-substp (sg) ∧ var-substp (s) ∧ subsetp (domain (s), new-free) ∧ termp (f, p) ∧ theorem-list (subst (f, s, p)) ∧ disjoint (domain (sg),

all-vars (f,

goals-disjoint-from-vars (p, new-free, domain-1 )))

∧ all-vars-disjoint-or-subsetp (p, new-free, domain-1 )) → theorem-list (subst (f, append (s1 , s2 ), p)) endlet

;; Now to clean up the goals that have been pushed above:
;; << 59 >>

Theorem: main-hyps-relieved-6-rest let g be caar (state),

p be cdar (state), free be cdr (state), s be witnessing-instantiation (generalize (sg, state))

in let new-g be subst (t, invert (sg), g) in let domain-1 be gen-closure (cons (new-g, p),

free,

all-vars (t, new-g))

in let s1 be restrict (s, domain-1 ), s2 be apply-to-subst (nullify-subst (sg),

co-restrict (s, domain-1 ))

in (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → theorem-list (subst (f, append (s1 , s2 ), p)) endlet endlet endlet endlet

;; << 60 >>

Theorem: main-hyps-relieved-6 (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → theorem-list (subst (f,

append (restrict (witnessing-instantiation (generalize (sg,

state)),

gen-closure (cons (subst (t, invert (sg), caar (state)),

cdar (state)), cdr (state), all-vars (t,

subst (t, invert (sg), caar (state))))),

apply-to-subst (nullify-subst (sg),

co-restrict (witnessing-instantiation (generalize (sg,

state)),

gen-closure (cons (subst (t, invert (sg), caar (state)),

cdar (state)), cdr (state), all-vars (t,

subst (t, invert (sg), caar (state))))))),

cons (subst (t, invert (sg), caar (state)), cdar (state))))

;; << 61 >>

Theorem: main-hyps-relieved (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → main-hyps (restrict (witnessing-instantiation (generalize (sg, state)),

gen-closure (cons (subst (t, invert (sg), caar (state)), cdar (state)),

cdr (state), all-vars (t,

subst (t, invert (sg), caar (state))))),

apply-to-subst (nullify-subst (sg),

co-restrict (witnessing-instantiation (generalize (sg,

state)),

gen-closure (cons (subst (t, invert (sg), caar (state)),

cdar (state)), cdr (state), all-vars (t,

subst (t, invert (sg), caar (state)))))),

sg,

caar (state), cdar (state))

;; << 62 >>

Theorem: main-theorem-1-case-4 (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → theorem-list (subst (f, gen-inst (sg, state), car (state)))

;; << 63 >>

Theorem: main-theorem-1 let wit be gen-inst (sg, state) in (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → (statep (state)

∧ var-substp (wit)

∧ subsetp (domain (wit), cdr (state))

∧ theorem-list (subst (f, wit, car (state)))) endlet

;; << 64 >>

Theorem: generalize-is-correct (generalize-okp (sg, state) ∧ valid-state (generalize (sg, state))) → valid-state (state)

Index

alist-defns, 18 alistp, 15, 18, 20, 26, 29, 30 alistp-append, 15 alistp-apply-to-subst, 26 alistp-co-restrict, 20 alistp-cons, 15 alistp-implies-properp, 15 alistp-nlistp, 15 alistp-restrict, 20 all-vars, 23–30, 33–35, 38, 40–42, 45–

48, 51, 54, 55, 58–61 all-vars-disjoint-or-subsetp, 47, 55,

59 all-vars-disjoint-or-subsetp-ge

n-closure, 55 all-vars-f-monotone, 25 all-vars-f-range-nullify-subst, 29 all-vars-flg-boolean, 23 all-vars-list-cons, 23 all-vars-subsetp-append-hack, 23 all-vars-subst, 26 all-vars-subst-lemma, 26 all-vars-t-cons, 23 all-vars-variable-listp, 28 all-vars-variablep, 24 append-assoc, 2 append-nil, 5 apply-to-subst, 25–30, 35, 40, 41,

44–47, 51, 54, 55, 58–61 apply-to-subst-append, 28 apply-to-subst-is-no-op-for-dis

joint-domain, 29

bind, 17, 19, 20 boundp-apply-to-subst, 26 boundp-bind, 19 boundp-in-var-substp-implies-va

riablep, 26 boundp-rembind, 19 boundp-subsetp, 19 boundp-value-invert, 19 car-generalize, 50 cardinality, 33 cdr-subsetp, 3 co-restrict, 18–21, 24, 27, 35, 44–47, 51, 54, 55, 59–61

compose, 25, 27 compose-property, 27 compose-property-reversed, 27

delete, 5–7, 19 delete-cons, 6 delete-delete, 6 delete-nlistp, 6 delete-non-member, 6 disjoint, 5, 7, 9–13, 18–20, 24, 26–

30, 33, 34, 38, 40–42, 44– 48, 54, 58, 59 disjoint-all-vars-goals-disjoint

-from-vars, 54 disjoint-all-vars-range-apply-s ubst-nullify-subst, 30 disjoint-all-vars-subst, 28 disjoint-all-vars-subst-nullify

-subst, 30 disjoint-append-left, 7 disjoint-append-right, 7 disjoint-cons-1, 7 disjoint-cons-2, 7 disjoint-domain-singleton, 19 disjoint-implies-empty-intersecti

on, 13 disjoint-intersection, 9 disjoint-intersection-append, 9 disjoint-intersection-commuter, 10 disjoint-intersection-set-diff-i ntersection, 12 disjoint-intersection3, 10 disjoint-intersection3-middle, 13 disjoint-nlistp, 7 disjoint-non-member, 7 disjoint-range-implies-disjoint

-value, 28 disjoint-set-diff-general, 11 disjoint-subsetp-hack, 13 disjoint-subsetp-monotone-secon

d, 7 disjoint-symmetry, 7 disjoint-wit, 5 disjoint-wit-witnesses, 5 disjointp-set-diff, 10 domain, 15, 18–21, 24–30, 32, 34,

36–38, 40–42, 44–46, 54, 58, 59, 61

domain-append, 15 domain-apply-to-subst, 27 domain-bind, 19 domain-co-restrict, 19 domain-cons, 15 domain-invert, 19 domain-nlistp, 15 domain-nullify-subst, 30 domain-rembind, 19 domain-restrict, 19

fix-properp, 4, 5, 9, 11, 12, 14, 15,

20, 28 fix-properp-append, 4 fix-properp-cons, 4 fix-properp-nlistp, 4 fix-properp-properp, 4 fn, 22, 29 function-symbol-intro, 22 function-symbol-p, 22, 23

gen-closure, 34, 35, 45–47, 51, 54,

55, 59–61 gen-closure-accept, 33 gen-closure-contains-third-arg, 51 gen-inst, 35–37, 61 gen-setting-substitutions, 37, 38, 40,

47 generalize, 34–37, 44–47, 50, 51, 54,

55, 59–61 generalize-is-correct, 61 generalize-okp, 34–36, 42, 44–47, 51,

54, 55, 60, 61 generalize-statep, 35 goals-disjoint-from-vars, 48, 54, 59 goals-disjoint-from-vars-subsetp, 54 goals-intersecting-vars, 48

intersection, 5, 7–14, 19, 24, 27, 33–

35, 47, 48, 51 intersection-append, 9 intersection-associative, 8 intersection-cons-1, 8 intersection-cons-2, 8 intersection-cons-3, 8 intersection-cons-subsetp, 8 intersection-disjoint, 7 intersection-elimination, 9 intersection-nlistp, 8 intersection-subsetp-identity, 11 intersection-symmetry, 8 intersection-x-x, 11 invert, 17–20, 26, 34, 35, 38, 40, 45–

47, 50, 51, 54, 55, 59–61 invert-cons, 17 invert-nlistp, 17

length, 2, 9, 11, 13, 33 length-append, 2 length-cons, 2 length-intersection, 9 length-intersection-set-diff, 11 length-nlistp, 2 length-set-diff-leq, 13 length-set-diff-lessp, 13 length-set-diff-opener, 11 lessp-length, 13 listp-delete, 6 listp-intersection, 13 listp-make-set, 12 listp-set-diff, 11

main-hyps, 38, 40, 41, 61 main-hyps-relieved, 60 main-hyps-relieved-1, 42 main-hyps-relieved-2, 42 main-hyps-relieved-3, 42 main-hyps-relieved-4, 42 main-hyps-relieved-5, 47 main-hyps-relieved-5-lemma-1, 44 main-hyps-relieved-5-lemma-2, 44 main-hyps-relieved-5-lemma-3, 44 main-hyps-relieved-5-lemma-4, 45 main-hyps-relieved-5-lemma-5, 46 main-hyps-relieved-5-lemma-5-wit, 45 main-hyps-relieved-5-lemma-6, 46 main-hyps-relieved-6, 60 main-hyps-relieved-6-first, 51 main-hyps-relieved-6-rest, 59 main-hyps-relieved-6-rest-gener

alization, 59 main-hyps-relieved-6-rest-lemma

-1, 54 -2, 55

main-hyps-suffice, 41 main-hyps-suffice-first, 40 main-hyps-suffice-first-lemma, 40 main-hyps-suffice-first-lemma-ge

neral, 40 main-hyps-suffice-rest, 41 main-hyps-suffice-rest-lemma, 40 main-theorem-1, 61 main-theorem-1-case-1, 36 main-theorem-1-case-2, 36 main-theorem-1-case-3, 37 main-theorem-1-case-4, 61 make-set, 12, 33 make-set-gives-setp, 12 make-set-preserves-member, 12 make-set-preserves-subsetp-1, 12 make-set-preserves-subsetp-2, 12 make-set-preserves-subsetp-3, 12 make-set-set-diff, 12 mapping, 18–21, 25, 26, 30 mapping-append, 20 mapping-apply-to-subst, 26 mapping-co-restrict, 21 mapping-implies-alistp, 18 mapping-implies-setp-domain, 18 mapping-nullify-subst, 30 mapping-restrict, 21 member-all-vars-subsetp, 25 member-append, 3 member-cons, 2 member-delete, 7 member-domain-sufficiency, 15 member-fix-properp, 12 member-intersection, 8 member-nlistp, 2 member-preserves-disjoint-all-v

ars, 24

ars-lemma, 24 member-set-diff, 10 member-subsetp, 3 member-subst, 29 member-variable-listp-implies-v

ariablep, 24

new-gen-vars, 33, 34 new-gen-vars-subset, 33 non-variablep-not-member-of-vari

able-listp, 27 nullify-subst, 29, 30, 35, 44–47, 51, 54, 55, 59–61

properp, 4–6, 11, 15–17, 22, 23, 29 properp-all-vars, 23 properp-append, 4 properp-cons, 4 properp-delete, 5 properp-domain, 15 properp-fix-properp, 4 properp-intersection, 5 properp-invert, 17 properp-nlistp, 4 properp-nullify-subst, 29 properp-range, 16 properp-set-diff, 6

range, 16, 18–20, 24–30, 34, 35, 38,

46 range-append, 16 range-cons, 16 range-invert, 19 range-nlistp, 16 rembind, 17, 19, 20 restrict, 18–21, 24, 27, 35, 44–47,

51, 54, 55, 59–61

set-defns, 6 set-diff, 6, 10–14, 19, 24, 33, 35 set-diff-append, 13 set-diff-cons, 10 set-diff-cons-non-member-1, 11 set-diff-make-set, 12 set-diff-nil, 11 set-diff-nlistp, 10 setp, 6, 7, 12, 14, 18 setp-append, 12 setp-cons, 12 setp-delete, 7 setp-implies-properp, 6 setp-intersection-sufficiency, 14 setp-nlistp, 12 setp-set-diff-sufficiency, 14 statep, 31, 32, 34–36, 61 subsetp, 2–4, 7–15, 19, 23, 25–27,

29, 32–34, 36, 37, 47, 51, 54, 55, 59, 61

subsetp-append, 3 subsetp-cdr-generalize, 37 subsetp-cons-1, 3 subsetp-cons-2, 3 subsetp-cons-not-member, 4 subsetp-disjoint-1, 7 subsetp-disjoint-2, 7 subsetp-disjoint-3, 7 subsetp-domain, 15 subsetp-fix-properp-1, 14 subsetp-fix-properp-2, 14 subsetp-intersection, 8 subsetp-intersection-append, 9 subsetp-intersection-commuter, 10 subsetp-intersection-eliminatio

n, 9 n-lemma, 9

subsetp-intersection-left-1, 8 subsetp-intersection-left-2, 8 subsetp-intersection-member, 9 subsetp-intersection-monotone-1, 9 subsetp-intersection-monotone-2, 10 subsetp-intersection-sufficienc

y-1, 8 y-2, 8

subsetp-is-transitive, 3 subsetp-nlistp, 4 subsetp-of-append-sufficiency, 4 subsetp-reflexivity, 3 subsetp-set-diff-1, 10 subsetp-set-diff-2, 10 subsetp-set-diff-mononone-2, 11 subsetp-set-diff-monotone-secon

d, 11 subsetp-set-diff-sufficiency, 14 subsetp-subst, 29 subsetp-wit, 3 subsetp-wit-witnesses, 3 subsetp-wit-witnesses-general-1, 3 subsetp-wit-witnesses-general-2, 3 subst, 25–32, 34–36, 38, 40, 41, 45–

47, 50, 51, 54, 55, 58–61 subst-append-not-occur-1, 28 subst-append-not-occur-2, 28 subst-apply-to-subst, 28 subst-apply-to-subst-eliminator, 58 subst-co-restrict, 27 subst-flg-not-list, 27 subst-invert, 26 subst-list-cons, 25 subst-list-nlistp, 26 subst-not-occur, 28 subst-occur, 26 subst-restrict, 27 subst-t-non-variablep, 26 subst-t-variablep, 26 substitution-defns, 30

term-defns, 24 termp, 22–31, 38, 40, 42, 58, 59 termp-domain, 27 termp-list-append, 28 termp-list-cons, 22 termp-list-implies-properp, 23 termp-list-nlistp, 23 termp-range-co-restrict, 24 termp-range-nullify-subst, 29 termp-range-restrict, 24 termp-subst, 27 termp-t-cons, 23 termp-t-nlistp, 23 termp-value, 27 theorem, 31, 40, 51, 58 theorem-intro, 31 theorem-list, 31, 32, 36, 38, 41, 59–

61 theorem-list-properties, 31 theorem-subst-apply-to-subst-wit

h-disjoint-domain, 58

valid-state, 32, 36, 37, 44–47, 51, 54,

55, 60, 61 valid-state-intro, 32 valid-state-opener, 36 valid-state-type, 32 value, 16–21, 25–28 value-append, 20 value-apply-to-subst, 27 value-bind, 20 value-co-restrict, 21 value-cons, 17 value-invert-not-member-of-domai

n, 18 value-nlistp, 17 value-rembind, 20 value-restrict, 21 value-value-invert, 20 value-when-not-bound, 20 var-substp, 25, 26, 31, 32, 34, 36,

38, 44, 58, 59, 61 var-substp-apply-to-subst, 27 variable-listp, 22, 24–29, 31, 40, 58 variable-listp-append, 28 variable-listp-cons, 22 variable-listp-domain-co-restri

ct, 24 variable-listp-domain-restrict, 24 variable-listp-implies-properp, 22 variable-listp-intersection, 24 variable-listp-set-diff, 24 variable-nlistp, 22 variablep, 22–27 variablep-intro, 22 variablep-value-invert, 26

witnessing-instantiation, 32, 35, 36,

44–47, 51, 54, 55, 59–61 witnessing-instantiation-is-dis

joint-from-generalizing-substitution, 44