#|
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-molecular.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))

;;;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))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; moldefn.ev ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;* Well-formed states

Definition: molws (n, l, g, h) = ((n ∈ N)

∧ listp (l) ∧ listp (g) ∧ listp (h) ∧ (length (l) = n) ∧ (length (g) = n) ∧ (length (h) = 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)) ∧ all-union (h, n, nset (1 + n)))

Event: Disable molws.

;* Transitions

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

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

Definition: mrhoi1b (n, i, l, g, h, lp, gp, hp) = (at (l, i, 1) ∧ (gp = g) ∧ (lp = l) ∧ (hp = h))

Definition: mrhoi2 (n, i, l, g, h, lp, gp, hp) = (at (l, i, 2)

∧ (lp = move (l, i, 3)) ∧ (gp = move (g, i, 1)) ∧ (hp = move (h, i, 1)))

Definition: mrhoi3a (n, i, l, g, h, lp, gp, hp) = (at (l, i, 3)

∧ (gp = g) ∧ (hp = h) ∧ at (h, i, 1 + n) ∧ (lp = move (l, i, 4)))

Definition: mrhoi3b (n, i, l, g, h, lp, gp, hp) = (at (l, i, 3)

∧ (gp = g) ∧ (lp = l) ∧ (nth (h, i) < (1 + n)) ∧ (hp = move (h, i, 1 + nth (h, i))) ∧ union-at-n (g, nth (h, i), '(0 1 2)))

Definition: mrhoi4 (n, i, l, g, h, lp, gp, hp) = (at (l, i, 4)

∧ (gp = move (g, i, 3)) ∧ (lp = move (l, i, 5)) ∧ (hp = move (h, i, 1)))

Definition: mrhoi5a (n, i, l, g, h, lp, gp, hp) = (at (l, i, 5)

∧ (gp = g) ∧ (hp = h) ∧ at (h, i, 1 + n) ∧ (lp = move (l, i, 8)))

Definition: mrhoi5b (n, i, l, g, h, lp, gp, hp) = (at (l, i, 5)

∧ (gp = g) ∧ (hp = h) ∧ (nth (h, i) < (1 + n)) ∧ at (g, nth (h, i), 1) ∧ (lp = move (l, i, 6)))

Definition: mrhoi5c (n, i, l, g, h, lp, gp, hp) = (at (l, i, 5)

∧ (gp = g) ∧ (lp = l) ∧ (nth (h, i) < (1 + n)) ∧ (¬ at (g, nth (h, i), 1)) ∧ (hp = move (h, i, 1 + nth (h, i))))

Definition: mrhoi6 (n, i, l, g, h, lp, gp, hp) = (at (l, i, 6)

∧ (gp = move (g, i, 2)) ∧ (lp = move (l, i, 7)) ∧ (hp = move (h, i, 1)))

Definition: mrhoi7a (n, i, l, g, h, lp, gp, hp) = (at (l, i, 7)

∧ (lp = move (l, i, 8)) ∧ at (g, nth (h, i), 4) ∧ (gp = g) ∧ (hp = h))

Definition: mrhoi7b (n, i, l, g, h, lp, gp, hp) = (at (l, i, 7)

∧ (¬ at (g, nth (h, i), 4)) ∧ (lp = l) ∧ (gp = g) ∧ (hp = move (h, i, 1 + ((nth (h, i) − 1) mod n))))

Definition: mrhoi8 (n, i, l, g, h, lp, gp, hp) = (at (l, i, 8)

∧ (gp = move (g, i, 4))

∧ (lp = move (l, i, 9)) ∧ (hp = move (h, i, 1)))

Definition: mrhoi9a (n, i, l, g, h, lp, gp, hp) = (at (l, i, 9)

∧ at (h, i, i) ∧ (lp = move (l, i, 10)) ∧ (gp = g) ∧ (hp = h))

Definition: mrhoi9b (n, i, l, g, h, lp, gp, hp) = (at (l, i, 9)

∧ (nth (h, i) < i) ∧ union-at-n (g, nth (h, i), '(0 1)) ∧ (hp = move (h, i, 1 + nth (h, i))) ∧ (gp = g) ∧ (lp = l))

Definition: mrhoi10 (n, i, l, g, h, lp, gp, hp) = (at (l, i, 10)

∧ (lp = move (l, i, 11)) ∧ (gp = g) ∧ (hp = move (h, i, 1 + i)))

Definition: mrhoi11a (n, i, l, g, h, lp, gp, hp) = (at (l, i, 11)

∧ at (h, i, 1 + n) ∧ (lp = move (l, i, 12)) ∧ (gp = g) ∧ (hp = h))

Definition: mrhoi11b (n, i, l, g, h, lp, gp, hp) = (at (l, i, 11)

∧ (nth (h, i) < (1 + n)) ∧ (¬ union-at-n (g, nth (h, i), '(2 3))) ∧ (hp = move (h, i, 1 + nth (h, i))) ∧ (gp = g) ∧ (lp = l))

Definition: mrhoi12 (n, i, l, g, h, lp, gp, hp) = (at (l, i, 12)

∧ (hp = h) ∧ (gp = move (g, i, 0)) ∧ (lp = move (l, i, 0)))

Definition: mrhoi (n, i, l, g, h, lp, gp, hp) = (mrhoi0 (n, i, l, g, h, lp, gp, hp)

∨ mrhoi1a (n, i, l, g, h, lp, gp, hp) ∨ mrhoi1b (n, i, l, g, h, lp, gp, hp) ∨ mrhoi2 (n, i, l, g, h, lp, gp, hp) ∨ mrhoi3a (n, i, l, g, h, lp, gp, hp) ∨ mrhoi3b (n, i, l, g, h, lp, gp, hp) ∨ mrhoi4 (n, i, l, g, h, lp, gp, hp) ∨ mrhoi5a (n, i, l, g, h, lp, gp, hp) ∨ mrhoi5b (n, i, l, g, h, lp, gp, hp) ∨ mrhoi5c (n, i, l, g, h, lp, gp, hp) ∨ mrhoi6 (n, i, l, g, h, lp, gp, hp) ∨ mrhoi7a (n, i, l, g, h, lp, gp, hp) ∨ mrhoi7b (n, i, l, g, h, lp, gp, hp) ∨ mrhoi8 (n, i, l, g, h, lp, gp, hp) ∨ mrhoi9a (n, i, l, g, h, lp, gp, hp) ∨ mrhoi9b (n, i, l, g, h, lp, gp, hp) ∨ mrhoi10 (n, i, l, g, h, lp, gp, hp) ∨ mrhoi11a (n, i, l, g, h, lp, gp, hp) ∨ mrhoi11b (n, i, l, g, h, lp, gp, hp) ∨ mrhoi12 (n, i, l, g, h, lp, gp, hp))

Event: Disable mrhoi.

;*  Invariants
;;;b0

Definition: b0a (n, l, h, i, j ) = ((at (l, i, 5) ∧ (j < nth (h, i))) → (¬ at (l, j , 4)))

Event: Disable b0a.

Definition: b0b (n, l, h, i, j ) = ((at (l, i, 5) ∧ (j < nth (h, i)) ∧ at (l, j , 3)) → (i ≮ nth (h, j )))

Event: Disable b0b.

;;;b1

Definition: b1a (l, i, j ) = (union-at-n (l, i, '(8 9 10 11 12)) → (¬ at (l, j , 4)))

Event: Disable b1a.

Definition: hint-8-12-3-4-at-n (n, l, g, h, j ) = (intersect-8-12-3-4-at-n (n, l, g) ∧ (n ≮ nth (h, j )))

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

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

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

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

Definition: b1b (n, l, g, h, i, j ) = ((union-at-n (l, i, '(8 9 10 11 12)) ∧ at (l, j , 3))

→ exist-hint-8-12-3-4 (n, l, g, h, j ))

Event: Disable b1b.

Definition: b1c (n, l, g, h, i) = ((union-at-n (l, i, '(8 9 10 11 12))

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

→ ((nth (h, i) ∈ nset (n)) ∧ at (g, nth (h, i), 4)))

Event: Disable b1c.

Definition: b1d (n, l, h, i) = (at (l, i, 7) → (nth (h, i) ∈ nset (n)))

Event: Disable b1d.

;;;; b2

Definition: b2a (l, i, j ) = (((j < i) ∧ union-at-n (l, i, '(10 11 12)))

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

Event: Disable b2a.

Definition: b2b (l, h, i, j ) = (((j < i) ∧ at (l, i, 9) ∧ (j < nth (h, i)))

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

Event: Disable b2b.

;;;b3

Definition: b3a (l, g, i, j ) = ((at (l, i, 12) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12)))

→ at (g, j , 4))

Event: Disable b3a.

Definition: b3b (l, g, h, i, j ) = ((at (l, i, 11)

∧ (j < nth (h, i))

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

Event: Disable b3b.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; molbasic.ev ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

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

Theorem: n-not-less-j (n < j ) → (j ∉ nset (n))

;;;molws implies that n is a number.

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

;;;molws implies that l is a list.

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

;;;molws implies that g is a list.

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

;;;molws implies that h is a list.

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

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

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

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

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

;;;molws implies that length of h is n.

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

;;;molws and mrho imply that lp is a list.

Theorem: molws-ln-lp (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp)) → listp (lp)

;;;molws and mrho imply that gp is a list.

Theorem: molws-ln-gp (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp)) → listp (gp)

;;;molws and mrho imply that hp is a list.

Theorem: molws-ln-hp (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp)) → listp (hp)

;;;Another version of nset-number.
;;;This is available in the theorem
;;;where molws is disabled.

Theorem: molws-num-k (molws (n, l, g, h) ∧ (k ∈ nset (n))) → (k ∈ N)

Theorem: molws-union-h molws (n, l, g, h) → all-union (h, n, nset (1 + n))

Theorem: lm-nth-numberp ((i ∈ N) ∧ all-union (h, n, nset (i)) ∧ (k ∈ nset (n))) → (nth (h, k) ∈ N)

Theorem: nth-numberp (molws (n, l, g, h) ∧ (k ∈ nset (n))) → (nth (h, k) ∈ N)

;;;molws implies that n is nonzero.

Theorem: molws-n-not-0 molws (n, l, g, h) → (n ≠ 0)

;;;Auxiliary lemma.

Theorem: lm-l-mrholemma (listp (l) ∧ (j ∈ nset (length (l))) ∧ (k ∈ nset (length (l))) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (k ≠ j )) → (nth (l, j ) = nth (lp, j ))

Event: Disable lm-l-mrholemma.

;;;Mrholemma for list l.

Theorem: l-mrholemma (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (k ≠ j )) → (nth (l, j ) = nth (lp, j ))

;;;Auxiliary lemma.

Theorem: lm-g-mrholemma (listp (g) ∧ (j ∈ nset (length (g))) ∧ (k ∈ nset (length (g))) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (k ≠ j )) → (nth (g, j ) = nth (gp, j ))

Event: Disable lm-g-mrholemma.

;;;Mrholemma for list g.

Theorem: g-mrholemma (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (k ≠ j )) → (nth (g, j ) = nth (gp, j ))

;;;Auxiliary lemma.

Theorem: lm-h-mrholemma (listp (h) ∧ (j ∈ nset (length (h))) ∧ (k ∈ nset (length (h))) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (k ≠ j )) → (nth (h, j ) = nth (hp, j ))

Event: Disable lm-h-mrholemma.

;;;Mrholemma for list g.

Theorem: h-mrholemma (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (k ≠ j )) → (nth (h, j ) = nth (hp, 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: m-lp-same-l (molws (n, l, g, h) ∧ listp (m) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (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: m-l-same-lp (molws (n, l, g, h) ∧ listp (m) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ union-at-n (lp, j , m)) → union-at-n (l, j , m)

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

;;;Another version of Rholemma for g.

Theorem: m-gp-same-g (molws (n, l, g, h) ∧ listp (m) ∧ (j ∈ nset (n))

∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (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: m-g-same-gp (molws (n, l, g, h) ∧ listp (m) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ union-at-n (gp, j , m)) → union-at-n (g, j , m)

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

;;;Another version of Rholemma for h.

Theorem: m-hp-same-h (molws (n, l, g, h) ∧ listp (m) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ union-at-n (h, j , m)) → union-at-n (hp, j , m)

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

Theorem: m-h-same-hp (molws (n, l, g, h) ∧ listp (m) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ union-at-n (hp, j , m)) → union-at-n (h, j , m)

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

Theorem: m-l-same-lp-at (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ (m ∈ N) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (k ≠ j ) ∧ at (lp, j , m)) → at (l, j , m)

Theorem: m-gp-same-g-at (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ (m ∈ N) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (k ≠ j ) ∧ at (g, j , m)) → at (gp, j , m)

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

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; mollg.ev ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;mrhoi0

Theorem: n-neq-k-mrhoi0 (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-mrhoi0.

Theorem: n-eq-k-mrhoi0 (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-mrhoi0.

Theorem: lg-at-mrhoi0 (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-mrhoi0.

Theorem: lg-mrhoi0 (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-mrhoi0.

Theorem: mrhoi0-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi0 (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi1a

Theorem: n-neq-k-mrhoi1a (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-mrhoi1a.

Theorem: n-eq-k-mrhoi1a (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-mrhoi1a.

Theorem: lg-at-mrhoi1a (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-mrhoi1a.

Theorem: lg-mrhoi1a (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-mrhoi1a.

Theorem: mrhoi1a-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi1a (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi1b

Theorem: mrhoi1b-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi1b (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi2

Theorem: n-neq-k-mrhoi2 (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-mrhoi2.

Theorem: n-eq-k-mrhoi2 (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-mrhoi2.

Theorem: lg-at-mrhoi2 (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-mrhoi2.

Theorem: lg-mrhoi2 (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-mrhoi2.

Theorem: mrhoi2-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi2 (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi3a

Theorem: n-neq-k-mrhoi3a (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-mrhoi3a.

Theorem: n-eq-k-mrhoi3a (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-mrhoi3a.

Theorem: lg-at-mrhoi3a (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-mrhoi3a.

Theorem: lg-mrhoi3a (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-mrhoi3a.

Theorem: mrhoi3a-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi3a (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi3b

Theorem: mrhoi3b-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi3b (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi4

Theorem: n-neq-k-mrhoi4 (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-mrhoi4.

Theorem: n-eq-k-mrhoi4 (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-mrhoi4.

Theorem: lg-at-mrhoi4 (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-mrhoi4.

Theorem: lg-mrhoi4 (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-mrhoi4.

Theorem: mrhoi4-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi4 (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi5a

Theorem: n-neq-k-mrhoi5a (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-mrhoi5a.

Theorem: n-eq-k-mrhoi5a (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-mrhoi5a.

Theorem: lg-at-mrhoi5a (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-mrhoi5a.

Theorem: lg-mrhoi5a (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-mrhoi5a.

Theorem: mrhoi5a-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi5a (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi5b

Theorem: n-neq-k-mrhoi5b (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-mrhoi5b.

Theorem: n-eq-k-mrhoi5b (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-mrhoi5b.

Theorem: lg-at-mrhoi5b (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-mrhoi5b.

Theorem: lg-mrhoi5b (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-mrhoi5b.

Theorem: mrhoi5b-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi5b (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi5c

Theorem: mrhoi5c-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n))

∧ mrhoi5c (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi6

Theorem: n-neq-k-mrhoi6 (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-mrhoi6.

Theorem: n-eq-k-mrhoi6 (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-mrhoi6.

Theorem: lg-at-mrhoi6 (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-mrhoi6.

Theorem: lg-mrhoi6 (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-mrhoi6.

Theorem: mrhoi6-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi6 (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi7a

Theorem: n-neq-k-mrhoi7a (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-mrhoi7a.

Theorem: n-eq-k-mrhoi7a (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-mrhoi7a.

Theorem: lg-at-mrhoi7a (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-mrhoi7a.

Theorem: lg-mrhoi7a (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-mrhoi7a.

Theorem: mrhoi7a-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi7a (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi7b

Theorem: mrhoi7b-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi7b (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi8

Theorem: n-neq-k-mrhoi8 (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-mrhoi8.

Theorem: n-eq-k-mrhoi8 (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-mrhoi8.

Theorem: lg-at-mrhoi8 (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-mrhoi8.

Theorem: lg-mrhoi8 (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-mrhoi8.

Theorem: mrhoi8-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi8 (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi9a

Theorem: n-neq-k-mrhoi9a (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-mrhoi9a.

Theorem: n-eq-k-mrhoi9a (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-mrhoi9a.

Theorem: lg-at-mrhoi9a (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-mrhoi9a.

Theorem: lg-mrhoi9a (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-mrhoi9a.

Theorem: mrhoi9a-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi9a (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi9b

Theorem: mrhoi9b-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi9b (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi10

Theorem: n-neq-k-mrhoi10 (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-mrhoi10.

Theorem: n-eq-k-mrhoi10 (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-mrhoi10.

Theorem: lg-at-mrhoi10 (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-mrhoi10.

Theorem: lg-mrhoi10 (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-mrhoi10.

Theorem: mrhoi10-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi10 (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi11a

Theorem: n-neq-k-mrhoi11a (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-mrhoi11a.

Theorem: n-eq-k-mrhoi11a (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-mrhoi11a.

Theorem: lg-at-mrhoi11a (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-mrhoi11a.

Theorem: lg-mrhoi11a (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-mrhoi11a.

Theorem: mrhoi11a-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi11a (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi11b

Theorem: mrhoi11b-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi11b (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp)

;;;mrhoi12

Theorem: n-neq-k-mrhoi12 (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-mrhoi12.

Theorem: n-eq-k-mrhoi12 (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-mrhoi12.

Theorem: lg-at-mrhoi12 (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-mrhoi12.

Theorem: lg-mrhoi12 (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-mrhoi12. Theorem: mrhoi12-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi12 (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp) Theorem: mrho-preserves-lg (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → lg (n, lp, gp) Event: Disable mrhoi0-preserves-lg. Event: Disable mrhoi1a-preserves-lg. Event: Disable mrhoi1b-preserves-lg. Event: Disable mrhoi2-preserves-lg. Event: Disable mrhoi3a-preserves-lg. Event: Disable mrhoi3b-preserves-lg. Event: Disable mrhoi4-preserves-lg. Event: Disable mrhoi5a-preserves-lg. Event: Disable mrhoi5b-preserves-lg. Event: Disable mrhoi5c-preserves-lg. Event: Disable mrhoi6-preserves-lg. Event: Disable mrhoi7a-preserves-lg.

Event: Disable mrhoi7b-preserves-lg.

Event: Disable mrhoi8-preserves-lg.

Event: Disable mrhoi9a-preserves-lg.

Event: Disable mrhoi9b-preserves-lg.

Event: Disable mrhoi10-preserves-lg.

Event: Disable mrhoi11a-preserves-lg.

Event: Disable mrhoi11b-preserves-lg.

Event: Disable mrhoi12-preserves-lg.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;   b0.ev   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;   b0a   ;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;Common in mole and atom.

Theorem: b0a-if1 ((j ∈ nset (n)) ∧ lg (n, l, g) ∧ (¬ at (g, j , 1))) → (¬ at (l, j , 4))

;;;;;;;;;;;;;comm end.

Theorem: if1-nth-h-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (h, k, j ) ∧ (¬ at (g, nth (h, k), 1))) → (¬ at (l, j , 4))

Theorem: l5-not-g1 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (j ∈ nset (n))

∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (h, k, j ) ∧ at (l, k, 5) ∧ at (lp, k, 5)) → (¬ at (g, nth (h, k), 1))

Theorem: l5-nth-h-k-eq-j (at (h, k, j ) ∧ molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, k, 5) ∧ at (lp, k, 5)) → (¬ at (l, j , 4))

Theorem: l5-j-lt-nth-k ((j < nth (h, k)) ∧ molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b0a (n, l, h, k, j ) ∧ at (l, k, 5)) → (¬ at (l, j , 4))

Theorem: nth-k-lt-j-or-eq-j (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ ((j − 1) < nth (h, k)) ∧ (j ≮ nth (h, k))) → at (h, k, j )

Theorem: lm-j-not-in-l4 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b0a (n, l, h, k, j ) ∧ at (l, k, 5) ∧ at (lp, k, 5) ∧ ((j − 1) < nth (h, k))) → (¬ at (l, j , 4))

Theorem: cond-l5 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 5) ∧ (j < nth (hp, k))) → ((j − 1) < nth (h, k))

Theorem: j-not-in-l4 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b0a (n, l, h, k, j ) ∧ at (l, k, 5) ∧ at (lp, k, 5) ∧ (j < nth (hp, k))) → (¬ at (l, j , 4))

Theorem: k-in-l5 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (lp, k, 5) ∧ (j < nth (hp, k))) → at (l, k, 5)

;;;The order of the hints is crucial.

Theorem: lm-b0a-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b0a (n, l, h, k, j ) ∧ at (lp, k, 5) ∧ (j < nth (hp, k))) → (¬ at (l, j , 4))

Theorem: b0a-i-eq-k-j-neq-k (molws (n, l, g, h)

∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ b0a (n, l, h, k, j )) → b0a (n, lp, hp, k, j )

Theorem: b0a-i-j-eq-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b0a (n, l, h, k, k)) → b0a (n, lp, hp, k, k)

Theorem: b0a-i-eq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b0a (n, l, h, k, j )) → b0a (n, lp, hp, k, j )

;;;n-not-less-j is necessary.

Theorem: cond-lp4 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 3) ∧ (i ≮ nth (h, k))) → (¬ at (lp, k, 4))

Theorem: not-l3-then-lp4 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (¬ at (l, k, 3))) → (¬ at (lp, k, 4))

Theorem: i-in-l5 (molws (n, l, g, h) ∧ (i ∈ nset (n))

∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b0b (n, l, h, i, k) ∧ at (l, i, 5) ∧ (k < nth (h, i))) → (¬ at (lp, k, 4))

Theorem: lm-b0a-i-neq-k-j-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ b0b (n, l, h, i, k) ∧ at (lp, i, 5) ∧ (k < nth (h, i))) → (¬ at (lp, k, 4))

Theorem: b0a-i-neq-k-j-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ b0a (n, l, h, i, k) ∧ b0b (n, l, h, i, k)) → b0a (n, lp, hp, i, k)

Theorem: b0a-i-j-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (j ≠ k) ∧ b0a (n, l, h, i, j ) ∧ b0b (n, l, h, i, j )) → b0a (n, lp, hp, i, j )

Theorem: b0a-i-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n))

∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ b0a (n, l, h, i, j ) ∧ b0b (n, l, h, i, j )) → b0a (n, lp, hp, i, j )

Theorem: rho-preserves-b0a (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b0a (n, l, h, i, j ) ∧ b0b (n, l, h, i, j )) → b0a (n, lp, hp, i, j )

;;;;;;;;;;;;;   b0b   ;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;Common in mole and atom.

Theorem: b0b-if1 ((j ∈ nset (n)) ∧ lg (n, l, g) ∧ at (l, j , 3)) → at (g, j , 1)

Theorem: b0b-if3 ((i ∈ nset (n)) ∧ lg (n, l, g) ∧ at (l, i, 5)) → (¬ union-at-n (g, i, '(0 1 2)))

;;;;;;;;;;;;;;;;;Common in mole and atom end.

Theorem: lm-j-neq-h-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, j , 3) ∧ (¬ at (g, nth (h, k), 1))) → (¬ at (h, k, j ))

Theorem: h-k-not-g1 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp)

∧ at (l, k, 5) ∧ at (lp, k, 5)) → (¬ at (g, nth (h, k), 1))

Theorem: j-neq-h-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (lp, k, 5) ∧ at (l, k, 5) ∧ at (l, j , 3)) → (¬ at (h, k, j ))

Theorem: n-k-leq-sub1-i (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (i ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (¬ at (h, k, i)) ∧ (i ≮ nth (h, k))) → ((i − 1) ≮ nth (h, k))

;;;This is proved with help of n-k-leq-sub1-i.

Theorem: lm1-j-in-l3 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b0b (n, l, h, k, j ) ∧ at (l, k, 5) ∧ at (lp, k, 5) ∧ at (l, j , 3) ∧ ((j − 1) < nth (h, k))) → (k ≮ nth (h, j ))

Theorem: lm-j-in-l3 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)

∧ b0b (n, l, h, k, j ) ∧ at (l, k, 5) ∧ at (lp, k, 5) ∧ at (l, j , 3) ∧ (j < nth (hp, k))) → (k ≮ nth (h, j ))

;;;The order of hints is crucial.

Theorem: j-in-l3 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b0b (n, l, h, k, j ) ∧ at (lp, k, 5) ∧ at (l, j , 3) ∧ (j < nth (hp, k))) → (k ≮ nth (h, j ))

Theorem: lm-b0b-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ b0b (n, l, h, k, j ) ∧ at (lp, k, 5) ∧ at (lp, j , 3) ∧ (j < nth (hp, k))) → (k ≮ nth (h, j ))

Theorem: b0b-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ b0b (n, l, h, k, j )) → b0b (n, lp, hp, k, j )

Theorem: b0b-i-j-eq-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)) → b0b (n, lp, hp, k, k)

Theorem: b0b-i-eq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b0b (n, l, h, k, j )) → b0b (n, lp, hp, k, j )

Theorem: lm-i-neq-h-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (i ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, i, 5) ∧ union-at-n (g, nth (h, k), '(0 1 2))) → (¬ at (h, k, i))

Theorem: h-k-g02 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 3) ∧ at (lp, k, 3)) → union-at-n (g, nth (h, k), '(0 1 2))

Theorem: i-neq-h-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (i ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, i, 5) ∧ at (l, k, 3) ∧ at (lp, k, 3)) → (¬ at (h, k, i))

Theorem: lm1-k-in-l3-imp (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (i ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, i, 5) ∧ at (l, k, 3) ∧ at (lp, k, 3) ∧ (i ≮ nth (h, k))) → ((i − 1) ≮ nth (h, k))

Theorem: lm-k-in-l3-imp (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (i ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b0b (n, l, h, i, k) ∧ at (l, i, 5) ∧ at (l, k, 3) ∧ at (lp, k, 3) ∧ (k < nth (h, i))) → ((i − 1) ≮ nth (h, k))

Theorem: cond-l3 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (i ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 3) ∧ (i < nth (hp, k))) → ((i − 1) < nth (h, k))

Theorem: k-in-l3-imp (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b0b (n, l, h, i, k) ∧ at (l, i, 5) ∧ at (l, k, 3) ∧ at (lp, k, 3) ∧ (k < nth (h, i))) → (i ≮ nth (hp, k))

Theorem: k-in-l2-imp (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (lp, k, 3) ∧ at (l, k, 2)) → (i ≮ nth (hp, k))

Theorem: lp3-then-l2-or-l3 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (lp, k, 3) ∧ (¬ at (l, k, 2))) → at (l, k, 3)

Theorem: b0b-i-in-l5 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b0b (n, l, h, i, k) ∧ at (l, i, 5) ∧ at (lp, k, 3) ∧ (k < nth (h, i))) → (i ≮ nth (hp, k))

Theorem: lm-b0b-i-neq-k-j-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ b0b (n, l, h, i, k) ∧ lg (n, l, g) ∧ at (lp, i, 5) ∧ at (lp, k, 3) ∧ (k < nth (h, i))) → (i ≮ nth (hp, k))

Theorem: b0b-i-neq-k-j-eq-k (molws (n, l, g, h)

∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ b0b (n, l, h, i, k) ∧ lg (n, l, g)) → b0b (n, lp, hp, i, k)

Theorem: b0b-i-j-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (j ≠ k) ∧ b0b (n, l, h, i, j )) → b0b (n, lp, hp, i, j )

Theorem: b0b-i-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ b0b (n, l, h, i, j )) → b0b (n, lp, hp, i, j )

Theorem: rho-preserves-b0b (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b0b (n, l, h, i, j )) → b0b (n, lp, hp, i, j )

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;   b1.ev   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;   b1a   ;;;;;;;;;;;;;;;;

Theorem: lm-h-k-eq-add1-n-nex-hint ((n ≄ 0) ∧ listp (h) ∧ (n ≮ i) ∧ (k ∈ nset (n)) ∧ (n < nth (h, k))) → (¬ exist-hint-8-12-3-4 (i, l, g, h, k))

Theorem: h-k-eq-add1-n-nex-hint (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ at (h, k, 1 + n)) → (¬ exist-hint-8-12-3-4 (n, l, g, h, k))

Theorem: h-k-eq-add1-n-k-not-in-l3 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1b (n, l, g, h, i, k) ∧ at (h, k, 1 + n) ∧ union-at-n (l, i, '(8 9 10 11 12))) → (¬ at (l, k, 3))

Theorem: not-l3-then-not-lp4 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (¬ at (l, k, 3))) → (¬ at (lp, k, 4))

Theorem: h-k-eq-add1-n (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1b (n, l, g, h, i, k) ∧ at (h, k, 1 + n) ∧ union-at-n (l, i, '(8 9 10 11 12))) → (¬ at (lp, k, 4))

Theorem: h-k-neq-add1-n (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (¬ at (h, k, 1 + n))) → (¬ at (lp, k, 4))

;;;The order of the hints is crucial.

Theorem: lm-b1a-i-neq-k-j-eq-k (molws (n, l, g, h)

∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1b (n, l, g, h, i, k) ∧ union-at-n (l, i, '(8 9 10 11 12))) → (¬ at (lp, k, 4))

;;;need m-l-same-lp.

Theorem: b1a-i-neq-k-j-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ b1b (n, l, g, h, i, k)) → b1a (lp, i, k)

Theorem: b1a-i-j-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (j ≠ k) ∧ b1a (l, i, j )) → b1a (lp, i, j )

Theorem: b1a-i-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ b1a (l, i, j ) ∧ b1b (n, l, g, h, i, j )) → b1a (lp, i, j )

Theorem: cond-l7 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 7)

∧ union-at-n (lp, k, '(8 9 10 11 12))) → at (g, nth (h, k), 4)

Theorem: k-in-l7-imp (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ at (l, k, 7) ∧ b1a (l, nth (h, k), j ) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → (¬ at (l, j , 4))

Theorem: l5-j-lt-h-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 5) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → (j < nth (h, k))

Theorem: k-in-l5-then-j-not-l4 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 5) ∧ union-at-n (lp, k, '(8 9 10 11 12)) ∧ b0a (n, l, h, k, j )) → (¬ at (l, j , 4))

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

Theorem: k-in-lp9-12-then-j-not-l4 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n))

∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1a (l, k, j ) ∧ union-at-n (lp, k, '(9 10 11 12))) → (¬ at (l, j , 4))

Theorem: k-not-in-l7-then-lp9-12-or-l5 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ union-at-n (lp, k, '(8 9 10 11 12)) ∧ (¬ at (l, k, 7)) ∧ (¬ union-at-n (lp, k, '(9 10 11 12)))) → at (l, k, 5)

Theorem: k-in-not-l7-imp (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (¬ at (l, k, 7)) ∧ b0a (n, l, h, k, j ) ∧ b1a (l, k, j ) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → (¬ at (l, j , 4))

;;;I wonder why the following two do not imply
;;;lm-b1a-i-eq-k-j-neq-k although those without
;;;(member u (nset n)) are perfectly able to
;;;imply it.
;;;(prove-lemma k-in-lp9-12-then-j-not-l4 (rewrite)
;;;   (implies (and (molws n l g h)
;;;                 (member j (nset n))
;;;                 (member k (nset n))
;;;                 (mrhoi n k l g h lp gp hp)
;;;                 (b1a l k j)
;;;                 (union-at-n lp k '(9 10 11 12)))
;;;            (not (at l j 4))))
;;;
;;;(prove-lemma k-in-lp8-then-j-not-l4 (rewrite)
;;;   (implies (and (at lp k 8)
;;;                 (molws n l g h)
;;;                 (member j (nset n))
;;;                 (member u (nset n))
;;;                 (member k (nset n))
;;;                 (mrhoi n k l g h lp gp hp)

;;;                 (lg n l g)
;;;                 (b0a n l h k j)
;;;                 (b1a l (nth h k) j))
;;;            (not (at l j 4))))

Theorem: lm-b1a-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ b0a (n, l, h, k, j ) ∧ b1a (l, k, j ) ∧ b1a (l, nth (h, k), j ) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → (¬ at (l, j , 4))

;;;m-l-same-lp-at-not is used.

Theorem: b1a-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ b0a (n, l, h, k, j ) ∧ b1a (l, k, j ) ∧ b1a (l, nth (h, k), j )) → b1a (lp, k, j )

Theorem: b1a-i-j-eq-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1a (l, k, k)) → b1a (lp, k, k)

Theorem: b1a-i-eq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n))

∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ b0a (n, l, h, k, j ) ∧ b1a (l, k, j ) ∧ b1a (l, nth (h, k), j )) → b1a (lp, k, j )

Theorem: mrho-preserves-b1a (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, i) ∧ lg (n, l, g) ∧ b0a (n, l, h, i, j ) ∧ b1a (l, i, j ) ∧ b1a (l, nth (h, i), j ) ∧ b1b (n, l, g, h, i, j )) → b1a (lp, i, j )

;;;;;;;;;;;;;   b1b   ;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;common in mole and atom.

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

Theorem: l8-11-k-in-gp34 ((r ∈ nset (n)) ∧ lg (n, l, g) ∧ union-at-n (l, r, '(8 9 10 11))) → union-at-n (gp, r, '(3 4))

Theorem: u-if4 ((u ∈ nset (n)) ∧ lg (n, l, g) ∧ at (g, u, 4)) → (¬ at (l, u, 2))

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

Theorem: r-neq-k (union-at-n (l, k, '(8 9 10 11)) ∧ at (l, r, 12)) → (k ≠ r)

;;;;;;;;;;;;;;;;;common in mole and atom end.
;;;;;;;;;;;;;;;;;Lemmas on hints.

Theorem: ex-hint-in-l8-12 exist-hint-8-12-3-4 (n, l, g, h, j ) → union-at-n (l, exist-hint-8-12-3-4 (n, l, g, h, j ), '(8 9 10 11 12))

Theorem: ex-hint-in-g34 exist-hint-8-12-3-4 (n, l, g, h, k) → union-at-n (g, exist-hint-8-12-3-4 (n, l, g, h, k), '(3 4))

Theorem: ex-hint-l-g-h exist-hint-8-12-3-4 (n, l, g, h, j ) → (exist-hint-8-12-3-4 (n, l, g, h, j ) ≮ nth (h, j ))

Theorem: ex-hint-lp-gp-h-in-int-8-12-3-4 exist-hint-8-12-3-4 (n, lp, gp, h, j ) → intersect-8-12-3-4-at-n (exist-hint-8-12-3-4 (n, lp, gp, h, j ), lp, gp)

Theorem: ex-hint-lp-gp-h-leq-h-j exist-hint-8-12-3-4 (n, lp, gp, h, j ) → (exist-hint-8-12-3-4 (n, lp, gp, h, j ) ≮ nth (h, j ))

Theorem: ex-hint-not-in-g02 exist-hint-8-12-3-4 (n, l, g, h, k) → (¬ union-at-n (g, exist-hint-8-12-3-4 (n, l, g, h, k), '(0 1 2)))

Theorem: hint-wtn ((r ∈ nset (n)) ∧ intersect-8-12-3-4-at-n (r, lp, gp) ∧ (r ≮ nth (h, j ))) → exist-hint-8-12-3-4 (n, lp, gp, h, j )

;;;;;;;;;;;;;;;;;Lemmas on hints end.

Theorem: lm-k-in-l7-imp (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ at (l, k, 7) ∧ b1b (n, l, g, h, nth (h, k), j ) ∧ at (l, j , 3) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → exist-hint-8-12-3-4 (n, l, g, h, j )

Theorem: ex-hint-neq-k-imp (molws (n, l, g, h) ∧ (k ∈ nset (n))

∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ exist-hint-8-12-3-4 (n, l, g, h, j ) ∧ (k ≠ exist-hint-8-12-3-4 (n, l, g, h, j ))) → intersect-8-12-3-4-at-n (exist-hint-8-12-3-4 (n, l, g, h, j ), lp, gp)

Theorem: ex-hint-neq-k-in-l7 (at (l, k, 7) ∧ exist-hint-8-12-3-4 (n, l, g, h, j )) → (k ≠ exist-hint-8-12-3-4 (n, l, g, h, j ))

Theorem: ex-hint-in-int-8-12-3-4-l7 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 7) ∧ exist-hint-8-12-3-4 (n, l, g, h, j )) → intersect-8-12-3-4-at-n (exist-hint-8-12-3-4 (n, l, g, h, j ), lp, gp)

Theorem: ex-hint-wtn-l7 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 7) ∧ exist-hint-8-12-3-4 (n, l, g, h, j )) → exist-hint-8-12-3-4 (n, lp, gp, h, j )

Theorem: b1b-k-in-l7-imp (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ at (l, k, 7) ∧ b1b (n, l, g, h, nth (h, k), j ) ∧ at (l, j , 3) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → exist-hint-8-12-3-4 (n, lp, gp, h, j )

Theorem: h-j-leq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, j , 3) ∧ at (l, k, 5) ∧ b0b (n, l, h, k, j )

∧ union-at-n (lp, k, '(8 9 10 11 12))) → (k ≮ nth (h, j ))

Theorem: lm-lp8-then-k-in-g34 (listp (l) ∧ (n ∈ N) ∧ (length (l) = n) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (k ∈ nset (n)) ∧ lg (n, l, g) ∧ at (l, k, 5) ∧ at (lp, k, 8)) → union-at-n (gp, k, '(3 4))

Event: Disable lm-lp8-then-k-in-g34.

Theorem: lp8-then-k-in-g34 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, k, 5) ∧ at (lp, k, 8)) → union-at-n (gp, k, '(3 4))

Theorem: lm-k-in-g34 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ lg (n, lp, gp) ∧ at (l, k, 5) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → union-at-n (gp, k, '(3 4))

Theorem: k-in-g34 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, k, 5) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → union-at-n (gp, k, '(3 4))

Theorem: k-in-int (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, k, 5) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → intersect-8-12-3-4-at-n (k, lp, gp)

Theorem: k-in-l5-imp (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, j , 3) ∧ at (l, k, 5) ∧ b0b (n, l, h, k, j ) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → exist-hint-8-12-3-4 (n, lp, gp, h, j )

;;;This is slow.

Theorem: ex-hint-in-l12 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ union-at-n (l, k, '(8 9 10 11)) ∧ exist-hint-8-12-3-4 (n, l, g, h, j ) ∧ at (l, exist-hint-8-12-3-4 (n, l, g, h, j ), 12)) → intersect-8-12-3-4-at-n (exist-hint-8-12-3-4 (n, l, g, h, j ), lp, gp)

Theorem: r-neq-k-l8-11-k-in-lp8-12 (molws (n, l, g, h) ∧ (r ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (r ≠ k) ∧ union-at-n (l, r, '(8 9 10 11))) → union-at-n (lp, r, '(8 9 10 11))

Theorem: r-eq-k-l8-11-k-in-lp8-12 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp)

∧ union-at-n (l, k, '(8 9 10 11))) → union-at-n (lp, k, '(8 9 10 11 12))

Theorem: l8-11-k-in-lp8-12 (molws (n, l, g, h) ∧ (r ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ union-at-n (l, r, '(8 9 10 11))) → union-at-n (lp, r, '(8 9 10 11 12))

Theorem: hint-in-l8-11 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ exist-hint-8-12-3-4 (n, l, g, h, j ) ∧ union-at-n (l, exist-hint-8-12-3-4 (n, l, g, h, j ), '(8 9 10 11))) → intersect-8-12-3-4-at-n (exist-hint-8-12-3-4 (n, l, g, h, j ), lp, gp)

Theorem: ex-hint-not-in-l12 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ exist-hint-8-12-3-4 (n, l, g, h, j ) ∧ (¬ at (l, exist-hint-8-12-3-4 (n, l, g, h, j ), 12))) → intersect-8-12-3-4-at-n (exist-hint-8-12-3-4 (n, l, g, h, j ), lp, gp)

Theorem: ex-hint-in-int-8-12-3-4-l8-11 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ union-at-n (l, k, '(8 9 10 11)) ∧ exist-hint-8-12-3-4 (n, l, g, h, j )) → intersect-8-12-3-4-at-n (exist-hint-8-12-3-4 (n, l, g, h, j ), lp, gp)

Theorem: ex-hint-wtn-l8-11 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ union-at-n (l, k, '(8 9 10 11)) ∧ exist-hint-8-12-3-4 (n, l, g, h, j )) → exist-hint-8-12-3-4 (n, lp, gp, h, j )

Theorem: k-in-l8-11-imp (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, j , 3) ∧ b1b (n, l, g, h, k, j ) ∧ union-at-n (l, k, '(8 9 10 11))) → exist-hint-8-12-3-4 (n, lp, gp, h, j )

Theorem: m-lp9-12-k-in-l8-11 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ union-at-n (lp, k, '(9 10 11 12))) → union-at-n (l, k, '(8 9 10 11))

Theorem: k-in-lp9-12-imp (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, j , 3) ∧ b1b (n, l, g, h, k, j ) ∧ union-at-n (lp, k, '(9 10 11 12))) → exist-hint-8-12-3-4 (n, lp, gp, h, j )

Theorem: k-not-in-l7-imp (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, j , 3) ∧ (¬ at (l, k, 7)) ∧ b0b (n, l, h, k, j ) ∧ b1b (n, l, g, h, k, j ) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → exist-hint-8-12-3-4 (n, lp, gp, h, j )

Theorem: lm1-b1b-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp)

∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ at (l, j , 3) ∧ b0b (n, l, h, k, j ) ∧ b1b (n, l, g, h, k, j ) ∧ b1b (n, l, g, h, nth (h, k), j ) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → exist-hint-8-12-3-4 (n, lp, gp, h, j )

Theorem: ex-hint-lp-gp-h-leq-hp-j (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ exist-hint-8-12-3-4 (n, lp, gp, h, j )) → (exist-hint-8-12-3-4 (n, lp, gp, h, j ) ≮ nth (hp, j ))

Theorem: j-neq-k-then-hp-eq-h (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ exist-hint-8-12-3-4 (n, lp, gp, h, j )) → exist-hint-8-12-3-4 (n, lp, gp, hp, j )

Theorem: lm-b1b-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ b0b (n, l, h, k, j ) ∧ b1b (n, l, g, h, k, j ) ∧ b1b (n, l, g, h, nth (h, k), j ) ∧ at (l, j , 3) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → exist-hint-8-12-3-4 (n, lp, gp, hp, j )

Theorem: b1b-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n))

∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ b0b (n, l, h, k, j ) ∧ b1b (n, l, g, h, k, j ) ∧ b1b (n, l, g, h, nth (h, k), j )) → b1b (n, lp, gp, hp, k, j )

Theorem: b1b-i-j-eq-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1b (n, l, g, h, k, k)) → b1b (n, lp, gp, hp, k, k)

;;;I wonder if (b1d n l h i) is
;;;better than (b1d n l h k).

Theorem: b1b-i-eq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ b0b (n, l, h, k, j ) ∧ b1b (n, l, g, h, k, j ) ∧ b1b (n, l, g, h, nth (h, k), j )) → b1b (n, lp, gp, hp, k, j )

;;;I wonder why the following two do not imply
;;;lm-b1b-i-neq-k-j-eq-k.
;;;(prove-lemma k-not-in-l3 (rewrite)
;;;   (implies (and (molws n l g h)
;;;                 (member i (nset n))
;;;                 (member k (nset n))
;;;                 (mrhoi n k l g h lp gp hp)
;;;                 (not (equal i k))
;;;                 (lg n l g)
;;;                 (at lp k 3)
;;;                 (not (at l k 3))
;;;                 (union-at-n l i '(8 9 10 11 12)))
;;;         (exist-hint-8-12-3-4 n lp gp hp k)))

;;;
;;;(prove-lemma k-in-l3 (rewrite)
;;;   (implies (and (molws n l g h)
;;;                 (member i (nset n))
;;;                 (member k (nset n))
;;;                 (mrhoi n k l g h lp gp hp)
;;;                 (at l k 3)
;;;                 (at lp k 3)
;;;                 (union-at-n l i '(8 9 10 11 12)))
;;;         (exist-hint-8-12-3-4 n lp gp hp k)))
;;;
;;;(prove-lemma lm-b1b-i-neq-k-j-eq-k (rewrite)
;;;   (implies (and (molws n l g h)
;;;                 (member i (nset n))
;;;                 (member k (nset n))
;;;                 (mrhoi n k l g h lp gp hp)
;;;                 (not (equal i k))
;;;                 (lg n l g)
;;;                 (at lp k 3)
;;;                 (union-at-n l i '(8 9 10 11 12)))
;;;         (exist-hint-8-12-3-4 n lp gp hp k)))

Theorem: ex-hint-leq-h-k exist-hint-8-12-3-4 (n, l, g, h, k) → (exist-hint-8-12-3-4 (n, l, g, h, k) ≮ nth (h, k))

Theorem: h-k-leq-sub1-ex-hint (exist-hint-8-12-3-4 (n, l, g, h, k) ∧ (nth (h, k) ≠ exist-hint-8-12-3-4 (n, l, g, h, k))) → ((exist-hint-8-12-3-4 (n, l, g, h, k) − 1) ≮ nth (h, k))

Theorem: ex-hint-neq-h-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ exist-hint-8-12-3-4 (n, l, g, h, k) ∧ at (l, k, 3) ∧ at (lp, k, 3)) → (nth (h, k) ≠ exist-hint-8-12-3-4 (n, l, g, h, k))

Theorem: lm-hp-k-leq-ex-l-g-h (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp)

∧ at (l, k, 3) ∧ at (lp, k, 3) ∧ exist-hint-8-12-3-4 (n, l, g, h, k)) → ((exist-hint-8-12-3-4 (n, l, g, h, k) − 1) ≮ nth (h, k))

Theorem: ex-cond-l3 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 3) ∧ exist-hint-8-12-3-4 (n, l, g, h, k) ∧ ((exist-hint-8-12-3-4 (n, l, g, h, k) − 1) ≮ nth (h, k))) → (exist-hint-8-12-3-4 (n, l, g, h, k) ≮ nth (hp, k))

Theorem: hp-k-leq-ex-l-g-h (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 3) ∧ at (lp, k, 3) ∧ exist-hint-8-12-3-4 (n, l, g, h, k)) → (exist-hint-8-12-3-4 (n, l, g, h, k) ≮ nth (hp, k))

Theorem: ex-hint-neq-k-in-l3 (at (l, k, 3) ∧ union-at-n (l, exist-hint-8-12-3-4 (n, l, g, h, k), '(8 9 10 11 12))) → (k ≠ exist-hint-8-12-3-4 (n, l, g, h, k))

;;;This is successfully proved
;;;by m-gp-same-g and m-lp-same-l.
;;;This is successfully proved by ex-hint-neq-k-imp,
;;;ex-hint-neq-k-in-l3 and ex-hint-in-l8-12.

Theorem: ex-hint-l-g-h-in-int-8-12-3-4 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 3) ∧ exist-hint-8-12-3-4 (n, l, g, h, k)) → intersect-8-12-3-4-at-n (exist-hint-8-12-3-4 (n, l, g, h, k), lp, gp)

Theorem: ex-l-g-h-k-in-l3 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp)

∧ at (l, k, 3) ∧ at (lp, k, 3) ∧ exist-hint-8-12-3-4 (n, l, g, h, k)) → exist-hint-8-12-3-4 (n, lp, gp, hp, k)

Theorem: lm-k-in-l3 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 3) ∧ at (lp, k, 3) ∧ union-at-n (l, i, '(8 9 10 11 12)) ∧ b1b (n, l, g, h, i, k)) → exist-hint-8-12-3-4 (n, lp, gp, hp, k)

Theorem: k-in-l3 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ at (l, k, 3) ∧ b1b (n, l, g, h, i, k)) → b1b (n, lp, gp, hp, i, k)

Theorem: hp-k-leq-i (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 2) ∧ at (lp, k, 3)) → (i ≮ nth (hp, k))

Theorem: b1b-u-neq-k ((u ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ lg (n, l, g) ∧ at (g, u, 4) ∧ at (l, k, 2)) → (k ≠ u)

Theorem: lm-u-in-int-8-12-3-4 (molws (n, l, g, h)

∧ (u ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, k, 2) ∧ at (g, u, 4) ∧ union-at-n (lp, u, '(8 9 10 11 12))) → intersect-8-12-3-4-at-n (u, lp, gp)

Theorem: k-neq-u-in-lp8-12 (molws (n, l, g, h) ∧ (u ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (u ≠ k) ∧ lg (n, l, g) ∧ at (g, u, 4)) → union-at-n (lp, u, '(8 9 10 11 12))

Theorem: lm1-u-in-int-8-12-3-4 (molws (n, l, g, h) ∧ (u ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, k, 2) ∧ at (g, u, 4)) → union-at-n (lp, u, '(8 9 10 11 12))

Theorem: u-in-int-8-12-3-4 (molws (n, l, g, h) ∧ (u ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, k, 2) ∧ at (g, u, 4)) → intersect-8-12-3-4-at-n (u, lp, gp)

;;;I wonder why the following does not trigger
;;;molws-ln-lp, molws-ln-gp.
;;;(prove-lemma h-i-in-g34-imp (rewrite)
;;;   (implies (and (molws n l g h)
;;;                 (member k (nset n))
;;;                 (mrhoi n k l g h lp gp hp)

;;;                 (member (nth h i) (nset n))
;;;                 (lg n l g)
;;;                 (at l k 2)
;;;                 (at lp k 3)
;;;                 (at g (nth h i) 4))
;;;            (exist-hint-8-12-3-4 n lp gp hp k)))
;;;although
;;;(prove-lemma h-i-in-g34-imp (rewrite)
;;;   (implies (and (member (nth h i) (nset n))
;;;                 (molws n l g h)
;;;                 (member k (nset n))
;;;                 (mrhoi n k l g h lp gp hp)
;;;                 (lg n l g)
;;;                 (at l k 2)
;;;                 (at lp k 3)
;;;                 (at g (nth h i) 4))
;;;            (exist-hint-8-12-3-4 n lp gp hp k)))
;;;does.

Theorem: h-i-in-g34-imp ((nth (h, i) ∈ nset (n)) ∧ molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, k, 2) ∧ at (lp, k, 3) ∧ at (g, nth (h, i), 4)) → exist-hint-8-12-3-4 (n, lp, gp, hp, k)

Theorem: i-not-in-g34 ((¬ union-at-n (g, i, '(3 4))) ∧ molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, k, 2) ∧ at (lp, k, 3) ∧ b1c (n, l, g, h, i) ∧ union-at-n (l, i, '(8 9 10 11 12))) → exist-hint-8-12-3-4 (n, lp, gp, hp, k)

Theorem: i-in-int-8-12-3-4 (union-at-n (g, i, '(3 4)) ∧ molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ union-at-n (l, i, '(8 9 10 11 12))) → intersect-8-12-3-4-at-n (i, lp, gp)

Theorem: i-in-g34 (union-at-n (g, i, '(3 4)) ∧ molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ at (l, k, 2) ∧ at (lp, k, 3) ∧ union-at-n (l, i, '(8 9 10 11 12))) → exist-hint-8-12-3-4 (n, lp, gp, hp, k)

Theorem: k-in-l2 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ at (l, k, 2) ∧ at (lp, k, 3) ∧ b1c (n, l, g, h, i) ∧ union-at-n (l, i, '(8 9 10 11 12))) → exist-hint-8-12-3-4 (n, lp, gp, hp, k)

Theorem: lp3-then-l3-or-l2 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (¬ at (l, k, 3)) ∧ at (lp, k, 3)) → at (l, k, 2)

Theorem: lm-k-not-in-l3 (molws (n, l, g, h)

∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ (¬ at (l, k, 3)) ∧ at (lp, k, 3) ∧ b1c (n, l, g, h, i) ∧ union-at-n (l, i, '(8 9 10 11 12))) → exist-hint-8-12-3-4 (n, lp, gp, hp, k)

Theorem: k-not-in-l3 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ (¬ at (l, k, 3)) ∧ b1b (n, l, g, h, i, k) ∧ b1c (n, l, g, h, i)) → b1b (n, lp, gp, hp, i, k)

Theorem: b1b-i-neq-k-j-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ b1b (n, l, g, h, i, k) ∧ b1c (n, l, g, h, i)) → b1b (n, lp, gp, hp, i, k)

Theorem: lm-i-neq-k-in-int-8-12-3-4 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ at (g, i, 4))

→ intersect-8-12-3-4-at-n (i, lp, gp)

Theorem: i-neq-k-in-int-8-12-3-4 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ union-at-n (l, i, '(8 9 10 11 12)) ∧ lg (n, l, g) ∧ at (l, exist-hint-8-12-3-4 (n, l, g, h, j ), 12) ∧ b3a (l, g, exist-hint-8-12-3-4 (n, l, g, h, j ), i)) → intersect-8-12-3-4-at-n (i, lp, gp)

Theorem: h-j-leq-i (union-at-n (l, i, '(8 9 10 11 12)) ∧ exist-hint-8-12-3-4 (n, l, g, h, j ) ∧ at (l, exist-hint-8-12-3-4 (n, l, g, h, j ), 12) ∧ b2a (l, exist-hint-8-12-3-4 (n, l, g, h, j ), i)) → (i ≮ nth (h, j ))

Theorem: i-neq-k-ex-hint-in-l12 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ union-at-n (l, i, '(8 9 10 11 12)) ∧ exist-hint-8-12-3-4 (n, l, g, h, j ) ∧ at (l, exist-hint-8-12-3-4 (n, l, g, h, j ), 12) ∧ b2a (l, exist-hint-8-12-3-4 (n, l, g, h, j ), i) ∧ b3a (l, g, exist-hint-8-12-3-4 (n, l, g, h, j ), i)) → exist-hint-8-12-3-4 (n, lp, gp, h, j )

Theorem: i-neq-k-ex-hint-not-in-l12 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ exist-hint-8-12-3-4 (n, l, g, h, j ) ∧ (¬ at (l, exist-hint-8-12-3-4 (n, l, g, h, j ), 12))) → exist-hint-8-12-3-4 (n, lp, gp, h, j )

Theorem: lm1-b1b-i-j-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ union-at-n (l, i, '(8 9 10 11 12)) ∧ exist-hint-8-12-3-4 (n, l, g, h, j ) ∧ b2a (l, exist-hint-8-12-3-4 (n, l, g, h, j ), i) ∧ b3a (l, g, exist-hint-8-12-3-4 (n, l, g, h, j ), i)) → exist-hint-8-12-3-4 (n, lp, gp, h, j )

Theorem: lm-b1b-i-j-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ union-at-n (l, i, '(8 9 10 11 12)) ∧ b2a (l, exist-hint-8-12-3-4 (n, l, g, h, j ), i) ∧ b3a (l, g, exist-hint-8-12-3-4 (n, l, g, h, j ), i) ∧ exist-hint-8-12-3-4 (n, l, g, h, j )) → exist-hint-8-12-3-4 (n, lp, gp, hp, j )

Theorem: b1b-i-j-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ b1b (n, l, g, h, i, j ) ∧ b2a (l, exist-hint-8-12-3-4 (n, l, g, h, j ), i) ∧ b3a (l, g, exist-hint-8-12-3-4 (n, l, g, h, j ), i)) → b1b (n, lp, gp, hp, i, j )

Theorem: b1b-i-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n))

∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ b0b (n, l, h, i, j ) ∧ b1b (n, l, g, h, i, j ) ∧ b1c (n, l, g, h, i) ∧ b2a (l, exist-hint-8-12-3-4 (n, l, g, h, j ), i) ∧ b3a (l, g, exist-hint-8-12-3-4 (n, l, g, h, j ), i)) → b1b (n, lp, gp, hp, i, j )

;;;I wonder if (b1d n l h i) and
;;;(b1d n l h j) are better than
;;;(b1d n l h k).
;;;(b1b n l g h (nth h i) j) and (b1b n l g h (nth h k) j).
;;;What about (b2a l (exist-hint-8-12-3-4 n l g h j) i)
;;;           (b3a l g (exist-hint-8-12-3-4 n l g h j) i) ?

Theorem: mrho-preserves-b1b (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ b0b (n, l, h, i, j ) ∧ b1b (n, l, g, h, nth (h, k), j ) ∧ b1b (n, l, g, h, i, j ) ∧ b1c (n, l, g, h, i) ∧ b2a (l, exist-hint-8-12-3-4 (n, l, g, h, j ), i) ∧ b3a (l, g, exist-hint-8-12-3-4 (n, l, g, h, j ), i)) → b1b (n, lp, gp, hp, i, j )

;;;;;;;;;;;;;   b1c   ;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;common in mole and atom.

Theorem: not-g34-then-not-g4 (¬ union-at-n (g, i, '(3 4))) → (¬ at (g, i, 4))

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

;;;;;;;;;;;;;;common in mole and atom end.

Theorem: lp8-not-l5-then-l7 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (¬ at (l, k, 5)) ∧ at (lp, k, 8)) → at (l, k, 7)

Theorem: lp8-not-g34-then-k-in-l7 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (lp, k, 8) ∧ union-at-n (lp, k, '(8 9 10 11 12)) ∧ (¬ union-at-n (gp, k, '(3 4)))) → at (l, k, 7)

Theorem: lm-k-in-l7 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ lg (n, lp, gp) ∧ union-at-n (lp, k, '(8 9 10 11 12)) ∧ (¬ union-at-n (gp, k, '(3 4)))) → at (l, k, 7)

Theorem: k-in-l7 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ union-at-n (lp, k, '(8 9 10 11 12)) ∧ (¬ union-at-n (gp, k, '(3 4)))) → at (l, k, 7)

Theorem: h-k-cond-l7 (molws (n, l, g, h)

∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 7) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → (nth (hp, k) = nth (h, k))

Theorem: lm-h-k-g4 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ at (l, k, 7) ∧ union-at-n (lp, k, '(8 9 10 11 12))) → ((nth (hp, k) ∈ nset (n)) ∧ at (g, nth (hp, k), 4))

Theorem: h-k-g4 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ union-at-n (lp, k, '(8 9 10 11 12)) ∧ (¬ union-at-n (gp, k, '(3 4)))) → ((nth (hp, k) ∈ nset (n)) ∧ at (g, nth (hp, k), 4))

Theorem: lm1-i-eq-k-then-h-k-neq-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ at (l, k, 7) ∧ at (g, nth (hp, k), 4)) → (¬ at (hp, k, k))

;;;Need k-in-l7.

Theorem: lm-i-eq-k-then-h-k-neq-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ at (l, k, 7)

∧ union-at-n (lp, k, '(8 9 10 11 12)) ∧ (¬ union-at-n (gp, k, '(3 4)))) → (¬ at (hp, k, k))

Theorem: i-eq-k-then-h-k-neq-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ union-at-n (lp, k, '(8 9 10 11 12)) ∧ (¬ union-at-n (gp, k, '(3 4)))) → (¬ at (hp, k, k))

Theorem: b1c-i-eq-k-hp-k-neq-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ (¬ at (hp, k, k)) ∧ lg (n, l, g) ∧ union-at-n (lp, k, '(8 9 10 11 12)) ∧ (¬ union-at-n (gp, k, '(3 4)))) → ((nth (hp, k) ∈ nset (n)) ∧ at (gp, nth (hp, k), 4))

Theorem: b1c-i-eq-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ lg (n, l, g)) → b1c (n, lp, gp, hp, k)

Theorem: l9-11-then-in-lp9-12 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (¬ at (l, k, 12)) ∧ union-at-n (l, k, '(9 10 11 12))) → union-at-n (lp, k, '(9 10 11 12))

Theorem: k-in-lp9-12 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp)

∧ lg (n, l, g) ∧ at (g, k, 4) ∧ (¬ at (l, k, 12))) → union-at-n (lp, k, '(9 10 11 12))

Theorem: lm-k-not-in-l12-imp (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ lg (n, lp, gp) ∧ at (g, k, 4) ∧ (¬ at (l, k, 12))) → at (gp, k, 4)

Theorem: k-not-in-l12-imp (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (g, k, 4) ∧ (¬ at (l, k, 12))) → at (gp, k, 4)

Theorem: k-not-in-l12 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b3a (l, g, k, i) ∧ union-at-n (l, i, '(8 9 10 11 12)) ∧ (¬ union-at-n (g, i, '(3 4)))) → (¬ at (l, k, 12))

Theorem: lm1-b1c-i-neq-k-h-i-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (nth (h, i) = k) ∧ lg (n, l, g) ∧ b1c (n, l, g, h, i) ∧ b3a (l, g, nth (h, i), i) ∧ union-at-n (l, i, '(8 9 10 11 12)) ∧ (¬ union-at-n (g, i, '(3 4)))) → at (gp, k, 4)

Theorem: lm-b1c-i-neq-k-h-i-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (h, i, k) ∧ lg (n, l, g) ∧ b1c (n, l, g, h, i) ∧ b3a (l, g, nth (h, i), i) ∧ union-at-n (l, i, '(8 9 10 11 12)) ∧ (¬ union-at-n (g, i, '(3 4)))) → ((nth (h, i) ∈ nset (n)) ∧ at (gp, nth (h, i), 4))

Theorem: b3a-h-rholemma (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ b3a (l, g, nth (h, i), i)) → b3a (l, g, nth (hp, i), i)

;;;m-l-same-lp and m-gp-same-g are used.

Theorem: b1c-i-neq-k-h-i-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ at (h, i, k) ∧ lg (n, l, g) ∧ b1c (n, l, g, h, i) ∧ b3a (l, g, nth (h, i), i)) → b1c (n, lp, gp, hp, i)

Theorem: lm-b1c-i-h-i-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (¬ at (h, i, k)) ∧ b1c (n, l, g, h, i) ∧ union-at-n (l, i, '(8 9 10 11 12)) ∧ (¬ union-at-n (g, i, '(3 4)))) → ((nth (h, i) ∈ nset (n)) ∧ at (gp, nth (h, i), 4))

Theorem: b1c-i-h-i-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (¬ at (h, i, k)) ∧ b1c (n, l, g, h, i)) → b1c (n, lp, gp, hp, i)

Theorem: b1c-i-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ b1c (n, l, g, h, i) ∧ b3a (l, g, nth (h, i), i)) → b1c (n, lp, gp, hp, i)

Theorem: mrho-preserves-b1c (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k) ∧ lg (n, l, g) ∧ b1c (n, l, g, h, i) ∧ b3a (l, g, nth (h, i), i)) → b1c (n, lp, gp, hp, i)

;;;;;;;;;;;;;   b1d   ;;;;;;;;;;;;;;;;

Theorem: remainder-quotient (x mod (1 + x)) = fix (x)

Theorem: lm1-member-remainder (x ≮ n) → ((1 + x) ∉ nset (n − 1))

Theorem: lm-member-remainder ((1 + x) ∈ nset (n − 1)) → ((1 + (x mod n)) ∈ nset (n − 1))

Theorem: member-remainder (j ∈ nset (n)) → ((1 + ((j − 1) mod n)) ∈ nset (n))

Theorem: one-nset (n ≄ 0) → (1 ∈ nset (n))

Theorem: lm-b1d-i-eq-k (listp (l) ∧ listp (h) ∧ (n ∈ N) ∧ (nth (h, k) ∈ N) ∧ (length (l) = n) ∧ (length (h) = n) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k)) → b1d (n, lp, hp, k)

Theorem: b1d-i-eq-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, k)) → b1d (n, lp, hp, k)

Theorem: b1d-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ b1d (n, l, h, i)) → b1d (n, lp, hp, i)

Theorem: mrhoi-preserves-b1d (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1d (n, l, h, i)) → b1d (n, lp, hp, i)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;   b2.ev   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;   b2a   ;;;;;;;;;;;;;;;;
;* i-eq-k-j-neq-k

Theorem: j-lt-h-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j < k) ∧ at (l, k, 9) ∧ union-at-n (lp, k, '(10 11 12))) → (j < nth (h, k))

Theorem: lm-case-k-in-l9 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ (j < k) ∧ b2b (l, h, k, j ) ∧ at (l, k, 9) ∧ (j < nth (h, k)) ∧ union-at-n (lp, k, '(10 11 12))) → (¬ union-at-n (l, j , '(5 6 7 8 9 10 11 12)))

;;;In the rewrite rule a set of hypotheses is replaced
;;;by anther set of formulas. Thus if in a proof
;;;intended beforehand there is a formula belonging to
;;;more than one set of hypotheses which are expected to
;;;be replaced, Bmp is very likely to be unsuccessful.
;;;If j is not equal to k and the k's entry in l is
;;;between 10 and 12, then the j's entry in lp is not
;;;between 5 and 12.

Theorem: case-k-in-l9 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ (j < k) ∧ b2b (l, h, k, j ) ∧ at (l, k, 9) ∧ union-at-n (lp, k, '(10 11 12))) → (¬ union-at-n (lp, j , '(5 6 7 8 9 10 11 12)))

;;;need un10-11-then-un10-12.

Theorem: case-k-in-l10-11 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ (j < k) ∧ b2a (l, k, j ) ∧ union-at-n (l, k, '(10 11))) → (¬ union-at-n (lp, j , '(5 6 7 8 9 10 11 12)))

Theorem: k-in-l10-11-or-l9 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ union-at-n (lp, k, '(10 11 12)) ∧ (¬ union-at-n (l, k, '(10 11)))) → at (l, k, 9)

Theorem: lm-b2a-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ (j < k) ∧ lg (n, l, g) ∧ b2a (l, k, j ) ∧ b2b (l, h, k, j ) ∧ union-at-n (lp, k, '(10 11 12))) → (¬ union-at-n (lp, j , '(5 6 7 8 9 10 11 12)))

;;;I proved
;;;(prove-lemma lm-b2a-i-eq-k-j-neq-k (rewrite)
;;;   (implies (and (molws n l g h)
;;;                 (member j (nset n))
;;;                 (member k (nset n))
;;;                 (mrhoi n k l g h lp gp hp)
;;;                 (not (equal j k))
;;;                 (lessp j k)
;;;                 (lg n l g)
;;;                 (b2a l k j)
;;;                 (b2b l h k j)
;;;                 (union-at-n lp k '(10 11 12)))
;;;             (not (union-at-n l j '(5 6 7 8 9 10 11 12)))))

;;;and tried to prove the following lemma counting on
;;;m-lp-same-l, but it was unsuccessful.

Theorem: b2a-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ (j < k) ∧ lg (n, l, g) ∧ b2b (l, h, k, j ) ∧ b2a (l, k, j )) → b2a (lp, k, j )

;* i-neq-k-j-eq-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: m-k-in-lp5-7-not-l4-then-l5-7 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (¬ 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: m-k-in-lp5-7-then-l5-11 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (¬ 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 k's entry
;;;in l is either 5 or 7.

Theorem: m-lp8-k-in-l57 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (lp, k, 8)) → union-at-n (l, k, '(5 7))

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

Theorem: m-k-in-lp8-then-l5-11 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ 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: m-k-in-lp9-12-then-l5-11 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ 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 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: m-k-in-l5-11 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (¬ 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))

Theorem: m-k-not-in-l4 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (¬ 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)))

Theorem: m-k-not-in-lp5-12 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1a (l, i, 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)))

Theorem: lm-b2a-i-neq-k-j-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (k < i) ∧ b1a (l, i, k) ∧ b2a (l, i, k) ∧ union-at-n (lp, i, '(10 11 12))) → (¬ union-at-n (lp, k, '(5 6 7 8 9 10 11 12)))

Theorem: b2a-i-neq-k-j-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (k < i) ∧ b1a (l, i, k) ∧ b2a (l, i, k)) → b2a (lp, i, k)

;* i-j-neq-k-neq-k

Theorem: b2a-i-j-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (j ≠ k) ∧ (j < i)

∧ b2a (l, i, j )) → b2a (lp, i, j )

Theorem: b2a-i-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (j < i) ∧ b1a (l, i, j ) ∧ b2a (l, i, j ) ∧ b2b (l, h, i, j )) → b2a (lp, i, j )

Theorem: b2a-i-eq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j < k) ∧ lg (n, l, g) ∧ b2a (l, k, j ) ∧ b2b (l, h, k, j )) → b2a (lp, k, j )

Theorem: mrho-preserves-b2a (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j < i) ∧ lg (n, l, g) ∧ b1a (l, i, j ) ∧ b2a (l, i, j ) ∧ b2b (l, h, i, j )) → b2a (lp, i, j )

;;;;;;;;;;;;;   b2b   ;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;Common in atom and mole.

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

;;;;;;;;;;;;;;Common in atom and mole end.

Theorem: lg-nth-h-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (h, k, j ) ∧ union-at-n (g, nth (h, k), '(0 1))) → (¬ union-at-n (l, j , '(5 6 7 8 9 10 11 12)))

Theorem: l9-g01 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (h, k, j ) ∧ at (l, k, 9) ∧ at (lp, k, 9)) → union-at-n (g, nth (h, k), '(0 1))

Theorem: l9-nth-h-k-eq-j (at (h, k, j ) ∧ molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, k, 9) ∧ at (lp, k, 9)) → (¬ union-at-n (l, j , '(5 6 7 8 9 10 11 12)))

Theorem: lm-j-not-in-l5-12 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j < k) ∧ lg (n, l, g) ∧ b2b (l, h, k, j ) ∧ at (l, k, 9) ∧ at (lp, k, 9) ∧ ((j − 1) < nth (h, k))) → (¬ union-at-n (l, j , '(5 6 7 8 9 10 11 12)))

Theorem: cond-l9 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 9) ∧ (j < nth (hp, k))) → ((j − 1) < nth (h, k))

Theorem: j-not-in-l5-12 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j < k) ∧ lg (n, l, g) ∧ b2b (l, h, k, j ) ∧ at (l, k, 9) ∧ at (lp, k, 9) ∧ (j < nth (hp, k))) → (¬ union-at-n (l, j , '(5 6 7 8 9 10 11 12)))

Theorem: k-in-l9 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (lp, k, 9) ∧ (j < nth (hp, k))) → at (l, k, 9)

;;;The order of the hints if crucial.

Theorem: lm-b2b-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ (j < k) ∧ lg (n, l, g) ∧ b2b (l, h, k, j ) ∧ at (lp, k, 9) ∧ (j < nth (hp, k))) → (¬ union-at-n (lp, j , '(5 6 7 8 9 10 11 12)))

Theorem: b2b-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ (j < k) ∧ lg (n, l, g) ∧ b2b (l, h, k, j )) → b2b (lp, hp, k, j )

Theorem: b2b-i-eq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j < k) ∧ lg (n, l, g) ∧ b2b (l, h, k, j )) → b2b (lp, hp, k, j )

Theorem: not-k-in-l5-12-imp (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1a (l, i, k) ∧ at (l, i, 9) ∧ (¬ 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)))

;;;The order of hyptheses is crucial.

Theorem: lm-b2b-i-neq-k-j-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (k < i) ∧ b1a (l, i, k) ∧ b2b (l, h, i, k) ∧ at (l, i, 9) ∧ (k < nth (h, i))) → (¬ union-at-n (lp, k, '(5 6 7 8 9 10 11 12)))

Theorem: b2b-i-neq-k-j-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (k < i) ∧ b1a (l, i, k) ∧ b2b (l, h, i, k)) → b2b (lp, hp, i, k)

;;;The position of (member k (nset n)) is
;;;crucial to trigger rholemmas.

Theorem: b2b-i-j-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (j ≠ k) ∧ (j < i) ∧ b2b (l, h, i, j )) → b2b (lp, hp, i, j )

Theorem: b2b-i-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (j < i) ∧ b1a (l, i, j ) ∧ b2b (l, h, i, j )) → b2b (lp, hp, i, j )

Theorem: mrho-preserves-b2b (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j < i)

∧ lg (n, l, g) ∧ b1a (l, i, j ) ∧ b2b (l, h, i, j )) → b2b (lp, hp, i, j )

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;   b3.ev   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;   b3a   ;;;;;;;;;;;;;;;;
;* i-neq-k-j-eq-k

Theorem: lm-b3a-k-in-l9-11 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b3a (l, g, i, k) ∧ at (l, i, 12) ∧ union-at-n (l, k, '(5 6 7 8 9 10 11))) → union-at-n (l, k, '(9 10 11))

Theorem: b3a-k-in-l9-11 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b1a (l, i, k) ∧ b3a (l, g, i, k) ∧ 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))

Theorem: m-k-in-lp9-12 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ union-at-n (l, k, '(9 10 11))) → union-at-n (lp, k, '(9 10 11 12))

Theorem: lm-b3a-i-neq-k-j-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n))

∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ lg (n, lp, gp) ∧ b1a (l, i, k) ∧ b3a (l, g, i, k) ∧ at (l, i, 12) ∧ union-at-n (lp, k, '(5 6 7 8 9 10 11 12))) → at (gp, k, 4)

Theorem: b3a-i-neq-k-j-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ b1a (l, i, k) ∧ b3a (l, g, i, k)) → b3a (lp, gp, i, k)

;* i-eq-k-j-neq-k

Theorem: cond-lp12 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (lp, k, 12) ∧ at (l, k, 11)) → (j < nth (h, k))

Theorem: b3a-j-in-l5-12 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b3b (l, g, h, k, j ) ∧ 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)

Theorem: m-k-in-l11 (molws (n, l, g, h)

∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (lp, k, 12)) → at (l, k, 11)

Theorem: lm-b3a-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ b3b (l, g, h, k, j ) ∧ at (lp, k, 12) ∧ union-at-n (lp, j , '(5 6 7 8 9 10 11 12))) → at (g, j , 4)

Theorem: b3a-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ b3b (l, g, h, k, j )) → b3a (lp, gp, k, j )

;* i-j-neq-k

Theorem: b3a-i-j-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (j ≠ k) ∧ b3a (l, g, i, j )) → b3a (lp, gp, i, j )

Theorem: b3a-i-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n))

∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ b1a (l, i, j ) ∧ b3a (l, g, i, j )) → b3a (lp, gp, i, j )

;* i-j-eq-k

Theorem: b3a-i-j-eq-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b3a (l, g, k, k) ∧ b3b (l, g, h, k, k)) → b3a (lp, gp, k, k)

Theorem: b3a-i-eq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b3a (l, g, k, j ) ∧ b3b (l, g, h, k, j )) → b3a (lp, gp, k, j )

Theorem: mrho-preserves-b3a (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b1a (l, i, j ) ∧ b3a (l, g, i, j ) ∧ b3b (l, g, h, i, j )) → b3a (lp, gp, i, j )

;;;;;;;;;;;;;   b3b   ;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;common in atom and mole.

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

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

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

;;;;;;;;;;;;;;common in atom and mole end.
;* i-neq-k-j-eq-k

Theorem: lm-b3b-k-in-l9-11 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b3b (l, g, h, i, k) ∧ at (l, i, 11) ∧ (k < nth (h, i)) ∧ union-at-n (l, k, '(5 6 7 8 9 10 11))) → union-at-n (l, k, '(9 10 11))

Theorem: b3b-k-in-l9-11 (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b1a (l, i, k) ∧ b3b (l, g, h, i, k) ∧ lg (n, l, g) ∧ at (l, i, 11) ∧ (k < nth (h, i)) ∧ union-at-n (lp, k, '(5 6 7 8 9 10 11 12))) → union-at-n (l, k, '(9 10 11))

Theorem: lm-b3b-i-neq-k-j-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g)

∧ lg (n, lp, gp) ∧ b1a (l, i, k) ∧ b3b (l, g, h, i, k) ∧ at (l, i, 11) ∧ (k < nth (h, i)) ∧ union-at-n (lp, k, '(5 6 7 8 9 10 11 12))) → at (gp, k, 4)

Theorem: b3b-i-neq-k-j-eq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ b1a (l, i, k) ∧ b3b (l, g, h, i, k)) → b3b (lp, gp, hp, i, k)

;* i-eq-k-j-neq-k

Theorem: j-in-g4 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (h, k, j ) ∧ (¬ union-at-n (g, nth (h, k), '(2 3))) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12))) → at (g, j , 4)

Theorem: l11-g14 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (h, k, j ) ∧ at (l, k, 11) ∧ at (lp, k, 11)) → (¬ union-at-n (g, nth (h, k), '(2 3)))

Theorem: l11-nth-h-k-eq-j (at (h, k, j )

∧ molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ at (l, k, 11) ∧ at (lp, k, 11) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12))) → at (g, j , 4)

Theorem: lm-j-in-l5-12 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b3b (l, g, h, k, j ) ∧ at (l, k, 11) ∧ at (lp, k, 11) ∧ ((j − 1) < nth (h, k)) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12))) → at (g, j , 4)

Theorem: cond-l11 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (l, k, 11) ∧ (j < nth (hp, k))) → ((j − 1) < nth (h, k))

Theorem: j-in-l5-12 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ b3b (l, g, h, k, j ) ∧ at (l, k, 11) ∧ at (lp, k, 11) ∧ (j < nth (hp, k)) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12))) → at (g, j , 4)

Theorem: j-leq-add1k-then-k-not-in-l10 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ b2a (l, k, j ) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12)) ∧ (j ≠ k) ∧ (j < (1 + k))) → (¬ at (l, k, 10))

Theorem: not-j-leq-add1k-then-k-not-in-l10 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (lp, k, 11) ∧ (j < nth (hp, k)) ∧ (j ≮ (1 + k))) → (¬ at (l, k, 10))

;;;The order of (member k (nset n)) and
;;;(member j (nset n)) are switched deliberately.

Theorem: k-not-in-l10 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ b2a (l, k, j ) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12)) ∧ at (lp, k, 11) ∧ (j < nth (hp, k))) → (¬ at (l, k, 10))

Theorem: lp11-then-l11-or-l10 (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ at (lp, k, 11) ∧ (¬ at (l, k, 10))) → at (l, k, 11)

;;;When the order of (member j (nset n)) and

;;;(member k (nset n)) is switched, the order of
;;;hints must be switched, in order to make the proof
;;;successful.

Theorem: b3b-k-in-l11 (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ b2a (l, k, j ) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12)) ∧ at (lp, k, 11) ∧ (j < nth (hp, k))) → at (l, k, 11)

;;;When the order of (member j (nset n)) and
;;;(member k (nset n)) is switched then the order of
;;;hints must be switched in order to make the proof
;;;successful.

Theorem: lm-b3b-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ b2a (l, k, j ) ∧ b3b (l, g, h, k, j ) ∧ at (lp, k, 11) ∧ (j < nth (hp, k)) ∧ union-at-n (l, j , '(5 6 7 8 9 10 11 12))) → at (g, j , 4)

Theorem: b3b-i-eq-k-j-neq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (j ≠ k) ∧ lg (n, l, g) ∧ b3b (l, g, h, k, j ) ∧ b2a (l, k, j )) → b3b (lp, gp, hp, k, j )

Theorem: b3b-i-j-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ (j ≠ k) ∧ b3b (l, g, h, i, j )) → b3b (lp, gp, hp, i, j )

Theorem: b3b-i-neq-k (molws (n, l, g, h) ∧ (i ∈ nset (n)) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ (i ≠ k) ∧ lg (n, l, g) ∧ b1a (l, i, j ) ∧ b3b (l, g, h, i, j )) → b3b (lp, gp, hp, i, j )

Theorem: b3b-i-j-eq-k (molws (n, l, g, h) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b3b (l, g, h, k, k)) → b3b (lp, gp, hp, k, k)

Theorem: b3b-i-eq-k (molws (n, l, g, h) ∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b1a (l, k, j ) ∧ b3b (l, g, h, k, j ) ∧ b2a (l, k, j )) → b3b (lp, gp, hp, k, j )

Theorem: mrho-preserves-b3b (molws (n, l, g, h) ∧ (i ∈ nset (n))

∧ (j ∈ nset (n)) ∧ (k ∈ nset (n)) ∧ mrhoi (n, k, l, g, h, lp, gp, hp) ∧ lg (n, l, g) ∧ b1a (l, i, j ) ∧ b3b (l, g, h, i, j ) ∧ b2a (l, i, j )) → b3b (lp, gp, hp, i, j )

Index

a3-if4, 11 add1-nset, 5 all-union, 2, 13, 21 at, 2–4, 7–19, 25–43, 45–55, 57–69,

71–78, 80–86, 88–91, 93– 96, 98–100, 102–106

b0a, 17, 46–50, 59–62 b0a-i-eq-k, 48 b0a-i-eq-k-j-neq-k, 47 b0a-i-j-eq-k, 48 b0a-i-j-neq-k, 49 b0a-i-neq-k, 49 b0a-i-neq-k-j-eq-k, 49 b0a-if1, 45 b0b, 17, 49–56, 64, 66, 68–70, 80 b0b-i-eq-k, 53 b0b-i-eq-k-j-neq-k, 52 b0b-i-in-l5, 55 b0b-i-j-eq-k, 53 b0b-i-j-neq-k, 56 b0b-i-neq-k, 56 b0b-i-neq-k-j-eq-k, 55 b0b-if1, 50 b0b-if3, 50 b1a, 18, 58–62, 92, 93, 96–99, 101–

103, 107, 108 b1a-i-eq-k, 61 b1a-i-eq-k-j-neq-k, 61 b1a-i-j-eq-k, 61 b1a-i-j-neq-k, 58 b1a-i-neq-k, 58 b1a-i-neq-k-j-eq-k, 58 b1a-if4, 13 b1b, 18, 57, 58, 62–64, 68–70, 73,

77, 79, 80 b1b-i-eq-k, 70 b1b-i-eq-k-j-neq-k, 69 b1b-i-j-eq-k, 70 b1b-i-j-neq-k, 79 b1b-i-neq-k, 79 b1b-i-neq-k-j-eq-k, 77 b1b-k-in-l7-imp, 64 b1b-u-neq-k, 73 b1c, 18, 75–77, 80, 83–86 b1c-i-eq-k, 83 b1c-i-eq-k-hp-k-neq-k, 83 b1c-i-h-i-neq-k, 86 b1c-i-neq-k, 86 b1c-i-neq-k-h-i-eq-k, 85 b1d, 18, 59, 61–64, 69, 70, 76, 77,

80, 82, 83, 86, 87 b1d-i-eq-k, 87 b1d-neq-k, 87 b2a, 19, 78–80, 89, 90, 92, 93, 105–

108 b2a-i-eq-k, 93 b2a-i-eq-k-j-neq-k, 90 b2a-i-j-neq-k, 92 b2a-i-neq-k, 93 b2a-i-neq-k-j-eq-k, 92 b2b, 19, 88–90, 93–98 b2b-i-eq-k, 96 b2b-i-eq-k-j-neq-k, 96 b2b-i-j-neq-k, 97 b2b-i-neq-k, 97 b2b-i-neq-k-j-eq-k, 97 b3a, 19, 78–80, 84–86, 98–101 b3a-h-rholemma, 85 b3a-i-eq-k, 101 b3a-i-eq-k-j-neq-k, 100 b3a-i-j-eq-k, 101 b3a-i-j-neq-k, 100 b3a-i-neq-k, 100 b3a-i-neq-k-j-eq-k, 99 b3a-j-in-l5-12, 99 b3a-k-in-l9-11, 98 b3b, 19, 99–104, 106–108 b3b-i-eq-k, 107 b3b-i-eq-k-j-neq-k, 106 b3b-i-j-eq-k, 107 b3b-i-j-neq-k, 107 b3b-i-neq-k, 107 b3b-i-neq-k-j-eq-k, 103 b3b-k-in-l11, 106 b3b-k-in-l9-11, 102

case-k, 8 case-k-in-l10-11, 89 case-k-in-l9, 88 cond-l11, 104 cond-l3, 54 cond-l5, 47 cond-l7, 58 cond-l9, 95 cond-lp12, 99 cond-lp4, 48 contra-if4, 81

ex-cond-l3, 72 ex-hint-in-g34, 63 ex-hint-in-int-8-12-3-4-l7, 64 ex-hint-in-int-8-12-3-4-l8-11, 67 ex-hint-in-l12, 66 ex-hint-in-l8-12, 63 ex-hint-l-g-h, 63 ex-hint-l-g-h-in-int-8-12-3-4, 72 ex-hint-leq-h-k, 71 ex-hint-lp-gp-h-in-int-8-12-3-4, 63 ex-hint-lp-gp-h-leq-h-j, 63 ex-hint-lp-gp-h-leq-hp-j, 69 ex-hint-neq-h-k, 71 ex-hint-neq-k-imp, 63 ex-hint-neq-k-in-l3, 72 ex-hint-neq-k-in-l7, 64 ex-hint-not-in-g02, 63 ex-hint-not-in-l12, 67 ex-hint-wtn-l7, 64 ex-hint-wtn-l8-11, 67 ex-if4, 6 ex-l-g-h-k-in-l3, 72 ex-lp8-12-in-lp8-12, 6 ex-lp8-12-not-in-lp0, 9 exist-hint-8-12-3-4, 18, 19, 57, 63,

64, 66–69, 71–73, 75–80 exist-intersect-8-12-3-4, 3, 6–8 exist-union, 3, 6, 7, 9, 11, 12

g-mrholemma, 22 gp3-then-un34, 8

h-i-in-g34-imp, 75

h-j-leq-i, 78 h-j-leq-k, 64 h-k-cond-l7, 81 h-k-eq-add1-n, 57 h-k-eq-add1-n-k-not-in-l3, 57 h-k-eq-add1-n-nex-hint, 57 h-k-g02, 53 h-k-g4, 82 h-k-leq-sub1-ex-hint, 71 h-k-neq-add1-n, 57 h-k-not-g1, 50 h-mrholemma, 22 hint-8-12-3-4-at-n, 18 hint-in-l8-11, 67 hint-member, 19 hint-wtn, 63 hp-k-leq-ex-l-g-h, 72 hp-k-leq-i, 73

i-eq-k-then-h-k-neq-k, 83

i-in-g34, 76

i-in-int-8-12-3-4, 76

i-in-l5, 48 i-neq-h-k, 53 i-neq-k-ex-hint-in-l12, 78 i-neq-k-ex-hint-not-in-l12, 78 i-neq-k-in-int-8-12-3-4, 78 i-not-in-g34, 75 i-not-in-l12, 12 i-not-l10-12, 11 if1, 10 if1-nth-h-k, 45 if3, 12 if4, 9 int-8-12-3-4-then-un34, 7 int-wtn, 7 intersect-8-12-3-4-at-n, 3, 7, 18, 63,

64, 66, 67, 72, 74, 76, 78 intersect-8-12-3-4-then-3-4, 8 intersect-8-12-3-4-then-8-12, 8

j-ex-l8-12, 6 j-in-g4, 103 j-in-l3, 52 j-in-l5-12, 104 j-leq-add1k-then-k-not-in-l10, 105 j-lt-h-k, 88 j-neq-h-k, 51 j-neq-k-then-hp-eq-h, 69 j-not-in-l4, 47 j-not-in-l5-12, 95

k-in-g34, 65 k-in-int, 66 k-in-l10-11-or-l9, 89 k-in-l2, 76 k-in-l2-imp, 55 k-in-l3, 73 k-in-l3-imp, 54 k-in-l5, 47 k-in-l5-11-g4-then-l9-11, 11 k-in-l5-imp, 66 k-in-l5-then-j-not-l4, 59 k-in-l7, 81 k-in-l7-imp, 59 k-in-l8-11-imp, 68 k-in-l9, 95 k-in-lp5-7-or-lp8-or-lp9-12, 10 k-in-lp9-12, 83 k-in-lp9-12-imp, 68 k-in-lp9-12-or-lp8, 9 k-in-lp9-12-then-j-not-l4, 59 k-in-not-l7-imp, 60 k-neq-u-in-lp8-12, 74 k-not-0, 6 k-not-in-l10, 105 k-not-in-l12, 84 k-not-in-l12-imp, 84 k-not-in-l3, 77 k-not-in-l7-imp, 68 k-not-in-l7-then-lp9-12-or-l5, 60

l-mrholemma, 21 l10-then-un10-12, 102 l11-g14, 103 l11-nth-h-k-eq-j, 103 l11-then-un10-12, 12 l11-then-un8-12, 102 l11-then-un9-12, 102 l12-then-un10-12, 62 l12-then-un8-12, 12 l12-then-un9-12, 12 l34-empty, 7 l5-12-eq-l5-8-or-l9-12, 12 l5-j-lt-h-k, 59 l5-j-lt-nth-k, 46 l5-not-g1, 45 l5-nth-h-k-eq-j, 46 l8-11-k-in-gp34, 62 l8-11-k-in-lp8-12, 67 l9-11-then-in-lp9-12, 83 l9-g01, 94 l9-nth-h-k-eq-j, 94 l9-then-un8-12, 93 length, 2, 5, 13, 20–22, 26–43, 65,

87 lg, 4, 6–13, 26–48, 50–56, 59, 61–70,

73–86, 89, 90, 93–96, 98– 104, 106–108

lg-1-at-n, 3, 4 lg-2-at-n, 4 lg-3-at-n, 4 lg-at-mrhoi0, 26 lg-at-mrhoi10, 40 lg-at-mrhoi11a, 42 lg-at-mrhoi12, 43 lg-at-mrhoi1a, 27 lg-at-mrhoi2, 29 lg-at-mrhoi3a, 30 lg-at-mrhoi4, 31 lg-at-mrhoi5a, 33 lg-at-mrhoi5b, 34 lg-at-mrhoi6, 35 lg-at-mrhoi7a, 36 lg-at-mrhoi8, 38 lg-at-mrhoi9a, 39 lg-at-n, 4, 26–43 lg-l5-g3, 8 lg-mrhoi0, 26 lg-mrhoi10, 41 lg-mrhoi11a, 42 lg-mrhoi12, 43 lg-mrhoi1a, 28 lg-mrhoi2, 29 lg-mrhoi3a, 30 lg-mrhoi4, 32 lg-mrhoi5a, 33 lg-mrhoi5b, 34 lg-mrhoi6, 35 lg-mrhoi7a, 37 lg-mrhoi8, 38 lg-mrhoi9a, 39 lg-nth-h-k, 94 list-ln, 5 lm-b0a-i-eq-k-j-neq-k, 47 lm-b0a-i-neq-k-j-eq-k, 49 lm-b0b-i-eq-k-j-neq-k, 52 lm-b0b-i-neq-k-j-eq-k, 55 lm-b1a-i-eq-k-j-neq-k, 61 lm-b1a-i-neq-k-j-eq-k, 57 lm-b1b-i-eq-k-j-neq-k, 69 lm-b1b-i-j-neq-k, 79 lm-b1c-i-h-i-neq-k, 85 lm-b1c-i-neq-k-h-i-eq-k, 85 lm-b1d-i-eq-k, 87 lm-b2a-i-eq-k-j-neq-k, 89 lm-b2a-i-neq-k-j-eq-k, 92 lm-b2b-i-eq-k-j-neq-k, 95 lm-b2b-i-neq-k-j-eq-k, 96 lm-b3a-i-eq-k-j-neq-k, 100 lm-b3a-i-neq-k-j-eq-k, 98 lm-b3a-k-in-l9-11, 98 lm-b3b-i-eq-k-j-neq-k, 106 lm-b3b-i-neq-k-j-eq-k, 102 lm-b3b-k-in-l9-11, 102 lm-case-k-in-l9, 88 lm-g-mrholemma, 22 lm-h-k-eq-add1-n-nex-hint, 57 lm-h-k-g4, 82 lm-h-mrholemma, 22 lm-hp-k-leq-ex-l-g-h, 71 lm-i-eq-k-then-h-k-neq-k, 82 lm-i-neq-h-k, 53 lm-i-neq-k-in-int-8-12-3-4, 77 lm-j-in-l3, 51 lm-j-in-l5-12, 104 lm-j-neq-h-k, 50 lm-j-not-in-l4, 46 lm-j-not-in-l5-12, 94 lm-k-in-g34, 65 lm-k-in-l3, 73 lm-k-in-l3-imp, 54 lm-k-in-l7, 81 lm-k-in-l7-imp, 63 lm-k-not-in-l12-imp, 84 lm-k-not-in-l3, 76 lm-l-mrholemma, 21 lm-lp8-then-k-in-g34, 65 lm-member-remainder, 86 lm-nth-numberp, 21 lm-u-in-int-8-12-3-4, 73 lm1-b1b-i-eq-k-j-neq-k, 68 lm1-b1b-i-j-neq-k, 79 lm1-b1c-i-neq-k-h-i-eq-k, 84 lm1-i-eq-k-then-h-k-neq-k, 82 lm1-j-in-l3, 51 lm1-k-in-l3-imp, 54 lm1-member-remainder, 86 lm1-u-in-int-8-12-3-4, 74 lp11-then-l11-or-l10, 105 lp3-then-l2-or-l3, 55 lp3-then-l3-or-l2, 76 lp4-then-un34, 7 lp8-not-g34-then-k-in-l7, 81 lp8-not-l5-then-l7, 81 lp8-then-k-in-g34, 65 lp9-12-k-in-l8-12, 59 lp9-12-then-k-in-g34, 13

m-g-same-gp, 24 m-gp-same-g, 23 m-gp-same-g-at, 25 m-gp-same-g-not, 24 m-h-same-hp, 25 m-hp-same-h, 24 m-k-in-l11, 99 m-k-in-l5-11, 91 m-k-in-lp5-7-not-l4-then-l5-7, 90 m-k-in-lp5-7-then-l5-11, 90 m-k-in-lp8-then-l5-11, 91 m-k-in-lp9-12, 98 m-k-in-lp9-12-then-l5-11, 91 m-k-not-in-l4, 91 m-k-not-in-lp5-12, 92 m-l-same-lp, 23 m-l-same-lp-at, 25 m-l-same-lp-at-not, 25 m-lp-same-l, 23 m-lp-same-l-not, 23 m-lp8-k-in-l57, 91 m-lp9-12-k-in-l8-11, 68 member-ex-union, 6 member-intersect, 6 member-remainder, 86 molws, 13, 20–25, 27–34, 36–38, 40–

42, 44–107 molws-list-g, 20 molws-list-h, 20 molws-list-l, 20 molws-ln-g, 20 molws-ln-gp, 20 molws-ln-h, 20 molws-ln-hp, 21 molws-ln-l, 20 molws-ln-lp, 20 molws-n-not-0, 21 molws-num-k, 21 molws-num-n, 20 molws-union-h, 21 move, 2, 5, 13–17, 26–43 move-is-list, 5 move-nth, 5 move-unchange-length, 5 move-unchange-other-than-nth, 5 mrho-preserves-b1a, 62 mrho-preserves-b1b, 80 mrho-preserves-b1c, 86 mrho-preserves-b2a, 93 mrho-preserves-b2b, 97 mrho-preserves-b3a, 101 mrho-preserves-b3b, 107 mrho-preserves-lg, 44 mrhoi, 17, 20–25, 44–108 mrhoi-preserves-b1d, 87 mrhoi0, 13, 17, 27 mrhoi0-preserves-lg, 27 mrhoi10, 16, 17, 41 mrhoi10-preserves-lg, 41 mrhoi11a, 16, 17, 42 mrhoi11a-preserves-lg, 42 mrhoi11b, 16, 17, 42 mrhoi11b-preserves-lg, 42 mrhoi12, 16, 17, 44 mrhoi12-preserves-lg, 44 mrhoi1a, 14, 17, 28 mrhoi1a-preserves-lg, 28 mrhoi1b, 14, 17, 28 mrhoi1b-preserves-lg, 28 mrhoi2, 14, 17, 29 mrhoi2-preserves-lg, 29 mrhoi3a, 14, 17, 30 mrhoi3a-preserves-lg, 30 mrhoi3b, 14, 17, 31 mrhoi3b-preserves-lg, 31 mrhoi4, 14, 17, 32 mrhoi4-preserves-lg, 32 mrhoi5a, 14, 17, 33 mrhoi5a-preserves-lg, 33 mrhoi5b, 15, 17, 34 mrhoi5b-preserves-lg, 34 mrhoi5c, 15, 17, 35 mrhoi5c-preserves-lg, 34 mrhoi6, 15, 17, 36 mrhoi6-preserves-lg, 36 mrhoi7a, 15, 17, 37 mrhoi7a-preserves-lg, 37 mrhoi7b, 15, 17, 37 mrhoi7b-preserves-lg, 37 mrhoi8, 15, 17, 38 mrhoi8-preserves-lg, 38 mrhoi9a, 16, 17, 40 mrhoi9a-preserves-lg, 40 mrhoi9b, 16, 17, 40 mrhoi9b-preserves-lg, 40

n-eq-k-mrhoi0, 26 n-eq-k-mrhoi10, 40 n-eq-k-mrhoi11a, 41 n-eq-k-mrhoi12, 43 n-eq-k-mrhoi1a, 27 n-eq-k-mrhoi2, 28 n-eq-k-mrhoi3a, 30 n-eq-k-mrhoi4, 31 n-eq-k-mrhoi5a, 32 n-eq-k-mrhoi5b, 34 n-eq-k-mrhoi6, 35 n-eq-k-mrhoi7a, 36 n-eq-k-mrhoi8, 38 n-eq-k-mrhoi9a, 39 n-in-nset, 5 n-k-leq-sub1-i, 51 n-neq-k-mrhoi0, 26 n-neq-k-mrhoi10, 40 n-neq-k-mrhoi11a, 41 n-neq-k-mrhoi12, 43 n-neq-k-mrhoi1a, 27 n-neq-k-mrhoi2, 28 n-neq-k-mrhoi3a, 29 n-neq-k-mrhoi4, 31 n-neq-k-mrhoi5a, 32 n-neq-k-mrhoi5b, 33 n-neq-k-mrhoi6, 35 n-neq-k-mrhoi7a, 36 n-neq-k-mrhoi8, 37 n-neq-k-mrhoi9a, 39 n-not-less-j, 19 not-g34-then-not-g4, 80 not-j-leq-add1k-then-k-not-in-l

10, 105 not-k-in-l5-12-imp, 96 not-l3-then-lp4, 48 not-l3-then-not-lp4, 57 nset, 4–13, 18–108 nset-number, 5 nth, 1, 2, 5, 14–19, 21, 22, 45–55,

57, 59, 61–65, 69–73, 75, 78, 80, 82–88, 94–96, 99, 102–106

nth-k-lt-j-or-eq-j, 46 nth-numberp, 21 number-ex-union, 6 number-intersect, 6

one-nset, 87

r-eq-k-l8-11-k-in-lp8-12, 66

r-neq-k, 62

r-neq-k-l8-11-k-in-lp8-12, 66 remainder-quotient, 86 rho-preserves-b0a, 50 rho-preserves-b0b, 56

u-if4, 62

u-in-int-8-12-3-4, 74

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-11-then-un8-12, 62 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–14, 16, 18, 19,

23–25, 50, 53, 57–69, 72– 85, 88–96, 98–100, 102–106

zero-not-member-nset, 5