Using SET-VAR to Prove the Heine Borel Theorem W. W. Bledsoe ATP 120 25 January 1994 $$$$ 6May94: See note on Page 2. $$$$ Theorem (Heine-Borel). If G is a family of open sets on the real line which cover the closed interval [a,b], then some finite subset H of G also covers [a,b]. The least-upper-bound axiom (LUB), or something equivalent to it is needed for the proof. LUB: If A is a non-empty, bounded-above subset of real numbers, then A has a least upper bound. When we describe a version of a theorem to be proved, that version will depend on the lemmas that are given for the proof. Our version uses LUB and Lemmas 0-20 shown below. The following is a "hand-proof" of HB, our version of the Heine-Borel Theorem, done by the computer (SPARCstation ELC), but using a set of instructions (prepared by the author) to our SET-VAR program, [1],[2]. The proof was first done by hand, using resolution, equality substitution, and the rules of SET-VAR; and then done interactively by the computer. Instead of using the Rule1 of [1], we here use Rule1-g, a generalization of Rule1. (See [3]). This Rule1-g is the "Old Rule1" that we first worked with in the late 1980's (which I presented at my CADE-1990 after-dinner talk), and later simplified to the Rule1 of [1]. Rule1 is a special case of Rule1-g, and not vice versa, and it now appears that Rule1-g is needed for difficult theorems like the Heine Borel theorem. (It also appears that we need two more "combining rules" for the completeness of SET-VAR. See [3]) Here is a special case of Rule1-g, the only SET-VAR rule that is used in this HB proof. Rule1-g. 1. X(A) e A v Cr(A) 2. ~P(x(A)u) v ~Q(u) v ~R(u) v Cr'(A) -------------------------------------- 3. A ~<< {z: SOME [P(z,u) ^ Q(u) ^ R(u)]} v Cr(A) v Cr'(A) (In this paper the expression, (D << E), means "D is a subset of E", and (D ~<< E), means "D is not a subset of E". Similarly for >>.) $$$$ 6May94. NOTE: $$$$ We now feel that the use of this version of Rule1, namely Rule1-v (given below), instead of the Rule1-g (given above), will work just as well for the proof of the Heine-Borel theorem. And, not only that, but this revised version, Rule1-v, is much more useful in other applications such as the revised search strategy, CAAT. See ATP.122. This revised version is simply the same as Rule1-g, except the quantifier, SOME u is removed. Rule1-v. 1. X(A) e A v Cr(A) 2. ~P(x(A),u) v ~Q(u) v ~R(u) v Cr'(A) -------------------------------------- 3. A ~<< {z: [P(z,u) ^ Q(u) ^ R(u)]} v Cr(A) v Cr'(A) In the following proof, one line often represents more than one resolution step. This was done because a single-step presentation is so very long. For example, Step 20 of the proof, 20 ((NOT (SUBSET H (G0))) (NOT (E B (G0))) (NOT (FINITE H)) (NOT (SUBSET (NT (A0) Z) (UNION H))) (NOT (SUBSET (NT A* (B0)) B)) (NOT (<= A* Z))) (4 (1 2 3) ((L13 3) (L12 2) (L9 4)) RES-MULTIPLE) represents the resolution of Clause 4 against Clauses L13, L12, and L9, upon Literals 1, 2, and 3 of Clause 4, and Literal 3, 2, and 4 of Clauses L13,L12, and L9. Both the single step and the multiple step versions were done by the computer, the latter producing the output shown below. We list here, in LISP notation, the input clauses, 1-4, for HB, (the Heine-Borel Theorem), along with Clauses 5-8 for LUB, and L0-L20 for the lemmas. And that is followed by the computer generated proof. Here are the input clauses, lemmas, and resolvents that lead to []. This is the "^" version, where we allow conjoined literals. For example, Clause 13, 13 ((NOT (E R A)) (^ (E (ZS A Y) A) (NOT (<= (ZS A Y) Y))) (<= (LS A) Y)) is a shortened representation of the two clauses 13.1 ((NOT (E R A)) (E (ZS A Y) A) (<= (LS A) Y)) 13.2 ((NOT (E R A)) (NOT (<= (ZS A Y) Y)) (<= (LS A) Y)) ------------------------------------------------------------------ (setq ClausesA-HB& '( (1 ( (<= (a0) (b0)) )) (2 ( (not (e B (G0))) (open B))) (3 ( (subset (nt (a0) (b0)) (union (G0))))) (4 ( (not (subset H (G0))) (not (finite H)) (not (subset (nt (a0) (b0)) (union H))))) (5 ( (e (xS A) A) (not (e x A)) (<= x (Ls A)))) ;Not needed (6 ( (not (<= (xS A) u)) (not (e x A)) (<= x (Ls A)))) (7 ( (e (xS A) A) (not (e r A)) ;Not needed (^ (e (zS A y) A) (not (<= (zS A y) y))) (<= (Ls A) y))) (8 ( (not (<= (xS A) u)) (not (e r A)) (^ (e (zS A y) A) (not (<= (zS A y) y))) (<= (Ls A) y))) ;;--Lemmas-- -------------------------------------------------------------- (L0 ( (not (<= l b)) (= l b) (< l b))) ;;L1. a<=b ^ [a b]subset(union G) --> Some B1,B2 [(B1eG ^ aeB1)^(B2eG ^ beB2)] (L1 ( (not (<= a1 b1)) (not (subset (nt a1 b1) (union G))) (^ (e (B1S a1 b1 G) G) (e a1 (B1S a1 b1 G)) (e (B2S a1 b1 G) G) (e b1 (B2S a1 b1 G))))) ;;L2. BeG -> {B}subset G (L2 ( (not (e B G)) (subset (sng B) G))) ;;L3. aeB -> [a a] subset union{B} (L3 ( (not (e a3 B)) (subset (nt a3 a3) (union (sng B))))) ;;L4. finite{B} (L4 ( (finite (sng B)))) ;;L5. a<=L<=b -> Le[a b] (L5 ( (not (<= a5 L)) (not (<= L b5)) (e L (nt a5 b5)))) ;;L6. xeB ^ Bsubset D -> xeD (L6 ( (not (e x B)) (not (subset B D)) (e x D))) ;;L7.(e a1 (B1S a1 b1 G)) xe(union G) --> some B(BeG ^ xeB) (L7 ( (not (e x (union G))) (^ (e (B3s x G) G) (e x (B3s x G))))) ;;L8. L Some a2,b2(a2 ;; [a' b']subset(union(H' U {B})) (L9 ( (not (subset (nt a9 z) (union H*))) (not (subset (nt a* b*) B)) (not (<= a* z)) (subset (nt a9 b*) (union (U H* (sng B)))))) ;;L11. [a' b]subset B ^ a'<=a --> [a b]subset B (L11 ( (not (subset (nt a* b) B)) (not (<= a* a11)) (subset (nt a11 b) B))) ;;L12. finite G --> finite(G U {B}) (L12 ( (not (finite G)) (finite (U G (sng B))))) ;;L13. H subset G ^ BeG --> (H U {B})subset G (L13 ( (not (subset H G)) (not (e B G)) (subset (U H (sng B)) G))) ;;L14. LeB ^ open B --> Some a4(a4 x <= y (L15 ( (<= y x) (<= x y))) ;;L16. x < y <-> y ~<= x (L16 ( (not (< x y)) (not (<= y x)))) ;;L17. [x y] subset B ^ u <= y --> [x u] subset B (L17 ( (not (subset (nt x y) B)) (not (<= u y)) (subset (nt x u) B))) ;;L18. l < b v l = b v b < l (L18 ( (< l b) (= l b) (< b l))) ;;L19. x e B --> [x x] subset B (L19 ( (not (e x B)) (subset (nt x x) B))) ;;L20. All x Some y (x <= y) (L20 ( (<= x (ys x)))) )) -------------------------------------------------------------------- -------------------------------------------------------------------- Computer Output of the proof: 1 ((<= (A0) (B0))) INPUT 2 ((NOT (E B (G0))) (OPEN B)) INPUT 3 ((SUBSET (NT (A0) (B0)) (UNION (G0)))) INPUT 4 ((NOT (SUBSET H (G0))) (NOT (FINITE H)) (NOT (SUBSET (NT (A0) (B0)) (UNION H)))) INPUT 5 ((E (XS A) A) (NOT (E X A)) (<= X (LS A))) INPUT 6 ((NOT (<= (XS A) U)) (NOT (E X A)) (<= X (LS A))) INPUT 7 ((E (XS A) A) (NOT (E R A)) (^ (E (ZS A Y) A) (NOT (<= (ZS A Y) Y))) (<= (LS A) Y)) INPUT 8 ((NOT (<= (XS A) U)) (NOT (E R A)) (^ (E (ZS A Y) A) (NOT (<= (ZS A Y) Y))) (<= (LS A) Y)) INPUT L0 ((NOT (<= L B)) (= L B) (< L B)) INPUT L1 ((NOT (<= A1 B1)) (NOT (SUBSET (NT A1 B1) (UNION G))) (^ (E (B1S A1 B1 G) G) (E A1 (B1S A1 B1 G)) (E (B2S A1 B1 G) G) (E B1 (B2S A1 B1 G)))) INPUT L2 ((NOT (E B G)) (SUBSET (SNG B) G)) INPUT L3 ((NOT (E A3 B)) (SUBSET (NT A3 A3) (UNION (SNG B)))) INPUT L4 ((FINITE (SNG B))) INPUT L5 ((NOT (<= A5 L)) (NOT (<= L B5)) (E L (NT A5 B5))) INPUT L6 ((NOT (E X B)) (NOT (SUBSET B D)) (E X D)) INPUT L7 ((NOT (E X (UNION G))) (^ (E (B3S X G) G) (E X (B3S X G)))) INPUT L8 ((<= B8 L) (NOT (E L B)) (NOT (OPEN B)) (^ (NOT (<= L (A2S B8 L B))) (NOT (<= (B2S B8 L B) L)) (<= (B2S B8 L B) B8) (SUBSET (NT (A2S B8 L B) (B2S B8 L B)) B))) INPUT L9 ((NOT (SUBSET (NT A9 Z) (UNION H*))) (NOT (SUBSET (NT A* B*) B)) (NOT (<= A* Z)) (SUBSET (NT A9 B*) (UNION (U H* (SNG B))))) INPUT L11 ((NOT (SUBSET (NT A* B) B)) (NOT (<= A* A11)) (SUBSET (NT A11 B) B)) INPUT L12 ((NOT (FINITE G)) (FINITE (U G (SNG B)))) INPUT L13 ((NOT (SUBSET H G)) (NOT (E B G)) (SUBSET (U H (SNG B)) G)) INPUT L14 ((NOT (E L B)) (NOT (OPEN B)) (^ (NOT (<= L (A4S L B))) (SUBSET (NT (A4S L B) L) B))) INPUT L15 ((<= Y X) (<= X Y)) INPUT L16 ((NOT (< X Y)) (NOT (<= Y X))) INPUT L17 ((NOT (SUBSET (NT X Y) B)) (NOT (<= U Y)) (SUBSET (NT X U) B)) INPUT L18 ((< L B) (= L B) (< B L)) INPUT L19 ((NOT (E X B)) (SUBSET (NT X X) B)) INPUT L20 ((<= X (YS X))) INPUT ----------------------------------------------------------------- ----------------------------------------------------------------- For each of the following proof "lines" (produced by the computer), we show the produced resolvent along with the explanation of how that resolvent was obtained. For example, ((6 1) (L20 1) RES), simply means that Clause 6 was resolved upon Literal 1, with Clause L20 upon Leteral 1. As mentioned above, we also show several resolvents done at once, using the notation "RES-MULTIPLE". Also, we use notations: RULE1-g, SUB=, COLLAPSE, SIMP, and COMBINE-RESOLVENTS, all of which are rather obvious except RULE1-g and COLLAPSE. RULE1-g is explained after Step 22 below, and COLLAPSE is explained after Line 36C. Resolvents: 11 ((NOT (E X A)) (<= X (LS A))) ((6 1) (L20 1) RES) 13 ((NOT (E R A)) (^ (E (ZS A Y) A) (NOT (<= (ZS A Y) Y))) (<= (LS A) Y)) ((8 1) (L20 1) RES) 20 ((NOT (SUBSET H (G0))) (NOT (E B (G0))) (NOT (FINITE H)) (NOT (SUBSET (NT (A0) Z) (UNION H))) (NOT (SUBSET (NT A* (B0)) B)) (NOT (<= A* Z))) (4 (1 2 3) ((L13 3) (L12 2) (L9 4)) RES-MULTIPLE) 21P ((NOT (E R A)) (<= (LS A) Y) (<= Y (ZS A Y))) ((13 2 (^ 2)) (L15 1) RES) 21 ((NOT (E R A)) (<= (LS A) Y) (NOT (SUBSET H (G0))) (NOT (E B (G0))) (NOT (FINITE H)) (NOT (SUBSET (NT (A0) (ZS A Y)) (UNION H))) (NOT (SUBSET (NT Y (B0)) B))) ((21P 3) (20 6) RES) 22 ((NOT (SUBSET A (AA))) (<= (LS A) Y) (NOT (E R A)) (NOT (E B (G0))) (NOT (SUBSET (NT Y (B0)) B))) ((13 2 (^ 1)) (21 6 (ZS A Y)) RULE1-g) NOTE: First, for shortness we use here the notation, (AA), to represent the set-value, (SET-OF Z% (SOME H (^ (SUBSET H (G0)) (FINITE H) (SUBSET (NT (A0) Z%) (UNION H))))) And use that same notation for the rest of the proof. So actually, Clause 22 is 22 ((not (subset A (SET-OF Z% (SOME H (^ (SUBSET H (G0)) (FINITE H) (SUBSET (NT (A0) Z%) (UNION H)) ))))) (<= (LS A) Y) (NOT (E R A)) (NOT (E B (G0))) (NOT (SUBSET (NT Y (B0)) B))) It greatly shortens the presentation of this proof to use (AA). Secondly, the notation, ((13 2 (^ 1)) (21 6 (ZS A Y)) RULE1-g), means that we use Rule1-g on the first conjunct of Literal 2 of Clause 13, against Clause 21. I.e., (E (ZS A Y) A) is Rule1-g used against ((NOT (E R A)) (<= (LS A) Y) (NOT (SUBSET H (G0))) (NOT (E B (G0))) (NOT (FINITE H)) (NOT (SUBSET (NT (A0) (ZS A Y)) (UNION H))) (NOT (SUBSET (NT Y (B0)) B))) Where, the (21 6 (ZS A Y)) part of the notation, just means that we target on the term (ZS A Y) of Literal 6 of of Clause 21. Since Literal 6 contains the variable H (outside the term (ZS A Y)) it is necessary, by Rule1-g, to include in the definition of (AA), all literals of Clause 21 which contain H, namely Literals 3,5,6. 24 ((NOT (SUBSET A (AA))) (NOT (E R A)) (NOT (E B (G0))) (NOT (SUBSET (NT Y (B0)) B)) (NOT (<= Y (LS A))) (= (LS A) Y)) ((22 2) (L18 3) RES) 86 ((^ (E (B1S (A0) (B0) (G0)) (G0)) (E (A0) (B1S (A0) (B0) (G0))) (E (B2S (A0) (B0) (G0)) (G0)) (E (B0) (B2S (A0) (B0) (G0))))) (L1 (1 2) ((1 1) (3 1)) RES-MULTIPLE) 94 ((SUBSET (SNG (B1S (A0) (B0) (G0))) (G0))) ((L2 1) (86 1 (^ 1)) RES) 95 ((SUBSET (NT (A0) (A0)) (UNION (SNG (B1S (A0) (B0) (G0)))))) ((L3 1) (86 1 (^ 2)) RES) 96 ((SUBSET (NT (B0) (B0)) (B2S (A0) (B0) (G0)))) ((L19 1) (86 1 (^ 4)) RES) 97 ((OPEN (B2S (A0) (B0) (G0)))) ((2 1) (86 1 (^ 3)) RES) 25 ((NOT (SUBSET A (AA))) (NOT (E R A)) (NOT (<= (B0) (LS A))) (= (LS A) (B0))) (24 (3 4) ((86 1 (^ 3)) (96 1)) RES-MULTIPLE) 26 ((NOT (SUBSET A (AA))) (NOT (E R A)) (NOT (<= (B0) (LS A))) (E (LS A) (B2S (A0) (B0) (G0)))) ((25 4 2) (86 1 1 (^ 4))) SUB= 27 ((NOT (SUBSET A (AA))) (^ (NOT (<= (LS A) (A4S (LS A) (B2S (A0) (B0) (G0))))) (SUBSET (NT (A4S (LS A) (B2S (A0) (B0) (G0))) (LS A)) (B2S (A0) (B0) (G0)))) (NOT (E R A)) (NOT (<= (B0) (LS A)))) (L14 (1 2) ((26 4) (97 1)) RES-MULTIPLE) 28 ((NOT (SUBSET A (AA))) (NOT (E R A)) (NOT (<= (B0) (LS A))) (SUBSET (NT (A4S (LS A) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0)))) ((25 4 1) (27 2 2 (^ 2))) SUB= 29 ((NOT (SUBSET A (AA))) (NOT (<= (B0) (LS A))) (NOT (E R A)) (^ (E (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) A) (NOT (<= (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) (A4S (LS A) (B2S (A0) (B0) (G0))))))) ((27 2 (^ 1)) (13 3) RES) 32 ((NOT (SUBSET A (AA))) (NOT (E R A)) (^ (E (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) A) (NOT (<= (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) (A4S (LS A) (B2S (A0) (B0) (G0)))))) (<= (LS A) (B0))) ((29 2) (L15 1) RES) 33 ((NOT (SUBSET A (AA))) (NOT (E R A)) (^ (E (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) A) (NOT (<= (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) (A4S (LS A) (B2S (A0) (B0) (G0)))))) (NOT (<= AH (LS A))) (E (LS A) (NT AH (B0)))) ((32 4) (L5 2) RES) 35 ((NOT (SUBSET A (AA))) (E (LS A) (UNION (G0))) (NOT (E R A)) (^ (E (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) A) (NOT (<= (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) (A4S (LS A) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS A)))) (L6 (1 (I 2)) ((33 5) (3 1)) RES-MULTIPLE) 36 ((NOT (SUBSET A (AA))) (NOT (E R A)) (^ (E (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) A) (NOT (<= (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) (A4S (LS A) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS A))) (^ (E (B3S (LS A) (G0)) (G0)) (E (LS A) (B3S (LS A) (G0))))) ((35 2) (L7 1) RES) 38 ((NOT (SUBSET A (AA))) (NOT (E R A)) (^ (E (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) A) (NOT (<= (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) (A4S (LS A) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS A))) (OPEN (B3S (LS A) (G0)))) ((36 5 (^ 1)) (2 1) RES) 39 ((NOT (SUBSET A (AA))) (^ (NOT (<= (LS A) (A2S (B0) (LS A) (B3S (LS A) (G0))))) (NOT (<= (B2S (B0) (LS A) (B3S (LS A) (G0))) (LS A))) (<= (B2S (B0) (LS A) (B3S (LS A) (G0))) (B0)) (SUBSET (NT (A2S (B0) (LS A) (B3S (LS A) (G0))) (B2S (B0) (LS A) (B3S (LS A) (G0)))) (B3S (LS A) (G0)))) (^ (E (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) A) (NOT (<= (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) (A4S (LS A) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS A))) (NOT (E R A))) (L8 (1 2 3) ((29 2) (36 5 (^ 2)) (38 5)) RES-MULTIPLE) 40 ((NOT (SUBSET A (AA))) (^ (E (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) A) (NOT (<= (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) (A4S (LS A) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS A))) (NOT (E R A)) (^ (E (ZS A (A2S (B0) (LS A) (B3S (LS A) (G0)))) A) (NOT (<= (ZS A (A2S (B0) (LS A) (B3S (LS A) (G0)))) (A2S (B0) (LS A) (B3S (LS A) (G0))))))) ((39 2 (^ 1)) (13 3 (^ 2)) RES) 41 ((NOT (SUBSET A (AA))) (^ (E (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) A) (NOT (<= (ZS A (A4S (LS A) (B2S (A0) (B0) (G0)))) (A4S (LS A) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS A))) (NOT (E (B2S (B0) (LS A) (B3S (LS A) (G0))) A))) ((39 2 (^ 2)) (11 2) RES) 36C ((NOT (E R (AA))) (^ (E (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (AA)) (NOT (<= (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS (AA)))) (^ (E (B3S (LS (AA)) (G0)) (G0)) (E (LS (AA)) (B3S (LS (AA)) (G0))))) ((36 1) COLLAPSE) NOTE: The first literal of Clause 36 is (NOT (SUBSET A (AA))), where (AA) (SET-OF Z% (SOME H (^ (SUBSET H (G0)) (FINITE H) (SUBSET (NT (A0) Z%) (UNION H))))) (See Step 22 for the definition of (AA)) The notation ((36 1) COLLAPSE) means that Clause 36 is "collapsed" by substituting the set-value, (AA) for A in the remaining literals of Clause 36. 39C ((^ (NOT (<= (LS (AA)) (A2S (B0) (LS (AA)) (B3S (LS (AA)) (G0))))) (NOT (<= (B2S (B0) (LS (AA)) (B3S (LS (AA)) (G0))) (LS (AA)))) (<= (B2S (B0) (LS (AA)) (B3S (LS (AA)) (G0))) (B0)) (SUBSET (NT (A2S (B0) (LS (AA)) (B3S (LS (AA)) (G0))) (B2S (B0) (LS (AA)) (B3S (LS (AA)) (G0)))) (B3S (LS (AA)) (G0)))) (^ (E (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (AA)) (NOT (<= (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) ((39 1) COLLAPSE) 40C ((^ (E (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (AA)) (NOT (<= (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA))) (^ (E (ZS (AA) (A2S (B0) (LS (AA)) (B3S (LS (AA)) (G0)))) (AA)) (NOT (<= (ZS (AA) (A2S (B0) (LS (AA)) (B3S (LS (AA)) (G0)))) (A2S (B0) (LS (AA)) (B3S (LS (AA)) (G0))))))) ((40 1) COLLAPSE) 41C ((^ (E (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (AA)) (NOT (<= (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS (AA)))) (NOT (E (B2S (B0) (LS (AA)) (B3S (LS (AA)) (G0))) (AA)))) ((41 1) COLLAPSE) 40CS ((^ (E (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (AA)) (NOT (<= (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA))) (^ (SUBSET (NT (A0) (ZS (AA) (A2S (B0) (LS (AA)) (B3S (LS (AA)) (G0))))) (UNION (H16S R))) (SUBSET (H16S R) (G0)) (FINITE (H16S R)))) ((40C 4 (^ 1)) SIMP) 41CS ((^ (E (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (AA)) (NOT (<= (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS (AA)))) (NOT (SUBSET (NT (A0) (B2S (B0) (LS (AA)) (B3S (LS (AA)) (G0)))) (UNION H))) (NOT (SUBSET H (G0))) (NOT (FINITE H))) ((41C 3) SIMP) 42@1 ((SUBSET (NT (A0) (B2S (B0) (LS (AA)) (B3S (LS (AA)) (G0)))) (UNION (U (H16S R) (SNG (B3S (LS (AA)) (G0)))))) (^ (E (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (AA)) (NOT (<= (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) (L9 (1 2 3) ((40CS 4 (^ 1)) (39C 1 (^ 4)) (40C 4 (^ 2))) RES-MULTIPLE) 42@2 ((SUBSET (U (H16S R) (SNG (B3S (LS (AA)) (G0)))) (G0)) (^ (E (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (AA)) (NOT (<= (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) (L13 (1 2) ((40CS 4 (^ 2)) (36C 4 (^ 1))) RES-MULTIPLE) 42@3 ((FINITE (U (H16S R) (SNG B))) (^ (E (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (AA)) (NOT (<= (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) ((L12 1) (40CS 4 (^ 3)) RES) 42 ((^ (SUBSET (NT (A0) (B2S (B0) (LS (AA)) (B3S (LS (AA)) (G0)))) (UNION (U (H16S R) (SNG (B3S (LS (AA)) (G0)))))) (SUBSET (U (H16S R) (SNG (B3S (LS (AA)) (G0)))) (G0)) (FINITE (U (H16S R) (SNG B)))) (^ (E (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (AA)) (NOT (<= (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0))) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) ((L9 (1 2 3) ((40CS 4 (^ 1)) (39C 1 (^ 4)) (40C 4 (^ 2))) RES-MULTIPLE) (L13 (1 2) ((40CS 4 (^ 2)) (36C 4 (^ 1))) RES-MULTIPLE) ((L12 1) (40CS 4 (^ 3)) RES) COMBINE-RESOLVENTS) 43 ((^ (E (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (AA)) (NOT (<= (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))) (A4S (LS (AA)) (B2S (A0) (B0) (G0)))))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) (41CS (3 4 5) ((42@1 1) (42@2 1) (42@3 1)) RES-MULTIPLE) 52 ((NOT (SUBSET A (AA))) (NOT (E R A)) (SUBSET (NT (A4S (LS A) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (<= (LS A) (B0))) ((28 3) (L15 1) RES) 53 ((NOT (SUBSET A (AA))) (NOT (E R A)) (SUBSET (NT (A4S (LS A) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= AH (LS A))) (E (LS A) (NT AH (B0)))) ((52 4) (L5 2) RES) 54 ((NOT (SUBSET A (AA))) (NOT (E R A)) (SUBSET (NT (A4S (LS A) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= AH (LS A))) (NOT (SUBSET (NT AH (B0)) D)) (E (LS A) D)) ((53 5) (L6 1) RES) 55 ((NOT (SUBSET A (AA))) (NOT (E R A)) (SUBSET (NT (A4S (LS A) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS A))) (E (LS A) (UNION (G0)))) ((54 5) (3 1) RES) 56 ((NOT (SUBSET A (AA))) (NOT (E R A)) (SUBSET (NT (A4S (LS A) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS A))) (^ (E (B3S (LS A) (G0)) (G0)) (E (LS A) (B3S (LS A) (G0))))) ((55 5) (L7 1) RES) 58 ((NOT (SUBSET A (AA))) (NOT (E R A)) (SUBSET (NT (A4S (LS A) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS A))) (OPEN (B3S (LS A) (G0)))) ((56 5 (^ 1)) (2 1) RES) 59 ((NOT (SUBSET A (AA))) (^ (NOT (<= (LS A) (A2S (B0) (LS A) (B3S (LS A) (G0))))) (NOT (<= (B2S (B0) (LS A) (B3S (LS A) (G0))) (LS A))) (<= (B2S (B0) (LS A) (B3S (LS A) (G0))) (B0)) (SUBSET (NT (A2S (B0) (LS A) (B3S (LS A) (G0))) (B2S (B0) (LS A) (B3S (LS A) (G0)))) (B3S (LS A) (G0)))) (SUBSET (NT (A4S (LS A) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS A))) (NOT (E R A))) (L8 (1 2 3) ((28 3) (56 5 (^ 2)) (58 5)) RES-MULTIPLE) 60 ((NOT (SUBSET A (AA))) (^ (E (ZS A (A2S (B0) (LS A) (B3S (LS A) (G0)))) A) (NOT (<= (ZS A (A2S (B0) (LS A) (B3S (LS A) (G0)))) (A2S (B0) (LS A) (B3S (LS A) (G0)))))) (SUBSET (NT (A4S (LS A) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS A))) (NOT (E R A))) ((13 3) (59 2 (^ 1)) RES) 61 ((NOT (SUBSET A (AA))) (NOT (E (B2S (B0) (LS A) (B3S (LS A) (G0))) A)) (SUBSET (NT (A4S (LS A) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS A)))) ((11 2) (59 2 (^ 2)) RES) 56C ((NOT (E R (AA))) (SUBSET (NT (A4S (LS (AA)) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS (AA)))) (^ (E (B3S (LS (AA)) (G0)) (G0)) (E (LS (AA)) (B3S (LS (AA)) (G0))))) ((56 1) COLLAPSE) 59C ((^ (NOT (<= (LS (AA)) (A2S (B0) (LS (AA)) (B3S (LS (AA)) (G0))))) (NOT (<= (B2S (B0) (LS (AA)) (B3S (LS (AA)) (G0))) (LS (AA)))) (<= (B2S (B0) (LS (AA)) (B3S (LS (AA)) (G0))) (B0)) (SUBSET (NT (A2S (B0) (LS (AA)) (B3S (LS (AA)) (G0))) (B2S (B0) (LS (AA)) (B3S (LS (AA)) (G0)))) (B3S (LS (AA)) (G0)))) (SUBSET (NT (A4S (LS (AA)) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) ((59 1) COLLAPSE) 60C ((^ (E (ZS (AA) (A2S (B0) (LS (AA)) (B3S (LS (AA)) (G0)))) (AA)) (NOT (<= (ZS (AA) (A2S (B0) (LS (AA)) (B3S (LS (AA)) (G0)))) (A2S (B0) (LS (AA)) (B3S (LS (AA)) (G0)))))) (SUBSET (NT (A4S (LS (AA)) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) ((60 1) COLLAPSE) 61C ((NOT (E (B2S (B0) (LS (AA)) (B3S (LS (AA)) (G0))) (AA))) (SUBSET (NT (A4S (LS (AA)) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS (AA))))) ((61 1) COLLAPSE) 60CS ((^ (SUBSET (NT (A0) (ZS (AA) (A2S (B0) (LS (AA)) (B3S (LS (AA)) (G0))))) (UNION (H17S R))) (SUBSET (H17S R) (G0)) (FINITE (H17S R))) (SUBSET (NT (A4S (LS (AA)) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) ((60C 1 (^ 1)) SIMP) 61CS ((SUBSET (NT (A4S (LS (AA)) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS (AA)))) (NOT (SUBSET (NT (A0) (B2S (B0) (LS (AA)) (B3S (LS (AA)) (G0)))) (UNION H))) (NOT (SUBSET H (G0))) (NOT (FINITE H))) ((61C 1) SIMP) 62@1 ((SUBSET (NT (A0) (B2S (B0) (LS (AA)) (B3S (LS (AA)) (G0)))) (UNION (U (H17S R) (SNG (B3S (LS (AA)) (G0)))))) (SUBSET (NT (A4S (LS (AA)) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) (L9 (1 2 3) ((60CS 1 (^ 1)) (59C 1 (^ 4)) (60C 1 (^ 2))) RES-MULTIPLE) 62@2 ((SUBSET (U (H17S R) (SNG (B3S (LS (AA)) (G0)))) (G0)) (SUBSET (NT (A4S (LS (AA)) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) (L13 (1 2) ((60CS 1 (^ 2)) (56C 4 (^ 1))) RES-MULTIPLE) 62@3 ((FINITE (U (H17S R) (SNG B))) (SUBSET (NT (A4S (LS (AA)) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) ((L12 1) (60CS 1 (^ 3)) RES) 62 ((^ (SUBSET (NT (A0) (B2S (B0) (LS (AA)) (B3S (LS (AA)) (G0)))) (UNION (U (H17S R) (SNG (B3S (LS (AA)) (G0)))))) (SUBSET (U (H17S R) (SNG (B3S (LS (AA)) (G0)))) (G0)) (FINITE (U (H17S R) (SNG B)))) (SUBSET (NT (A4S (LS (AA)) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) ((L9 (1 2 3) ((60CS 1 (^ 1)) (59C 1 (^ 4)) (60C 1 (^ 2))) RES-MULTIPLE) (L13 (1 2) ((60CS 1 (^ 2)) (56C 4 (^ 1))) RES-MULTIPLE) ((L12 1) (60CS 1 (^ 3)) RES) COMBINE-RESOLVENTS) 63 ((SUBSET (NT (A4S (LS (AA)) (B2S (A0) (B0) (G0))) (B0)) (B2S (A0) (B0) (G0))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) (61CS (3 4 5) ((62@1 1) (62@2 1) (62@3 1)) RES-MULTIPLE) |43S| ((^ (SUBSET (NT (A0) (ZS (AA) (A4S (LS (AA)) (B2S (A0) (B0) (G0))))) (UNION (H18S R))) (SUBSET (H18S R) (G0)) (FINITE (H18S R))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) ((43 1 (^ 1)) SIMP) 44@1 ((SUBSET (NT (A0) (B0)) (UNION (U (H18S R) (SNG (B2S (A0) (B) (G0)))))) (NOT (<= (A0) (L (AA)))) (NOT (E R (AA)))) (L9 (1 2 3) ((|43S| 1 (^ 1)) (63 1) (43 1 (^ 2))) RES-MULTIPLE) 44@2 ((SUBSET (U (H18S R) (SNG (B2S (A0) (B0) (G0)))) (G0)) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) (L13 (1 2) ((|43S| 1 (^ 2)) (86 1 (^ 3))) RES-MULTIPLE) 44@3 ((FINITE (U (H18S R) (SNG B))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) ((L12 1) (|43S| 1 (^ 3)) RES) 44 ((^ (SUBSET (NT (A0) (B0)) (UNION (U (H18S R) (SNG (B2S (A0) (B0) (G0)))))) (SUBSET (U (H18S R) (SNG (B2S (A0) (B0) (G0)))) (G0)) (FINITE (U (H18S R) (SNG B)))) (NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) ((L9 (1 2 3) ((|43S| 1 (^ 1)) (63 1) (43 1 (^ 2))) RES-MULTIPLE) (L13 (1 2) ((|43S| 1 (^ 2)) (86 1 (^ 3))) RES-MULTIPLE) ((L12 1) (|43S| 1 (^ 3)) RES) COMBINE-RESOLVENTS) 45 ((NOT (<= (A0) (LS (AA)))) (NOT (E R (AA)))) (4 (1 2 3) ((44@2 1) (44@3 1) (44@1 1)) RES-MULTIPLE) 46 ((NOT (E (A0) (AA)))) ((11 2) (45 1) RES) 49 ((NOT (SUBSET (NT (A0) (A0)) (UNION H))) (NOT (SUBSET H (G0))) (NOT (FINITE H))) ((46 1) SIMP) 50 [] (49 (1 2 3) ((95 1) (94 1) (L4 1)) RES-MULTIPLE) References. [1] Bledsoe, W.W., and Guohui Feng, "SET-VAR", JAR 11 (1993) 293-314. [2] Bledsoe, W.W., "SET-VAR-implementation", Univ of Texas CS Dept Memo ATP 119, May 1993. [3] Bledsoe, W.W., and Guohui Feng, "Extended SET-VAR", Univ of Texas CS Dept Memo ATP 121, 7 April 1994.