relink-fancy-scion

Included Books

base perm term-ordered-perms convert-perm-to-how-many merge-sort-term-order

other

(in-package "ACL2")

include-book

(include-book "base")

local

(local (include-book "sorting/perm" :dir :system))

local

(local (include-book "sorting/term-ordered-perms" :dir :system))

local

(local (include-book "sorting/convert-perm-to-how-many" :dir :system))

local

(local (include-book "sorting/merge-sort-term-order" :dir :system))

true-car/cdr-nestpfunction

(defun true-car/cdr-nestp
  (term var)
  (declare (xargs :guard (symbolp var)))
  (cond ((variablep term) (eq term var))
    ((fquotep term) nil)
    ((and (or (eq (ffn-symb term) 'car) (eq (ffn-symb term) 'cdr))) (and (consp (cdr term))
        (null (cddr term))
        (true-car/cdr-nestp (fargn term 1) var)))
    (t nil)))

true-car/cdr-nestp-on-a-varfunction

(defun true-car/cdr-nestp-on-a-var
  (term)
  (declare (xargs :guard t))
  (cond ((variablep term) (symbolp term))
    ((fquotep term) nil)
    ((and (or (eq (ffn-symb term) 'car) (eq (ffn-symb term) 'cdr))) (and (consp (cdr term))
        (null (cddr term))
        (true-car/cdr-nestp-on-a-var (fargn term 1))))
    (t nil)))

*bad*constant

(defconst *bad* "BAD")

car/cdr-valfunction

(defun car/cdr-val
  (term actual)
  (declare (xargs :guard (and (true-car/cdr-nestp-on-a-var term)
        (pseudo-termp actual))
      :verify-guards nil))
  (cond ((variablep term) actual)
    ((eq (ffn-symb term) 'car) (let ((arg-val (car/cdr-val (fargn term 1) actual)))
        (cond ((equal arg-val *bad*) *bad*)
          ((variablep arg-val) *bad*)
          ((fquotep arg-val) (if (atom (unquote arg-val))
              *nil*
              (kwote (car (unquote arg-val)))))
          ((eq (ffn-symb arg-val) 'cons) (fargn arg-val 1))
          (t *bad*))))
    ((eq (ffn-symb term) 'cdr) (let ((arg-val (car/cdr-val (fargn term 1) actual)))
        (cond ((equal arg-val *bad*) *bad*)
          ((variablep arg-val) *bad*)
          ((fquotep arg-val) (if (atom (unquote arg-val))
              *nil*
              (kwote (cdr (unquote arg-val)))))
          ((eq (ffn-symb arg-val) 'cons) (fargn arg-val 2))
          (t *bad*))))
    (t *bad*)))

local

(local (defthm pseudo-termp-car/cdr-val
    (implies (and (pseudo-termp actual)
        (not (equal (car/cdr-val term actual) *bad*)))
      (pseudo-termp (car/cdr-val term actual)))))

other

(verify-guards car/cdr-val
  :hints (("Subgoal *1/1" :in-theory (disable pseudo-termp-car/cdr-val)
     :use ((:instance pseudo-termp-car/cdr-val
        (term (cadr (cadr term)))
        (actual actual))))))

car/cdr-to-val-alistmutual-recursion

(mutual-recursion (defun car/cdr-to-val-alist
    (term var actual)
    (declare (xargs :guard (and (pseudo-termp term)
          (symbolp var)
          (pseudo-termp actual))
        :verify-guards nil))
    (cond ((variablep term) (if (eq term var)
          *bad*
          nil))
      ((fquotep term) nil)
      ((true-car/cdr-nestp term var) (let ((val (car/cdr-val term actual)))
          (if (equal val *bad*)
            *bad*
            (list (cons term val)))))
      (t (car/cdr-to-val-alist-list (fargs term) var actual))))
  (defun car/cdr-to-val-alist-list
    (terms var actual)
    (declare (xargs :guard (and (pseudo-term-listp terms)
          (symbolp var)
          (pseudo-termp actual))))
    (cond ((endp terms) nil)
      (t (let ((temp1 (car/cdr-to-val-alist (car terms) var actual)))
          (cond ((equal temp1 *bad*) *bad*)
            (t (let ((temp2 (car/cdr-to-val-alist-list (cdr terms) var actual)))
                (cond ((equal temp2 *bad*) *bad*)
                  (t (union-equal temp1 temp2)))))))))))

local

(local (defun tree-induction
    (x)
    (cond ((atom x) x)
      (t (list (tree-induction (car x)) (tree-induction (cdr x)))))))

local

(local (defthm alistp-car/cdr-to-val-alist
    (and (implies (not (equal (car/cdr-to-val-alist term var actuals) *bad*))
        (alistp (car/cdr-to-val-alist term var actuals)))
      (implies (not (equal (car/cdr-to-val-alist-list term var actuals) *bad*))
        (alistp (car/cdr-to-val-alist-list term var actuals))))
    :hints (("Goal" :induct (tree-induction term)))
    :rule-classes ((:forward-chaining :corollary (implies (not (equal (car/cdr-to-val-alist term var actuals) *bad*))
         (alistp (car/cdr-to-val-alist term var actuals)))) (:forward-chaining :corollary (implies (not (equal (car/cdr-to-val-alist-list term var actuals) *bad*))
          (alistp (car/cdr-to-val-alist-list term var actuals)))))))

other

(verify-guards car/cdr-to-val-alist)

make-cdr-nestfunction

(defun make-cdr-nest
  (n term)
  (declare (xargs :guard (natp n)))
  (cond ((zp n) term)
    (t (list 'cdr (make-cdr-nest (- n 1) term)))))

make-nthfunction

(defun make-nth
  (n gvar)
  (declare (xargs :guard (natp n)))
  (list 'car (make-cdr-nest n gvar)))

local

(local (defthm nth-position-equal-ac
    (implies (and (natp n) (member-equal e lst))
      (equal (nth (- (position-equal-ac e lst n) n) lst) e))
    :rule-classes nil))

local

(local (defthm nth-position
    (implies (member-equal e lst)
      (equal (nth (position-equal e lst) lst) e))
    :hints (("Goal" :use (:instance nth-position-equal-ac (e e) (lst lst) (n 0))))))

local

(local (defthm integerp-position-equal-ac
    (implies (and (natp n) (member-equal e lst))
      (integerp (position-equal-ac e lst n)))))

local

(local (defthm integerp-position-equal
    (implies (member-equal e lst)
      (integerp (position-equal e lst)))))

local

(local (defthm bounds-position-equal-ac
    (implies (and (natp n) (member-equal e lst))
      (and (<= 0 (position-equal-ac e lst n))
        (< (position-equal-ac e lst n) (+ n (len lst)))))
    :rule-classes :linear))

local

(local (defthm bounds-position-equal
    (implies (member-equal e lst)
      (and (<= 0 (position-equal e lst))
        (< (position-equal e lst) (len lst))))
    :rule-classes :linear))

local

(local (in-theory (disable position-equal)))

all-true-car/cdr-nestsfunction

(defun all-true-car/cdr-nests
  (flg x var)
  (declare (xargs :guard (and (if flg
          (pseudo-termp x)
          (pseudo-term-listp x))
        (symbolp var))
      :verify-guards nil))
  (if flg
    (cond ((variablep x) nil)
      ((quotep x) nil)
      ((or (eq (ffn-symb x) 'car) (eq (ffn-symb x) 'cdr)) (cond ((true-car/cdr-nestp x var) (list x))
          (t (all-true-car/cdr-nests nil (fargs x) var))))
      (t (all-true-car/cdr-nests nil (fargs x) var)))
    (cond ((endp x) nil)
      (t (union-equal (all-true-car/cdr-nests t (car x) var)
          (all-true-car/cdr-nests nil (cdr x) var))))))

local

(local (defthm true-car/cdr-nestp-implies-pseudo-termp
    (implies (and (true-car/cdr-nestp x var) (symbolp var))
      (pseudo-termp x))
    :rule-classes :forward-chaining))

local

(local (defthm pseudo-term-listp-all-true-car/cdr-nests
    (implies (symbolp var)
      (pseudo-term-listp (all-true-car/cdr-nests flg x var)))))

other

(verify-guards all-true-car/cdr-nests)

local

(local (defthm perm-merge-sort-term-order
    (perm (merge-sort-term-order x) x)))

local

(local (defcong perm
    equal
    (subsetp a b)
    1
    :hints (("Goal" :in-theory (disable convert-perm-to-how-many)))))

local

(local (defthm subsetp-reflexive-lemma
    (implies (subsetp a (cdr b)) (subsetp a b))))

local

(local (defthm subsetp-reflexive (subsetp a a)))

local

(local (defthm perm-implies-subsetp-1
    (implies (perm a b) (subsetp a b))
    :rule-classes nil))

local

(local (defthm perm-implies-subsetp-2
    (implies (perm a b) (subsetp b a))
    :rule-classes nil))

local

(local (defthm subsetp-implies-member
    (implies (and (subsetp a b) (member-equal e a))
      (member-equal e b))))

local

(local (defcong perm
    iff
    (member-equal e a)
    2
    :hints (("Goal" :in-theory (disable perm-implies-equal-subsetp-1
         convert-perm-to-how-many
         perm-is-an-equivalence)
       :use ((:instance perm-implies-subsetp-1 (a a) (b a-equiv)) (:instance perm-implies-subsetp-2 (a a) (b a-equiv)))
       :do-not-induct t))))

local

(local (defcong perm
    equal
    (subsetp a b)
    2
    :hints (("Goal" :in-theory (disable convert-perm-to-how-many)))))

local

(local (defthm member-equal-strip-cars-assoc-equal
    (implies (and (alistp alist) (member-equal e (strip-cars alist)))
      (assoc-equal e alist))))

local

(local (defthm member-equal-cdr-assoc-equal
    (implies (and (assoc-equal term alist)
        (subsetp-equal (strip-cdrs alist) relevant-vals))
      (member-equal (cdr (assoc-equal term alist)) relevant-vals))))

local

(local (encapsulate nil
    (local (defthm subsetp-equal-union-equal-1-lemma
        (implies (and (subsetp-equal (union-equal a b) c) (member-equal e b))
          (member-equal e c))))
    (defthm subsetp-equal-union-equal-1
      (equal (subsetp-equal (union-equal a b) c)
        (and (subsetp-equal a c) (subsetp-equal b c))))))

relink-termmutual-recursion

(mutual-recursion (defun relink-term
    (old-alist gvar relevant-vals term)
    (declare (xargs :guard (and (alistp old-alist)
          (symbolp gvar)
          (true-listp relevant-vals)
          (pseudo-termp term)
          (subsetp-equal (all-true-car/cdr-nests t term gvar)
            (strip-cars old-alist))
          (subsetp-equal (strip-cdrs old-alist) relevant-vals))))
    (cond ((variablep term) term)
      ((fquotep term) term)
      ((or (eq (ffn-symb term) 'car) (eq (ffn-symb term) 'cdr)) (cond ((true-car/cdr-nestp term gvar) (make-nth (position (cdr (assoc-equal term old-alist))
                relevant-vals
                :test 'equal)
              gvar))
          (t (list (ffn-symb term)
              (relink-term old-alist gvar relevant-vals (cadr term))))))
      (t (cons (ffn-symb term)
          (relink-term-list old-alist gvar relevant-vals (fargs term))))))
  (defun relink-term-list
    (old-alist gvar relevant-vals terms)
    (declare (xargs :guard (and (alistp old-alist)
          (symbolp gvar)
          (true-listp relevant-vals)
          (pseudo-term-listp terms)
          (subsetp-equal (all-true-car/cdr-nests nil terms gvar)
            (strip-cars old-alist))
          (subsetp-equal (strip-cdrs old-alist) relevant-vals))))
    (cond ((endp terms) nil)
      (t (cons (relink-term old-alist gvar relevant-vals (car terms))
          (relink-term-list old-alist gvar relevant-vals (cdr terms)))))))

*fancy-loop$-scions*constant

(defconst *fancy-loop$-scions*
  (strip-caddrs *for-loop$-keyword-info*))

make-true-cons-nestfunction

(defun make-true-cons-nest
  (terms)
  (declare (xargs :guard (true-listp terms)))
  (if (consp terms)
    (xxxjoin 'cons (append terms '('nil)))
    *nil*))

local

(local (defthm pseudo-term-listp-strip-cdrs-car/cdr-to-val-alist
    (and (implies (and (pseudo-termp actuals)
          (not (equal (car/cdr-to-val-alist term var actuals) *bad*)))
        (pseudo-term-listp (strip-cdrs (car/cdr-to-val-alist term var actuals))))
      (implies (and (pseudo-termp actuals)
          (not (equal (car/cdr-to-val-alist-list term var actuals) *bad*)))
        (pseudo-term-listp (strip-cdrs (car/cdr-to-val-alist-list term var actuals)))))
    :hints (("Goal" :induct (tree-induction term)))))

local

(local (defthm member-strip-cdrs
    (implies (member-equal e b)
      (member-equal (cdr e) (strip-cdrs b)))))

local

(local (defthm member-strip-cdrs-union-equal
    (implies (member-equal e b)
      (member-equal (cdr e) (strip-cdrs (union-equal a b))))))

local

(local (defthm member-strip-cars-union-equal
    (implies (member-equal e b)
      (member-equal (car e) (strip-cars (union-equal a b))))))

local

(local (defthm strip-cdrs-union-equal-1
    (subsetp-equal (strip-cdrs a)
      (strip-cdrs (union-equal a b)))))

local

(local (defthm strip-cdrs-union-equal-2
    (subsetp-equal (strip-cdrs b)
      (strip-cdrs (union-equal a b)))))

local

(local (defthm transitivity-of-subsetp-equal
    (implies (and (subsetp-equal a b) (subsetp-equal b c))
      (subsetp-equal a c))))

local

(local (defthm transitivity-corollary-1
    (implies (subsetp-equal (strip-cdrs (union-equal a b)) c)
      (subsetp-equal (strip-cdrs a) c))))

local

(local (defthm transitivity-corollary-2
    (implies (subsetp-equal (strip-cdrs (union-equal a b)) c)
      (subsetp-equal (strip-cdrs b) c))))

local

(local (defthm member-union-equal
    (iff (member-equal e (union-equal a b))
      (or (member-equal e a) (member-equal e b)))))

local

(local (defun set-equalp
    (x y)
    (and (subsetp-equal x y) (subsetp-equal y x))))

local

(local (defequiv set-equalp))

local

(local (defthm equal-subsetp-equal
    (equal (equal (subsetp-equal a b) (subsetp-equal c d))
      (iff (subsetp-equal a b) (subsetp-equal c d)))))

local

(local (defcong set-equalp equal (subsetp-equal x y) 1))

local

(local (defcong set-equalp equal (subsetp-equal x y) 2))

local

(local (encapsulate nil
    (local (defthm strip-cdrs-union-equal-distributivity-1
        (subsetp-equal (strip-cdrs (union-equal a b))
          (union-equal (strip-cdrs a) (strip-cdrs b)))
        :rule-classes nil))
    (defthm strip-cdrs-union-equal-distributivity
      (set-equalp (strip-cdrs (union-equal a b))
        (union-equal (strip-cdrs a) (strip-cdrs b))))))

local

(local (encapsulate nil
    (local (defthm strip-cars-union-equal-distributivity-1
        (subsetp-equal (strip-cars (union-equal a b))
          (union-equal (strip-cars a) (strip-cars b)))
        :rule-classes nil))
    (defthm strip-cars-union-equal-distributivity
      (set-equalp (strip-cars (union-equal a b))
        (union-equal (strip-cars a) (strip-cars b))))))

local

(local (defthm subsetp-equal-union-equal-2
    (implies (subsetp-equal a c)
      (subsetp-equal a (union-equal b c)))))

local

(local (defthm relink-term-reqmt-on-alist-general
    (implies (not (equal (if flg
            (car/cdr-to-val-alist x var old-global-actual)
            (car/cdr-to-val-alist-list x var old-global-actual))
          *bad*))
      (subsetp-equal (all-true-car/cdr-nests flg x var)
        (strip-cars (if flg
            (car/cdr-to-val-alist x var old-global-actual)
            (car/cdr-to-val-alist-list x var old-global-actual)))))
    :rule-classes nil))

local

(local (defthm relink-term-reqmt-on-alist
    (and (implies (not (equal (car/cdr-to-val-alist x var old-global-actual) *bad*))
        (subsetp-equal (all-true-car/cdr-nests t x var)
          (strip-cars (car/cdr-to-val-alist x var old-global-actual))))
      (implies (not (equal (car/cdr-to-val-alist-list x var old-global-actual)
            *bad*))
        (subsetp-equal (all-true-car/cdr-nests nil x var)
          (strip-cars (car/cdr-to-val-alist-list x var old-global-actual)))))
    :hints (("Goal" :use ((:instance relink-term-reqmt-on-alist-general (flg t)) (:instance relink-term-reqmt-on-alist-general (flg nil)))))))

local

(local (defthm pseudo-term-listp-remove-duplicates-equal
    (implies (true-listp x)
      (equal (pseudo-term-listp (remove-duplicates-equal x))
        (pseudo-term-listp x)))))

local

(local (defthm member-equal-remove-duplicates-equal
    (iff (member-equal x (remove-duplicates-equal l))
      (member-equal x l))))

local

(local (defthm subsetp-equal-remove-duplicates-equal
    (subsetp-equal (remove-duplicates-equal x) x)))

local

(local (defthm subsetp-equal-remove-duplicates-equal-corollary
    (equal (subsetp-equal x (remove-duplicates-equal y))
      (subsetp-equal x y))
    :hints (("Goal" :induct (remove-duplicates-equal y)))))

relink-fancy-scionfunction

(defun relink-fancy-scion
  (term)
  (declare (xargs :guard (pseudo-termp term)))
  (case-match term
    ((scion ('quote ('lambda (gvar ivar) body))
       old-global-actual
       target-tuples) (cond ((and (member-eq scion *fancy-loop$-scions*)
           (symbolp gvar)
           (symbolp ivar)
           (not (eq gvar ivar))
           (pseudo-termp body)) (let ((old-alist (car/cdr-to-val-alist body gvar old-global-actual)))
            (cond ((equal old-alist *bad*) term)
              (t (let* ((new-actuals (merge-sort-term-order (remove-duplicates-equal (strip-cdrs old-alist)))) (new-body (relink-term old-alist gvar new-actuals body))
                    (new-global-actual (make-true-cons-nest new-actuals)))
                  (cond ((equal body new-body) term)
                    (t `(,SCION '(lambda (,GVAR ,IVAR) ,NEW-BODY)
                        ,NEW-GLOBAL-ACTUAL
                        ,TARGET-TUPLES))))))))
        (t term)))
    (& term)))

relink-fancy-scion-hypfnfunction

(defun relink-fancy-scion-hypfn
  (term)
  (declare (xargs :guard (pseudo-termp term)))
  (cond ((consp term) `(tamep-functionp ,(FARGN TERM 1)))
    (t *nil*)))

local

(local (defun tamep-listp
    (terms)
    (cond ((endp terms) t)
      (t (and (tamep (car terms)) (tamep-listp (cdr terms)))))))

local

(local (defthm cdr-append-list-nil
    (iff (cdr (append lst '('nil))) (consp lst))))

local

(local (defthm tamep-xxxjoin-cons
    (implies (and (consp lst) (tamep-listp lst))
      (tamep (xxxjoin 'cons (append lst '('nil)))))))

local

(local (defthm ev$-make-true-cons-nest
    (implies (tamep-listp terms)
      (equal (ev$ (make-true-cons-nest terms) a)
        (ev$-list terms a)))))

local

(local (in-theory (disable make-true-cons-nest)))

local

(local (defthm tamep-make-cdr-nest
    (implies (symbolp var) (tamep (make-cdr-nest n var)))))

ev$-cartheorem

(defthm ev$-car
  (implies (tamep x)
    (equal (ev$ (list 'car x) a) (car (ev$ x a)))))

ev$-cdrtheorem

(defthm ev$-cdr
  (implies (tamep x)
    (equal (ev$ (list 'cdr x) a) (cdr (ev$ x a)))))

ev$-constheorem

(defthm ev$-cons
  (implies (and (tamep x) (tamep y))
    (equal (ev$ (list 'cons x y) a) (cons (ev$ x a) (ev$ y a)))))

local

(local (defthm cdr-nthcdr
    (implies (natp n)
      (equal (cdr (nthcdr n lst)) (nthcdr (+ 1 n) lst)))))

local

(local (defthm ev$-make-cdr-nest
    (implies (and (natp n) (symbolp var))
      (equal (ev$ (make-cdr-nest n var) a)
        (nthcdr n (cdr (assoc-eq var a)))))
    :hints (("Goal" :induct (make-cdr-nest n var)))))

local

(local (defthm ev$-make-nth
    (implies (and (natp n) (symbolp var))
      (equal (ev$ (make-nth n var) a)
        (nth n (cdr (assoc-eq var a)))))))

local

(local (defthm tamep-make-nth
    (implies (and (natp n) (symbolp var))
      (tamep (make-nth n var)))))

local

(local (in-theory (disable make-nth)))

local

(local (defun flagged-tamep-hint
    (flg n flags x)
    (if flg
      (cond ((variablep x) (list n flags x))
        ((fquotep x) x)
        ((symbolp (ffn-symb x)) (flagged-tamep-hint nil
            (access apply$-badge (badge (ffn-symb x)) :arity)
            (if (eq (access apply$-badge (badge (ffn-symb x)) :ilks) t)
              nil
              (access apply$-badge (badge (ffn-symb x)) :ilks))
            (fargs x)))
        ((consp (ffn-symb x)) (flagged-tamep-hint nil (len (fargs x)) nil (fargs x)))
        (t x))
      (cond ((endp x) nil)
        (t (cons (flagged-tamep-hint t n flags (car x))
            (flagged-tamep-hint nil (- n 1) (cdr flags) (cdr x))))))))

local

(local (defun suitably-tamep-listp-hint
    (n flags x)
    (if (zp n)
      (list flags x)
      (suitably-tamep-listp-hint (- n 1) (cdr flags) (cdr x)))))

local

(local (defthm suitably-tamep-listp-implies-len
    (implies (suitably-tamep-listp n nil args)
      (suitably-tamep-listp (len args) nil args))
    :hints (("Goal" :induct (suitably-tamep-listp-hint n nil args)))))

local

(local (defthm tamep-relink-term-general
    (if flg
      (implies (and (tamep x)
          (symbolp gvar)
          (alistp old-alist)
          (subsetp-equal (all-true-car/cdr-nests t x gvar)
            (strip-cars old-alist))
          (subsetp-equal (strip-cdrs old-alist) relevant-vals))
        (tamep (relink-term old-alist gvar relevant-vals x)))
      (implies (and (suitably-tamep-listp n flags x)
          (symbolp gvar)
          (alistp old-alist)
          (subsetp-equal (all-true-car/cdr-nests nil x gvar)
            (strip-cars old-alist))
          (subsetp-equal (strip-cdrs old-alist) relevant-vals))
        (suitably-tamep-listp n
          flags
          (relink-term-list old-alist gvar relevant-vals x))))
    :hints (("Goal" :induct (flagged-tamep-hint flg n flags x)
       :expand ((suitably-tamep-listp n flags x) (tamep x)
         (relink-term old-alist gvar relevant-vals x))))
    :rule-classes nil))

local

(local (defthm tamep-relink-term
    (and (implies (and (tamep x)
          (symbolp gvar)
          (alistp old-alist)
          (subsetp-equal (all-true-car/cdr-nests t x gvar)
            (strip-cars old-alist))
          (subsetp-equal (strip-cdrs old-alist) relevant-vals))
        (tamep (relink-term old-alist gvar relevant-vals x)))
      (implies (and (suitably-tamep-listp n flags x)
          (symbolp gvar)
          (alistp old-alist)
          (subsetp-equal (all-true-car/cdr-nests nil x gvar)
            (strip-cars old-alist))
          (subsetp-equal (strip-cdrs old-alist) relevant-vals))
        (suitably-tamep-listp n
          flags
          (relink-term-list old-alist gvar relevant-vals x))))
    :hints (("Goal" :use ((:instance tamep-relink-term-general (flg t)) (:instance tamep-relink-term-general (flg nil)))))))

other

(defevaluator evalator
  evalator-list
  ((car x) (cdr x)
    (cons x y)
    (tamep-functionp fn)
    (sum$+ fn globals lst)
    (always$+ fn globals lst)
    (thereis$+ fn globals lst)
    (collect$+ fn globals lst)
    (append$+ fn globals lst)
    (until$+ fn globals lst)
    (when$+ fn globals lst)))

local

(local (defthm len-relink-term-list
    (equal (len (relink-term-list old-alist gvar new-actuals x))
      (len x))))

local

(local (defun strong-alist-propertyp
    (alist gvar actual)
    (cond ((endp alist) (equal alist nil))
      ((and (consp (car alist))
         (consp (car (car alist)))
         (true-car/cdr-nestp (car (car alist)) gvar)
         (equal (car/cdr-val (car (car alist)) actual)
           (cdr (car alist)))
         (pseudo-termp (cdr (car alist)))) (strong-alist-propertyp (cdr alist) gvar actual))
      (t nil))))

local

(local (defthm strong-alist-propertyp-union-equal
    (implies (and (strong-alist-propertyp a gvar actual)
        (strong-alist-propertyp b gvar actual))
      (strong-alist-propertyp (union-equal a b) gvar actual))))

local

(local (defun term-induction
    (flg x)
    (if flg
      (cond ((variablep x) x)
        ((fquotep x) x)
        (t (term-induction nil (cdr x))))
      (cond ((endp x) x)
        (t (list (term-induction t (car x))
            (term-induction nil (cdr x))))))))

local

(local (defthm strong-alist-propertyp-car/cdr-to-val-alist-general
    (if flg
      (implies (and (pseudo-termp actual)
          (not (equal (car/cdr-to-val-alist x gvar actual) *bad*)))
        (strong-alist-propertyp (car/cdr-to-val-alist x gvar actual)
          gvar
          actual))
      (implies (and (pseudo-termp actual)
          (not (equal (car/cdr-to-val-alist-list x gvar actual) *bad*)))
        (strong-alist-propertyp (car/cdr-to-val-alist-list x gvar actual)
          gvar
          actual)))
    :hints (("Goal" :induct (term-induction flg x)))
    :rule-classes nil))

local

(local (defthm strong-alist-propertyp-car/cdr-to-val-alist
    (and (implies (and (pseudo-termp actual)
          (not (equal (car/cdr-to-val-alist x gvar actual) *bad*)))
        (strong-alist-propertyp (car/cdr-to-val-alist x gvar actual)
          gvar
          actual))
      (implies (and (pseudo-termp actual)
          (not (equal (car/cdr-to-val-alist-list x gvar actual) *bad*)))
        (strong-alist-propertyp (car/cdr-to-val-alist-list x gvar actual)
          gvar
          actual)))
    :hints (("Goal" :use ((:instance strong-alist-propertyp-car/cdr-to-val-alist-general
          (flg t)) (:instance strong-alist-propertyp-car/cdr-to-val-alist-general
           (flg nil)))))))

local

(local (defthm assoc-equal-put-assoc-equal
    (equal (assoc-equal key (put-assoc-equal key val a))
      (cons key val))))

local

(local (defthm len-evalator-list
    (equal (len (evalator-list x a)) (len x))))

local

(local (defthm nth-evalator-list
    (equal (nth n (evalator-list x a)) (evalator (nth n x) a))))

local

(local (defthm tamep-true-car/cdr-nestp
    (implies (and (true-car/cdr-nestp x var) (symbolp var))
      (tamep x))))

local

(local (defthm ev$-true-car/cdr-nest
    (implies (and (symbolp gvar)
        (true-car/cdr-nestp x gvar)
        (not (equal (car/cdr-val x actual) *bad*)))
      (equal (ev$ x (put-assoc-equal gvar (evalator actual a1) a2))
        (evalator (car/cdr-val x actual) a1)))
    :hints (("Goal" :induct (true-car/cdr-nestp x gvar)
       :do-not-induct t
       :expand ((ev$ x (put-assoc-equal gvar (evalator actual a1) a2)))))))

local

(local (defthm strong-alist-property-cdr-assoc-equal-1
    (implies (and (strong-alist-propertyp old-alist gvar global-actual)
        (assoc-equal x old-alist))
      (equal (cdr (assoc-equal x old-alist))
        (car/cdr-val x global-actual)))))

local

(local (in-theory (disable strong-alist-property-cdr-assoc-equal-1)))

local

(local (defthm strong-alist-property-cdr-assoc-equal-2
    (implies (and (strong-alist-propertyp old-alist gvar global-actual)
        (assoc-equal x old-alist))
      (not (equal (car/cdr-val x global-actual) *bad*)))))

local

(local (in-theory (disable strong-alist-property-cdr-assoc-equal-2)))

local

(local (defthm strong-alist-property-implies-cadr-not-bad
    (implies (and (strong-alist-propertyp old-alist gvar global-actual)
        (symbolp gvar)
        (true-car/cdr-nestp x gvar)
        (assoc-equal x old-alist))
      (and (consp (car/cdr-val (cadr x) global-actual))
        (or (eq (car (car/cdr-val (cadr x) global-actual)) 'cons)
          (eq (car (car/cdr-val (cadr x) global-actual)) 'quote))))
    :rule-classes nil))

local

(local (defthm strong-alist-propertyp-implies-alistp
    (implies (strong-alist-propertyp alist gvar global-actual)
      (alistp alist))
    :rule-classes :forward-chaining))

local

(local (defthm ev$-relink-term-general
    (if flg
      (implies (and (tamep x)
          (not (equal (car/cdr-to-val-alist x gvar global-actual) *bad*))
          (pseudo-termp global-actual)
          (symbolp gvar)
          (subsetp-equal (all-true-car/cdr-nests t x gvar)
            (strip-cars old-alist))
          (strong-alist-propertyp old-alist gvar global-actual)
          (set-equalp (strip-cdrs old-alist) relevant-vals))
        (equal (ev$ (relink-term old-alist gvar relevant-vals x)
            (put-assoc-equal gvar (evalator-list relevant-vals a1) a2))
          (ev$ x
            (put-assoc-equal gvar (evalator global-actual a1) a2))))
      (implies (and (suitably-tamep-listp n flags x)
          (not (equal (car/cdr-to-val-alist-list x gvar global-actual)
              *bad*))
          (pseudo-termp global-actual)
          (symbolp gvar)
          (subsetp-equal (all-true-car/cdr-nests nil x gvar)
            (strip-cars old-alist))
          (strong-alist-propertyp old-alist gvar global-actual)
          (set-equalp (strip-cdrs old-alist) relevant-vals))
        (equal (ev$-list (relink-term-list old-alist gvar relevant-vals x)
            (put-assoc-equal gvar (evalator-list relevant-vals a1) a2))
          (ev$-list x
            (put-assoc-equal gvar (evalator global-actual a1) a2)))))
    :rule-classes nil
    :hints (("Goal" :induct (flagged-tamep-hint flg n flags x)
       :expand ((suitably-tamep-listp n flags x) (suitably-tamep-listp 1 nil (cdr x))
         (tamep x)
         (ev$ x a2)
         (relink-term old-alist gvar relevant-vals x)
         (ev$ (cons (car x)
             (relink-term-list old-alist gvar relevant-vals (cdr x)))
           (put-assoc-equal gvar (evalator-list relevant-vals a1) a2))
         (ev$ x
           (put-assoc-equal gvar (evalator global-actual a1) a2)))) ("Subgoal *1/3" :use (:instance strong-alist-property-implies-cadr-not-bad))
      (and stable-under-simplificationp
        '(:in-theory (enable strong-alist-property-cdr-assoc-equal-1))))))

local

(local (defthm ev$-relink-term
    (implies (and (tamep x)
        (not (equal (car/cdr-to-val-alist x gvar global-actual) *bad*))
        (pseudo-termp global-actual)
        (symbolp gvar))
      (equal (ev$ (relink-term (car/cdr-to-val-alist x gvar global-actual)
            gvar
            (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist x gvar global-actual))))
            x)
          (list (cons gvar
              (evalator-list (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist x gvar global-actual))))
                a1))
            (cons ivar target-tuple)))
        (ev$ x
          (list (cons gvar (evalator global-actual a1))
            (cons ivar target-tuple)))))
    :hints (("Goal" :use (:instance ev$-relink-term-general
         (flg t)
         (old-alist (car/cdr-to-val-alist x gvar global-actual))
         (relevant-vals (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist x gvar global-actual)))))
         (a2 (list (cons gvar any) (cons ivar target-tuple))))))))

local

(local (defthm relink-fancy-scion-lemma-sum$+
    (implies (and (tamep-functionp `(lambda (,GVAR ,IVAR) ,BODY))
        (symbolp gvar)
        (symbolp ivar)
        (not (eq gvar ivar))
        (pseudo-termp global-actual)
        (not (equal (car/cdr-to-val-alist body gvar global-actual) *bad*)))
      (equal (sum$+ (list 'lambda
            (list gvar ivar)
            (relink-term (car/cdr-to-val-alist body gvar global-actual)
              gvar
              (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist body gvar global-actual))))
              body))
          (evalator-list (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist body gvar global-actual))))
            a)
          targets)
        (sum$+ `(lambda (,GVAR ,IVAR) ,BODY)
          (evalator global-actual a)
          targets)))
    :hints (("Goal" :induct (sum$+ `(lambda (,GVAR ,IVAR) ,BODY)
         (evalator global-actual a)
         targets)))))

local

(local (defthm relink-fancy-scion-lemma-always$+
    (implies (and (tamep-functionp `(lambda (,GVAR ,IVAR) ,BODY))
        (symbolp gvar)
        (symbolp ivar)
        (not (eq gvar ivar))
        (pseudo-termp global-actual)
        (not (equal (car/cdr-to-val-alist body gvar global-actual) *bad*)))
      (equal (always$+ (list 'lambda
            (list gvar ivar)
            (relink-term (car/cdr-to-val-alist body gvar global-actual)
              gvar
              (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist body gvar global-actual))))
              body))
          (evalator-list (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist body gvar global-actual))))
            a)
          targets)
        (always$+ `(lambda (,GVAR ,IVAR) ,BODY)
          (evalator global-actual a)
          targets)))
    :hints (("Goal" :induct (always$+ `(lambda (,GVAR ,IVAR) ,BODY)
         (evalator global-actual a)
         targets)))))

local

(local (defthm relink-fancy-scion-lemma-thereis$+
    (implies (and (tamep-functionp `(lambda (,GVAR ,IVAR) ,BODY))
        (symbolp gvar)
        (symbolp ivar)
        (not (eq gvar ivar))
        (pseudo-termp global-actual)
        (not (equal (car/cdr-to-val-alist body gvar global-actual) *bad*)))
      (equal (thereis$+ (list 'lambda
            (list gvar ivar)
            (relink-term (car/cdr-to-val-alist body gvar global-actual)
              gvar
              (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist body gvar global-actual))))
              body))
          (evalator-list (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist body gvar global-actual))))
            a)
          targets)
        (thereis$+ `(lambda (,GVAR ,IVAR) ,BODY)
          (evalator global-actual a)
          targets)))
    :hints (("Goal" :induct (thereis$+ `(lambda (,GVAR ,IVAR) ,BODY)
         (evalator global-actual a)
         targets)))))

local

(local (defthm relink-fancy-scion-lemma-collect$+
    (implies (and (tamep-functionp `(lambda (,GVAR ,IVAR) ,BODY))
        (symbolp gvar)
        (symbolp ivar)
        (not (eq gvar ivar))
        (pseudo-termp global-actual)
        (not (equal (car/cdr-to-val-alist body gvar global-actual) *bad*)))
      (equal (collect$+ (list 'lambda
            (list gvar ivar)
            (relink-term (car/cdr-to-val-alist body gvar global-actual)
              gvar
              (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist body gvar global-actual))))
              body))
          (evalator-list (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist body gvar global-actual))))
            a)
          targets)
        (collect$+ `(lambda (,GVAR ,IVAR) ,BODY)
          (evalator global-actual a)
          targets)))
    :hints (("Goal" :induct (collect$+ `(lambda (,GVAR ,IVAR) ,BODY)
         (evalator global-actual a)
         targets)))))

local

(local (defthm relink-fancy-scion-lemma-append$+
    (implies (and (tamep-functionp `(lambda (,GVAR ,IVAR) ,BODY))
        (symbolp gvar)
        (symbolp ivar)
        (not (eq gvar ivar))
        (pseudo-termp global-actual)
        (not (equal (car/cdr-to-val-alist body gvar global-actual) *bad*)))
      (equal (append$+ (list 'lambda
            (list gvar ivar)
            (relink-term (car/cdr-to-val-alist body gvar global-actual)
              gvar
              (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist body gvar global-actual))))
              body))
          (evalator-list (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist body gvar global-actual))))
            a)
          targets)
        (append$+ `(lambda (,GVAR ,IVAR) ,BODY)
          (evalator global-actual a)
          targets)))
    :hints (("Goal" :induct (append$+ `(lambda (,GVAR ,IVAR) ,BODY)
         (evalator global-actual a)
         targets)))))

local

(local (defthm relink-fancy-scion-lemma-until$+
    (implies (and (tamep-functionp `(lambda (,GVAR ,IVAR) ,BODY))
        (symbolp gvar)
        (symbolp ivar)
        (not (eq gvar ivar))
        (pseudo-termp global-actual)
        (not (equal (car/cdr-to-val-alist body gvar global-actual) *bad*)))
      (equal (until$+ (list 'lambda
            (list gvar ivar)
            (relink-term (car/cdr-to-val-alist body gvar global-actual)
              gvar
              (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist body gvar global-actual))))
              body))
          (evalator-list (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist body gvar global-actual))))
            a)
          targets)
        (until$+ `(lambda (,GVAR ,IVAR) ,BODY)
          (evalator global-actual a)
          targets)))
    :hints (("Goal" :induct (until$+ `(lambda (,GVAR ,IVAR) ,BODY)
         (evalator global-actual a)
         targets)))))

local

(local (defthm relink-fancy-scion-lemma-when$+
    (implies (and (tamep-functionp `(lambda (,GVAR ,IVAR) ,BODY))
        (symbolp gvar)
        (symbolp ivar)
        (not (eq gvar ivar))
        (pseudo-termp global-actual)
        (not (equal (car/cdr-to-val-alist body gvar global-actual) *bad*)))
      (equal (when$+ (list 'lambda
            (list gvar ivar)
            (relink-term (car/cdr-to-val-alist body gvar global-actual)
              gvar
              (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist body gvar global-actual))))
              body))
          (evalator-list (merge-sort-term-order (remove-duplicates-equal (strip-cdrs (car/cdr-to-val-alist body gvar global-actual))))
            a)
          targets)
        (when$+ `(lambda (,GVAR ,IVAR) ,BODY)
          (evalator global-actual a)
          targets)))
    :hints (("Goal" :induct (when$+ `(lambda (,GVAR ,IVAR) ,BODY)
         (evalator global-actual a)
         targets)))))

local

(local (defthm make-true-cons-nest-opener
    (and (implies (atom tail)
        (equal (make-true-cons-nest tail) ''nil))
      (equal (make-true-cons-nest (cons a tail))
        `(cons ,A ,(MAKE-TRUE-CONS-NEST TAIL))))
    :hints (("Goal" :in-theory (enable make-true-cons-nest)))))

local

(local (defthm evalator-make-true-cons-nest
    (equal (evalator (make-true-cons-nest lst) a)
      (evalator-list lst a))
    :hints (("Goal" :induct (len lst)))))

relink-fancy-scion-correcttheorem

(defthm relink-fancy-scion-correct
  (implies (and (pseudo-termp x)
      (evalator (relink-fancy-scion-hypfn x) a))
    (equal (evalator x a) (evalator (relink-fancy-scion x) a)))
  :hints (("Goal" :in-theory (disable lambda-object-formals lambda-object-body)))
  :rule-classes ((:meta :trigger-fns (sum$+ always$+ thereis$+ collect$+ append$+ until$+ when$+))))