Filtering...

loop-lemmas

books/projects/apply/loop-lemmas

Included Books

base top-with-meta floor-mod
other
(in-package "ACL2")
include-book
(include-book "base")
assoc-eq-safe-cons-constheorem
(defthm assoc-eq-safe-cons-cons
  (implies (syntaxp (and (quotep key1) (quotep key2)))
    (equal (assoc-eq-safe key1 (cons (cons key2 val2) rest))
      (if (equal key1 key2)
        (cons key2 val2)
        (assoc-eq-safe key1 rest)))))
assoc-eq-safe-niltheorem
(defthm assoc-eq-safe-nil
  (equal (assoc-eq-safe key1 nil) nil))
in-theory
(in-theory (disable (:definition assoc-eq-safe)))
true-list-listp-tailstheorem
(defthm true-list-listp-tails
  (implies (true-listp lst) (true-list-listp (tails lst))))
true-list-listp-until$theorem
(defthm true-list-listp-until$
  (implies (true-list-listp lst)
    (true-list-listp (until$ fn lst))))
true-list-listp-until$+theorem
(defthm true-list-listp-until$+
  (implies (true-list-listp lst)
    (true-list-listp (until$+ fn globals lst))))
true-list-listp-when$theorem
(defthm true-list-listp-when$
  (implies (true-list-listp lst)
    (true-list-listp (when$ fn lst))))
true-list-listp-when$+theorem
(defthm true-list-listp-when$+
  (implies (true-list-listp lst)
    (true-list-listp (when$+ fn globals lst))))
true-listp-car-loop$-as-tupletheorem
(defthm true-listp-car-loop$-as-tuple
  (implies (true-list-listp tuple)
    (true-listp (car-loop$-as-tuple tuple))))
len-car-loop$-as-tupletheorem
(defthm len-car-loop$-as-tuple
  (equal (len (car-loop$-as-tuple tuple)) (len tuple)))
len-cdr-loop$-as-tupletheorem
(defthm len-cdr-loop$-as-tuple
  (equal (len (cdr-loop$-as-tuple tuple)) (len tuple)))
true-list-listp-cdr-loop$-as-tupletheorem
(defthm true-list-listp-cdr-loop$-as-tuple
  (implies (true-list-listp tuple)
    (true-list-listp (cdr-loop$-as-tuple tuple))))
true-list-listp-loop$-astheorem
(defthm true-list-listp-loop$-as
  (implies (true-list-listp tuple)
    (true-list-listp (loop$-as tuple))))
len-member-equal-loop$-astheorem
(defthm len-member-equal-loop$-as
  (implies (member-equal newv (loop$-as tuple))
    (equal (len newv) (len tuple)))
  :hints (("Goal" :induct (loop$-as tuple))))
from-to-by-x-xtheorem
(defthm from-to-by-x-x
  (equal (from-to-by x x y)
    (if (and (integerp x) (integerp y) (< 0 y))
      (list x)
      nil))
  :hints (("Goal" :expand ((from-to-by x x y) (from-to-by (+ x y) x y)))))
nat-listp-from-to-bytheorem
(defthm nat-listp-from-to-by
  (implies (natp i) (nat-listp (from-to-by i j k))))
integer-listp-from-to-bytheorem
(defthm integer-listp-from-to-by
  (implies (and (integerp i) (integerp k))
    (integer-listp (from-to-by i j k))))
integer-listp-until$theorem
(defthm integer-listp-until$
  (implies (integer-listp lst)
    (integer-listp (until$ fn lst))))
integer-listp-when$theorem
(defthm integer-listp-when$
  (implies (integer-listp lst) (integer-listp (when$ fn lst))))
member-equal-from-to-by-exactencapsulate
(encapsulate nil
  (local (include-book "arithmetic/top-with-meta" :dir :system))
  (local (include-book "centaur/bitops/floor-mod" :dir :system))
  (local (in-theory (disable floor mod)))
  (defthm member-equal-from-to-by-exact
    (implies (and (integerp i) (integerp j) (integerp k) (< 0 k))
      (iff (member-equal newv (from-to-by i j k))
        (and (integerp newv)
          (<= i newv)
          (<= newv j)
          (equal (mod (- newv i) k) 0))))
    :hints (("goal" :induct (from-to-by i j k)
       :expand ((mod (+ (- i) newv) k) (mod 0 k)))))
  (defthm integerp==>numerator-=-x
    (implies (integerp x) (equal (numerator x) x)))
  (defthm integerp==>denominator-=-1
    (implies (integerp x) (equal (denominator x) 1))))
member-equal-when$theorem
(defthm member-equal-when$
  (iff (member-equal e (when$ p lst))
    (and (member-equal e lst) (apply$ p (list e)))))
member-equal-until$theorem
(defthm member-equal-until$
  (iff (member-equal newv (until$ q lst))
    (and (member-equal newv lst)
      (< (mempos newv lst) (len (until$ q lst))))))
member-equal-when$+theorem
(defthm member-equal-when$+
  (iff (member-equal e (when$+ p pglob lst))
    (and (member-equal e lst) (apply$ p (list pglob e)))))
member-equal-until$+theorem
(defthm member-equal-until$+
  (iff (member-equal newv (until$+ q qglob lst))
    (and (member-equal newv lst)
      (< (mempos newv lst) (len (until$+ q qglob lst))))))
member-equal-newvar-components-1theorem
(defthm member-equal-newvar-components-1
  (implies (member-equal newvar (loop$-as (list t1)))
    (member-equal (car newvar) t1)))
member-equal-newvar-components-2theorem
(defthm member-equal-newvar-components-2
  (implies (member-equal newvar (loop$-as (list t1 t2)))
    (and (member-equal (car newvar) t1)
      (member-equal (cadr newvar) t2)))
  :hints (("Goal" :induct (pairlis$ t1 t2))))
member-equal-newvar-components-3theorem
(defthm member-equal-newvar-components-3
  (implies (member-equal newvar (loop$-as (list t1 t2 t3)))
    (and (member-equal (car newvar) t1)
      (member-equal (cadr newvar) t2)
      (member-equal (caddr newvar) t3)))
  :hints (("Goal" :induct (list (pairlis$ t1 t2) (pairlis$ t2 t3)))))
member-equal-acl2-count-smaller-0theorem
(defthm member-equal-acl2-count-smaller-0
  (implies (member-equal nv lst)
    (< (acl2-count nv) (acl2-count lst)))
  :rule-classes :linear)
member-equal-acl2-count-smaller-1theorem
(defthm member-equal-acl2-count-smaller-1
  (implies (member-equal nv (loop$-as (list lst1)))
    (< (acl2-count (car nv)) (acl2-count lst1)))
  :rule-classes :linear)
member-equal-acl2-count-smaller-2theorem
(defthm member-equal-acl2-count-smaller-2
  (implies (member-equal nv (loop$-as (list lst1 lst2)))
    (and (< (acl2-count (car nv)) (acl2-count lst1))
      (< (acl2-count (cadr nv)) (acl2-count lst2))))
  :hints (("Goal" :induct (pairlis$ lst1 lst2)))
  :rule-classes :linear)
member-equal-acl2-count-smaller-3theorem
(defthm member-equal-acl2-count-smaller-3
  (implies (member-equal nv (loop$-as (list lst1 lst2 lst3)))
    (and (< (acl2-count (car nv)) (acl2-count lst1))
      (< (acl2-count (cadr nv)) (acl2-count lst2))
      (< (acl2-count (caddr nv)) (acl2-count lst3))))
  :hints (("Goal" :induct (cons (pairlis$ lst1 lst2) (pairlis$ lst2 lst3))))
  :rule-classes :linear)
always$-p-lst-implies-p-elementtheorem
(defthm always$-p-lst-implies-p-element
  (implies (and (always$ fnp lst) (member-equal newv lst))
    (apply$ fnp (list newv))))
integer-listp-implies-integerptheorem
(defthm integer-listp-implies-integerp
  (implies (and (member-equal newv lst)
      (syntaxp (not (and (consp lst)
            (or (eq (car lst) 'loop$-as) (eq (car lst) 'tails)))))
      (integer-listp lst))
    (integerp newv)))
rational-listp-implies-rationalptheorem
(defthm rational-listp-implies-rationalp
  (implies (and (member-equal newv lst)
      (syntaxp (not (and (consp lst)
            (or (eq (car lst) 'loop$-as) (eq (car lst) 'tails)))))
      (rational-listp lst))
    (rationalp newv)))
acl2-number-listp-implies-acl2-numberptheorem
(defthm acl2-number-listp-implies-acl2-numberp
  (implies (and (member-equal newv lst)
      (syntaxp (not (and (consp lst)
            (or (eq (car lst) 'loop$-as) (eq (car lst) 'tails)))))
      (acl2-number-listp lst))
    (acl2-numberp newv)))
symbol-listp-implies-symbolptheorem
(defthm symbol-listp-implies-symbolp
  (implies (and (member-equal newv lst)
      (syntaxp (not (and (consp lst)
            (or (eq (car lst) 'loop$-as) (eq (car lst) 'tails)))))
      (symbol-listp lst))
    (symbolp newv)))
true-list-listp-implies-true-listp-xxxtheorem
(defthm true-list-listp-implies-true-listp-xxx
  (implies (and (syntaxp (not (and (consp lst) (eq (car lst) 'loop$-as))))
      (true-list-listp lst)
      (not (true-listp newv)))
    (not (member-equal newv lst))))
always$-p-lst-implies-p-element-corollarytheorem
(defthm always$-p-lst-implies-p-element-corollary
  (implies (and (always$ fnp lst)
      (syntaxp (not (and (consp lst)
            (or (eq (car lst) 'loop$-as) (eq (car lst) 'tails)))))
      (not (apply$ fnp (list newv))))
    (not (member-equal newv lst))))
nat-listp-implies-always$-natptheorem
(defthm nat-listp-implies-always$-natp
  (implies (nat-listp lst) (always$ 'natp lst)))
integer-listp-implies-always$-integerptheorem
(defthm integer-listp-implies-always$-integerp
  (implies (integer-listp lst) (always$ 'integerp lst)))
rational-listp-implies-always$-rationalptheorem
(defthm rational-listp-implies-always$-rationalp
  (implies (rational-listp lst) (always$ 'rationalp lst)))
acl2-number-listp-implies-always$-acl2-numberptheorem
(defthm acl2-number-listp-implies-always$-acl2-numberp
  (implies (acl2-number-listp lst)
    (always$ 'acl2-numberp lst)))
symbol-listp-implies-always$-symbolptheorem
(defthm symbol-listp-implies-always$-symbolp
  (implies (symbol-listp lst) (always$ 'symbolp lst)))
true-list-listp-implies-always$-true-listptheorem
(defthm true-list-listp-implies-always$-true-listp
  (implies (true-list-listp lst) (always$ 'true-listp lst)))
acl2-number-listp-from-to-bytheorem
(defthm acl2-number-listp-from-to-by
  (implies (and (integerp i) (integerp j) (integerp k) (< 0 k))
    (acl2-number-listp (from-to-by i j k))))
not-member-loop$-as-generalencapsulate
(encapsulate nil
  (local (defthm member-equal-nth-car-loop$-as-tuple
      (implies (and (consp tuple)
          (not (empty-loop$-as-tuplep tuple))
          (natp n)
          (< n (len tuple)))
        (member-equal (nth n (car-loop$-as-tuple tuple))
          (nth n tuple)))))
  (local (defthm member-equal-nth-cdr-loop$-as-tuple
      (implies (and (consp tuple)
          (not (empty-loop$-as-tuplep tuple))
          (member-equal (nth n newv)
            (nth n (cdr-loop$-as-tuple tuple))))
        (member-equal (nth n newv) (nth n tuple)))))
  (local (defthm member-equal-loop$-as-implies-member-equal-nth
      (implies (and (member-equal newv (loop$-as tuple))
          (natp n)
          (< n (len tuple)))
        (member-equal (nth n newv) (nth n tuple)))))
  (defthm not-member-loop$-as-general
    (implies (and (always$ fnp (nth n tuple))
        (not (apply$ fnp (list (nth n newv))))
        (natp n)
        (< n (len tuple)))
      (not (member-equal newv (loop$-as tuple))))))
not-member-loop$-as-always$-1theorem
(defthm not-member-loop$-as-always$-1
  (implies (and (always$ fnp lst1)
      (not (apply$ fnp (list (car newv)))))
    (not (member-equal newv (loop$-as (cons lst1 rest)))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (tuple (cons lst1 rest))
       (n 0)))))
not-member-loop$-as-always$-2theorem
(defthm not-member-loop$-as-always$-2
  (implies (and (always$ fnp lst2)
      (not (apply$ fnp (list (cadr newv)))))
    (not (member-equal newv (loop$-as (cons lst1 (cons lst2 rest))))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (tuple (cons lst1 (cons lst2 rest)))
       (n 1)))))
not-member-loop$-as-always-3theorem
(defthm not-member-loop$-as-always-3
  (implies (and (always$ fnp lst3)
      (not (apply$ fnp (list (caddr newv)))))
    (not (member-equal newv
        (loop$-as (cons lst1 (cons lst2 (cons lst3 rest)))))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (tuple (cons lst1 (cons lst2 (cons lst3 rest))))
       (n 2)))))
not-member-loop$-as-natp-1theorem
(defthm not-member-loop$-as-natp-1
  (implies (and (not (natp (car newv))) (nat-listp lst1))
    (not (member-equal newv (loop$-as (cons lst1 rest)))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'natp)
       (tuple (cons lst1 rest))
       (n 0)))))
not-member-loop$-as-natp-2theorem
(defthm not-member-loop$-as-natp-2
  (implies (and (not (natp (cadr newv))) (nat-listp lst2))
    (not (member-equal newv (loop$-as (cons lst1 (cons lst2 rest))))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'natp)
       (tuple (cons lst1 (cons lst2 rest)))
       (n 1)))))
not-member-loop$-as-natp-3theorem
(defthm not-member-loop$-as-natp-3
  (implies (and (not (natp (caddr newv))) (nat-listp lst3))
    (not (member-equal newv
        (loop$-as (cons lst1 (cons lst2 (cons lst3 rest)))))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'natp)
       (tuple (cons lst1 (cons lst2 (cons lst3 rest))))
       (n 2)))))
not-member-loop$-as-integer-1theorem
(defthm not-member-loop$-as-integer-1
  (implies (and (not (integerp (car newv))) (integer-listp lst1))
    (not (member-equal newv (loop$-as (cons lst1 rest)))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'integerp)
       (tuple (cons lst1 rest))
       (n 0)))))
not-member-loop$-as-integer-2theorem
(defthm not-member-loop$-as-integer-2
  (implies (and (not (integerp (cadr newv))) (integer-listp lst2))
    (not (member-equal newv (loop$-as (cons lst1 (cons lst2 rest))))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'integerp)
       (tuple (cons lst1 (cons lst2 rest)))
       (n 1)))))
not-member-loop$-as-integer-3theorem
(defthm not-member-loop$-as-integer-3
  (implies (and (not (integerp (caddr newv))) (integer-listp lst3))
    (not (member-equal newv
        (loop$-as (cons lst1 (cons lst2 (cons lst3 rest)))))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'integerp)
       (tuple (cons lst1 (cons lst2 (cons lst3 rest))))
       (n 2)))))
not-member-loop$-as-rational-1theorem
(defthm not-member-loop$-as-rational-1
  (implies (and (not (rationalp (car newv))) (rational-listp lst1))
    (not (member-equal newv (loop$-as (cons lst1 rest)))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'rationalp)
       (tuple (cons lst1 rest))
       (n 0)))))
not-member-loop$-as-rational-2theorem
(defthm not-member-loop$-as-rational-2
  (implies (and (not (rationalp (cadr newv))) (rational-listp lst2))
    (not (member-equal newv (loop$-as (cons lst1 (cons lst2 rest))))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'rationalp)
       (tuple (cons lst1 (cons lst2 rest)))
       (n 1)))))
not-member-loop$-as-rational-3theorem
(defthm not-member-loop$-as-rational-3
  (implies (and (not (rationalp (caddr newv))) (rational-listp lst3))
    (not (member-equal newv
        (loop$-as (cons lst1 (cons lst2 (cons lst3 rest)))))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'rationalp)
       (tuple (cons lst1 (cons lst2 (cons lst3 rest))))
       (n 2)))))
not-member-loop$-as-acl2-number-1theorem
(defthm not-member-loop$-as-acl2-number-1
  (implies (and (not (acl2-numberp (car newv)))
      (acl2-number-listp lst1))
    (not (member-equal newv (loop$-as (cons lst1 rest)))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'acl2-numberp)
       (tuple (cons lst1 rest))
       (n 0)))))
not-member-loop$-as-acl2-number-2theorem
(defthm not-member-loop$-as-acl2-number-2
  (implies (and (not (acl2-numberp (cadr newv)))
      (acl2-number-listp lst2))
    (not (member-equal newv (loop$-as (cons lst1 (cons lst2 rest))))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'acl2-numberp)
       (tuple (cons lst1 (cons lst2 rest)))
       (n 1)))))
not-member-loop$-as-acl2-number-3theorem
(defthm not-member-loop$-as-acl2-number-3
  (implies (and (not (acl2-numberp (caddr newv)))
      (acl2-number-listp lst3))
    (not (member-equal newv
        (loop$-as (cons lst1 (cons lst2 (cons lst3 rest)))))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'acl2-numberp)
       (tuple (cons lst1 (cons lst2 (cons lst3 rest))))
       (n 2)))))
not-member-loop$-as-symbol-1theorem
(defthm not-member-loop$-as-symbol-1
  (implies (and (not (symbolp (car newv))) (symbol-listp lst1))
    (not (member-equal newv (loop$-as (cons lst1 rest)))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'symbolp)
       (tuple (cons lst1 rest))
       (n 0)))))
not-member-loop$-as-symbol-2theorem
(defthm not-member-loop$-as-symbol-2
  (implies (and (not (symbolp (cadr newv))) (symbol-listp lst2))
    (not (member-equal newv (loop$-as (cons lst1 (cons lst2 rest))))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'symbolp)
       (tuple (cons lst1 (cons lst2 rest)))
       (n 1)))))
not-member-loop$-as-symbol-3theorem
(defthm not-member-loop$-as-symbol-3
  (implies (and (not (symbolp (caddr newv))) (symbol-listp lst3))
    (not (member-equal newv
        (loop$-as (cons lst1 (cons lst2 (cons lst3 rest)))))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'symbolp)
       (tuple (cons lst1 (cons lst2 (cons lst3 rest))))
       (n 2)))))
not-member-loop$-as-true-list-1theorem
(defthm not-member-loop$-as-true-list-1
  (implies (and (not (true-listp (car newv))) (true-list-listp lst1))
    (not (member-equal newv (loop$-as (cons lst1 rest)))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'true-listp)
       (tuple (cons lst1 rest))
       (n 0)))))
not-member-loop$-as-true-list-2theorem
(defthm not-member-loop$-as-true-list-2
  (implies (and (not (true-listp (cadr newv))) (true-list-listp lst2))
    (not (member-equal newv (loop$-as (cons lst1 (cons lst2 rest))))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'true-listp)
       (tuple (cons lst1 (cons lst2 rest)))
       (n 1)))))
not-member-loop$-as-true-list-3theorem
(defthm not-member-loop$-as-true-list-3
  (implies (and (not (true-listp (caddr newv))) (true-list-listp lst3))
    (not (member-equal newv
        (loop$-as (cons lst1 (cons lst2 (cons lst3 rest)))))))
  :hints (("Goal" :in-theory (disable not-member-loop$-as-general)
     :use (:instance not-member-loop$-as-general
       (fnp 'true-listp)
       (tuple (cons lst1 (cons lst2 (cons lst3 rest))))
       (n 2)))))
structure-of-loop$-as-elementstheorem
(defthm structure-of-loop$-as-elements
  (implies (member-equal newv (loop$-as tuple))
    (and (true-listp newv) (equal (len newv) (len tuple))))
  :rule-classes nil)
structure-of-loop$-as-elements-bridgetheorem
(defthm structure-of-loop$-as-elements-bridge
  (and (implies (not (true-listp newv))
      (not (member-equal newv (loop$-as tuple))))
    (implies (not (equal (len newv) (len tuple)))
      (not (member-equal newv (loop$-as tuple)))))
  :hints (("Goal" :use structure-of-loop$-as-elements)))
not-member-loop$-as-rational-listp-1theorem
(defthm not-member-loop$-as-rational-listp-1
  (implies (and (not (rational-listp (car newv)))
      (always$ 'rational-listp lst1))
    (not (member-equal newv (loop$-as (cons lst1 rest)))))
  :hints (("Goal" :use (:instance not-member-loop$-as-general
       (fnp 'rational-listp)
       (tuple (cons lst1 rest))
       (n 0)))))
not-member-loop$-as-rational-listp-2theorem
(defthm not-member-loop$-as-rational-listp-2
  (implies (and (not (rational-listp (cadr newv)))
      (always$ 'rational-listp lst2))
    (not (member-equal newv (loop$-as (cons lst1 (cons lst2 rest))))))
  :hints (("Goal" :use (:instance not-member-loop$-as-general
       (fnp 'rational-listp)
       (tuple (cons lst1 (cons lst2 rest)))
       (n 1)))))
not-member-loop$-as-rational-listp-3theorem
(defthm not-member-loop$-as-rational-listp-3
  (implies (and (not (rational-listp (caddr newv)))
      (always$ 'rational-listp lst3))
    (not (member-equal newv
        (loop$-as (cons lst1 (cons lst2 (cons lst3 rest)))))))
  :hints (("Goal" :use (:instance not-member-loop$-as-general
       (fnp 'rational-listp)
       (tuple (cons lst1 (cons lst2 (cons lst3 rest))))
       (n 2)))))
not-member-loop$-as-identity-1theorem
(defthm not-member-loop$-as-identity-1
  (implies (and (not (car newv)) (always$ 'identity lst1))
    (not (member-equal newv (loop$-as (cons lst1 rest)))))
  :hints (("Goal" :use (:instance not-member-loop$-as-general
       (fnp 'identity)
       (tuple (cons lst1 rest))
       (n 0)))))
not-member-loop$-as-identity-2theorem
(defthm not-member-loop$-as-identity-2
  (implies (and (not (cadr newv)) (always$ 'identity lst2))
    (not (member-equal newv (loop$-as (cons lst1 (cons lst2 rest))))))
  :hints (("Goal" :use (:instance not-member-loop$-as-general
       (fnp 'identity)
       (tuple (cons lst1 (cons lst2 rest)))
       (n 1)))))
not-member-loop$-as-identity-3theorem
(defthm not-member-loop$-as-identity-3
  (implies (and (not (caddr newv)) (always$ 'identity lst3))
    (not (member-equal newv
        (loop$-as (cons lst1 (cons lst2 (cons lst3 rest)))))))
  :hints (("Goal" :use (:instance not-member-loop$-as-general
       (fnp 'identity)
       (tuple (cons lst1 (cons lst2 (cons lst3 rest))))
       (n 2)))))
always-rational-listp-tailstheorem
(defthm always-rational-listp-tails
  (implies (rational-listp lst)
    (always$ 'rational-listp (tails lst))))
no-element-tails-emptytheorem
(defthm no-element-tails-empty
  (always$ 'identity (tails lst)))
true-listp-append-rewritetheorem
(defthm true-listp-append-rewrite
  (equal (true-listp (append a b)) (true-listp b)))
not-member-tails-integer-listptheorem
(defthm not-member-tails-integer-listp
  (implies (and (integer-listp lst) (not (integer-listp newv)))
    (not (member-equal newv (tails lst)))))
not-member-tails-rational-listptheorem
(defthm not-member-tails-rational-listp
  (implies (and (rational-listp lst) (not (rational-listp newv)))
    (not (member-equal newv (tails lst)))))
not-member-tails-acl2-number-listptheorem
(defthm not-member-tails-acl2-number-listp
  (implies (and (acl2-number-listp lst) (not (acl2-number-listp newv)))
    (not (member-equal newv (tails lst)))))
not-member-tails-symbol-listptheorem
(defthm not-member-tails-symbol-listp
  (implies (and (symbol-listp lst) (not (symbol-listp newv)))
    (not (member-equal newv (tails lst)))))
not-member-tails-true-list-listptheorem
(defthm not-member-tails-true-list-listp
  (implies (and (true-list-listp lst) (not (true-list-listp newv)))
    (not (member-equal newv (tails lst)))))
from-to-by-downfunction
(defun from-to-by-down
  (i j)
  (declare (xargs :measure (nfix (- (+ 1 (ifix j)) (ifix i)))))
  (cond ((integerp j) (if (< j (ifix i))
        nil
        (append (from-to-by-down i (- j 1)) (list j))))
    (t nil)))
from-to-by-down-inductiontheorem
(defthm from-to-by-down-induction
  t
  :rule-classes ((:induction :pattern (from-to-by i j 1)
     :scheme (from-to-by-down i j))))
from-to-by-down-openertheorem
(defthm from-to-by-down-opener
  (implies (and (integerp i) (integerp j))
    (equal (from-to-by i j 1)
      (if (<= i j)
        (append (from-to-by i (- j 1) 1) (list j))
        nil)))
  :hints (("Subgoal *1/4'''" :expand ((from-to-by i i 1) (from-to-by (+ 1 i) i 1))))
  :rule-classes ((:definition :install-body nil)))
in-theory
(in-theory (disable (:induction from-to-by)))
from-to-by1function
(defun from-to-by1
  (i j k)
  (declare (xargs :measure (from-to-by-measure i j)))
  (cond ((and (integerp i) (integerp j) (integerp k) (< 0 k)) (cond ((<= i j) (cons i (from-to-by1 (+ i k) j k))) (t nil)))
    (t nil)))
sum$-ftb-ruletheorem
(defthm sum$-ftb-rule
  t
  :rule-classes ((:induction :pattern (sum$ fn (from-to-by lo hi by))
     :scheme (from-to-by1 lo hi by))))
always$-ftb-ruletheorem
(defthm always$-ftb-rule
  t
  :rule-classes ((:induction :pattern (always$ fn (from-to-by lo hi by))
     :scheme (from-to-by1 lo hi by))))
thereis$-ftb-ruletheorem
(defthm thereis$-ftb-rule
  t
  :rule-classes ((:induction :pattern (thereis$ fn (from-to-by lo hi by))
     :scheme (from-to-by1 lo hi by))))
collect$-ftb-ruletheorem
(defthm collect$-ftb-rule
  t
  :rule-classes ((:induction :pattern (collect$ fn (from-to-by lo hi by))
     :scheme (from-to-by1 lo hi by))))
append$-ftb-ruletheorem
(defthm append$-ftb-rule
  t
  :rule-classes ((:induction :pattern (append$ fn (from-to-by lo hi by))
     :scheme (from-to-by1 lo hi by))))
until$-ftb-ruletheorem
(defthm until$-ftb-rule
  t
  :rule-classes ((:induction :pattern (until$ fn (from-to-by lo hi by))
     :scheme (from-to-by1 lo hi by))))
when$-ftb-ruletheorem
(defthm when$-ftb-rule
  t
  :rule-classes ((:induction :pattern (when$ fn (from-to-by lo hi by))
     :scheme (from-to-by1 lo hi by))))
loop$-as-cdr-ruletheorem
(defthm loop$-as-cdr-rule
  t
  :rule-classes ((:induction :pattern (loop$-as (list lst))
     :condition (syntaxp (variablep lst))
     :scheme (len lst)) (:induction :pattern (loop$-as (list (tails lst)))
      :condition (syntaxp (variablep lst))
      :scheme (len lst))))
loop$-as-ftb-ruletheorem
(defthm loop$-as-ftb-rule
  t
  :rule-classes ((:induction :pattern (loop$-as (list (from-to-by lo hi by)))
     :condition (syntaxp (variablep lo))
     :scheme (from-to-by1 lo hi by))))
loop$-as-cdr-cdrfunction
(defun loop$-as-cdr-cdr
  (lst1 lst2)
  (declare (xargs :measure (+ (acl2-count lst1) (acl2-count lst2))))
  (cond ((endp lst1) nil)
    ((endp lst2) nil)
    (t (loop$-as-cdr-cdr (cdr lst1) (cdr lst2)))))
loop$-as-cdr-cdr-ruletheorem
(defthm loop$-as-cdr-cdr-rule
  t
  :rule-classes ((:induction :pattern (loop$-as (list lst1 lst2))
     :condition (syntaxp (and (variablep lst1) (variablep lst2) (not (eq lst1 lst2))))
     :scheme (loop$-as-cdr-cdr lst1 lst2)) (:induction :pattern (loop$-as (list lst1 (tails lst2)))
      :condition (syntaxp (and (variablep lst1) (variablep lst2) (not (eq lst1 lst2))))
      :scheme (loop$-as-cdr-cdr lst1 lst2))
    (:induction :pattern (loop$-as (list (tails lst2) lst1))
      :condition (syntaxp (and (variablep lst1) (variablep lst2) (not (eq lst1 lst2))))
      :scheme (loop$-as-cdr-cdr lst1 lst2))
    (:induction :pattern (loop$-as (list (tails lst1) (tails lst2)))
      :condition (syntaxp (and (variablep lst1) (variablep lst2) (not (eq lst1 lst2))))
      :scheme (loop$-as-cdr-cdr lst1 lst2))
    (:induction :pattern (loop$-as (list lst1 lst1))
      :condition (syntaxp (variablep lst1))
      :scheme (len lst1))
    (:induction :pattern (loop$-as (list (tails lst1) lst1))
      :condition (syntaxp (variablep lst1))
      :scheme (len lst1))
    (:induction :pattern (loop$-as (list lst1 (tails lst1)))
      :condition (syntaxp (variablep lst1))
      :scheme (len lst1))
    (:induction :pattern (loop$-as (list (tails lst1) (tails lst1)))
      :condition (syntaxp (variablep lst1))
      :scheme (len lst1))))
loop$-as-cdr-fbfunction
(defun loop$-as-cdr-fb
  (lst lo by)
  (cond ((endp lst) (list lst lo by))
    (t (loop$-as-cdr-fb (cdr lst) (+ by lo) by))))
loop$-as-cdr-ftbfunction
(defun loop$-as-cdr-ftb
  (lst lo hi by)
  (if (and (integerp lo) (integerp hi) (integerp by) (< 0 by))
    (cond ((endp lst) (list lst lo hi by))
      ((< hi lo) (list lst lo hi by))
      (t (loop$-as-cdr-ftb (cdr lst) (+ by lo) hi by)))
    (list lst lo hi by)))
loop$-as-cdr-fbt-ruletheorem
(defthm loop$-as-cdr-fbt-rule
  t
  :rule-classes ((:induction :pattern (loop$-as (list lst (from-to-by lo hi by)))
     :condition (syntaxp (and (variablep lst) (member lst (all-vars hi))))
     :scheme (loop$-as-cdr-fb lst lo by)) (:induction :pattern (loop$-as (list (from-to-by lo hi by) lst))
      :condition (syntaxp (and (variablep lst) (member lst (all-vars hi))))
      :scheme (loop$-as-cdr-fb lst lo by))
    (:induction :pattern (loop$-as (list (tails lst) (from-to-by lo hi by)))
      :condition (syntaxp (and (variablep lst) (member lst (all-vars hi))))
      :scheme (loop$-as-cdr-fb lst lo by))
    (:induction :pattern (loop$-as (list (from-to-by lo hi by) (tails lst)))
      :condition (syntaxp (and (variablep lst) (member lst (all-vars hi))))
      :scheme (loop$-as-cdr-fb lst lo by))
    (:induction :pattern (loop$-as (list lst (from-to-by lo hi by)))
      :condition (syntaxp (and (variablep lst) (not (member lst (all-vars hi)))))
      :scheme (loop$-as-cdr-ftb lst lo hi by))
    (:induction :pattern (loop$-as (list (from-to-by lo hi by) lst))
      :condition (syntaxp (and (variablep lst) (not (member lst (all-vars hi)))))
      :scheme (loop$-as-cdr-ftb lst lo hi by))
    (:induction :pattern (loop$-as (list (tails lst) (from-to-by lo hi by)))
      :condition (syntaxp (and (variablep lst) (not (member lst (all-vars hi)))))
      :scheme (loop$-as-cdr-ftb lst lo hi by))
    (:induction :pattern (loop$-as (list (from-to-by lo hi by) (tails lst)))
      :condition (syntaxp (and (variablep lst) (not (member lst (all-vars hi)))))
      :scheme (loop$-as-cdr-ftb lst lo hi by))))
loop$-as-ftb-ftbfunction
(defun loop$-as-ftb-ftb
  (lo1 hi1 by1 lo2 hi2 by2)
  (declare (xargs :measure (+ (from-to-by-measure lo1 hi1)
        (from-to-by-measure lo2 hi2))))
  (if (and (integerp lo1)
      (integerp hi1)
      (integerp by1)
      (integerp lo2)
      (integerp hi2)
      (integerp by2)
      (< 0 by1)
      (< 0 by2))
    (cond ((< hi1 lo1) (list lo1 hi1 by1 lo2 hi2 by2))
      ((< hi2 lo2) (list lo1 hi1 by1 lo2 hi2 by2))
      (t (loop$-as-ftb-ftb (+ by1 lo1) hi1 by1 (+ by2 lo2) hi2 by2)))
    (list lo1 hi1 by1 lo2 hi2 by2)))
loop$-as-ftb-ftb-ruletheorem
(defthm loop$-as-ftb-ftb-rule
  t
  :rule-classes ((:induction :pattern (loop$-as (list (from-to-by lo1 hi1 by1) (from-to-by lo2 hi2 by2)))
     :condition (syntaxp (and (variablep lo1) (variablep lo2)))
     :scheme (loop$-as-ftb-ftb lo1 hi1 by1 lo2 hi2 by2))))
len-collect$+-1theorem
(defthm len-collect$+-1
  (equal (len (collect$+ fn gvars (loop$-as (list lst))))
    (len lst)))
len-collect$+-2theorem
(defthm len-collect$+-2
  (equal (len (collect$+ fn gvars (loop$-as (list lst1 lst2))))
    (min (len lst1) (len lst2))))
always$-ttheorem
(defthm always$-t (equal (always$ `(lambda (,E) 't) lst) t))
sum$-appendtheorem
(defthm sum$-append
  (equal (sum$ fn (append a b)) (+ (sum$ fn a) (sum$ fn b))))
always$-appendtheorem
(defthm always$-append
  (equal (always$ fn (append a b))
    (and (always$ fn a) (always$ fn b))))
thereis$-appendtheorem
(defthm thereis$-append
  (equal (thereis$ fn (append a b))
    (or (thereis$ fn a) (thereis$ fn b))))
collect$-appendtheorem
(defthm collect$-append
  (equal (collect$ fn (append a b))
    (append (collect$ fn a) (collect$ fn b))))
append$-appendtheorem
(defthm append$-append
  (equal (append$ fn (append a b))
    (append (append$ fn a) (append$ fn b))))
until$-appendtheorem
(defthm until$-append
  (equal (until$ fn (append a b))
    (if (thereis$ fn a)
      (until$ fn a)
      (append a (until$ fn b)))))
when$-appendtheorem
(defthm when$-append
  (equal (when$ fn (append a b))
    (append (when$ fn a) (when$ fn b))))
sum$+-append-1theorem
(defthm sum$+-append-1
  (equal (sum$+ fn gvars (loop$-as (list (append a b))))
    (+ (sum$+ fn gvars (loop$-as (list a)))
      (sum$+ fn gvars (loop$-as (list b))))))
sum$+-append-2atheorem
(defthm sum$+-append-2a
  (equal (sum$+ fn gvars (loop$-as (list (append a b) c)))
    (cond ((< (len a) (len c)) (+ (sum$+ fn gvars (loop$-as (list a c)))
          (sum$+ fn gvars (loop$-as (list b (nthcdr (len a) c))))))
      (t (sum$+ fn gvars (loop$-as (list a c)))))))
sum$+-append-2btheorem
(defthm sum$+-append-2b
  (equal (sum$+ fn gvars (loop$-as (list c (append a b))))
    (cond ((< (len a) (len c)) (+ (sum$+ fn gvars (loop$-as (list c a)))
          (sum$+ fn gvars (loop$-as (list (nthcdr (len a) c) b)))))
      (t (sum$+ fn gvars (loop$-as (list c a)))))))
always$+-append-1theorem
(defthm always$+-append-1
  (equal (always$+ fn gvars (loop$-as (list (append a b))))
    (and (always$+ fn gvars (loop$-as (list a)))
      (always$+ fn gvars (loop$-as (list b))))))
always$+-append-2atheorem
(defthm always$+-append-2a
  (equal (always$+ fn gvars (loop$-as (list (append a b) c)))
    (cond ((< (len a) (len c)) (and (always$+ fn gvars (loop$-as (list a c)))
          (always$+ fn gvars (loop$-as (list b (nthcdr (len a) c))))))
      (t (always$+ fn gvars (loop$-as (list a c)))))))
always$+-append-2btheorem
(defthm always$+-append-2b
  (equal (always$+ fn gvars (loop$-as (list c (append a b))))
    (cond ((< (len a) (len c)) (and (always$+ fn gvars (loop$-as (list c a)))
          (always$+ fn gvars (loop$-as (list (nthcdr (len a) c) b)))))
      (t (always$+ fn gvars (loop$-as (list c a)))))))
thereis$+-append-1theorem
(defthm thereis$+-append-1
  (equal (thereis$+ fn gvars (loop$-as (list (append a b))))
    (or (thereis$+ fn gvars (loop$-as (list a)))
      (thereis$+ fn gvars (loop$-as (list b))))))
thereis$+-append-2atheorem
(defthm thereis$+-append-2a
  (equal (thereis$+ fn gvars (loop$-as (list (append a b) c)))
    (cond ((< (len a) (len c)) (or (thereis$+ fn gvars (loop$-as (list a c)))
          (thereis$+ fn gvars (loop$-as (list b (nthcdr (len a) c))))))
      (t (thereis$+ fn gvars (loop$-as (list a c)))))))
thereis$+-append-2btheorem
(defthm thereis$+-append-2b
  (equal (thereis$+ fn gvars (loop$-as (list c (append a b))))
    (cond ((< (len a) (len c)) (or (thereis$+ fn gvars (loop$-as (list c a)))
          (thereis$+ fn gvars (loop$-as (list (nthcdr (len a) c) b)))))
      (t (thereis$+ fn gvars (loop$-as (list c a)))))))
collect$+-append-1theorem
(defthm collect$+-append-1
  (equal (collect$+ fn gvars (loop$-as (list (append a b))))
    (append (collect$+ fn gvars (loop$-as (list a)))
      (collect$+ fn gvars (loop$-as (list b))))))
collect$+-append-2atheorem
(defthm collect$+-append-2a
  (equal (collect$+ fn gvars (loop$-as (list (append a b) c)))
    (cond ((< (len a) (len c)) (append (collect$+ fn gvars (loop$-as (list a c)))
          (collect$+ fn gvars (loop$-as (list b (nthcdr (len a) c))))))
      (t (collect$+ fn gvars (loop$-as (list a c)))))))
collect$+-append-2btheorem
(defthm collect$+-append-2b
  (equal (collect$+ fn gvars (loop$-as (list c (append a b))))
    (cond ((< (len a) (len c)) (append (collect$+ fn gvars (loop$-as (list c a)))
          (collect$+ fn gvars (loop$-as (list (nthcdr (len a) c) b)))))
      (t (collect$+ fn gvars (loop$-as (list c a)))))))
append$+-append-1theorem
(defthm append$+-append-1
  (equal (append$+ fn gvars (loop$-as (list (append a b))))
    (append (append$+ fn gvars (loop$-as (list a)))
      (append$+ fn gvars (loop$-as (list b))))))
append$+-append-2atheorem
(defthm append$+-append-2a
  (equal (append$+ fn gvars (loop$-as (list (append a b) c)))
    (cond ((< (len a) (len c)) (append (append$+ fn gvars (loop$-as (list a c)))
          (append$+ fn gvars (loop$-as (list b (nthcdr (len a) c))))))
      (t (append$+ fn gvars (loop$-as (list a c)))))))
append$+-append-2btheorem
(defthm append$+-append-2b
  (equal (append$+ fn gvars (loop$-as (list c (append a b))))
    (cond ((< (len a) (len c)) (append (append$+ fn gvars (loop$-as (list c a)))
          (append$+ fn gvars (loop$-as (list (nthcdr (len a) c) b)))))
      (t (append$+ fn gvars (loop$-as (list c a)))))))
until$+-append-1theorem
(defthm until$+-append-1
  (equal (until$+ fn gvars (loop$-as (list (append a b))))
    (if (thereis$+ fn gvars (loop$-as (list a)))
      (until$+ fn gvars (loop$-as (list a)))
      (append (loop$-as (list a))
        (until$+ fn gvars (loop$-as (list b)))))))
until$+-append-2atheorem
(defthm until$+-append-2a
  (equal (until$+ fn gvars (loop$-as (list (append a b) c)))
    (cond ((< (len a) (len c)) (if (thereis$+ fn gvars (loop$-as (list a c)))
          (until$+ fn gvars (loop$-as (list a c)))
          (append (loop$-as (list a c))
            (until$+ fn gvars (loop$-as (list b (nthcdr (len a) c)))))))
      (t (until$+ fn gvars (loop$-as (list a c)))))))
until$+-append-2btheorem
(defthm until$+-append-2b
  (equal (until$+ fn gvars (loop$-as (list c (append a b))))
    (cond ((< (len a) (len c)) (if (thereis$+ fn gvars (loop$-as (list c a)))
          (until$+ fn gvars (loop$-as (list c a)))
          (append (loop$-as (list c a))
            (until$+ fn gvars (loop$-as (list (nthcdr (len a) c) b))))))
      (t (until$+ fn gvars (loop$-as (list c a)))))))
when$+-append-1theorem
(defthm when$+-append-1
  (equal (when$+ fn gvars (loop$-as (list (append a b))))
    (append (when$+ fn gvars (loop$-as (list a)))
      (when$+ fn gvars (loop$-as (list b))))))
when$+-append-2atheorem
(defthm when$+-append-2a
  (equal (when$+ fn gvars (loop$-as (list (append a b) c)))
    (cond ((< (len a) (len c)) (append (when$+ fn gvars (loop$-as (list a c)))
          (when$+ fn gvars (loop$-as (list b (nthcdr (len a) c))))))
      (t (when$+ fn gvars (loop$-as (list a c)))))))
when$+-append-2btheorem
(defthm when$+-append-2b
  (equal (when$+ fn gvars (loop$-as (list c (append a b))))
    (cond ((< (len a) (len c)) (append (when$+ fn gvars (loop$-as (list c a)))
          (when$+ fn gvars (loop$-as (list (nthcdr (len a) c) b)))))
      (t (when$+ fn gvars (loop$-as (list c a)))))))
sum$-singletontheorem
(defthm sum$-singleton
  (equal (sum$ fn (list x)) (fix (apply$ fn (list x)))))
always$-singletontheorem
(defthm always$-singleton
  (equal (always$ fn (list x))
    (if (apply$ fn (list x))
      t
      nil)))
thereis$-singletontheorem
(defthm thereis$-singleton
  (equal (thereis$ fn (list x)) (apply$ fn (list x))))
collect$-singletontheorem
(defthm collect$-singleton
  (equal (collect$ fn (list x)) (list (apply$ fn (list x)))))
true-listp-true-list-fix-idtheorem
(defthm true-listp-true-list-fix-id
  (implies (true-listp x) (equal (true-list-fix x) x)))
len-true-list-fixtheorem
(defthm len-true-list-fix
  (equal (len (true-list-fix x)) (len x)))
append$-singletontheorem
(defthm append$-singleton
  (equal (append$ fn (list x))
    (true-list-fix (apply$ fn (list x)))))
until$-singletontheorem
(defthm until$-singleton
  (equal (until$ fn (list x))
    (if (apply$ fn (list x))
      nil
      (list x))))
when$-singletontheorem
(defthm when$-singleton
  (equal (when$ fn (list x))
    (if (apply$ fn (list x))
      (list x)
      nil)))
sum$+-singletontheorem
(defthm sum$+-singleton
  (equal (sum$+ fn gvars (list ituple))
    (fix (apply$ fn (list gvars ituple)))))
always$+-singletontheorem
(defthm always$+-singleton
  (equal (always$+ fn gvars (list ituple))
    (if (apply$ fn (list gvars ituple))
      t
      nil)))
thereis$+-singletontheorem
(defthm thereis$+-singleton
  (equal (thereis$+ fn gvars (list ituple))
    (apply$ fn (list gvars ituple))))
collect$+-singletontheorem
(defthm collect$+-singleton
  (equal (collect$+ fn gvars (list ituple))
    (list (apply$ fn (list gvars ituple)))))
append$+-singletontheorem
(defthm append$+-singleton
  (equal (append$+ fn gvars (list ituple))
    (true-list-fix (apply$ fn (list gvars ituple)))))
until$+-singletontheorem
(defthm until$+-singleton
  (equal (until$+ fn gvars (list ituple))
    (if (apply$ fn (list gvars ituple))
      nil
      (list ituple))))
when$+-singletontheorem
(defthm when$+-singleton
  (equal (when$+ fn gvars (list ituple))
    (if (apply$ fn (list gvars ituple))
      (list ituple)
      nil)))
compose-thereis-collecttheorem
(defthm compose-thereis-collect
  (and (implies (and (tamep expr1) (tamep expr2) (symbolp u1) (symbolp v1))
      (equal (thereis$ `(lambda (,U1) ,EXPR1)
          (collect$ `(lambda (,V1) ,EXPR2) lst))
        (thereis$ `(lambda (,V1) ((lambda (,U1) ,EXPR1) ,EXPR2))
          lst)))
    (implies (and (tamep expr1)
        (tamep expr2)
        (symbolp u1)
        (symbolp v1)
        (symbolp v2))
      (equal (thereis$ `(lambda (,U1) ,EXPR1)
          (collect$+ `(lambda (,V1 ,V2) ,EXPR2)
            gvars
            (loop$-as (list lst))))
        (thereis$+ `(lambda (,V1 ,V2) ((lambda (,U1) ,EXPR1) ,EXPR2))
          gvars
          (loop$-as (list lst)))))
    (implies (and (tamep expr1)
        (tamep expr2)
        (symbolp u1)
        (symbolp v1)
        (not (eq u1 v1))
        (not (eq u1 v2))
        (symbolp u2)
        (symbolp v2)
        (not (eq u2 v2)))
      (equal (thereis$+ `(lambda (,U1 ,V1) ,EXPR1)
          gvars
          (loop$-as (list (collect$ `(lambda (,V2) ,EXPR2) lst))))
        (thereis$+ `(lambda (,U1 ,V2)
            ((lambda (,U1 ,V1) ,EXPR1) ,U1
              (cons ((lambda (,V2) ,EXPR2) (car ,V2)) 'nil)))
          gvars
          (loop$-as (list lst)))))
    (implies (and (tamep expr1)
        (tamep expr2)
        (symbolp u1)
        (symbolp v1)
        (not (eq u1 v1))
        (symbolp u2)
        (symbolp v2)
        (not (eq u2 v2)))
      (equal (thereis$+ `(lambda (,U1 ,V1) ,EXPR1)
          gvars1
          (loop$-as (list (collect$+ `(lambda (,U2 ,V2) ,EXPR2)
                gvars2
                (loop$-as (list lst))))))
        (thereis$+ `(lambda (,U2 ,V2)
            ((lambda (,U1 ,V1) ,EXPR1) (car ,U2)
              ((lambda (,U2 ,V2) (cons ,EXPR2 'nil)) (car (cdr ,U2)) ,V2)))
          (list gvars1 gvars2)
          (loop$-as (list lst)))))
    (implies (and (tamep expr1)
        (tamep expr2)
        (symbolp u1)
        (symbolp v1)
        (not (eq u1 v1))
        (symbolp u2)
        (symbolp v2)
        (not (eq u2 v2)))
      (equal (thereis$+ `(lambda (,U1 ,V1) ,EXPR1)
          gvars
          (loop$-as (list (collect$+ `(lambda (,U2 ,V2) ,EXPR2)
                gvars
                (loop$-as (list lst))))))
        (thereis$+ `(lambda (,U2 ,V2)
            ((lambda (,U1 ,V1) ,EXPR1) ,U2 (cons ,EXPR2 'nil)))
          gvars
          (loop$-as (list lst)))))))
compose-always-collecttheorem
(defthm compose-always-collect
  (and (implies (and (tamep expr1) (tamep expr2) (symbolp u1) (symbolp v1))
      (equal (always$ `(lambda (,U1) ,EXPR1)
          (collect$ `(lambda (,V1) ,EXPR2) lst))
        (always$ `(lambda (,V1) ((lambda (,U1) ,EXPR1) ,EXPR2)) lst)))
    (implies (and (tamep expr1)
        (tamep expr2)
        (symbolp u1)
        (symbolp v1)
        (symbolp v2))
      (equal (always$ `(lambda (,U1) ,EXPR1)
          (collect$+ `(lambda (,V1 ,V2) ,EXPR2)
            gvars
            (loop$-as (list lst))))
        (always$+ `(lambda (,V1 ,V2) ((lambda (,U1) ,EXPR1) ,EXPR2))
          gvars
          (loop$-as (list lst)))))
    (implies (and (tamep expr1)
        (tamep expr2)
        (symbolp u1)
        (symbolp v1)
        (not (eq u1 v1))
        (not (eq u1 v2))
        (symbolp u2)
        (symbolp v2)
        (not (eq u2 v2)))
      (equal (always$+ `(lambda (,U1 ,V1) ,EXPR1)
          gvars
          (loop$-as (list (collect$ `(lambda (,V2) ,EXPR2) lst))))
        (always$+ `(lambda (,U1 ,V2)
            ((lambda (,U1 ,V1) ,EXPR1) ,U1
              (cons ((lambda (,V2) ,EXPR2) (car ,V2)) 'nil)))
          gvars
          (loop$-as (list lst)))))
    (implies (and (tamep expr1)
        (tamep expr2)
        (symbolp u1)
        (symbolp v1)
        (not (eq u1 v1))
        (symbolp u2)
        (symbolp v2)
        (not (eq u2 v2)))
      (equal (always$+ `(lambda (,U1 ,V1) ,EXPR1)
          gvars1
          (loop$-as (list (collect$+ `(lambda (,U2 ,V2) ,EXPR2)
                gvars2
                (loop$-as (list lst))))))
        (always$+ `(lambda (,U2 ,V2)
            ((lambda (,U1 ,V1) ,EXPR1) (car ,U2)
              ((lambda (,U2 ,V2) (cons ,EXPR2 'nil)) (car (cdr ,U2)) ,V2)))
          (list gvars1 gvars2)
          (loop$-as (list lst)))))
    (implies (and (tamep expr1)
        (tamep expr2)
        (symbolp u1)
        (symbolp v1)
        (not (eq u1 v1))
        (symbolp u2)
        (symbolp v2)
        (not (eq u2 v2)))
      (equal (always$+ `(lambda (,U1 ,V1) ,EXPR1)
          gvars
          (loop$-as (list (collect$+ `(lambda (,U2 ,V2) ,EXPR2)
                gvars
                (loop$-as (list lst))))))
        (always$+ `(lambda (,U2 ,V2)
            ((lambda (,U1 ,V1) ,EXPR1) ,U2 (cons ,EXPR2 'nil)))
          gvars
          (loop$-as (list lst)))))))