#|
Copyright (C) 1994 by Misao Nagayama and Carolyn Talcott.  All Rights Reserved.
You may copy and distribute verbatim copies of this Nqthm-1992 event script as
you receive it, in any medium, including embedding it verbatim in derivative
works, provided that you conspicuously and appropriately publish on each copy
a valid copyright notice "Copyright (C) 1994 by Misao Nagayama and Carolyn
Talcott.  All Rights Reserved."
NO WARRANTY
Misao Nagayama and Carolyn Talcott PROVIDE 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 Misao Nagayama or Carolyn Talcott 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.
|#

Event: Start with the initial nqthm theory.

;;;;;;;;;;;;;;;;;;;;;;   mutex-atomic.ev    ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;  com.ev  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;*sequence and finite set utilities
;;;The ith entry in l.

Definition: nth (l, i) = if listp (l) then if i = 1 then car (l)

else nth (cdr (l), i − 1) endif elseif l ∈ N then if i = 1 then l else f endif

else f endif

Event: Disable nth.

;;;update ith entry of l to be k

Definition: move (l, i, k) = if i = 0 then l

elseif l ≃ nil

then if i = 1 then k else l endif

elseif i = 1 then cons (k, cdr (l))

else cons (car (l), move (cdr (l), i − 1, k)) endif

Event: Disable move.

Definition: at (l, i, k) = (nth (l, i) = k)

Event: Disable at.

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

else zero endif

Event: Disable length.

;;;The nth entry in l is in the list i.

Definition: union-at-n (l, n, i) = (nth (l, n) ∈ i)

Event: Disable union-at-n.

;;;Any entry in l is in the list i.

Definition: all-union (l, n, i) = if n ≃ 0 then t

else union-at-n (l, n, i) ∧ all-union (l, n − 1, i) endif Event: Disable all-union.

;;;There exists an entry in l which belongs to
;;;the list i, moreover when exists, some such
;;;j is returned.

Definition: exist-union (l, n, i) = if n ≃ 0 then f

elseif union-at-n (l, n, i) then n else exist-union (l, n − 1, i) endif

Event: Disable exist-union.

;;;n is in the intersection of l8-12 and g34.

Definition: intersect-8-12-3-4-at-n (n, l, g) = (union-at-n (l, n, '(8 9 10 11 12)) ∧ union-at-n (g, n, '(3 4)))

Event: Disable intersect-8-12-3-4-at-n.

;;;There exists n in the intersection of l8-12 and g34.

Definition: exist-intersect-8-12-3-4 (n, l, g) = if n ≃ 0 then f

elseif intersect-8-12-3-4-at-n (n, l, g) then n else exist-intersect-8-12-3-4 (n − 1, l, g) endif

Event: Disable exist-intersect-8-12-3-4.

;*Flag invariant.

Definition: lg-1-at-n (n, l, g) = ((at (l, n, 0) ∧ at (g, n, 0))

∨ (at (l, n, 1) ∧ at (g, n, 0)) ∨ (at (l, n, 2) ∧ at (g, n, 0)) ∨ (at (l, n, 3) ∧ at (g, n, 1)) ∨ (at (l, n, 4) ∧ at (g, n, 1)))

Event: Disable lg-1-at-n.

Definition: lg-2-at-n (n, l, g) = ((at (l, n, 5) ∧ at (g, n, 3))

∨ (at (l, n, 6) ∧ at (g, n, 3)) ∨ (at (l, n, 7) ∧ at (g, n, 2)) ∨ (at (l, n, 8) ∧ at (g, n, 3)) ∨ (at (l, n, 8) ∧ at (g, n, 2)))

Event: Disable lg-2-at-n.

Definition: lg-3-at-n (n, l, g) = ((at (l, n, 9) ∧ at (g, n, 4))

∨ (at (l, n, 10) ∧ at (g, n, 4)) ∨ (at (l, n, 11) ∧ at (g, n, 4)) ∨ (at (l, n, 12) ∧ at (g, n, 4)))

Event: Disable lg-3-at-n.

Definition: lg-at-n (n, l, g) = (lg-1-at-n (n, l, g) ∧ lg-2-at-n (n, l, g) ∧ lg-3-at-n (n, l, g))

Event: Disable lg-at-n.

Definition: lg (n, l, g) = if n ≃ 0 then t

else lg-at-n (n, l, g) ∧ lg (n − 1, l, g) endif

Event: Disable lg.

;*The set {1...n}.

Definition: nset (n) = if n ≃ 0 then nil

else cons (n, nset (n − 1)) endif

Event: Disable nset.

;;;n belongs to nset.

Theorem: n-in-nset (n ≄ 0) → (n ∈ nset (n))

;;;Any element in nset is a number.

Theorem: nset-number (k ∈ nset (n)) → (k ∈ N)

;;;If a nonzero number plus one belongs to nset,
;;;then so does the nonzero number itself.

Theorem: add1-nset ((k ≄ 0) ∧ ((1 + k) ∈ nset (n))) → (k ∈ nset (n))

;;;Any list has its length at least nonzero.

Theorem: list-ln listp (l) → (length (l) ≠ 0)

;;;(move l k i) is again a list if l is a list.

Theorem: move-is-list listp (l) → listp (move (l, k, i)) Event: Enable length.

;;;(move l k i) has i as its kth entry.
;;;(enable length) is critical to prove this lemma.

Theorem: move-nth (listp (l) ∧ (k ∈ nset (length (l)))) → (nth (move (l, k, i), k) = i) Theorem: zero-not-member-nset 0 ∉ nset (n)

;;;Lists l and (move l k i) have the same length.

Theorem: move-unchange-length (listp (l) ∧ (k ∈ nset (length (l)))) → (length (move (l, k, i)) = length (l))

;;;Lists l and (move l k i) have the same entries
;;;except kth one.

Theorem: move-unchange-other-than-nth (listp (l) ∧ (k ∈ nset (length (l))) ∧ (j ≠ k)) → (nth (move (l, k, i), j ) = nth (l, j ))

Theorem: member-ex-union exist-union (l, n, i) → (exist-union (l, n, i) ∈ nset (n))

;;;(exist-union l n i) is a number.

Theorem: number-ex-union exist-union (l, n, i) → (exist-union (l, n, i) ∈ N)

;;;(exist-intersect-8-12-3-4 n l g) belongs to nset.

Theorem: member-intersect exist-intersect-8-12-3-4 (n, l, g) → (exist-intersect-8-12-3-4 (n, l, g) ∈ nset (n))

;;;(exist-intersect-8-12-3-4 n l g) is a number.

Theorem: number-intersect exist-intersect-8-12-3-4 (n, l, g) → (exist-intersect-8-12-3-4 (n, l, g) ∈ N)

;;;any member of nset is nonzero.

Theorem: k-not-0 (k ∈ nset (n)) → (k ≄ 0)

;*lemmas for a0
;;;If j's entry in l is between 8..12 then
;;;(exist-union l n '(8 9 10 11 12)) holds.

Theorem: j-ex-l8-12 ((j ∈ nset (n)) ∧ union-at-n (l, j , '(8 9 10 11 12))) → exist-union (l, n, '(8 9 10 11 12))

;;;Witness of (exist-union lp n '(8 9 10 11 12))
;;;has in lp its entry between 8...12.

Theorem: ex-lp8-12-in-lp8-12 exist-union (lp, n, '(8 9 10 11 12)) → union-at-n (lp,

exist-union (lp, n, '(8 9 10 11 12)),

              '(8 9 10 11 12))
;;;If (not (exist-union l n '(8 9 10 11 12)))
;;;holds, then (not (exist-union g n '(4))) by lg.

Theorem: ex-if4 ((¬ exist-union (l, n, '(8 9 10 11 12))) ∧ lg (n, l, g)) → (¬ exist-union (g, n, '(4)))

;;;If (not (exist-union g n '(1))) holds,
;;; then there is no entry either 3 or 4.

Theorem: l34-empty ((j ∈ nset (n)) ∧ lg (n, l, g) ∧ (¬ exist-union (g, n, '(1)))) → (¬ union-at-n (l, j , '(3 4)))

;;;If j's entry in lp is 4, then (certainly)
;;;it is either 3 or 4.

Theorem: lp4-then-un34 at (lp, j , 4) → union-at-n (lp, j , '(3 4))

;;;If (exist-intersect-8-12-3-4 n l g) holds,
;;;then so does (exist-union g n '(3 4)).

Theorem: int-8-12-3-4-then-un34 exist-intersect-8-12-3-4 (n, l, g) → exist-union (g, n, '(3 4))

;*lemmas for a1
;;;i is the witness of
;;;(exist-intersect-8-12-3-4 n lp gp).

Theorem: int-wtn ((j ∈ nset (n)) ∧ intersect-8-12-3-4-at-n (j , lp, gp)) → exist-intersect-8-12-3-4 (n, lp, gp)

;;;If there exists j such that j's entry in lp
;;;is between 8..12 and entry in gp is either 3 or 4
;;;then (intersect-8-12-3-4-at-n j lp gp) holds.

Theorem: un8-12-and-un34-then-int (union-at-n (lp, j , '(8 9 10 11 12)) ∧ union-at-n (gp, j , '(3 4))) → intersect-8-12-3-4-at-n (j , lp, gp)

;;;By the two lemmas above,
;;;(exist-intersect-8-12-3-4 n lp gp) holds provided
;;;that there exists j such that j's entry in lp is
;;;between 8..12 and entry in gp is either 3 or 4.
;* ep-l8-12
;;;If the k's entry in l is 5, then the k's entry
;;;in g is 3 by lg.

Theorem: lg-l5-g3 ((k ∈ nset (n)) ∧ lg (n, l, g) ∧ at (l, k, 5)) → at (g, k, 3)

;;;If the k's entry in gp is 3 then certainly
;;;it is either 3 or 4.

Theorem: gp3-then-un34 at (gp, k, 3) → union-at-n (gp, k, '(3 4))

;;;nep-l8-12
;;;If the k's entry in l is between 8..12 then
;;;it is either between 8..11 or equal to 12.

Theorem: case-k (union-at-n (l, k, '(8 9 10 11 12)) ∧ (¬ union-at-n (l, k, '(8 9 10 11)))) → at (l, k, 12)

;;;;;k-not-l8-12
;;;If (exist-intersect-8-12-3-4 n l g) holds
;;;then the witness has its entry in g either equal
;;;to 3 or 4.

Theorem: intersect-8-12-3-4-then-3-4 exist-intersect-8-12-3-4 (n, l, g) → union-at-n (g, exist-intersect-8-12-3-4 (n, l, g), '(3 4))

;;;If (exist-intersect-8-12-3-4 n l g) holds,
;;; then the witness has its entry in g between 8 and 12.

Theorem: intersect-8-12-3-4-then-8-12 exist-intersect-8-12-3-4 (n, l, g) → union-at-n (l, exist-intersect-8-12-3-4 (n, l, g), '(8 9 10 11 12))

;;;k-in-l8-11
;;;If k's entry in lp is between 9 and 12,
;;;then it is certainly between 8 and 12.

Theorem: un9-12-then-un8-12 union-at-n (lp, k, '(9 10 11 12)) → union-at-n (lp, k, '(8 9 10 11 12))

;;;If the i's entry in l is between 9 and 12,
;;;then the k's entry in g is 4.

Theorem: if4 ((j ∈ nset (n)) ∧ lg (n, l, g) ∧ union-at-n (l, j , '(9 10 11 12))) → at (g, j , 4)

;;;k-in-l12
;;;If (exist-union lp n '(8 9 10 11 12)) holds then
;;;its witness does not have its entry in lp equal to 1.

Theorem: ex-lp8-12-not-in-lp0 exist-union (lp, n, '(8 9 10 11 12)) → (¬ at (lp, exist-union (lp, n, '(8 9 10 11 12)), 0))

;;;If k's entry in lp is between 8 and 12,
;;; then it is either between 8 and 11 or 12.

Theorem: k-in-lp9-12-or-lp8 (union-at-n (lp, k, '(8 9 10 11 12)) ∧ (¬ union-at-n (lp, k, '(9 10 11 12)))) → at (lp, k, 8)

;;;If the k's entry is either 5 or 7,
;;;then it is between 5 and 7.

Theorem: un57-then-un5-12 union-at-n (l, k, '(5 7)) → union-at-n (l, k, '(5 6 7 8 9 10 11 12))

;;;If the k's entry in l is between 8 and 11,
;;;then it is between 5 and 12.

Theorem: un8-11-then-un5-12 union-at-n (l, k, '(8 9 10 11)) → union-at-n (l, k, '(5 6 7 8 9 10 11 12))

;;;If the k's entry in l is between 8 and 12,
;;;then it is between 5 and 12.

Theorem: un8-12-then-un5-12 union-at-n (l, k, '(8 9 10 11 12)) → union-at-n (l, k, '(5 6 7 8 9 10 11 12))

;*lemmas for a2
;;;i-eq-k-j-neq-k
;;;If the k's entry in l is either 10 or 11,
;;;then the k's entry in l is between 10 and 12.

Theorem: un10-11-then-un10-12 union-at-n (l, k, '(10 11)) → union-at-n (l, k, '(10 11 12))

;;;If the j's entry in g is either 0 or 1 then
;;;the j's entry in l is not between 5 and 12.

Theorem: if1 ((j ∈ nset (n)) ∧ lg (n, l, g) ∧ union-at-n (g, j , '(0 1))) → (¬ union-at-n (l, j , '(5 6 7 8 9 10 11 12)))

;;;j-eq-k-i-neq-k
;;;If the k's entry in l is between 5 and 7,
;;;then it is certainly between 5 and 12.

Theorem: un5-7-then-un5-11 union-at-n (l, k, '(5 6 7)) → union-at-n (l, k, '(5 6 7 8 9 10 11))

;;;If the k's entry in lp is between 5 and 7 then
;;;it is certain between 5 and 11.

Theorem: un57-then-un5-11 union-at-n (l, k, '(5 7)) → union-at-n (l, k, '(5 6 7 8 9 10 11))

;;;If the k's entry in l is between 8 and 11,
;;;then it is certainly between 5 and 11.

Theorem: un8-11-then-un5-11 union-at-n (l, k, '(8 9 10 11)) → union-at-n (l, k, '(5 6 7 8 9 10 11))

;;;If the k's entry in lp is between 5 and 12 and
;;;the k's entry in lp is between 5 and 7, then
;;;the k's entry in lp in fact is between 9 and 12.

Theorem: k-in-lp5-7-or-lp8-or-lp9-12 (union-at-n (lp, k, '(5 6 7 8 9 10 11 12)) ∧ (¬ union-at-n (lp, k, '(5 6 7))) ∧ (¬ at (lp, k, 8))) → union-at-n (lp, k, '(9 10 11 12))

;;;If the k's entry in l is between 5 and 11,
;;; then it is certainly between 5 and 12.

Theorem: un5-11-then-un5-12 union-at-n (l, k, '(5 6 7 8 9 10 11)) → union-at-n (l, k, '(5 6 7 8 9 10 11 12))

;;;If the k's entry in l is between 10 and 12,
;;; then it is certainly between 8 and 12.

Theorem: un10-12-then-un8-12 union-at-n (l, i, '(10 11 12)) → union-at-n (l, i, '(8 9 10 11 12))

;;;j-eq-k-i-neq-k
;;;If (exist-union l n '(8 9 10 11 12)) does not hold,
;;;then the i's entry in l is not between 10 and 12.

Theorem: i-not-l10-12 ((i ∈ nset (n)) ∧ (¬ exist-union (l, n, '(8 9 10 11 12)))) → (¬ union-at-n (l, i, '(10 11 12)))

;*lemmas for a3
;;;j-eq-k-i-neq-k
;;;If the k's entry in l is between 5 and 11,
;;;then the k's entry in l is between 9 and 11.

Theorem: un5-11-eq-un58-or-un8-11 (union-at-n (l, k, '(5 6 7 8 9 10 11)) ∧ (¬ union-at-n (l, k, '(5 6 7 8)))) → union-at-n (l, k, '(9 10 11))

;;;If the k's entry in g is 4,
;;;then the k's entry in l is between 5 and 8.

Theorem: a3-if4 ((k ∈ nset (n)) ∧ lg (n, l, g) ∧ at (g, k, 4)) → (¬ union-at-n (l, k, '(5 6 7 8)))

;;;If the k's entry in l is between 5 and 11,
;;;and the k's entry in l is between 5 and 12,
;;;then the k's entry in l is 9 and 11.

Theorem: k-in-l5-11-g4-then-l9-11 ((k ∈ nset (n)) ∧ lg (n, l, g) ∧ union-at-n (l, k, '(5 6 7 8 9 10 11)) ∧ at (g, k, 4)) → union-at-n (l, k, '(9 10 11))

; dropped second use hint -- rsb
;;;If the i's entry in l is 12,
;;;then the i's entry in l is between 8 and 12.

Theorem: l12-then-un8-12 at (l, i, 12) → union-at-n (l, i, '(8 9 10 11 12))

;;;If (exist-union l n '(8 9 10 11 12)) does not hold,
;;;then the i's entry in l is 12.

Theorem: i-not-in-l12 ((i ∈ nset (n)) ∧ (¬ exist-union (l, n, '(8 9 10 11 12)))) → (¬ at (l, i, 12))

;;;j-neq-k-i-eq-k
;;;If the k's entry in l is 11,
;;; then the k's entry in l is between 10 and 12.

Theorem: l11-then-un10-12 at (l, k, 11) → union-at-n (l, k, '(10 11 12))

;;;If the j's entry in g is either 2 or 3,
;;;then the j's entry in l is between 5 and 8 by lg.

Theorem: if3 ((j ∈ nset (n)) ∧ lg (n, l, g) ∧ (¬ union-at-n (g, j , '(2 3)))) → (¬ union-at-n (l, j , '(5 6 7 8)))

;;;If the j's entry in l is between 5 and 12 and
;;;the j's entry in l is between 5 and 8, then
;;;the j's entry in l is 9 and 12.

Theorem: l5-12-eq-l5-8-or-l9-12 (union-at-n (l, j , '(5 6 7 8 9 10 11 12)) ∧ (¬ union-at-n (l, j , '(5 6 7 8)))) → union-at-n (l, j , '(9 10 11 12))

;;;i-j-eq-k
;;;If the k's entry in lp is 12,
;;;then it is certainly between 5 and 12.

Theorem: l12-then-un9-12 at (lp, k, 12) → union-at-n (lp, k, '(9 10 11 12))

;*lemmas for b1a
;;;If the u's entry in g is 4,
;;;then the u's entry in l is between 8 and 12 by lg.

Theorem: b1a-if4 ((u ∈ nset (n)) ∧ lg (n, l, g) ∧ at (g, u, 4)) → union-at-n (l, u, '(8 9 10 11 12))

;*lemmas for b1b
;;;If the k's entry in lp is between 9 and 12,
;;;then the k's entry in gp is iether 3 or 4 by lg.

Theorem: lp9-12-then-k-in-g34 ((k ∈ nset (n)) ∧ union-at-n (lp, k, '(9 10 11 12)) ∧ lg (n, lp, gp)) → union-at-n (gp, k, '(3 4))

;;;If the k's entry in lp is between 8 and 12, and
;;;it is not 8, then it is certainly between 9 and 12.

Theorem: un8-12-then-l8-or-l9-12 (union-at-n (lp, k, '(8 9 10 11 12)) ∧ (¬ at (lp, k, 8))) → union-at-n (lp, k, '(9 10 11 12))

;;;;;;;;;;;;;;;;;;;;;;;;;; defn.ev ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;Well-formed-state.

Definition: ws (n, l, g) = ((n ∈ N)

∧ listp (l) ∧ listp (g) ∧ (length (l) = n) ∧ (length (g) = n)

    ∧ all-union (l, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ all-union (g, n, '(0 1 2 3 4)))

Event: Disable ws.

;;;Transitions.

Definition: rhoi0 (n, i, l, g, lp, gp) = (at (l, i, 0) ∧ (gp = g) ∧ (lp = move (l, i, 1)))

Definition: rhoi1a (n, i, l, g, lp, gp) = (at (l, i, 1) ∧ (gp = g) ∧ (lp = move (l, i, 2)))

Definition: rhoi1b (n, i, l, g, lp, gp) = (at (l, i, 1) ∧ (g = gp) ∧ (lp = l))

Definition: rhoi2 (n, i, l, g, lp, gp) = (at (l, i, 2) ∧ (lp = move (l, i, 3)) ∧ (gp = move (g, i, 1)))

Definition: rhoi3a (n, i, l, g, lp, gp) = (at (l, i, 3)

∧ (gp = g)

∧ (lp = move (l, i, 4))

∧ (¬ exist-union (g, n, '(3 4))))

Definition: rhoi3b (n, i, l, g, lp, gp) = (at (l, i, 3)

∧ (gp = g) ∧ (lp = l) ∧ exist-union (g, n, '(3 4)))

Definition: rhoi4 (n, i, l, g, lp, gp) = (at (l, i, 4) ∧ (gp = move (g, i, 3)) ∧ (lp = move (l, i, 5)))

Definition: rhoi5a (n, i, l, g, lp, gp) = (at (l, i, 5)

∧ (gp = g)

∧ exist-union (g, n, '(1)) ∧ (lp = move (l, i, 6)))

Definition: rhoi5b (n, i, l, g, lp, gp) = (at (l, i, 5)

∧ (gp = g)

∧ (¬ exist-union (g, n, '(1))) ∧ (lp = move (l, i, 8)))

Definition: rhoi6 (n, i, l, g, lp, gp) = (at (l, i, 6) ∧ (gp = move (g, i, 2)) ∧ (lp = move (l, i, 7)))

Definition: rhoi7a (n, i, l, g, lp, gp) = (at (l, i, 7)

∧ exist-union (g, n, '(4)) ∧ (lp = move (l, i, 8)) ∧ (gp = g))

Definition: rhoi7b (n, i, l, g, lp, gp) = (at (l, i, 7)

∧ (¬ exist-union (g, n, '(4)))

∧ (lp = l) ∧ (gp = g))

Definition: rhoi8 (n, i, l, g, lp, gp) = (at (l, i, 8) ∧ (gp = move (g, i, 4)) ∧ (lp = move (l, i, 9)))

Definition: phi9 (i, n, g) = if (g ≃ nil) ∨ (i ∉ N) ∨ (n ∉ N) then f

elseif n = 0 then t

else ((n ≮ i) ∧ phi9 (i, n − 1, g)) ∨ (union-at-n (g, n, '(0 1)) ∧ phi9 (i, n − 1, g)) endif

Event: Disable phi9.

Definition: rhoi9a (n, i, l, g, lp, gp) = (at (l, i, 9) ∧ (gp = g) ∧ phi9 (i, n, g) ∧ (lp = move (l, i, 10)))

Definition: rhoi9b (n, i, l, g, lp, gp) = (at (l, i, 9) ∧ (gp = g) ∧ (¬ phi9 (i, n, g)) ∧ (lp = l))

Definition: rhoi10 (n, i, l, g, lp, gp) = (at (l, i, 10) ∧ (lp = move (l, i, 11)) ∧ (gp = g))

Definition: phi11 (i, n, g) = if (g ≃ nil) ∨ (i ∉ N) ∨ (n ∉ N) then f

elseif n = 0 then t

else ((i ≮ n) ∧ phi11 (i, n − 1, g))

∨ ((¬ union-at-n (g, n, '(2 3))) ∧ phi11 (i, n − 1, g)) endif Event: Disable phi11.

Definition: rhoi11a (n, i, l, g, lp, gp) = (at (l, i, 11)

∧ (gp = g) ∧ phi11 (i, n, g) ∧ (lp = move (l, i, 12)))

Definition: rhoi11b (n, i, l, g, lp, gp) = (at (l, i, 11) ∧ (gp = g) ∧ (¬ phi11 (i, n, g)) ∧ (lp = l))

Definition: rhoi12 (n, i, l, g, lp, gp) = (at (l, i, 12) ∧ (gp = move (g, i, 0)) ∧ (lp = move (l, i, 0)))

;;;The transition operates on i'th.

Definition: rhoi (n, i, l, g, lp, gp) = (rhoi0 (n, i, l, g, lp, gp)

∨ rhoi1a (n, i, l, g, lp, gp) ∨ rhoi1b (n, i, l, g, lp, gp) ∨ rhoi2 (n, i, l, g, lp, gp) ∨ rhoi3a (n, i, l, g, lp, gp) ∨ rhoi3b (n, i, l, g, lp, gp) ∨ rhoi4 (n, i, l, g, lp, gp) ∨ rhoi5a (n, i, l, g, lp, gp) ∨ rhoi5b (n, i, l, g, lp, gp) ∨ rhoi6 (n, i, l, g, lp, gp) ∨ rhoi7a (n, i, l, g, lp, gp) ∨ rhoi7b (n, i, l, g, lp, gp) ∨ rhoi8 (n, i, l, g, lp, gp) ∨ rhoi9a (n, i, l, g, lp, gp) ∨ rhoi9b (n, i, l, g, lp, gp) ∨ rhoi10 (n, i, l, g, lp, gp) ∨ rhoi11a (n, i, l, g, lp, gp) ∨ rhoi11b (n, i, l, g, lp, gp) ∨ rhoi12 (n, i, l, g, lp, gp))

Event: Disable rhoi.

;;;  Propositions

;;;a0

Definition: a0 (n, l, k) = (((k ∈ nset (n)) ∧ exist-union (l, n, '(8 9 10 11 12)))

→ (¬ at (l, k, 4)))

Event: Disable a0.

;;;a1

Definition: a1 (n, l, g) = (exist-union (l, n, '(8 9 10 11 12))

→ exist-intersect-8-12-3-4 (n, l, g))

Event: Disable a1.

;;;; a2

Definition: a2-at-n1-n2 (n1 , n2 , l) = if union-at-n (l, n1 , '(10 11 12))

then ¬ union-at-n (l, n2 , '(5 6 7 8 9 10 11 12))

else t endif

Event: Disable a2-at-n1-n2.

Definition: a2-at-n2 (n1 , n2 , l) = if n2 ≃ 0 then t

elseif n2 ≮ n1 then a2-at-n2 (n1 , n2 − 1, l)

else a2-at-n1-n2 (n1 , n2 , l) ∧ a2-at-n2 (n1 , n2 − 1, l) endif

Event: Disable a2-at-n2.

Definition: a2 (n1 , n2 , l) = if n1 ≃ 0 then t

else a2-at-n2 (n1 , n2 , l) ∧ a2 (n1 − 1, n2 , l) endif Event: Disable a2.

;;;a3

Definition: a3-at-n1-n2 (n1 , n2 , l, g) = if at (l, n1 , 12) ∧ union-at-n (l, n2 , '(5 6 7 8 9 10 11 12))

then at (g, n2 , 4)

else t endif

Event: Disable a3-at-n1-n2.

Definition: a3-at-n2 (n1 , n2 , l, g) = if n2 ≃ 0 then t

else a3-at-n1-n2 (n1 , n2 , l, g) ∧ a3-at-n2 (n1 , n2 − 1, l, g) endif

Event: Disable a3-at-n2.

Definition: a3 (n1 , n2 , l, g) = if n1 ≃ 0 then t

else a3-at-n2 (n1 , n2 , l, g) ∧ a3 (n1 − 1, n2 , l, g) endif

Event: Disable a3.

;;;;;;;;;;;;;;;;;;;;;;;;;; basic.ev ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;ws implies that n is a number.

Theorem: ws-num-n ws (n, l, g) → (n ∈ N)

;;;ws implies that l is a list.

Theorem: ws-list-l ws (n, l, g) → listp (l)

;;;ws implies that g is a list.

Theorem: ws-list-g ws (n, l, g) → listp (g)

;;;ws implies that length of l is n.

Theorem: ws-ln-l ws (n, l, g) → (length (l) = n)

;;;ws implies that length of g is n.

Theorem: ws-ln-g ws (n, l, g) → (length (g) = n)

;;;ws and rho imply that lp is a list.

Theorem: ws-ln-lp (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp)) → listp (lp)

;;;ws and rho imply that gp is a list.

Theorem: ws-ln-gp (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp)) → listp (gp)

;;;ws implies that n is nonzero.

Theorem: ws-n-not-0 ws (n, l, g) → (n ≄ 0)

Theorem: n-not-0 ws (n, l, g) → (n ∈ nset (n))

;*the rho! lemmas
;;;Auxiliary lemma.

Theorem: lm-l-rholemma (listp (l) ∧ (j ∈ nset (length (l))) ∧ (k ∈ nset (length (l))) ∧ rhoi (n, k, l, g, lp, gp) ∧ (k ≠ j )) → (nth (l, j ) = nth (lp, j ))

Event: Disable lm-l-rholemma.

;;;Rholemma for list l.

Theorem: l-rholemma (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (k ≠ j )) → (nth (l, j ) = nth (lp, j ))

;;;Auxiliary lemma.

Theorem: lm-g-rholemma (listp (g) ∧ (j ∈ nset (length (g))) ∧ (k ∈ nset (length (g))) ∧ rhoi (n, k, l, g, lp, gp) ∧ (k ≠ j )) → (nth (g, j ) = nth (gp, j ))

Event: Disable lm-g-rholemma.

;;;Rholemma for list g.

Theorem: g-rholemma (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (k ≠ j )) → (nth (g, j ) = nth (gp, j ))

;;; lp-gp-same-l-g
;;;Another version of Rholemma for l.
;;;It applies to (union-at-n l j m) in stead of
;;;(nth l j).

Theorem: lp-same-l (ws (n, l, g) ∧ listp (m) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ union-at-n (l, j , m)) → union-at-n (lp, j , m)

;;;Contrast to the one above,
;;;the order of l and lp is reversed.

Theorem: l-same-lp (ws (n, l, g) ∧ listp (m) ∧ (j ∈ nset (n))

∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ union-at-n (lp, j , m)) → union-at-n (l, j , m)

Theorem: lp-same-l-not (ws (n, l, g) ∧ listp (m) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ (¬ union-at-n (l, j , m))) → (¬ union-at-n (lp, j , m))

;;;Another version of Rholemma for g.

Theorem: gp-same-g (ws (n, l, g) ∧ listp (m) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ union-at-n (g, j , m)) → union-at-n (gp, j , m)

;;;Contrast to the one above,
;;;the order of g and gp is reversed.

Theorem: g-same-gp (ws (n, l, g) ∧ listp (m) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ union-at-n (gp, j , m)) → union-at-n (g, j , m)

;;;It applies to (at l j m) in stead of
;;;(nth l j).

Theorem: l-same-lp-at (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ (m ∈ N) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ at (lp, j , m)) → at (l, j , m)

Theorem: gp-same-g-at (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ (m ∈ N) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ at (g, j , m)) → at (gp, j , m)

Theorem: l-same-lp-at-not (ws (n, l, g) ∧ (m ∈ N) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ (¬ at (l, j , m))) → (¬ at (lp, j , m))

;*basic properties of a2
;;;Auxiliary lemma.

Theorem: lm-a2-at-n2-a2-at-n1-n2 ((n ∈ N) ∧ (k ∈ N) ∧ (j ∈ nset (n)) ∧ (j < k) ∧ a2-at-n2 (k, n, l)) → a2-at-n1-n2 (k, j , l)

Event: Disable lm-a2-at-n2-a2-at-n1-n2.

Theorem: a2-at-n2-a2-at-n1-n2 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (j < k) ∧ a2-at-n2 (k, n, l)) → a2-at-n1-n2 (k, j , l)

Theorem: lm-a2-a2-at-n2 ((n ∈ N) ∧ (i ∈ N) ∧ (k ∈ nset (n)) ∧ a2 (n, i, l)) → a2-at-n2 (k, i, l)

Theorem: a2-a2-at-n2 (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ a2 (n, i, l)) → a2-at-n2 (k, i, l)

;*basic properties of a3

Theorem: lm-a3-at-n2-a3-at-n1-n2 ((n ∈ N) ∧ (u ∈ N) ∧ (j ∈ nset (n)) ∧ a3-at-n2 (u, n, l, g)) → a3-at-n1-n2 (u, j , l, g)

Event: Disable lm-a3-at-n2-a3-at-n1-n2.

Theorem: a3-at-n2-a3-at-n1-n2 (ws (n, l, g) ∧ (u ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ a3-at-n2 (u, n, l, g)) → a3-at-n1-n2 (u, j , l, g)

Theorem: lm-a3-a3-at-n2 ((n ∈ N) ∧ (i ∈ N) ∧ (u ∈ nset (n)) ∧ a3 (n, i, l, g)) → a3-at-n2 (u, i, l, g)

Event: Disable lm-a3-a3-at-n2.

Theorem: a3-a3-at-n2 (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (u ∈ nset (n)) ∧ a3 (n, i, l, g)) → a3-at-n2 (u, i, l, g)

;;;;;;;Instances used in the proofs of
;;;;;;;a1 a2 and a3.
;;;(a2 n n l) and (a3 n n l g) are involved
;;;in double bounded quantifiers
;;;\forall i \leq n \forall j \leq n,
;;;with their quantifier-free formulas
;;;(a3-at-n1-n2 i j l g) and (a2-at-n1-n2 i j l)
;;;respectively. What follows are all instances of
;;;the following type: If (a3 n n l g) holds, then
;;;in particular, so its instance
;;;(a3-at-n1-n2 i j l g) does.
;;;The instances are i and j.

Theorem: a3-i-j-a3-at-n1-n2 (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ a3 (n, n, l, g)) → a3-at-n1-n2 (i, j , l, g)

;;;The instances are k and
;;;(exist-union lp n '(8 9 10 11 12)).

Theorem: a3-ex-a3-at-n1-n2 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ a3 (n, n, l, g) ∧ exist-union (lp, n, '(8 9 10 11 12))) → a3-at-n1-n2 (k, exist-union (lp, n, '(8 9 10 11 12)), l, g)

Theorem: a2-n-a2-at-n2 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ a2 (n, n, l)) → a2-at-n2 (k, n, l)

;;;The instances are i and j.

Theorem: a2-i-j-a2-at-n1-n2 (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ a2 (n, n, l) ∧ (j < i)) → a2-at-n1-n2 (i, j , l)

;;;;;;;;;;;;;;;;;;;;;;;;;;; ws.ev ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Theorem: j-eq-k-move-member-g (listp (g) ∧ listp (m) ∧ (i ∈ m) ∧ (k ∈ nset (length (g)))) → (nth (move (g, k, i), k) ∈ m)

Theorem: j-neq-k-move-member-g (listp (g) ∧ listp (m) ∧ (k ∈ nset (length (g))) ∧ (j ≠ k) ∧ (i ∈ m) ∧ (nth (g, j ) ∈ m)) → (nth (move (g, k, i), j ) ∈ m)

Theorem: move-member-g (listp (g) ∧ listp (m) ∧ (i ∈ m)

∧ (k ∈ nset (length (g))) ∧ (nth (g, j ) ∈ m)) → (nth (move (g, k, i), j ) ∈ m)

Theorem: move-member-l (listp (l) ∧ listp (m) ∧ (j ∈ N) ∧ (i ∈ m) ∧ (k ∈ nset (length (l))) ∧ (nth (l, j ) ∈ m)) → (nth (move (l, k, i), j ) ∈ m)

Theorem: ws-union-g ws (n, l, g) → all-union (g, n, '(0 1 2 3 4))

Theorem: ws-union-l ws (n, l, g) → all-union (l, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho0-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi0 (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: rho1a-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi1a (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: rho1b-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi1b (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: lm-rho2-preserves-union-g (listp (g) ∧ (length (g) = n) ∧ (k ∈ nset (n)) ∧ all-union (g, j , '(0 1 2 3 4)) ∧ rhoi2 (n, k, l, g, lp, gp)) → all-union (gp, j , '(0 1 2 3 4))

Theorem: rho2-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi2 (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: rho3a-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi3a (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: rho3b-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi3b (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: lm-rho4-preserves-union-g (listp (g) ∧ (length (g) = n) ∧ (k ∈ nset (n)) ∧ all-union (g, j , '(0 1 2 3 4)) ∧ rhoi4 (n, k, l, g, lp, gp)) → all-union (gp, j , '(0 1 2 3 4))

Theorem: rho4-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi4 (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: rho5a-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi5a (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: rho5b-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi5b (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: lm-rho6-preserves-union-g (listp (g) ∧ (length (g) = n) ∧ (k ∈ nset (n)) ∧ all-union (g, j , '(0 1 2 3 4)) ∧ rhoi6 (n, k, l, g, lp, gp)) → all-union (gp, j , '(0 1 2 3 4))

Theorem: rho6-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi6 (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: rho7a-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi7a (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: rho7b-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi7b (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: lm-rho8-preserves-union-g (listp (g) ∧ (length (g) = n) ∧ (k ∈ nset (n)) ∧ all-union (g, j , '(0 1 2 3 4)) ∧ rhoi8 (n, k, l, g, lp, gp)) → all-union (gp, j , '(0 1 2 3 4))

Theorem: rho8-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi8 (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: rho9a-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi9a (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: rho9b-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi9b (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: lm-rho10-preserves-union-g (listp (g) ∧ (length (g) = n) ∧ (k ∈ nset (n)) ∧ all-union (g, j , '(0 1 2 3 4)) ∧ rhoi10 (n, k, l, g, lp, gp)) → all-union (gp, j , '(0 1 2 3 4))

Theorem: rho10-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi10 (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: rho11a-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi11a (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: rho11b-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi11b (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: lm-rho12-preserves-union-g (listp (g) ∧ (length (g) = n) ∧ (k ∈ nset (n)) ∧ all-union (g, j , '(0 1 2 3 4)) ∧ rhoi12 (n, k, l, g, lp, gp)) → all-union (gp, j , '(0 1 2 3 4))

Theorem: rho12-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi12 (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: rho-preserves-union-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp)) → all-union (gp, n, '(0 1 2 3 4))

Theorem: lm-rho0-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi0 (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho0-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi0 (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho1a-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi1a (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho1a-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi1a (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho1b-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi1b (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho1b-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi1b (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho2-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi2 (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho2-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi2 (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho3a-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi3a (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho3a-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi3a (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho3b-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi3b (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho3b-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi3b (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho4-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi4 (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho4-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi4 (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho5a-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi5a (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho5a-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi5a (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho5b-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi5b (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho5b-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi5b (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho6-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi6 (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho6-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi6 (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho7a-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi7a (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho7a-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi7a (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho7b-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi7b (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho7b-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi7b (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho8-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi8 (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho8-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi8 (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho9a-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi9a (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho9a-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi9a (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho9b-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi9b (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho9b-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi9b (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho10-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi10 (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho10-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi10 (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho11a-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi11a (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho11a-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi11a (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho11b-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi11b (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho11b-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi11b (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho12-preserves-union-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n))

 ∧ all-union (l, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ rhoi12 (n, k, l, g, lp, gp))

→ all-union (lp, j , '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho12-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi12 (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: rho-preserves-union-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp))

→ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

Theorem: lm-rho-preserves-ln-l (listp (l) ∧ (length (l) = n) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp)) → (length (lp) = n)

Theorem: rho-preserves-ln-l (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp)) → (length (lp) = n)

Theorem: lm-rho-preserves-ln-g (listp (g) ∧ (length (g) = n) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp)) → (length (gp) = n)

Theorem: rho-preserves-ln-g (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp)) → (length (gp) = n)

Theorem: lm-rho-preserves-ws ((n ∈ N) ∧ listp (lp) ∧ listp (gp) ∧ (length (lp) = n) ∧ (length (gp) = n)

 ∧ all-union (lp, n, '(0 1 2 3 4 5 6 7 8 9 10 11 12))

∧ all-union (gp, n, '(0 1 2 3 4))) → ws (n, lp, gp)

Theorem: rho-preserves-ws (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp)) → ws (n, lp, gp)

;;;;;;;;;;;;;;;;;;;;;;;;;;; lg.ev ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;rhoi0

Theorem: n-neq-k-rhoi0 (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ (k ≠ n) ∧ at (l, k, 0) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 1), g)

Event: Disable n-neq-k-rhoi0.

Theorem: n-eq-k-rhoi0 (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 0) ∧ lg-at-n (k, l, g)) → lg-at-n (k, move (l, k, 1), g)

Event: Disable n-eq-k-rhoi0.

Theorem: lg-at-rhoi0 (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 0) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 1), g)

Event: Disable lg-at-rhoi0.

Theorem: lg-rhoi0 (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ (n ∈ N) ∧ at (l, k, 0) ∧ lg (n, l, g)) → lg (n, move (l, k, 1), g)

Event: Disable lg-rhoi0.

Theorem: rhoi0-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi0 (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi1a

Theorem: n-neq-k-rhoi1a (listp (l) ∧ listp (g)

∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ (k ≠ n) ∧ at (l, k, 1) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 2), g)

Event: Disable n-neq-k-rhoi1a.

Theorem: n-eq-k-rhoi1a (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 1) ∧ lg-at-n (k, l, g)) → lg-at-n (n, move (l, k, 2), g)

Event: Disable n-eq-k-rhoi1a.

Theorem: lg-at-rhoi1a (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 1) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 2), g)

Event: Disable lg-at-rhoi1a.

Theorem: lg-rhoi1a (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ (n ∈ N) ∧ at (l, k, 1) ∧ lg (n, l, g)) → lg (n, move (l, k, 2), g)

Event: Disable lg-rhoi1a.

Theorem: rhoi1a-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi1a (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi1b

Theorem: rhoi1b-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi1b (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi2

Theorem: n-neq-k-rhoi2 (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ (k ≠ n) ∧ at (l, k, 2) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 3), move (g, k, 1))

Event: Disable n-neq-k-rhoi2.

Theorem: n-eq-k-rhoi2 (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 2) ∧ lg-at-n (k, l, g)) → lg-at-n (n, move (l, k, 3), move (g, k, 1))

Event: Disable n-eq-k-rhoi2.

Theorem: lg-at-rhoi2 (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 2) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 3), move (g, k, 1))

Event: Disable lg-at-rhoi2.

Theorem: lg-rhoi2 (listp (l) ∧ listp (g)

∧ (k ∈ nset (length (l))) ∧ (n ∈ N) ∧ at (l, k, 2) ∧ lg (n, l, g)) → lg (n, move (l, k, 3), move (g, k, 1))

Event: Disable lg-rhoi2.

Theorem: rhoi2-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi2 (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi3a

Theorem: n-neq-k-rhoi3a (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ (k ≠ n) ∧ at (l, k, 3) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 4), g)

Event: Disable n-neq-k-rhoi3a.

Theorem: n-eq-k-rhoi3a (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 3) ∧ lg-at-n (k, l, g)) → lg-at-n (k, move (l, k, 4), g)

Event: Disable n-eq-k-rhoi3a.

Theorem: lg-at-rhoi3a (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 3) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 4), g)

Event: Disable lg-at-rhoi3a.

Theorem: lg-rhoi3a (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ (n ∈ N) ∧ at (l, k, 3) ∧ lg (n, l, g)) → lg (n, move (l, k, 4), g)

Event: Disable lg-rhoi3a.

Theorem: rhoi3a-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi3a (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi3b

Theorem: rhoi3b-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi3b (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi4

Theorem: n-neq-k-rhoi4 (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ (k ≠ n) ∧ at (l, k, 4) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 5), move (g, k, 3))

Event: Disable n-neq-k-rhoi4.

Theorem: n-eq-k-rhoi4 (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 4) ∧ lg-at-n (k, l, g)) → lg-at-n (n, move (l, k, 5), move (g, k, 3))

Event: Disable n-eq-k-rhoi4.

Theorem: lg-at-rhoi4 (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 4) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 5), move (g, k, 3))

Event: Disable lg-at-rhoi4.

Theorem: lg-rhoi4 (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ (n ∈ N) ∧ at (l, k, 4) ∧ lg (n, l, g)) → lg (n, move (l, k, 5), move (g, k, 3))

Event: Disable lg-rhoi4.

Theorem: rhoi4-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi4 (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi5a

Theorem: n-neq-k-rhoi5a (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ (k ≠ n) ∧ at (l, k, 5) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 6), g)

Event: Disable n-neq-k-rhoi5a.

Theorem: n-eq-k-rhoi5a (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 5) ∧ lg-at-n (k, l, g)) → lg-at-n (k, move (l, k, 6), g)

Event: Disable n-eq-k-rhoi5a.

Theorem: lg-at-rhoi5a (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 5) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 6), g)

Event: Disable lg-at-rhoi5a.

Theorem: lg-rhoi5a (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ (n ∈ N) ∧ at (l, k, 5) ∧ lg (n, l, g)) → lg (n, move (l, k, 6), g)

Event: Disable lg-rhoi5a.

Theorem: rhoi5a-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi5a (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi5b

Theorem: n-neq-k-rhoi5b (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ (k ≠ n)

∧ at (l, k, 5) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 8), g)

Event: Disable n-neq-k-rhoi5b.

Theorem: n-eq-k-rhoi5b (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 5) ∧ lg-at-n (k, l, g)) → lg-at-n (k, move (l, k, 8), g)

Event: Disable n-eq-k-rhoi5b.

Theorem: lg-at-rhoi5b (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 5) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 8), g)

Event: Disable lg-at-rhoi5b.

Theorem: lg-rhoi5b (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ (n ∈ N) ∧ at (l, k, 5) ∧ lg (n, l, g)) → lg (n, move (l, k, 8), g)

Event: Disable lg-rhoi5b.

Theorem: rhoi5b-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi5b (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi6

Theorem: n-neq-k-rhoi6 (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ (k ≠ n) ∧ at (l, k, 6) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 7), move (g, k, 2))

Event: Disable n-neq-k-rhoi6.

Theorem: n-eq-k-rhoi6 (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 6) ∧ lg-at-n (k, l, g)) → lg-at-n (n, move (l, k, 7), move (g, k, 2))

Event: Disable n-eq-k-rhoi6.

Theorem: lg-at-rhoi6 (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 6) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 7), move (g, k, 2))

Event: Disable lg-at-rhoi6.

Theorem: lg-rhoi6 (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ (n ∈ N) ∧ at (l, k, 6) ∧ lg (n, l, g)) → lg (n, move (l, k, 7), move (g, k, 2))

Event: Disable lg-rhoi6.

Theorem: rhoi6-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi6 (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi7a

Theorem: n-neq-k-rhoi7a (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ (k ≠ n) ∧ at (l, k, 7) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 8), g)

Event: Disable n-neq-k-rhoi7a.

Theorem: n-eq-k-rhoi7a (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 7) ∧ lg-at-n (k, l, g)) → lg-at-n (k, move (l, k, 8), g)

Event: Disable n-eq-k-rhoi7a.

Theorem: lg-at-rhoi7a (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 7) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 8), g)

Event: Disable lg-at-rhoi7a.

Theorem: lg-rhoi7a (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l)))

∧ (n ∈ N) ∧ at (l, k, 7) ∧ lg (n, l, g)) → lg (n, move (l, k, 8), g)

Event: Disable lg-rhoi7a.

Theorem: rhoi7a-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi7a (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi7b

Theorem: rhoi7b-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi7b (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi8

Theorem: n-neq-k-rhoi8 (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ (k ≠ n) ∧ at (l, k, 8) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 9), move (g, k, 4))

Event: Disable n-neq-k-rhoi8.

Theorem: n-eq-k-rhoi8 (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 8) ∧ lg-at-n (k, l, g)) → lg-at-n (n, move (l, k, 9), move (g, k, 4))

Event: Disable n-eq-k-rhoi8.

Theorem: lg-at-rhoi8 (listp (l) ∧ listp (g)

∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 8) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 9), move (g, k, 4))

Event: Disable lg-at-rhoi8.

Theorem: lg-rhoi8 (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ (n ∈ N) ∧ at (l, k, 8) ∧ lg (n, l, g)) → lg (n, move (l, k, 9), move (g, k, 4))

Event: Disable lg-rhoi8.

Theorem: rhoi8-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi8 (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi9a

Theorem: n-neq-k-rhoi9a (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ (k ≠ n) ∧ at (l, k, 9) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 10), g)

Event: Disable n-neq-k-rhoi9a.

Theorem: n-eq-k-rhoi9a (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 9) ∧ lg-at-n (k, l, g)) → lg-at-n (k, move (l, k, 10), g)

Event: Disable n-eq-k-rhoi9a.

Theorem: lg-at-rhoi9a (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 9) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 10), g)

Event: Disable lg-at-rhoi9a.

Theorem: lg-rhoi9a (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ (n ∈ N) ∧ at (l, k, 9) ∧ lg (n, l, g)) → lg (n, move (l, k, 10), g)

Event: Disable lg-rhoi9a.

Theorem: rhoi9a-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi9a (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi9b

Theorem: rhoi9b-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi9b (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi10

Theorem: n-neq-k-rhoi10 (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ (k ≠ n) ∧ at (l, k, 10) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 11), g)

Event: Disable n-neq-k-rhoi10.

Theorem: n-eq-k-rhoi10 (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 10) ∧ lg-at-n (k, l, g)) → lg-at-n (k, move (l, k, 11), g)

Event: Disable n-eq-k-rhoi10.

Theorem: lg-at-rhoi10 (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 10) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 11), g)

Event: Disable lg-at-rhoi10.

Theorem: lg-rhoi10 (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ (n ∈ N) ∧ at (l, k, 10) ∧ lg (n, l, g)) → lg (n, move (l, k, 11), g)

Event: Disable lg-rhoi10.

Theorem: rhoi10-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi10 (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi11a

Theorem: n-neq-k-rhoi11a (listp (l) ∧ listp (g)

∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ (k ≠ n) ∧ at (l, k, 11) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 12), g)

Event: Disable n-neq-k-rhoi11a.

Theorem: n-eq-k-rhoi11a (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 11) ∧ lg-at-n (k, l, g)) → lg-at-n (k, move (l, k, 12), g)

Event: Disable n-eq-k-rhoi11a.

Theorem: lg-at-rhoi11a (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 11) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 12), g)

Event: Disable lg-at-rhoi11a.

Theorem: lg-rhoi11a (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ (n ∈ N) ∧ at (l, k, 11) ∧ lg (n, l, g)) → lg (n, move (l, k, 12), g)

Event: Disable lg-rhoi11a.

Theorem: rhoi11a-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi11a (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

Theorem: rhoi11b-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi11b (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;rhoi12

Theorem: n-neq-k-rhoi12 (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ (k ≠ n) ∧ at (l, k, 12) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 0), move (g, k, 0))

Event: Disable n-neq-k-rhoi12.

Theorem: n-eq-k-rhoi12 (listp (l) ∧ listp (g) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 12) ∧ lg-at-n (k, l, g)) → lg-at-n (n, move (l, k, 0), move (g, k, 0))

Event: Disable n-eq-k-rhoi12.

Theorem: lg-at-rhoi12 (listp (l) ∧ listp (g) ∧ (n ∈ N) ∧ (k ∈ nset (length (l))) ∧ at (l, k, 12) ∧ lg-at-n (n, l, g)) → lg-at-n (n, move (l, k, 0), move (g, k, 0))

Event: Disable lg-at-rhoi12.

Theorem: lg-rhoi12 (listp (l) ∧ listp (g)

∧ (k ∈ nset (length (l))) ∧ (n ∈ N) ∧ at (l, k, 12) ∧ lg (n, l, g)) → lg (n, move (l, k, 0), move (g, k, 0)) Event: Disable lg-rhoi12. Theorem: rhoi12-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi12 (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp) Theorem: rho-preserves-lg (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g)) → lg (n, lp, gp) Event: Disable rhoi0-preserves-lg. Event: Disable rhoi1a-preserves-lg. Event: Disable rhoi1b-preserves-lg. Event: Disable rhoi2-preserves-lg. Event: Disable rhoi3a-preserves-lg. Event: Disable rhoi3b-preserves-lg. Event: Disable rhoi4-preserves-lg. Event: Disable rhoi5a-preserves-lg. Event: Disable rhoi5b-preserves-lg. Event: Disable rhoi6-preserves-lg. Event: Disable rhoi7a-preserves-lg. Event: Disable rhoi7b-preserves-lg.

Event: Disable rhoi8-preserves-lg.

Event: Disable rhoi9a-preserves-lg.

Event: Disable rhoi9b-preserves-lg.

Event: Disable rhoi10-preserves-lg.

Event: Disable rhoi11a-preserves-lg.

Event: Disable rhoi11b-preserves-lg.

Event: Disable rhoi12-preserves-lg.

;;;;;;;;;;;;;;;;;;;;;;;;;;; a0.ev ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;(exist-union lp n '(8 9 10 11 12))  and
;;;(not (exist-union l n '(8 9 10 11 12)))
;;;implies that k is the witness of
;;;(exist-union lp n '(8 9 10 11 12)). This
;;;proposition would have been more natural
;;;if we had been able to prove:
;;;(prove-lemma exist-l8-12 (rewrite)
;;;   (implies (and (ws n l g)
;;;                 (member k (nset n))
;;;                 (rhoi n k l g lp gp)
;;;                 (exist-union lp n '(8 9 10 11 12))
;;;                 (not (exist-union l n '(8 9 10 11 12))))
;;;            (equal k (exist-union lp n '(8 9 10 11 12))))).
;;;However Bmp refused to rewrite equal clause.

Theorem: exist-l8-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ exist-union (lp, n, '(8 9 10 11 12)) ∧ (k ≠ exist-union (lp, n, '(8 9 10 11 12)))) → exist-union (l, n, '(8 9 10 11 12))

;;;If (exist-union lp n '(8 9 10 11 12)) and
;;;(not (exist-union l n '(8 9 10 11 12))) hold,

;;;then the k's entry of lp is between 8..12.

Theorem: k-in-lp8-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ exist-union (lp, n, '(8 9 10 11 12)) ∧ (¬ exist-union (l, n, '(8 9 10 11 12)))) → union-at-n (lp, k, '(8 9 10 11 12))

;;;If k's entry in lp is between 8..12 and
;;;k's entry of l is not between 8..12,
;;;then k's entry of l is either 5 or 7.

Theorem: k-not-in-l8-12-then-l57 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ union-at-n (lp, k, '(8 9 10 11 12)) ∧ (¬ union-at-n (l, k, '(8 9 10 11 12))) ∧ (¬ at (l, k, 7))) → at (l, k, 5)

;;;If k's entry in lp is between 8..12 and
;;;(not (exist-union l n '(8 9 10 11 12))) holds,
;;;then k's entry of l is either 5 or 7.

Theorem: k-in-l57 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ union-at-n (lp, k, '(8 9 10 11 12)) ∧ (¬ exist-union (l, n, '(8 9 10 11 12))) ∧ (¬ at (l, k, 7))) → at (l, k, 5)

;;;If (exist-union lp n '(8 9 10 11 12)) and
;;;(not (exist-union l n '(8 9 10 11 12))) hold,
;;;then the k's entry of l is between either 5 or 7.

Theorem: ex-k-in-l57 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ exist-union (lp, n, '(8 9 10 11 12))

∧ (¬ exist-union (l, n, '(8 9 10 11 12))) ∧ (¬ at (l, k, 7))) → at (l, k, 5)

;;;Auxiliary lemma for ex-cond-rhoi5.

Theorem: cond-rhoi5 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ union-at-n (lp, k, '(8 9 10 11 12)) ∧ at (l, k, 5)) → (¬ exist-union (g, n, '(1)))

;;;If (exist-union lp n '(8 9 10 11 12)) and
;;;(not (exist-union l n '(8 9 10 11 12))) and
;;;the k's entry in l is 5 then
;;;(not (exist-union g n '(1))) holds.

Theorem: ex-cond-rhoi5 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ exist-union (lp, n, '(8 9 10 11 12)) ∧ (¬ exist-union (l, n, '(8 9 10 11 12))) ∧ at (l, k, 5)) → (¬ exist-union (g, n, '(1)))

;;;Auxiliary lemma for ex-cond-rhoi7.

Theorem: cond-rhoi7 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ union-at-n (lp, k, '(8 9 10 11 12)) ∧ at (l, k, 7)) → exist-union (g, n, '(4))

;;;If (exist-union lp n '(8 9 10 11 12)) and
;;;(not (exist-union l n '(8 9 10 11 12))) and
;;;the k's entry in l is 7, then
;;;(exist-union g n '(4)) holds.

Theorem: ex-cond-rhoi7 (ws (n, l, g)

∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ exist-union (lp, n, '(8 9 10 11 12)) ∧ (¬ exist-union (l, n, '(8 9 10 11 12))) ∧ at (l, k, 7)) → exist-union (g, n, '(4))

;;;If (exist-union lp n '(8 9 10 11 12))
;;;and (not (exist-union l n '(8 9 10 11 12))),
;;;then (not (exist-union g n '(1))) holds.

Theorem: l5-only-lp8 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (¬ exist-union (l, n, '(8 9 10 11 12))) ∧ lg (n, l, g) ∧ exist-union (lp, n, '(8 9 10 11 12))) → (¬ exist-union (g, n, '(1)))

;;;If j is not equal to k and j's entry of l
;;;is neither 3 or 4, then j's entry of lp
;;;is not 4.

Theorem: j-neq-k-j-not-in-lp4 (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ (¬ union-at-n (l, j , '(3 4)))) → (¬ at (lp, j , 4))

;;;If k's entry of l is neither 3 or 4, then
;;;k's entry of lp is not 4.

Theorem: j-eq-k-j-not-in-lp4 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (¬ union-at-n (l, k, '(3 4)))) → (¬ at (lp, k, 4))

;;;If j's entry of l is neither 3 or 4, then
;;;j's entry of lp is not 4.

Theorem: lp4-empty (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (¬ union-at-n (l, j , '(3 4)))) → (¬ at (lp, j , 4))

;;;If (not (exist-union l n '(8 9 10 11 12)))
;;; and (exist-union lp n '(8 9 10 11 12)) hold,
;;;then there is no entry 4 in l.

Theorem: l8-l12-empty (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (¬ exist-union (l, n, '(8 9 10 11 12))) ∧ lg (n, l, g)) → a0 (n, lp, j )

;;;If (exist-union g n '(3 4)) holds and
;;;the k's entry in l is not 4, then
;;;the k's entry in lp is not 4 either.
;;;(Doorway is locked.)

Theorem: dwy-lckd (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ exist-union (g, n, '(3 4)) ∧ (¬ at (l, k, 4))) → (¬ at (lp, k, 4))

;;;If (exist-union l n '(8 9 10 11 12))
;;;holds and j is equal to k, then
;;;j's entry in lp is not 4.

Theorem: j-eq-k-l8-l12-nonemp (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ exist-union (l, n, '(8 9 10 11 12)) ∧ a0 (n, l, k) ∧ a1 (n, l, g)) → a0 (n, lp, k)

;;;If (exist-union l n '(8 9 10 11 12))
;;; holds and j is not equal to k, then
;;;the j's entry in lp is not 4.

Theorem: j-neq-k-l8-l12-nonemp (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ a0 (n, l, j ) ∧ exist-union (l, n, '(8 9 10 11 12))) → a0 (n, lp, j )

;;;If (exist-union l n '(8 9 10 11 12))
;;;holds then there is no entry 4 in lp.
;;;The order of the use hints is critical.
;;;Change the order and we fail.

Theorem: l8-l12-nonemp (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ exist-union (l, n, '(8 9 10 11 12)) ∧ a0 (n, l, j ) ∧ a1 (n, l, g)) → a0 (n, lp, j )

;;;If (exist-union lp n '(8 9 10 11 12))
;;;holds, then there is no entry 4 in lp.

Theorem: rho-preserves-a0 (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ a0 (n, l, j ) ∧ a1 (n, l, g)) → a0 (n, lp, j )

;;;;;;;;;;;;;;;;;;;;;;;;;;; a1.ev ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;* ep-l8-12
;;;Auxiliary lemma for at-gp-rhoi5

Theorem: gp-rhoi5 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ union-at-n (lp, k, '(8 9 10 11 12)) ∧ at (l, k, 5) ∧ at (g, k, 3)) → at (gp, k, 3)

;;;If (not (exist-union l n '(8 9 10 11 12))),
;;;(exist-union lp n '(8 9 10 11 12)) and the k's
;;;entry in l is 5 then the k's entry in gp is 3.

Theorem: ex-gp-rhoi5 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ (¬ exist-union (l, n, '(8 9 10 11 12))) ∧ exist-union (lp, n, '(8 9 10 11 12)) ∧ at (l, k, 5)) → at (gp, k, 3)

;;;If (not (exist-union l n '(8 9 10 11 12)))
;;;and (exist-union lp n '(8 9 10 11 12)) holds,
;;;then the k's entry is either 3 or 4.

Theorem: k-in-gp34 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ (¬ exist-union (l, n, '(8 9 10 11 12))) ∧ exist-union (lp, n, '(8 9 10 11 12))) → union-at-n (gp, k, '(3 4))

;;;If (exist-union lp n '(8 9 10 11 12)) and
;;;(not (exist-union l n '(8 9 10 11 12))) holds,
;;;then so does (exist-intersect-8-12-3-4 n lp gp).

Theorem: lm-a1-ep-l8-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ exist-union (lp, n, '(8 9 10 11 12))

∧ (¬ exist-union (l, n, '(8 9 10 11 12))) ∧ lg (n, l, g)) → exist-intersect-8-12-3-4 (n, lp, gp)

;;;If (not (exist-union l n '(8 9 10 11 12))) holds,
;;;then so does a1.

Theorem: a1-ep-l8-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ (¬ exist-union (l, n, '(8 9 10 11 12)))) → a1 (n, lp, gp)

;* nep-l8-12
;;;If (exist-intersect-8-12-3-4 n l g) holds and
;;;k is not its witness then
;;;(exist-intersect-8-12-3-4 n lp gp) holds.

Theorem: int-k-not-ex-int (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (k ≠ exist-intersect-8-12-3-4 (n, l, g)) ∧ exist-intersect-8-12-3-4 (n, l, g)) → exist-intersect-8-12-3-4 (n, lp, gp)

;;;If (exist-union l n '(8 9 10 11 12)) holds and
;;;k's enrty is not between 8 and 12 then
;;;(exist-intersect-8-12-3-4 n lp gp) holds.
;;; j \neq k

Theorem: a1-k-not-in-l8-12-nep-l8-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ exist-union (l, n, '(8 9 10 11 12)) ∧ (¬ union-at-n (l, k, '(8 9 10 11 12))) ∧ a1 (n, l, g)) → exist-intersect-8-12-3-4 (n, lp, gp)

;* k-in-l8-11
;;;If the k's entry in l is between 8 and 11,
;;;then the k's entry in lp is between 9 and 12.
;;;We need rho-preserves-lg.

Theorem: l8-11-k-in-lp9-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ union-at-n (l, k, '(8 9 10 11))) → union-at-n (lp, k, '(9 10 11 12))

;;;If the k's entry in l is between 8 and 11,
;;;then the k's entry in lp is between 8 and 12
;;;and the entry in gp is either 3 or 4.
;;;l8-11-k-in-lp9-12, un9-12-then-un8-12 and
;;;rho-preserves-lg are used.

Theorem: lm-a1-k-in-l8-11-nep-l8-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ union-at-n (l, k, '(8 9 10 11)) ∧ lg (n, l, g)) → (union-at-n (lp, k, '(8 9 10 11 12)) ∧ union-at-n (gp, k, '(3 4)))

;;;If (exist-union lp n '(8 9 10 11 12)) holds,
;;;and the k's entry in l is between 8 and 11 then
;;;(exist-intersect-8-12-3-4 n lp gp) holds.
;;; j \eq k and k \in l8-11

Theorem: a1-k-in-l8-11-nep-l8-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ exist-union (lp, n, '(8 9 10 11 12)) ∧ union-at-n (l, k, '(8 9 10 11))) → exist-intersect-8-12-3-4 (n, lp, gp)

;;;If the k's entry in l is 12 then the k's entry in l is 0.

Theorem: k-in-lp0 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ at (l, k, 12)) → at (lp, k, 0)

;;;If (exist-union lp n '(8 9 10 11 12)) holds
;;;and k's entry in l is 12, then k is not the
;;;witness of (exist-union lp n '(8 9 10 11 12)).

Theorem: k-not-ex-lp8-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ exist-union (lp, n, '(8 9 10 11 12)) ∧ at (l, k, 12)) → (k ≠ exist-union (lp, n, '(8 9 10 11 12)))

;;;If the k's entry in lp is 8,
;;;then k's entry in l is either 5 or 7.

Theorem: lp8-k-in-l57 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ at (lp, k, 8)) → union-at-n (l, k, '(5 7))

;;;If the k's entry in lp is 8,
;;;then k's entry in l is between 5 and 12.

Theorem: k-in-lp8-then-l5-12 (ws (n, l, g) ∧ rhoi (n, k, l, g, lp, gp) ∧ (k ∈ nset (n)) ∧ at (lp, k, 8)) → union-at-n (l, k, '(5 6 7 8 9 10 11 12))

;;;If the k's entry in lp is between 9 and 12,
;;;then  the k's entry in l is between 8 and 11.

Theorem: lp9-12-k-in-l8-11 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ union-at-n (lp, k, '(9 10 11 12))) → union-at-n (l, k, '(8 9 10 11))

;;;If the k's entry in lp is between 9 and 12,
;;;then the k's entry in l is between 5 and 12.

Theorem: k-in-lp9-12-then-l5-12 (ws (n, l, g) ∧ rhoi (n, k, l, g, lp, gp) ∧ (k ∈ nset (n)) ∧ union-at-n (lp, k, '(9 10 11 12))) → union-at-n (l, k, '(5 6 7 8 9 10 11 12))

;;;If the k's entry in lp is between 8 and 12,
;;;then the k's entry in l is between 5 and 12.

Theorem: k-in-l5-12 (ws (n, l, g) ∧ rhoi (n, k, l, g, lp, gp) ∧ (k ∈ nset (n)) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → union-at-n (l, k, '(5 6 7 8 9 10 11 12))

;;;If (exist-union lp n '(8 9 10 11 12)) holds
;;;and k is not its witness, then the witness has
;;;its entry in l between 5 and 12.
;;;ex-lp8-12-in-lp8-12, member-ex-union used.

Theorem: k-neq-ex-lp8-12-in-l5-12 (ws (n, l, g) ∧ rhoi (n, k, l, g, lp, gp) ∧ (k ∈ nset (n)) ∧ exist-union (lp, n, '(8 9 10 11 12)) ∧ (k ≠ exist-union (lp, n, '(8 9 10 11 12)))) → union-at-n (l,

exist-union (lp, n, '(8 9 10 11 12)),

              '(5 6 7 8 9 10 11 12))
;;;If (exist-union lp n '(8 9 10 11 12)) holds and
;;;the witness has its entry in lp between 8 and 12,
;;;then its entry in l is between 5 and 12.
;;;ex-lp8-12-in-lp8-12, member-ex-union used.

Theorem: ex-lp8-12-then-l5-12 (ws (n, l, g) ∧ rhoi (n, k, l, g, lp, gp) ∧ (k ∈ nset (n)) ∧ exist-union (lp, n, '(8 9 10 11 12))) → union-at-n (l,

exist-union (lp, n, '(8 9 10 11 12)),

              '(5 6 7 8 9 10 11 12))
;;;If (exist-union lp n '(8 9 10 11 12)) holds
;;;and k is not the witness of
;;;(exist-union lp n '(8 9 10 11 12)), then
;;;the witness has its entry 4 in gp.

Theorem: ex-lp8-12-in-gp4 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp)

∧ at (l, k, 12) ∧ a3-at-n1-n2 (k, exist-union (lp, n, '(8 9 10 11 12)), l, g) ∧ (k ≠ exist-union (lp, n, '(8 9 10 11 12))) ∧ exist-union (lp, n, '(8 9 10 11 12))) → at (gp, exist-union (lp, n, '(8 9 10 11 12)), 4)

;;;If (exist-union lp n '(8 9 10 11 12)) holds and
;;;k's entry in l is 12 then the witness has its
;;;entry in lp between 8 and 12 and in gp either 3 or 4.

Theorem: lm-a1-k-in-l12-nep-l8-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ exist-union (lp, n, '(8 9 10 11 12)) ∧ at (l, k, 12) ∧ a3-at-n1-n2 (k, exist-union (lp, n, '(8 9 10 11 12)), l, g)) → union-at-n (gp, exist-union (lp, n, '(8 9 10 11 12)), '(3 4))

;;;If (exist-union lp n '(8 9 10 11 12)) holds
;;;and k's entry in l is 12, then
;;;(exist-intersect-8-12-3-4 n lp gp) holds.

Theorem: a1-k-in-l12-nep-l8-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ exist-union (lp, n, '(8 9 10 11 12)) ∧ at (l, k, 12) ∧ a3-at-n1-n2 (k, exist-union (lp, n, '(8 9 10 11 12)), l, g)) → exist-intersect-8-12-3-4 (n, lp, gp)

;;;Auxiliary lemma for a1-nep-l8-12.
;;;We have an instance of a3 in the lemma.

Theorem: lm1-a1-nep-l8-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ a1 (n, l, g) ∧ a3-at-n1-n2 (k, exist-union (lp, n, '(8 9 10 11 12)), l, g) ∧ exist-union (lp, n, '(8 9 10 11 12)) ∧ exist-union (l, n, '(8 9 10 11 12))) → exist-intersect-8-12-3-4 (n, lp, gp)

Theorem: lm-a1-nep-l8-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ a1 (n, l, g) ∧ a3 (n, n, l, g) ∧ exist-union (l, n, '(8 9 10 11 12)) ∧ exist-union (lp, n, '(8 9 10 11 12))) → exist-intersect-8-12-3-4 (n, lp, gp)

;;;If (exist-union lp n '(8 9 10 11 12)) and
;;;(exist-union l n '(8 9 10 11 12)) hold,
;;;then so does (exist-intersect-8-12-3-4 n lp gp).

Theorem: a1-nep-l8-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ a1 (n, l, g) ∧ a3 (n, n, l, g) ∧ exist-union (l, n, '(8 9 10 11 12))) → a1 (n, lp, gp)

;;;If (exist-union lp n '(8 9 10 11 12)) holds,
;;;then so does (exist-intersect-8-12-3-4 n lp gp).

Theorem: rho-preserves-a1 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ a1 (n, l, g) ∧ a3 (n, n, l, g)) → a1 (n, lp, gp)

;;;;;;;;;;;;;;;;;;;;;;;;;;; a2.ev ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;* i-eq-k-j-neq-k
;;;If the k's entry in lp is between 10 and 12
;;;and the k's entry in l is between 10 and 12,
;;; then (phi9 k n g) holds.

Theorem: k-in-l10-11-or-phi9 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ union-at-n (lp, k, '(10 11 12)) ∧ (¬ union-at-n (l, k, '(10 11)))) → phi9 (k, n, g)

;;;If j is less than k and (phi9 k n g) holds,
;;;then the j's entry in g is either 0 or 1.

Theorem: phi9-j-in-g01 ((j ∈ nset (n)) ∧ (j < k) ∧ phi9 (k, n, g)) → union-at-n (g, j , '(0 1))

;;;If j is less than k and (phi9 k n g) holds,
;;;then the j's entry in lp is not between 5 and 12.
;;;lp-same-l-not is used.

Theorem: case-k-in-phi9 (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ (j < k) ∧ lg (n, l, g) ∧ phi9 (k, n, g)) → (¬ union-at-n (lp, j , '(5 6 7 8 9 10 11 12)))

;;;If j is not equal to k and the k's entry in l is
;;;either 10 or 11, then the j's entry in lp is not
;;;between 5 and 12.

Theorem: case-k-in-l10-11 (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ a2-at-n1-n2 (k, j , l) ∧ (j ≠ k) ∧ union-at-n (l, k, '(10 11))) → (¬ union-at-n (lp, j , '(5 6 7 8 9 10 11 12)))

;;;Auxiliary lemma for lm-i-eq-k-j-neq-k with
;;;(a2-at-n1-n2 k j l).

Theorem: lm1-i-eq-k-j-neq-k (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ (j < k) ∧ lg (n, l, g) ∧ a2-at-n1-n2 (k, j , l) ∧ union-at-n (lp, k, '(10 11 12))) → (¬ union-at-n (lp, j , '(5 6 7 8 9 10 11 12)))

;;;If j is less then k and the k's entry in lp is
;;;between 10 and 12, then the j's entry in lp is
;;;not between 5 and 12.

Theorem: lm-i-eq-k-j-neq-k (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ (j < k) ∧ lg (n, l, g) ∧ a2-at-n1-n2 (k, j , l)) → a2-at-n1-n2 (k, j , lp)

;;;If j is less than k,
;;;then (a2-at-n1-n2 k j lp) holds.

Theorem: i-eq-k-j-neq-k (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ (j < k) ∧ lg (n, l, g) ∧ a2 (n, n, l)) → a2-at-n1-n2 (k, j , lp)

;* j-eq-k-i-neq-k
;;;If the k's entry in l is not 4 and the k's entry in lp
;;;is between 5 and 7, then the k's entry in l is
;;;between 5 and 7.

Theorem: k-in-lp5-7-not-l4-then-l5-7 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (¬ at (l, k, 4)) ∧ union-at-n (lp, k, '(5 6 7))) → union-at-n (l, k, '(5 6 7))

;;;If the k's entry in lp is between 5 and 7 then
;;;the k's entry in l is  certainly between 5 and 12.

Theorem: k-in-lp5-7-then-l5-11 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (¬ at (l, k, 4)) ∧ union-at-n (lp, k, '(5 6 7))) → union-at-n (l, k, '(5 6 7 8 9 10 11))

;;;If the k's entry in lp is 8,
;;;then the k's entry in l is between 5 and 11.

Theorem: k-in-lp8-then-l5-11 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ at (lp, k, 8)) → union-at-n (l, k, '(5 6 7 8 9 10 11))

;;;If the k's entry in lp is between 9 and 12,
;;;then the k's entry in l is between 5 and 12.

Theorem: k-in-lp9-12-then-l5-11 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ union-at-n (lp, k, '(9 10 11 12))) → union-at-n (l, k, '(5 6 7 8 9 10 11))

;;;If the k's entry in l is not 4 an the k's entry in lp is
;;;between 5 and 12, then the k's entry in l is
;;;between 5 and 11.

Theorem: k-in-l5-11 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (¬ at (l, k, 4)) ∧ union-at-n (lp, k, '(5 6 7 8 9 10 11 12))) → union-at-n (l, k, '(5 6 7 8 9 10 11))

;;;If the k's entry in l is not 4, and the k's entry
;;;in lp is not between 5 and 12, then the k's entry
;;;in lp is not between 5 and 12.

Theorem: k-not-in-l4 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (¬ at (l, k, 4)) ∧ (¬ union-at-n (l, k, '(5 6 7 8 9 10 11 12)))) → (¬ union-at-n (lp, k, '(5 6 7 8 9 10 11 12)))

;;;If a0 holds, and the k's entry in l is not
;;;between 5 and 12, then the k's entry in lp is not
;;;between 5 and 12.

Theorem: k-not-in-lp5-12 (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ a0 (n, l, k) ∧ union-at-n (l, i, '(10 11 12)) ∧ (¬ union-at-n (l, k, '(5 6 7 8 9 10 11 12)))) → (¬ union-at-n (lp, k, '(5 6 7 8 9 10 11 12)))

;;;Auxiliary lemma for lm-i-neq-k-j-eq-k.
;;;There is (a2-at-n1-n2 i k l) in the lemma.

Theorem: lm1-i-neq-k-j-eq-k (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (i ≠ k) ∧ (k < i) ∧ a0 (n, l, k) ∧ a2-at-n1-n2 (i, k, l) ∧ union-at-n (lp, i, '(10 11 12))) → (¬ union-at-n (lp, k, '(5 6 7 8 9 10 11 12)))

;;;If k is less than i and the i's entry in lp is
;;;between 10 and 12, then the k's entry in lp is
;;;between 5 and 12.

Theorem: lm-i-neq-k-j-eq-k (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (i ≠ k) ∧ (k < i) ∧ a0 (n, l, k) ∧ a2-at-n1-n2 (i, k, l)) → a2-at-n1-n2 (i, k, lp)

;;;If k is less than i then (a2-at-n1-n2 i k lp) holds.

Theorem: i-neq-k-j-eq-k (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ (i ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (i ≠ k) ∧ (k < i) ∧ a0 (n, l, k) ∧ a2 (n, n, l)) → a2-at-n1-n2 (i, k, lp)

;* i-j-neq-k
;;;If i and j are not equal to k and the i's entry in lp is
;;;between 10 and 12, then the j's entry in lp is
;;;between 5 and 12.

Theorem: lm-i-j-neq-k (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (i ≠ k) ∧ (j ≠ k) ∧ (j < i) ∧ a2-at-n1-n2 (i, j , l)) → a2-at-n1-n2 (i, j , lp)

;;;If i and j are not equal to k,
;;; then (a2-at-n1-n2 i j lp) holds.

Theorem: i-j-neq-k (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (i ≠ k) ∧ (j ≠ k) ∧ (j < i) ∧ a2 (n, n, l)) → a2-at-n1-n2 (i, j , lp)

;;;If i is not equal to k and j is less than i,
;;;then (a2-at-n1-n2 i j lp) holds.
;;;The order of the hints is crucial.

Theorem: i-neq-k (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (i ≠ k) ∧ (j < i) ∧ a0 (n, l, k) ∧ a2 (n, n, l)) → a2-at-n1-n2 (i, j , lp)

;;;If j is less than k then (a2-at-n1-n2 k j lp) holds.

Theorem: i-eq-k (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j < k) ∧ lg (n, l, g) ∧ a2 (n, n, l)) → a2-at-n1-n2 (k, j , lp)

;;;If i is less than j then (a2-at-n1-n2 k j lp) holds.
;;;Again the order of the hints is crucial.

Theorem: rho-preserves-a2 (ws (n, l, g)

∧ (k ∈ nset (n)) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j < i) ∧ lg (n, l, g) ∧ a0 (n, l, k) ∧ a2 (n, n, l)) → a2-at-n1-n2 (i, j , lp)

;;;;;;;;;;;;;;;;;;;;;;;;;;; a3.ev ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;* j-eq-k-i-neq-k
;;;If the i's entry in l is 12 and the k's entry in lp is
;;;between 5 and 12 then the k's entry in l is between 9
;;;and 11.

Theorem: lm-k-in-l9-11 (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ a0 (n, l, k) ∧ a3-at-n1-n2 (i, k, l, g) ∧ at (l, i, 12) ∧ union-at-n (l, k, '(5 6 7 8 9 10 11))) → union-at-n (l, k, '(9 10 11))

;;;If i is not equal to k, the i's entry in l is 12,
;;;and the k's entry in lp is between 5 and 12,
;;;then the k's entry in l is between 9 and 11.

Theorem: k-in-l9-11 (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ a0 (n, l, k) ∧ a3-at-n1-n2 (i, k, l, g) ∧ at (l, i, 12) ∧ union-at-n (lp, k, '(5 6 7 8 9 10 11 12))) → union-at-n (l, k, '(9 10 11))

;;;If the k's entry in lp is between 9 and 11
;;;then the k's entry in lp is between 9 and 12.

Theorem: k-in-lp9-12 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ union-at-n (l, k, '(9 10 11))) → union-at-n (lp, k, '(9 10 11 12))

;;Auxiliary lemma for lm-a3-i-neq-k-j-eq-k.
;;;There is (a3-at-n1-n2 i k l g) in the lemma.

Theorem: lm1-a3-i-neq-k-j-eq-k (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ lg (n, lp, gp) ∧ a0 (n, l, k) ∧ a3-at-n1-n2 (i, k, l, g) ∧ at (l, i, 12) ∧ union-at-n (lp, k, '(5 6 7 8 9 10 11 12))) → at (gp, k, 4)

;;;If i is not equal to k, the i's entry in lp is 12,
;;;and the k's entry in lp is between 5 and 12,
;;;then the k's entry in gp is 4.

Theorem: lm-a3-i-neq-k-j-eq-k (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ a0 (n, l, k) ∧ a3-at-n1-n2 (i, k, l, g)) → a3-at-n1-n2 (i, k, lp, gp)

;;;If i is not equal to k,
;;;then (a3-at-n1-n2 i k lp gp) holds.
;;;The order of the hypotheses is crucial.

Theorem: a3-i-neq-k-j-eq-k (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ a0 (n, l, k) ∧ a3 (n, n, l, g) ∧ (i ≠ k)) → a3-at-n1-n2 (i, k, lp, gp)

;* i-eq-k-j-neq-k
;;;If the k's entry in lp is 12 then (phi11 k n g) holds.

Theorem: cond-rhoi11 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ at (lp, k, 12)) → phi11 (k, n, g)

;;;If the k's entry in l is between 10 and 12,
;;;the j's entry in l is between 5 and 12, and
;;;(a2-at-n2 k n l) holds, then k is less than j.
;;;Because Bmp does not rewrite the clause
;;;(lessp k j), we take its contrapositive.

Theorem: k-lt-j ((j ∈ nset (n)) ∧ (j ≠ k) ∧ union-at-n (l, k, '(10 11 12)) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12)) ∧ (k ≮ j )) → (¬ a2-at-n2 (k, n, l))

;;;If k is less than j and (phi11 k n g) holds,
;;;then the j's entry in g is either 2 or 3.

Theorem: phi11-j-not-in-g23 ((j ∈ nset (n)) ∧ (k < j ) ∧ phi11 (k, n, g)) → (¬ union-at-n (g, j , '(2 3)))

;;;If j is not equal to k, (a2-at-n2 k n l), (phi11 k n g)
;;;the k's entry in l is between 10 and 12 and
;;;the j's entry in l is between 5 and 12,
;;;then the j's entry in g is either 2 or 3.

Theorem: lm1-j-not-in-g23 ((j ∈ nset (n)) ∧ (j ≠ k) ∧ a2-at-n2 (k, n, l) ∧ phi11 (k, n, g) ∧ union-at-n (l, k, '(10 11 12)) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12))) → (¬ union-at-n (g, j , '(2 3)))

;;;If j is not equal to k, the k's entry in l is
;;;between 10 and 12, the k's entry in lp is 12 and
;;;the j's entry in l is between 5 and 12,
;;;then the j's entry in g is either 2 or 3.

Theorem: lm2-j-not-in-g23 (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ a2-at-n2 (k, n, l) ∧ at (lp, k, 12) ∧ at (l, k, 11) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12))) → (¬ union-at-n (g, j , '(2 3)))

;;;If j is not equal to k, the k's entry in lp is 12,
;;;and the j's entry in l is between 5 and 12,
;;;then the j's entry in g is either 2 or 3.

Theorem: j-not-in-g23 (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ a2 (n, n, l) ∧ at (l, k, 11) ∧ at (lp, k, 12) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12))) → (¬ union-at-n (g, j , '(2 3)))

Theorem: j-in-g4 ((j ∈ nset (n)) ∧ lg (n, l, g)

∧ (¬ union-at-n (g, j , '(2 3))) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12))) → at (g, j , 4)

;;;un9-12-then-un8-12, if3, j-not-in-g23,
;;;l5-12-eq-l5-8-or-l9-12, un8-12-then-un5-12,
;;;and j-in-g4 are used.
;;;If j is not equal to k, the k's entry in lp is 12,
;;;the j's entry in l is between 5 and 12,
;;;then the j's entry in g is 4.

Theorem: a3-j-in-l5-12 (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ a2 (n, n, l) ∧ at (l, k, 11) ∧ at (lp, k, 12) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12))) → at (g, j , 4)

;;;If the k's entry in lp is 12,
;;;then the k's entry in l is 11.

Theorem: k-in-l11 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ at (lp, k, 12)) → at (l, k, 11)

;;;If k is not equal to j and the j's entry in g is 4,
;;;then the j's entry in gp is 4.

Theorem: lm1-a3-i-eq-k-j-neq-k (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ a2 (n, n, l) ∧ at (lp, k, 12) ∧ union-at-n (lp, j , '(5 6 7 8 9 10 11 12))) → at (g, j , 4)

;;;If j is not equal to k, the k's entry in lp is 12,
;;;and the j's entry in lp is between 5 and 12,
;;;then the j's entry in gp is 4.

Theorem: lm-a3-i-eq-k-j-neq-k (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ a2 (n, n, l) ∧ a3-at-n1-n2 (k, j , l, g)) → a3-at-n1-n2 (k, j , lp, gp)

;;;If j is not equal to k then (a3-at-n1-n2 k j lp gp).

Theorem: a3-i-eq-k-j-neq-k (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ a2 (n, n, l) ∧ a3 (n, n, l, g)) → a3-at-n1-n2 (k, j , lp, gp)

;* i-j-neq-k
;;;If i,j are not equal to k, the i's entry in lp is 12
;;;and the j's entry in lp between 5 and 12
;;;then the j's entry in gp is 4.

Theorem: lm-a3-i-j-neq-k (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ (i ≠ k) ∧ (j ≠ k) ∧ a3-at-n1-n2 (i, j , l, g)) → a3-at-n1-n2 (i, j , lp, gp)

;;;If i,j are not equal to k,
;;;then (a3-at-n1-n2 i j lp gp).

Theorem: a3-i-j-neq-k (ws (n, l, g) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ a3 (n, n, l, g) ∧ (i ≠ k) ∧ (j ≠ k)) → a3-at-n1-n2 (i, j , lp, gp)

;* i-j-eq-k

Theorem: lm-a3-i-j-eq-k (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ a2 (n, n, l) ∧ a3-at-n1-n2 (k, k, l, g)) → a3-at-n1-n2 (k, k, lp, gp)

;;;(a3-at-n1-n2 k k lp gp) holds by lg.

Theorem: a3-i-j-eq-k (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ a2 (n, n, l) ∧ a3 (n, n, l, g)) → a3-at-n1-n2 (k, k, lp, gp)

;;;(a3-at-n1-n2 k j lp gp) holds.

Theorem: a3-i-eq-k (ws (n, l, g) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g)

∧ a2 (n, n, l) ∧ a3 (n, n, l, g)) → a3-at-n1-n2 (k, j , lp, gp)

;;;If i is not equal to k,
;;;then (a3-at-n1-n2 i j lp gp) holds.

Theorem: a3-i-neq-k (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ a0 (n, l, k) ∧ a2 (n, n, l) ∧ a3 (n, n, l, g) ∧ (i ≠ k)) → a3-at-n1-n2 (i, j , lp, gp)

;;;(a3-at-n1-n2 i j lp gp) holds.

Theorem: rho-preserves-a3 (ws (n, l, g) ∧ (k ∈ nset (n)) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ rhoi (n, k, l, g, lp, gp) ∧ lg (n, l, g) ∧ a0 (n, l, k) ∧ a2 (n, n, l) ∧ a3 (n, n, l, g)) → a3-at-n1-n2 (i, j , lp, gp)

Index

a0, 17, 55, 56, 67–72, 77 a1, 17, 55, 56, 58, 62, 63 a1-ep-l8-12, 58 a1-k-in-l12-nep-l8-12, 62 a1-k-in-l8-11-nep-l8-12, 59 a1-k-not-in-l8-12-nep-l8-12, 58 a1-nep-l8-12, 63 a2, 17, 23, 24, 65, 68–70, 73–77 a2-a2-at-n2, 23 a2-at-n1-n2, 17, 22, 24, 64, 65, 67–

70 a2-at-n2, 17, 22–24, 72, 73 a2-at-n2-a2-at-n1-n2, 22 a2-i-j-a2-at-n1-n2, 24 a2-n-a2-at-n2, 24 a3, 18, 23, 24, 63, 72, 75–77 a3-a3-at-n2, 23 a3-at-n1-n2, 18, 23, 24, 62, 70–72,

75–77 a3-at-n2, 18, 23 a3-at-n2-a3-at-n1-n2, 23 a3-ex-a3-at-n1-n2, 24 a3-i-eq-k, 76 a3-i-eq-k-j-neq-k, 75 a3-i-j-a3-at-n1-n2, 24 a3-i-j-eq-k, 76 a3-i-j-neq-k, 76 a3-i-neq-k, 77 a3-i-neq-k-j-eq-k, 72 a3-if4, 11 a3-j-in-l5-12, 74 add1-nset, 5 all-union, 2, 13, 25–33 at, 2–4, 7–18, 22, 33–50, 52–55, 57,

59, 60, 62, 66, 67, 70–74

b1a-if4, 13

case-k, 8 case-k-in-l10-11, 64 case-k-in-phi9, 64 cond-rhoi11, 72 cond-rhoi5, 53 cond-rhoi7, 53

dwy-lckd, 55

ex-cond-rhoi5, 53 ex-cond-rhoi7, 53 ex-gp-rhoi5, 57 ex-if4, 6 ex-k-in-l57, 52 ex-lp8-12-in-gp4, 61 ex-lp8-12-in-lp8-12, 6 ex-lp8-12-not-in-lp0, 9 ex-lp8-12-then-l5-12, 61 exist-intersect-8-12-3-4, 3, 6–8, 17, 58, 59, 62, 63

exist-l8-12, 51

exist-union, 3, 6, 7, 9, 11, 12, 14, 15, 17, 24, 51–63

g-rholemma, 20 g-same-gp, 21 gp-rhoi5, 57 gp-same-g, 21 gp-same-g-at, 22 gp3-then-un34, 8

i-eq-k, 69

i-eq-k-j-neq-k, 65 i-j-neq-k, 69 i-neq-k, 69 i-neq-k-j-eq-k, 68 i-not-in-l12, 12 i-not-l10-12, 11 if1, 10 if3, 12 if4, 9 int-8-12-3-4-then-un34, 7 int-k-not-ex-int, 58 int-wtn, 7 intersect-8-12-3-4-at-n, 3, 7 intersect-8-12-3-4-then-3-4, 8 intersect-8-12-3-4-then-8-12, 8

j-eq-k-j-not-in-lp4, 54 j-eq-k-l8-l12-nonemp, 55 j-eq-k-move-member-g, 24 j-ex-l8-12, 6 j-in-g4, 73 j-neq-k-j-not-in-lp4, 54 j-neq-k-l8-l12-nonemp, 56 j-neq-k-move-member-g, 24 j-not-in-g23, 73

k-in-gp34, 57 k-in-l10-11-or-phi9, 64 k-in-l11, 74 k-in-l5-11, 66 k-in-l5-11-g4-then-l9-11, 11 k-in-l5-12, 61 k-in-l57, 52 k-in-l9-11, 70 k-in-lp0, 59 k-in-lp5-7-not-l4-then-l5-7, 66 k-in-lp5-7-or-lp8-or-lp9-12, 10 k-in-lp5-7-then-l5-11, 66 k-in-lp8-12, 52 k-in-lp8-then-l5-11, 66 k-in-lp8-then-l5-12, 60 k-in-lp9-12, 71 k-in-lp9-12-or-lp8, 9 k-in-lp9-12-then-l5-11, 66 k-in-lp9-12-then-l5-12, 60 k-lt-j, 72 k-neq-ex-lp8-12-in-l5-12, 61 k-not-0, 6 k-not-ex-lp8-12, 60 k-not-in-l4, 67 k-not-in-l8-12-then-l57, 52 k-not-in-lp5-12, 67

l-rholemma, 19 l-same-lp, 20 l-same-lp-at, 22 l-same-lp-at-not, 22 l11-then-un10-12, 12 l12-then-un8-12, 12 l12-then-un9-12, 12 l34-empty, 7 l5-12-eq-l5-8-or-l9-12, 12 l5-only-lp8, 54 l8-11-k-in-lp9-12, 59 l8-l12-empty, 55 l8-l12-nonemp, 56 length, 2, 5, 13, 19, 20, 24–50 lg, 4, 6–13, 34–50, 54–59, 62–65, 69–

77 lg-1-at-n, 3, 4 lg-2-at-n, 4 lg-3-at-n, 4 lg-at-n, 4, 33–49 lg-at-rhoi0, 34 lg-at-rhoi10, 47 lg-at-rhoi11a, 48 lg-at-rhoi12, 49 lg-at-rhoi1a, 35 lg-at-rhoi2, 36 lg-at-rhoi3a, 37 lg-at-rhoi4, 39 lg-at-rhoi5a, 40 lg-at-rhoi5b, 41 lg-at-rhoi6, 42 lg-at-rhoi7a, 43 lg-at-rhoi8, 44 lg-at-rhoi9a, 46 lg-l5-g3, 8 lg-rhoi0, 34 lg-rhoi10, 47 lg-rhoi11a, 48 lg-rhoi12, 49 lg-rhoi1a, 35 lg-rhoi2, 36 lg-rhoi3a, 38 lg-rhoi4, 39 lg-rhoi5a, 40 lg-rhoi5b, 41 lg-rhoi6, 42 lg-rhoi7a, 43 lg-rhoi8, 45 lg-rhoi9a, 46 list-ln, 5 lm-a1-ep-l8-12, 57 lm-a1-k-in-l12-nep-l8-12, 62 lm-a1-k-in-l8-11-nep-l8-12, 59 lm-a1-nep-l8-12, 63 lm-a2-a2-at-n2, 23 lm-a2-at-n2-a2-at-n1-n2, 22 lm-a3-a3-at-n2, 23 lm-a3-at-n2-a3-at-n1-n2, 23 lm-a3-i-eq-k-j-neq-k, 75 lm-a3-i-j-eq-k, 76 lm-a3-i-j-neq-k, 75 lm-a3-i-neq-k-j-eq-k, 71 lm-g-rholemma, 20 lm-i-eq-k-j-neq-k, 65 lm-i-j-neq-k, 68 lm-i-neq-k-j-eq-k, 68 lm-k-in-l9-11, 70 lm-l-rholemma, 19 lm-rho-preserves-ln-g, 33 lm-rho-preserves-ln-l, 33 lm-rho-preserves-ws, 33 lm-rho0-preserves-union-l, 28 lm-rho10-preserves-union-g, 27 lm-rho10-preserves-union-l, 32 lm-rho11a-preserves-union-l, 32 lm-rho11b-preserves-union-l, 32 lm-rho12-preserves-union-g, 27 lm-rho12-preserves-union-l, 32 lm-rho1a-preserves-union-l, 28 lm-rho1b-preserves-union-l, 28 lm-rho2-preserves-union-g, 25 lm-rho2-preserves-union-l, 29 lm-rho3a-preserves-union-l, 29 lm-rho3b-preserves-union-l, 29 lm-rho4-preserves-union-g, 26 lm-rho4-preserves-union-l, 29 lm-rho5a-preserves-union-l, 30 lm-rho5b-preserves-union-l, 30 lm-rho6-preserves-union-g, 26 lm-rho6-preserves-union-l, 30 lm-rho7a-preserves-union-l, 30 lm-rho7b-preserves-union-l, 31 lm-rho8-preserves-union-g, 27 lm-rho8-preserves-union-l, 31 lm-rho9a-preserves-union-l, 31 lm-rho9b-preserves-union-l, 31 lm1-a1-nep-l8-12, 62 lm1-a3-i-eq-k-j-neq-k, 74 lm1-a3-i-neq-k-j-eq-k, 71 lm1-i-eq-k-j-neq-k, 65 lm1-i-neq-k-j-eq-k, 67 lm1-j-not-in-g23, 73 lm2-j-not-in-g23, 73 lp-same-l, 20 lp-same-l-not, 21 lp4-empty, 55 lp4-then-un34, 7 lp8-k-in-l57, 60 lp9-12-k-in-l8-11, 60 lp9-12-then-k-in-g34, 13

member-ex-union, 6 member-intersect, 6 move, 2, 5, 13–16, 24, 25, 33–50 move-is-list, 5 move-member-g, 24 move-member-l, 25 move-nth, 5 move-unchange-length, 5 move-unchange-other-than-nth, 5

n-eq-k-rhoi0, 34 n-eq-k-rhoi10, 47 n-eq-k-rhoi11a, 48 n-eq-k-rhoi12, 49 n-eq-k-rhoi1a, 35 n-eq-k-rhoi2, 36 n-eq-k-rhoi3a, 37 n-eq-k-rhoi4, 38 n-eq-k-rhoi5a, 40 n-eq-k-rhoi5b, 41 n-eq-k-rhoi6, 42 n-eq-k-rhoi7a, 43 n-eq-k-rhoi8, 44 n-eq-k-rhoi9a, 45 n-in-nset, 5 n-neq-k-rhoi0, 33 n-neq-k-rhoi10, 46 n-neq-k-rhoi11a, 47 n-neq-k-rhoi12, 49 n-neq-k-rhoi1a, 34 n-neq-k-rhoi2, 36 n-neq-k-rhoi3a, 37 n-neq-k-rhoi4, 38 n-neq-k-rhoi5a, 39 n-neq-k-rhoi5b, 40 n-neq-k-rhoi6, 42 n-neq-k-rhoi7a, 43 n-neq-k-rhoi8, 44 n-neq-k-rhoi9a, 45 n-not-0, 19 nset, 4–13, 17, 19–77 nset-number, 5 nth, 1, 2, 5, 19, 20, 24, 25 number-ex-union, 6 number-intersect, 6

phi11, 15, 16, 72, 73 phi11-j-not-in-g23, 72 phi9, 15, 64 phi9-j-in-g01, 64

rho-preserves-a0, 56 rho-preserves-a1, 63 rho-preserves-a2, 69 rho-preserves-a3, 77 rho-preserves-lg, 50 rho-preserves-ln-g, 33 rho-preserves-ln-l, 33 rho-preserves-union-g, 28 rho-preserves-union-l, 33 rho-preserves-ws, 33 rho0-preserves-union-g, 25 rho0-preserves-union-l, 28 rho10-preserves-union-g, 27 rho10-preserves-union-l, 32 rho11a-preserves-union-g, 27 rho11a-preserves-union-l, 32 rho11b-preserves-union-g, 27 rho11b-preserves-union-l, 32 rho12-preserves-union-g, 28 rho12-preserves-union-l, 32 rho1a-preserves-union-g, 25 rho1a-preserves-union-l, 28 rho1b-preserves-union-g, 25 rho1b-preserves-union-l, 28 rho2-preserves-union-g, 25 rho2-preserves-union-l, 29 rho3a-preserves-union-g, 25 rho3a-preserves-union-l, 29 rho3b-preserves-union-g, 26 rho3b-preserves-union-l, 29 rho4-preserves-union-g, 26 rho4-preserves-union-l, 29 rho5a-preserves-union-g, 26 rho5a-preserves-union-l, 30 rho5b-preserves-union-g, 26 rho5b-preserves-union-l, 30 rho6-preserves-union-g, 26 rho6-preserves-union-l, 30 rho7a-preserves-union-g, 26 rho7a-preserves-union-l, 30 rho7b-preserves-union-g, 26 rho7b-preserves-union-l, 31 rho8-preserves-union-g, 27 rho8-preserves-union-l, 31 rho9a-preserves-union-g, 27 rho9a-preserves-union-l, 31 rho9b-preserves-union-g, 27 rho9b-preserves-union-l, 31 rhoi, 16, 19–22, 28, 33, 50–77 rhoi0, 13, 16, 25, 28, 34 rhoi0-preserves-lg, 34 rhoi10, 15, 16, 27, 32, 47 rhoi10-preserves-lg, 47 rhoi11a, 16, 27, 32, 48 rhoi11a-preserves-lg, 48 rhoi11b, 16, 27, 32, 49 rhoi11b-preserves-lg, 49 rhoi12, 16, 27, 28, 32, 50 rhoi12-preserves-lg, 50 rhoi1a, 14, 16, 25, 28, 35 rhoi1a-preserves-lg, 35 rhoi1b, 14, 16, 25, 28, 36 rhoi1b-preserves-lg, 36 rhoi2, 14, 16, 25, 29, 37 rhoi2-preserves-lg, 37 rhoi3a, 14, 16, 25, 29, 38 rhoi3a-preserves-lg, 38 rhoi3b, 14, 16, 26, 29, 38 rhoi3b-preserves-lg, 38 rhoi4, 14, 16, 26, 29, 39 rhoi4-preserves-lg, 39 rhoi5a, 14, 16, 26, 30, 40 rhoi5a-preserves-lg, 40 rhoi5b, 14, 16, 26, 30, 41 rhoi5b-preserves-lg, 41 rhoi6, 14, 16, 26, 30, 43 rhoi6-preserves-lg, 43 rhoi7a, 15, 16, 26, 30, 44 rhoi7a-preserves-lg, 44 rhoi7b, 15, 16, 26, 31, 44 rhoi7b-preserves-lg, 44 rhoi8, 15, 16, 27, 31, 45 rhoi8-preserves-lg, 45 rhoi9a, 15, 16, 27, 31, 46 rhoi9a-preserves-lg, 46 rhoi9b, 15, 16, 27, 31, 46 rhoi9b-preserves-lg, 46

un10-11-then-un10-12, 10 un10-12-then-un8-12, 11 un5-11-eq-un58-or-un8-11, 11 un5-11-then-un5-12, 10 un5-7-then-un5-11, 10 un57-then-un5-11, 10 un57-then-un5-12, 9 un8-11-then-un5-11, 10 un8-11-then-un5-12, 9 un8-12-and-un34-then-int, 7 un8-12-then-l8-or-l9-12, 13 un8-12-then-un5-12, 9 un9-12-then-un8-12, 8 union-at-n, 2, 3, 6–13, 15, 17, 18,

20, 21, 52–55, 57–62, 64– 67, 70–74

ws, 13, 18–41, 43–77 ws-list-g, 18 ws-list-l, 18 ws-ln-g, 19 ws-ln-gp, 19 ws-ln-l, 19 ws-ln-lp, 19 ws-n-not-0, 19 ws-num-n, 18 ws-union-g, 25 ws-union-l, 25

zero-not-member-nset, 5