(BOOT-STRAP)
Nqthm-1992 mods: ("DEFN-SK")
[ 0.1 0.0 0.0 ]
GROUND-ZERO
(DEFN SET-STANDARD
(L)
(IF (LISTP L)
(AND (NOT (MEMBER (CAR L) (CDR L)))
(SET-STANDARD (CDR L)))
T))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT L) decreases according to the well-founded relation LESSP in each
recursive call. Hence, SET-STANDARD is accepted under the principle of
definition. From the definition we can conclude that:
(OR (FALSEP (SET-STANDARD L))
(TRUEP (SET-STANDARD L)))
is a theorem.
[ 0.0 0.0 0.0 ]
SET-STANDARD
(DEFN SET-MINUS
(L1 L2)
(IF (LISTP L1)
(IF (MEMBER (CAR L1) L2)
(SET-MINUS (CDR L1) L2)
(CONS (CAR L1)
(SET-MINUS (CDR L1) L2)))
L1))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT L1) decreases according to the well-founded relation LESSP in each
recursive call. Hence, SET-MINUS is accepted under the definitional principle.
[ 0.0 0.0 0.0 ]
SET-MINUS
(DEFN SET-DISJOINT
(L1 L2)
(IF (LISTP L1)
(IF (MEMBER (CAR L1) L2)
F
(SET-DISJOINT (CDR L1) L2))
T))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT L1) decreases according to the well-founded relation LESSP in each
recursive call. Hence, SET-DISJOINT is accepted under the definitional
principle. Note that:
(OR (FALSEP (SET-DISJOINT L1 L2))
(TRUEP (SET-DISJOINT L1 L2)))
is a theorem.
[ 0.0 0.0 0.0 ]
SET-DISJOINT
(DEFN DELETE
(X L)
(IF (LISTP L)
(IF (EQUAL X (CAR L))
(CDR L)
(CONS (CAR L) (DELETE X (CDR L))))
L))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT L) decreases according to the well-founded relation LESSP in each
recursive call. Hence, DELETE is accepted under the principle of definition.
[ 0.0 0.0 0.0 ]
DELETE
(DEFN SUBSET
(L1 L2)
(IF (LISTP L1)
(AND (MEMBER (CAR L1) L2)
(SUBSET (CDR L1) L2))
T))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT L1) decreases according to the well-founded relation LESSP in each
recursive call. Hence, SUBSET is accepted under the principle of definition.
Note that (OR (FALSEP (SUBSET L1 L2)) (TRUEP (SUBSET L1 L2))) is a theorem.
[ 0.0 0.0 0.0 ]
SUBSET
(DEFN CARDINAL
(L)
(IF (LISTP L)
(ADD1 (CARDINAL (CDR L)))
0))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT L) decreases according to the well-founded relation LESSP in each
recursive call. Hence, CARDINAL is accepted under the principle of definition.
From the definition we can conclude that (NUMBERP (CARDINAL L)) is a theorem.
[ 0.0 0.0 0.0 ]
CARDINAL
(PROVE-LEMMA SET-STANDARD-LEMMA
(REWRITE)
(IMPLIES (SET-STANDARD A)
(SET-STANDARD (SET-MINUS A B)))
((INDUCT (SET-MINUS A B))))
This formula can be simplified, using the abbreviations IMPLIES, NOT, OR, and
AND, to the following three new goals:
Case 3. (IMPLIES (AND (LISTP A)
(MEMBER (CAR A) B)
(IMPLIES (SET-STANDARD (CDR A))
(SET-STANDARD (SET-MINUS (CDR A) B)))
(SET-STANDARD A))
(SET-STANDARD (SET-MINUS A B))).
This simplifies, opening up IMPLIES, SET-STANDARD, and SET-MINUS, to:
T.
Case 2. (IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) B))
(IMPLIES (SET-STANDARD (CDR A))
(SET-STANDARD (SET-MINUS (CDR A) B)))
(SET-STANDARD A))
(SET-STANDARD (SET-MINUS A B))).
This simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and
expanding the definitions of IMPLIES, SET-STANDARD, and SET-MINUS, to:
(IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) B))
(SET-STANDARD (SET-MINUS (CDR A) B))
(NOT (MEMBER (CAR A) (CDR A)))
(SET-STANDARD (CDR A)))
(NOT (MEMBER (CAR A)
(SET-MINUS (CDR A) B)))).
Applying the lemma CAR-CDR-ELIM, replace A by (CONS X Z) to eliminate
(CAR A) and (CDR A). This produces:
(IMPLIES (AND (NOT (MEMBER X B))
(SET-STANDARD (SET-MINUS Z B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(NOT (MEMBER X (SET-MINUS Z B)))),
which we will name *1.
Case 1. (IMPLIES (AND (NOT (LISTP A)) (SET-STANDARD A))
(SET-STANDARD (SET-MINUS A B))).
This simplifies, unfolding SET-STANDARD and SET-MINUS, to:
T.
So let us turn our attention to:
(IMPLIES (AND (NOT (MEMBER X B))
(SET-STANDARD (SET-MINUS Z B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(NOT (MEMBER X (SET-MINUS Z B)))),
which is formula *1 above. Perhaps we can prove it by induction. There are
five plausible inductions. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP Z)
(MEMBER (CAR Z) B)
(p X (CDR Z) B))
(p X Z B))
(IMPLIES (AND (LISTP Z)
(NOT (MEMBER (CAR Z) B))
(p X (CDR Z) B))
(p X Z B))
(IMPLIES (NOT (LISTP Z)) (p X Z B))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT Z)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces the following nine new
formulas:
Case 9. (IMPLIES (AND (LISTP Z)
(MEMBER (CAR Z) B)
(NOT (SET-STANDARD (SET-MINUS (CDR Z) B)))
(NOT (MEMBER X B))
(SET-STANDARD (SET-MINUS Z B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(NOT (MEMBER X (SET-MINUS Z B)))).
This simplifies, unfolding the function SET-MINUS, to:
T.
Case 8. (IMPLIES (AND (LISTP Z)
(MEMBER (CAR Z) B)
(MEMBER X (CDR Z))
(NOT (MEMBER X B))
(SET-STANDARD (SET-MINUS Z B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(NOT (MEMBER X (SET-MINUS Z B)))).
This simplifies, opening up SET-MINUS and MEMBER, to:
T.
Case 7. (IMPLIES (AND (LISTP Z)
(MEMBER (CAR Z) B)
(NOT (SET-STANDARD (CDR Z)))
(NOT (MEMBER X B))
(SET-STANDARD (SET-MINUS Z B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(NOT (MEMBER X (SET-MINUS Z B)))).
This simplifies, expanding SET-MINUS, MEMBER, and SET-STANDARD, to:
T.
Case 6. (IMPLIES (AND (LISTP Z)
(MEMBER (CAR Z) B)
(NOT (MEMBER X (SET-MINUS (CDR Z) B)))
(NOT (MEMBER X B))
(SET-STANDARD (SET-MINUS Z B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(NOT (MEMBER X (SET-MINUS Z B)))).
This simplifies, expanding the functions SET-MINUS, MEMBER, and SET-STANDARD,
to:
T.
Case 5. (IMPLIES (AND (LISTP Z)
(NOT (MEMBER (CAR Z) B))
(NOT (SET-STANDARD (SET-MINUS (CDR Z) B)))
(NOT (MEMBER X B))
(SET-STANDARD (SET-MINUS Z B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(NOT (MEMBER X (SET-MINUS Z B)))).
This simplifies, applying CDR-CONS and CAR-CONS, and unfolding SET-MINUS and
SET-STANDARD, to:
T.
Case 4. (IMPLIES (AND (LISTP Z)
(NOT (MEMBER (CAR Z) B))
(MEMBER X (CDR Z))
(NOT (MEMBER X B))
(SET-STANDARD (SET-MINUS Z B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(NOT (MEMBER X (SET-MINUS Z B)))),
which simplifies, applying CDR-CONS and CAR-CONS, and expanding SET-MINUS,
SET-STANDARD, and MEMBER, to:
T.
Case 3. (IMPLIES (AND (LISTP Z)
(NOT (MEMBER (CAR Z) B))
(NOT (SET-STANDARD (CDR Z)))
(NOT (MEMBER X B))
(SET-STANDARD (SET-MINUS Z B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(NOT (MEMBER X (SET-MINUS Z B)))).
This simplifies, rewriting with CDR-CONS and CAR-CONS, and opening up the
definitions of SET-MINUS, SET-STANDARD, and MEMBER, to:
T.
Case 2. (IMPLIES (AND (LISTP Z)
(NOT (MEMBER (CAR Z) B))
(NOT (MEMBER X (SET-MINUS (CDR Z) B)))
(NOT (MEMBER X B))
(SET-STANDARD (SET-MINUS Z B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(NOT (MEMBER X (SET-MINUS Z B)))),
which simplifies, applying CDR-CONS and CAR-CONS, and opening up SET-MINUS,
SET-STANDARD, and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP Z))
(NOT (MEMBER X B))
(SET-STANDARD (SET-MINUS Z B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(NOT (MEMBER X (SET-MINUS Z B)))).
This simplifies, unfolding the functions SET-MINUS, SET-STANDARD, and MEMBER,
to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
SET-STANDARD-LEMMA
(PROVE-LEMMA SET-MINUS-LEMMA1 NIL
(LEQ (COUNT (SET-MINUS S S1))
(COUNT S)))
Call the conjecture *1.
We will try to prove it by induction. There is only one suggested
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP S)
(MEMBER (CAR S) S1)
(p (CDR S) S1))
(p S S1))
(IMPLIES (AND (LISTP S)
(NOT (MEMBER (CAR S) S1))
(p (CDR S) S1))
(p S S1))
(IMPLIES (NOT (LISTP S)) (p S S1))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT S)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates three new goals:
Case 3. (IMPLIES (AND (LISTP S)
(MEMBER (CAR S) S1)
(NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1)))))
(NOT (LESSP (COUNT S)
(COUNT (SET-MINUS S S1))))),
which simplifies, opening up the function SET-MINUS, to:
(IMPLIES (AND (LISTP S)
(MEMBER (CAR S) S1)
(NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1)))))
(NOT (LESSP (COUNT S)
(COUNT (SET-MINUS (CDR S) S1))))).
This again simplifies, using linear arithmetic and rewriting with the lemma
CDR-LESSEQP, to:
T.
Case 2. (IMPLIES (AND (LISTP S)
(NOT (MEMBER (CAR S) S1))
(NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1)))))
(NOT (LESSP (COUNT S)
(COUNT (SET-MINUS S S1))))),
which simplifies, applying the lemmas COUNT-CONS and SUB1-ADD1, and opening
up the definitions of SET-MINUS and LESSP, to two new conjectures:
Case 2.2.
(IMPLIES (AND (LISTP S)
(NOT (MEMBER (CAR S) S1))
(NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1)))))
(NOT (EQUAL (COUNT S) 0))).
Applying the lemma CAR-CDR-ELIM, replace S by (CONS X Z) to eliminate
(CAR S) and (CDR S). This produces the new conjecture:
(IMPLIES (AND (NOT (MEMBER X S1))
(NOT (LESSP (COUNT Z)
(COUNT (SET-MINUS Z S1)))))
(NOT (EQUAL (COUNT (CONS X Z)) 0))),
which further simplifies, rewriting with COUNT-CONS, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP S)
(NOT (MEMBER (CAR S) S1))
(NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1)))))
(NOT (LESSP (SUB1 (COUNT S))
(PLUS (COUNT (CAR S))
(COUNT (SET-MINUS (CDR S) S1)))))).
Appealing to the lemma CAR-CDR-ELIM, we now replace S by (CONS X Z) to
eliminate (CAR S) and (CDR S). The result is the conjecture:
(IMPLIES (AND (NOT (MEMBER X S1))
(NOT (LESSP (COUNT Z)
(COUNT (SET-MINUS Z S1)))))
(NOT (LESSP (SUB1 (COUNT (CONS X Z)))
(PLUS (COUNT X)
(COUNT (SET-MINUS Z S1)))))).
But this further simplifies, rewriting with the lemmas COUNT-CONS and
SUB1-ADD1, to:
(IMPLIES (AND (NOT (MEMBER X S1))
(NOT (LESSP (COUNT Z)
(COUNT (SET-MINUS Z S1)))))
(NOT (LESSP (PLUS (COUNT X) (COUNT Z))
(PLUS (COUNT X)
(COUNT (SET-MINUS Z S1)))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (NOT (LISTP S))
(NOT (LESSP (COUNT S)
(COUNT (SET-MINUS S S1))))),
which simplifies, expanding SET-MINUS, to:
(IMPLIES (NOT (LISTP S))
(NOT (LESSP (COUNT S) (COUNT S)))).
However this again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SET-MINUS-LEMMA1
(PROVE-LEMMA SET-MINUS-LEMMA2
(REWRITE)
(IMPLIES (NOT (MEMBER C A))
(EQUAL (SET-MINUS A (CONS C B))
(SET-MINUS A B))))
Give the conjecture the name *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest three inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP A) (p A C B))
(IMPLIES (AND (NOT (NLISTP A))
(EQUAL C (CAR A)))
(p A C B))
(IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL C (CAR A)))
(p (CDR A) C B))
(p A C B))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to show that the measure (COUNT A) decreases according to
the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme generates the following four new conjectures:
Case 4. (IMPLIES (AND (NLISTP A) (NOT (MEMBER C A)))
(EQUAL (SET-MINUS A (CONS C B))
(SET-MINUS A B))).
This simplifies, opening up the functions NLISTP, MEMBER, and SET-MINUS, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP A))
(EQUAL C (CAR A))
(NOT (MEMBER C A)))
(EQUAL (SET-MINUS A (CONS C B))
(SET-MINUS A B))).
This simplifies, unfolding the functions NLISTP and MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL C (CAR A)))
(MEMBER C (CDR A))
(NOT (MEMBER C A)))
(EQUAL (SET-MINUS A (CONS C B))
(SET-MINUS A B))).
This simplifies, expanding NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL C (CAR A)))
(EQUAL (SET-MINUS (CDR A) (CONS C B))
(SET-MINUS (CDR A) B))
(NOT (MEMBER C A)))
(EQUAL (SET-MINUS A (CONS C B))
(SET-MINUS A B))).
This simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS, and
expanding the functions NLISTP, MEMBER, and SET-MINUS, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SET-MINUS-LEMMA2
(PROVE-LEMMA SET-MINUS-LEMMA3 NIL
(EQUAL (MEMBER X (SET-MINUS S S1))
(AND (MEMBER X S)
(NOT (MEMBER X S1)))))
This formula simplifies, expanding NOT and AND, to three new conjectures:
Case 3. (IMPLIES (MEMBER X S1)
(EQUAL (MEMBER X (SET-MINUS S S1))
F)),
which again simplifies, clearly, to:
(IMPLIES (MEMBER X S1)
(NOT (MEMBER X (SET-MINUS S S1)))),
which we will name *1.
Case 2. (IMPLIES (NOT (MEMBER X S))
(EQUAL (MEMBER X (SET-MINUS S S1))
F)).
This again simplifies, trivially, to:
(IMPLIES (NOT (MEMBER X S))
(NOT (MEMBER X (SET-MINUS S S1)))),
which we would normally push and work on later by induction. But if we must
use induction to prove the input conjecture, we prefer to induct on the
original formulation of the problem. Thus we will disregard all that we
have previously done, give the name *1 to the original input, and work on it.
So now let us return to:
(EQUAL (MEMBER X (SET-MINUS S S1))
(AND (MEMBER X S)
(NOT (MEMBER X S1)))).
We named this *1. We will try to prove it by induction. There are three
plausible inductions. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP S)
(MEMBER (CAR S) S1)
(p X (CDR S) S1))
(p X S S1))
(IMPLIES (AND (LISTP S)
(NOT (MEMBER (CAR S) S1))
(p X (CDR S) S1))
(p X S S1))
(IMPLIES (NOT (LISTP S)) (p X S S1))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT S)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces three new conjectures:
Case 3. (IMPLIES (AND (LISTP S)
(MEMBER (CAR S) S1)
(EQUAL (MEMBER X (SET-MINUS (CDR S) S1))
(AND (MEMBER X (CDR S))
(NOT (MEMBER X S1)))))
(EQUAL (MEMBER X (SET-MINUS S S1))
(AND (MEMBER X S)
(NOT (MEMBER X S1))))),
which simplifies, opening up NOT, AND, SET-MINUS, MEMBER, and EQUAL, to the
formula:
(IMPLIES (AND (LISTP S)
(MEMBER (CAR S) S1)
(NOT (MEMBER X (CDR S)))
(EQUAL (MEMBER X (SET-MINUS (CDR S) S1))
F)
(EQUAL X (CAR S)))
(MEMBER X S1)).
This again simplifies, obviously, to:
T.
Case 2. (IMPLIES (AND (LISTP S)
(NOT (MEMBER (CAR S) S1))
(EQUAL (MEMBER X (SET-MINUS (CDR S) S1))
(AND (MEMBER X (CDR S))
(NOT (MEMBER X S1)))))
(EQUAL (MEMBER X (SET-MINUS S S1))
(AND (MEMBER X S)
(NOT (MEMBER X S1))))).
This simplifies, applying CDR-CONS and CAR-CONS, and expanding NOT, AND,
SET-MINUS, MEMBER, and EQUAL, to two new conjectures:
Case 2.2.
(IMPLIES (AND (LISTP S)
(NOT (MEMBER (CAR S) S1))
(MEMBER X S1)
(EQUAL (MEMBER X (SET-MINUS (CDR S) S1))
F))
(NOT (EQUAL X (CAR S)))),
which again simplifies, clearly, to:
T.
Case 2.1.
(IMPLIES (AND (LISTP S)
(NOT (MEMBER (CAR S) S1))
(NOT (MEMBER X (CDR S)))
(EQUAL (MEMBER X (SET-MINUS (CDR S) S1))
F)
(EQUAL X (CAR S)))
(NOT (MEMBER X S1))).
This again simplifies, trivially, to:
T.
Case 1. (IMPLIES (NOT (LISTP S))
(EQUAL (MEMBER X (SET-MINUS S S1))
(AND (MEMBER X S)
(NOT (MEMBER X S1))))).
This simplifies, expanding the functions SET-MINUS, MEMBER, NOT, AND, and
EQUAL, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SET-MINUS-LEMMA3
(PROVE-LEMMA SET-MINUS-LEMMA NIL
(IMPLIES (AND (LISTP S)
(MEMBER X S)
(MEMBER X S1))
(LESSP (COUNT (SET-MINUS S S1))
(COUNT S)))
((USE (SET-MINUS-LEMMA1 (S (CDR S))
(S1 S1)))
(INDUCT (SET-MINUS S S1))))
This simplifies, expanding the functions NOT, AND, IMPLIES, MEMBER, SET-MINUS,
and OR, to nine new formulas:
Case 9. (IMPLIES (AND (NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1))))
(LISTP S)
(NOT (MEMBER (CAR S) S1))
(NOT (MEMBER X (CDR S)))
(EQUAL X (CAR S))
(MEMBER X S1))
(LESSP (COUNT (CONS (CAR S) (SET-MINUS (CDR S) S1)))
(COUNT S))),
which again simplifies, obviously, to:
T.
Case 8. (IMPLIES (AND (NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1))))
(LISTP S)
(NOT (MEMBER (CAR S) S1))
(MEMBER X (CDR S))
(MEMBER X S1)
(LESSP (COUNT (SET-MINUS (CDR S) S1))
(COUNT (CDR S))))
(LESSP (COUNT (CONS (CAR S) (SET-MINUS (CDR S) S1)))
(COUNT S))).
But this again simplifies, appealing to the lemmas COUNT-CONS and SUB1-ADD1,
and expanding the definition of LESSP, to two new conjectures:
Case 8.2.
(IMPLIES (AND (NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1))))
(LISTP S)
(NOT (MEMBER (CAR S) S1))
(MEMBER X (CDR S))
(MEMBER X S1)
(LESSP (COUNT (SET-MINUS (CDR S) S1))
(COUNT (CDR S))))
(NOT (EQUAL (COUNT S) 0))),
which again simplifies, using linear arithmetic and rewriting with
CDR-LESSEQP, to:
T.
Case 8.1.
(IMPLIES (AND (NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1))))
(LISTP S)
(NOT (MEMBER (CAR S) S1))
(MEMBER X (CDR S))
(MEMBER X S1)
(LESSP (COUNT (SET-MINUS (CDR S) S1))
(COUNT (CDR S))))
(LESSP (PLUS (COUNT (CAR S))
(COUNT (SET-MINUS (CDR S) S1)))
(SUB1 (COUNT S)))).
Appealing to the lemma CAR-CDR-ELIM, we now replace S by (CONS V Z) to
eliminate (CDR S) and (CAR S). The result is:
(IMPLIES (AND (NOT (LESSP (COUNT Z)
(COUNT (SET-MINUS Z S1))))
(NOT (MEMBER V S1))
(MEMBER X Z)
(MEMBER X S1)
(LESSP (COUNT (SET-MINUS Z S1))
(COUNT Z)))
(LESSP (PLUS (COUNT V)
(COUNT (SET-MINUS Z S1)))
(SUB1 (COUNT (CONS V Z))))).
However this further simplifies, applying COUNT-CONS and SUB1-ADD1, to:
(IMPLIES (AND (NOT (LESSP (COUNT Z)
(COUNT (SET-MINUS Z S1))))
(NOT (MEMBER V S1))
(MEMBER X Z)
(MEMBER X S1)
(LESSP (COUNT (SET-MINUS Z S1))
(COUNT Z)))
(LESSP (PLUS (COUNT V)
(COUNT (SET-MINUS Z S1)))
(PLUS (COUNT V) (COUNT Z)))),
which again simplifies, using linear arithmetic, to:
T.
Case 7. (IMPLIES (AND (NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1))))
(LISTP S)
(NOT (MEMBER (CAR S) S1))
(MEMBER X S1)
(LESSP (COUNT (SET-MINUS (CDR S) S1))
(COUNT (CDR S)))
(EQUAL X (CAR S)))
(LESSP (COUNT (CONS (CAR S) (SET-MINUS (CDR S) S1)))
(COUNT S))),
which again simplifies, trivially, to:
T.
Case 6. (IMPLIES (AND (NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1))))
(LISTP S)
(NOT (MEMBER (CAR S) S1))
(NOT (LISTP (CDR S)))
(MEMBER X (CDR S))
(MEMBER X S1))
(LESSP (COUNT (CONS (CAR S) (SET-MINUS (CDR S) S1)))
(COUNT S))).
But this again simplifies, opening up SET-MINUS and MEMBER, to:
T.
Case 5. (IMPLIES (AND (NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1))))
(LISTP S)
(NOT (MEMBER (CAR S) S1))
(NOT (LISTP (CDR S)))
(EQUAL X (CAR S))
(MEMBER X S1))
(LESSP (COUNT (CONS (CAR S) (SET-MINUS (CDR S) S1)))
(COUNT S))),
which again simplifies, trivially, to:
T.
Case 4. (IMPLIES (AND (NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1))))
(LISTP S)
(MEMBER (CAR S) S1)
(MEMBER X (CDR S))
(MEMBER X S1)
(LESSP (COUNT (SET-MINUS (CDR S) S1))
(COUNT (CDR S))))
(LESSP (COUNT (SET-MINUS (CDR S) S1))
(COUNT S))).
But this again simplifies, using linear arithmetic and applying CDR-LESSEQP,
to:
T.
Case 3. (IMPLIES (AND (NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1))))
(LISTP S)
(MEMBER (CAR S) S1)
(NOT (LISTP (CDR S)))
(EQUAL X (CAR S))
(MEMBER X S1))
(LESSP (COUNT (SET-MINUS (CDR S) S1))
(COUNT S))).
But this again simplifies, using linear arithmetic and applying CDR-LESSP,
to:
T.
Case 2. (IMPLIES (AND (NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1))))
(LISTP S)
(MEMBER (CAR S) S1)
(NOT (LISTP (CDR S)))
(MEMBER X (CDR S))
(MEMBER X S1))
(LESSP (COUNT (SET-MINUS (CDR S) S1))
(COUNT S))).
However this again simplifies, using linear arithmetic and applying
CDR-LESSP, to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP (COUNT (CDR S))
(COUNT (SET-MINUS (CDR S) S1))))
(LISTP S)
(MEMBER (CAR S) S1)
(NOT (MEMBER X (CDR S)))
(EQUAL X (CAR S))
(MEMBER X S1))
(LESSP (COUNT (SET-MINUS (CDR S) S1))
(COUNT S))).
However this again simplifies, using linear arithmetic and applying
CDR-LESSP, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
SET-MINUS-LEMMA
(PROVE-LEMMA DELETE-LEMMA1 NIL
(IMPLIES (MEMBER X A)
(EQUAL (CARDINAL A)
(ADD1 (CARDINAL (DELETE X A))))))
Call the conjecture *1.
We will try to prove it by induction. There are three plausible
inductions. However, they merge into one likely candidate induction. We will
induct according to the following scheme:
(AND (IMPLIES (NLISTP A) (p A X))
(IMPLIES (AND (NOT (NLISTP A))
(EQUAL X (CAR A)))
(p A X))
(IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL X (CAR A)))
(p (CDR A) X))
(p A X))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT A) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme generates four new goals:
Case 4. (IMPLIES (AND (NLISTP A) (MEMBER X A))
(EQUAL (CARDINAL A)
(ADD1 (CARDINAL (DELETE X A))))),
which simplifies, opening up the functions NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP A))
(EQUAL X (CAR A))
(MEMBER X A))
(EQUAL (CARDINAL A)
(ADD1 (CARDINAL (DELETE X A))))),
which simplifies, expanding NLISTP, MEMBER, CARDINAL, and DELETE, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL X (CAR A)))
(NOT (MEMBER X (CDR A)))
(MEMBER X A))
(EQUAL (CARDINAL A)
(ADD1 (CARDINAL (DELETE X A))))),
which simplifies, expanding the functions NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL X (CAR A)))
(EQUAL (CARDINAL (CDR A))
(ADD1 (CARDINAL (DELETE X (CDR A)))))
(MEMBER X A))
(EQUAL (CARDINAL A)
(ADD1 (CARDINAL (DELETE X A))))),
which simplifies, applying the lemma CDR-CONS, and opening up the
definitions of NLISTP, MEMBER, CARDINAL, and DELETE, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.2 ]
DELETE-LEMMA1
(PROVE-LEMMA DELETE-LEMMA2
(REWRITE)
(IMPLIES (AND (MEMBER Y A) (NOT (EQUAL X Y)))
(MEMBER Y (DELETE X A))))
Give the conjecture the name *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest two inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP A) (p Y X A))
(IMPLIES (AND (NOT (NLISTP A))
(EQUAL Y (CAR A)))
(p Y X A))
(IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL Y (CAR A)))
(p Y X (CDR A)))
(p Y X A))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to show that the measure (COUNT A) decreases according to
the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme generates the following four new conjectures:
Case 4. (IMPLIES (AND (NLISTP A)
(MEMBER Y A)
(NOT (EQUAL X Y)))
(MEMBER Y (DELETE X A))).
This simplifies, opening up the functions NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP A))
(EQUAL Y (CAR A))
(MEMBER Y A)
(NOT (EQUAL X Y)))
(MEMBER Y (DELETE X A))).
This simplifies, rewriting with CAR-CONS, and opening up the definitions of
NLISTP, MEMBER, and DELETE, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL Y (CAR A)))
(NOT (MEMBER Y (CDR A)))
(MEMBER Y A)
(NOT (EQUAL X Y)))
(MEMBER Y (DELETE X A))),
which simplifies, unfolding the functions NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL Y (CAR A)))
(MEMBER Y (DELETE X (CDR A)))
(MEMBER Y A)
(NOT (EQUAL X Y)))
(MEMBER Y (DELETE X A))),
which simplifies, unfolding the definitions of NLISTP, MEMBER, and DELETE,
to the goal:
(IMPLIES (AND (LISTP A)
(NOT (EQUAL Y (CAR A)))
(MEMBER Y (DELETE X (CDR A)))
(MEMBER Y (CDR A))
(NOT (EQUAL X Y))
(NOT (EQUAL X (CAR A))))
(MEMBER Y
(CONS (CAR A) (DELETE X (CDR A))))).
But this again simplifies, rewriting with CDR-CONS and CAR-CONS, and opening
up the definition of MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
DELETE-LEMMA2
(PROVE-LEMMA DELETE-LEMMA3
(REWRITE)
(IMPLIES (AND (MEMBER X A)
(NOT (MEMBER X B))
(SUBSET B A))
(SUBSET B (DELETE X A)))
((USE (DELETE-LEMMA2 (Y (CAR B))))
(INDUCT (SUBSET B A))))
This conjecture simplifies, expanding the definitions of NOT, AND, IMPLIES,
MEMBER, SUBSET, and OR, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
DELETE-LEMMA3
(PROVE-LEMMA SUBSET-TRANSITIVITY
(REWRITE)
(IMPLIES (AND (SUBSET A B) (SUBSET B C))
(SUBSET A C)))
WARNING: Note that SUBSET-TRANSITIVITY contains the free variable B which
will be chosen by instantiating the hypothesis (SUBSET A B).
Call the conjecture *1.
Perhaps we can prove it by induction. Three inductions are suggested by
terms in the conjecture. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP A) (p (CDR A) C B))
(p A C B))
(IMPLIES (NOT (LISTP A)) (p A C B))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT A) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme leads to three
new goals:
Case 3. (IMPLIES (AND (LISTP A)
(NOT (SUBSET (CDR A) B))
(SUBSET A B)
(SUBSET B C))
(SUBSET A C)),
which simplifies, opening up the definition of SUBSET, to:
T.
Case 2. (IMPLIES (AND (LISTP A)
(SUBSET (CDR A) C)
(SUBSET A B)
(SUBSET B C))
(SUBSET A C)),
which simplifies, expanding SUBSET, to:
(IMPLIES (AND (LISTP A)
(SUBSET (CDR A) C)
(MEMBER (CAR A) B)
(SUBSET (CDR A) B)
(SUBSET B C))
(MEMBER (CAR A) C)).
Appealing to the lemma CAR-CDR-ELIM, we now replace A by (CONS Z X) to
eliminate (CDR A) and (CAR A). The result is the formula:
(IMPLIES (AND (SUBSET X C)
(MEMBER Z B)
(SUBSET X B)
(SUBSET B C))
(MEMBER Z C)).
Give the above formula the name *1.1.
Case 1. (IMPLIES (AND (NOT (LISTP A))
(SUBSET A B)
(SUBSET B C))
(SUBSET A C)).
This simplifies, unfolding the definition of SUBSET, to:
T.
So next consider:
(IMPLIES (AND (SUBSET X C)
(MEMBER Z B)
(SUBSET X B)
(SUBSET B C))
(MEMBER Z C)),
named *1.1 above. We will appeal to induction. There are five plausible
inductions. They merge into three likely candidate inductions. However, only
one is unflawed. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP X) (p Z C B (CDR X)))
(p Z C B X))
(IMPLIES (NOT (LISTP X))
(p Z C B X))).
Linear arithmetic and the lemma CDR-LESSP can be used to show that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme generates three new
formulas:
Case 3. (IMPLIES (AND (LISTP X)
(NOT (SUBSET (CDR X) C))
(SUBSET X C)
(MEMBER Z B)
(SUBSET X B)
(SUBSET B C))
(MEMBER Z C)),
which simplifies, expanding SUBSET, to:
T.
Case 2. (IMPLIES (AND (LISTP X)
(NOT (SUBSET (CDR X) B))
(SUBSET X C)
(MEMBER Z B)
(SUBSET X B)
(SUBSET B C))
(MEMBER Z C)),
which simplifies, unfolding the definition of SUBSET, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP X))
(SUBSET X C)
(MEMBER Z B)
(SUBSET X B)
(SUBSET B C))
(MEMBER Z C)),
which simplifies, expanding SUBSET, to:
(IMPLIES (AND (NOT (LISTP X))
(MEMBER Z B)
(SUBSET B C))
(MEMBER Z C)).
Eliminate the irrelevant term. This produces:
(IMPLIES (AND (MEMBER Z B) (SUBSET B C))
(MEMBER Z C)),
which we will name *1.1.1.
We will appeal to induction. There are three plausible inductions. They
merge into two likely candidate inductions. However, only one is unflawed.
We will induct according to the following scheme:
(AND (IMPLIES (NLISTP B) (p Z C B))
(IMPLIES (AND (NOT (NLISTP B))
(EQUAL Z (CAR B)))
(p Z C B))
(IMPLIES (AND (NOT (NLISTP B))
(NOT (EQUAL Z (CAR B)))
(p Z C (CDR B)))
(p Z C B))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP establish that the measure (COUNT B) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme leads to the following four new conjectures:
Case 4. (IMPLIES (AND (NLISTP B)
(MEMBER Z B)
(SUBSET B C))
(MEMBER Z C)).
This simplifies, expanding the functions NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP B))
(EQUAL Z (CAR B))
(MEMBER Z B)
(SUBSET B C))
(MEMBER Z C)).
This simplifies, expanding the definitions of NLISTP, MEMBER, and SUBSET, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP B))
(NOT (EQUAL Z (CAR B)))
(NOT (MEMBER Z (CDR B)))
(MEMBER Z B)
(SUBSET B C))
(MEMBER Z C)).
This simplifies, unfolding NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP B))
(NOT (EQUAL Z (CAR B)))
(NOT (SUBSET (CDR B) C))
(MEMBER Z B)
(SUBSET B C))
(MEMBER Z C)).
This simplifies, expanding the functions NLISTP, MEMBER, and SUBSET, to:
T.
That finishes the proof of *1.1.1, which, consequently, also finishes the
proof of *1.1, which, in turn, also finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSET-TRANSITIVITY
(PROVE-LEMMA SUBSET-LEMMA0
(REWRITE)
(IMPLIES (AND (SUBSET S1 S) (MEMBER X S1))
(MEMBER X S)))
WARNING: Note that SUBSET-LEMMA0 contains the free variable S1 which will be
chosen by instantiating the hypothesis (SUBSET S1 S).
Call the conjecture *1.
Perhaps we can prove it by induction. Three inductions are suggested by
terms in the conjecture. They merge into two likely candidate inductions.
However, only one is unflawed. We will induct according to the following
scheme:
(AND (IMPLIES (AND (LISTP S1) (p X S (CDR S1)))
(p X S S1))
(IMPLIES (NOT (LISTP S1))
(p X S S1))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT S1) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme leads to three
new goals:
Case 3. (IMPLIES (AND (LISTP S1)
(NOT (SUBSET (CDR S1) S))
(SUBSET S1 S)
(MEMBER X S1))
(MEMBER X S)),
which simplifies, opening up the definition of SUBSET, to:
T.
Case 2. (IMPLIES (AND (LISTP S1)
(NOT (MEMBER X (CDR S1)))
(SUBSET S1 S)
(MEMBER X S1))
(MEMBER X S)),
which simplifies, expanding SUBSET and MEMBER, to:
(IMPLIES (AND (LISTP S1)
(NOT (MEMBER X (CDR S1)))
(MEMBER (CAR S1) S)
(SUBSET (CDR S1) S)
(EQUAL X (CAR S1)))
(MEMBER X S)).
This again simplifies, trivially, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP S1))
(SUBSET S1 S)
(MEMBER X S1))
(MEMBER X S)).
This simplifies, opening up the functions SUBSET and MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSET-LEMMA0
(PROVE-LEMMA SUBSET-LEMMA1
(REWRITE)
(IMPLIES (SUBSET A B)
(SUBSET A (CONS C B))))
Give the conjecture the name *1.
Let us appeal to the induction principle. Two inductions are suggested
by terms in the conjecture. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP A) (p (CDR A) C B))
(p A C B))
(IMPLIES (NOT (LISTP A)) (p A C B))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT A)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates three new conjectures:
Case 3. (IMPLIES (AND (LISTP A)
(NOT (SUBSET (CDR A) B))
(SUBSET A B))
(SUBSET A (CONS C B))),
which simplifies, expanding the function SUBSET, to:
T.
Case 2. (IMPLIES (AND (LISTP A)
(SUBSET (CDR A) (CONS C B))
(SUBSET A B))
(SUBSET A (CONS C B))),
which simplifies, appealing to the lemmas CDR-CONS and CAR-CONS, and
expanding SUBSET and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP A)) (SUBSET A B))
(SUBSET A (CONS C B))),
which simplifies, opening up SUBSET, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSET-LEMMA1
(PROVE-LEMMA SUBSET-LEMMA2
(REWRITE)
(IMPLIES (SUBSET A B)
(SUBSET (SET-MINUS A C) B)))
Give the conjecture the name *1.
Let us appeal to the induction principle. Two inductions are suggested
by terms in the conjecture. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP A) (p (CDR A) C B))
(p A C B))
(IMPLIES (NOT (LISTP A)) (p A C B))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT A)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates three new conjectures:
Case 3. (IMPLIES (AND (LISTP A)
(NOT (SUBSET (CDR A) B))
(SUBSET A B))
(SUBSET (SET-MINUS A C) B)),
which simplifies, expanding the function SUBSET, to:
T.
Case 2. (IMPLIES (AND (LISTP A)
(SUBSET (SET-MINUS (CDR A) C) B)
(SUBSET A B))
(SUBSET (SET-MINUS A C) B)),
which simplifies, opening up the functions SUBSET and SET-MINUS, to:
(IMPLIES (AND (LISTP A)
(SUBSET (SET-MINUS (CDR A) C) B)
(MEMBER (CAR A) B)
(SUBSET (CDR A) B)
(NOT (MEMBER (CAR A) C)))
(SUBSET (CONS (CAR A) (SET-MINUS (CDR A) C))
B)).
But this again simplifies, rewriting with the lemmas CDR-CONS and CAR-CONS,
and opening up the function SUBSET, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP A)) (SUBSET A B))
(SUBSET (SET-MINUS A C) B)),
which simplifies, expanding SUBSET and SET-MINUS, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSET-LEMMA2
(PROVE-LEMMA SUBSET-REFLEXIVITY
(REWRITE)
(SUBSET A A))
Give the conjecture the name *1.
Perhaps we can prove it by induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP A) (p (CDR A)))
(p A))
(IMPLIES (NOT (LISTP A)) (p A))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT A)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates the following two new
formulas:
Case 2. (IMPLIES (AND (LISTP A)
(SUBSET (CDR A) (CDR A)))
(SUBSET A A)).
This simplifies, expanding the functions SUBSET and MEMBER, to the new goal:
(IMPLIES (AND (LISTP A)
(SUBSET (CDR A) (CDR A)))
(SUBSET (CDR A) A)).
Applying the lemma CAR-CDR-ELIM, replace A by (CONS Z X) to eliminate
(CDR A) and (CAR A). This produces:
(IMPLIES (SUBSET X X)
(SUBSET X (CONS Z X))),
which further simplifies, rewriting with SUBSET-LEMMA1, to:
T.
Case 1. (IMPLIES (NOT (LISTP A))
(SUBSET A A)).
This simplifies, unfolding the function SUBSET, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
SUBSET-REFLEXIVITY
(PROVE-LEMMA CARDINAL-LEMMA NIL
(IMPLIES (MEMBER X S)
(LEQ 1 (CARDINAL S))))
Call the conjecture *1.
We will appeal to induction. There are two plausible inductions.
However, they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (NLISTP S) (p S X))
(IMPLIES (AND (NOT (NLISTP S))
(EQUAL X (CAR S)))
(p S X))
(IMPLIES (AND (NOT (NLISTP S))
(NOT (EQUAL X (CAR S)))
(p (CDR S) X))
(p S X))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to establish that the measure (COUNT S) decreases according
to the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme generates four new formulas:
Case 4. (IMPLIES (AND (NLISTP S) (MEMBER X S))
(NOT (LESSP (CARDINAL S) 1))),
which simplifies, expanding the definitions of NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP S))
(EQUAL X (CAR S))
(MEMBER X S))
(NOT (LESSP (CARDINAL S) 1))),
which simplifies, applying the lemma SUB1-ADD1, and unfolding the
definitions of NLISTP, MEMBER, CARDINAL, SUB1, NUMBERP, EQUAL, and LESSP, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP S))
(NOT (EQUAL X (CAR S)))
(NOT (MEMBER X (CDR S)))
(MEMBER X S))
(NOT (LESSP (CARDINAL S) 1))),
which simplifies, expanding the definitions of NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP S))
(NOT (EQUAL X (CAR S)))
(NOT (LESSP (CARDINAL (CDR S)) 1))
(MEMBER X S))
(NOT (LESSP (CARDINAL S) 1))),
which simplifies, applying SUB1-ADD1, and expanding the functions NLISTP,
MEMBER, CARDINAL, SUB1, NUMBERP, EQUAL, and LESSP, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
CARDINAL-LEMMA
(PROVE-LEMMA CARDINAL-EQUALITY NIL
(IMPLIES (AND (SET-STANDARD A)
(NOT (MEMBER C B))
(MEMBER C A))
(EQUAL (CARDINAL (SET-MINUS A B))
(ADD1 (CARDINAL (SET-MINUS A (CONS C B))))))
((INDUCT (SET-MINUS A B))))
This conjecture can be simplified, using the abbreviations IMPLIES, NOT, OR,
and AND, to three new formulas:
Case 3. (IMPLIES
(AND
(LISTP A)
(MEMBER (CAR A) B)
(IMPLIES (AND (SET-STANDARD (CDR A))
(NOT (MEMBER C B))
(MEMBER C (CDR A)))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(ADD1 (CARDINAL (SET-MINUS (CDR A) (CONS C B))))))
(SET-STANDARD A)
(NOT (MEMBER C B))
(MEMBER C A))
(EQUAL (CARDINAL (SET-MINUS A B))
(ADD1 (CARDINAL (SET-MINUS A (CONS C B)))))),
which simplifies, appealing to the lemmas CDR-CONS, CAR-CONS, and
SET-MINUS-LEMMA2, and unfolding the definitions of NOT, AND, IMPLIES,
SET-STANDARD, MEMBER, SET-MINUS, and CARDINAL, to:
(IMPLIES (AND (LISTP A)
(MEMBER (CAR A) B)
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(ADD1 (CARDINAL (SET-MINUS (CDR A) (CONS C B)))))
(NOT (MEMBER (CAR A) (CDR A)))
(SET-STANDARD (CDR A))
(NOT (MEMBER C B)))
(NOT (EQUAL C (CAR A)))).
This again simplifies, trivially, to:
T.
Case 2. (IMPLIES
(AND
(LISTP A)
(NOT (MEMBER (CAR A) B))
(IMPLIES (AND (SET-STANDARD (CDR A))
(NOT (MEMBER C B))
(MEMBER C (CDR A)))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(ADD1 (CARDINAL (SET-MINUS (CDR A) (CONS C B))))))
(SET-STANDARD A)
(NOT (MEMBER C B))
(MEMBER C A))
(EQUAL (CARDINAL (SET-MINUS A B))
(ADD1 (CARDINAL (SET-MINUS A (CONS C B)))))).
This simplifies, appealing to the lemmas CDR-CONS, CAR-CONS,
SET-MINUS-LEMMA2, and ADD1-EQUAL, and opening up NOT, AND, IMPLIES,
SET-STANDARD, MEMBER, SET-MINUS, and CARDINAL, to the following three new
goals:
Case 2.3.
(IMPLIES
(AND (LISTP A)
(NOT (MEMBER (CAR A) B))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(ADD1 (CARDINAL (SET-MINUS (CDR A) (CONS C B)))))
(NOT (MEMBER (CAR A) (CDR A)))
(SET-STANDARD (CDR A))
(NOT (MEMBER C B)))
(NOT (EQUAL C (CAR A)))).
This again simplifies, appealing to the lemma SET-MINUS-LEMMA2, to:
T.
Case 2.2.
(IMPLIES
(AND (LISTP A)
(NOT (MEMBER (CAR A) B))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(ADD1 (CARDINAL (SET-MINUS (CDR A) (CONS C B)))))
(NOT (MEMBER (CAR A) (CDR A)))
(SET-STANDARD (CDR A))
(NOT (MEMBER C B))
(MEMBER C (CDR A))
(NOT (EQUAL (CAR A) C)))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(CARDINAL (CONS (CAR A)
(SET-MINUS (CDR A) (CONS C B)))))),
which again simplifies, applying the lemma CDR-CONS, and opening up the
function CARDINAL, to:
T.
Case 2.1.
(IMPLIES
(AND (LISTP A)
(NOT (MEMBER (CAR A) B))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(ADD1 (CARDINAL (SET-MINUS (CDR A) (CONS C B)))))
(NOT (MEMBER (CAR A) (CDR A)))
(SET-STANDARD (CDR A))
(NOT (MEMBER C B))
(MEMBER C (CDR A))
(EQUAL (CAR A) C))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(CARDINAL (SET-MINUS (CDR A) (CONS C B))))),
which again simplifies, obviously, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP A))
(SET-STANDARD A)
(NOT (MEMBER C B))
(MEMBER C A))
(EQUAL (CARDINAL (SET-MINUS A B))
(ADD1 (CARDINAL (SET-MINUS A (CONS C B)))))).
This simplifies, expanding the functions SET-STANDARD and MEMBER, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
CARDINAL-EQUALITY
(DEFN CARDINAL-INEQUALITY-INDUCT
(B A)
(IF (LISTP B)
(CARDINAL-INEQUALITY-INDUCT (CDR B)
(DELETE (CAR B) A))
T))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT B) decreases according to the well-founded relation LESSP in each
recursive call. Hence, CARDINAL-INEQUALITY-INDUCT is accepted under the
definitional principle. Observe that (TRUEP (CARDINAL-INEQUALITY-INDUCT B A))
is a theorem.
[ 0.0 0.0 0.0 ]
CARDINAL-INEQUALITY-INDUCT
(PROVE-LEMMA CARDINAL-INEQUALITY NIL
(IMPLIES (AND (SET-STANDARD B) (SUBSET B A))
(LEQ (CARDINAL B) (CARDINAL A)))
((USE (DELETE-LEMMA3 (X (CAR B))
(B (CDR B)))
(DELETE-LEMMA1 (X (CAR B)) (A A)))
(INDUCT (CARDINAL-INEQUALITY-INDUCT B A))))
This conjecture simplifies, rewriting with SUBSET-REFLEXIVITY and
SUBSET-TRANSITIVITY, and unfolding the functions NOT, AND, IMPLIES,
SET-STANDARD, SUBSET, CARDINAL, and OR, to eight new conjectures:
Case 8. (IMPLIES (AND (NOT (MEMBER (CAR B) A))
(NOT (LISTP B)))
(NOT (LESSP (CARDINAL A) 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 7. (IMPLIES (AND (MEMBER (CAR B) (CDR B))
(NOT (MEMBER (CAR B) A))
(NOT (LISTP B)))
(NOT (LESSP (CARDINAL A) 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 6. (IMPLIES (AND (MEMBER (CAR B) (CDR B))
(EQUAL (CARDINAL A)
(ADD1 (CARDINAL (DELETE (CAR B) A))))
(NOT (LISTP B)))
(NOT (LESSP (CARDINAL A) 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 5. (IMPLIES (AND (NOT (SUBSET (CDR B) A))
(NOT (MEMBER (CAR B) A))
(NOT (LISTP B)))
(NOT (LESSP (CARDINAL A) 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 4. (IMPLIES (AND (NOT (SUBSET (CDR B) A))
(EQUAL (CARDINAL A)
(ADD1 (CARDINAL (DELETE (CAR B) A))))
(NOT (LISTP B)))
(NOT (LESSP (CARDINAL A) 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 3. (IMPLIES (AND (SUBSET (CDR B) (DELETE (CAR B) A))
(NOT (MEMBER (CAR B) A))
(NOT (LISTP B)))
(NOT (LESSP (CARDINAL A) 0))),
which again simplifies, using linear arithmetic, to:
T.
Case 2. (IMPLIES (AND (SUBSET (CDR B) (DELETE (CAR B) A))
(EQUAL (CARDINAL A)
(ADD1 (CARDINAL (DELETE (CAR B) A))))
(LISTP B)
(SET-STANDARD (CDR B))
(NOT (LESSP (CARDINAL (DELETE (CAR B) A))
(CARDINAL (CDR B))))
(NOT (MEMBER (CAR B) (CDR B)))
(MEMBER (CAR B) A)
(SUBSET (CDR B) A))
(NOT (LESSP (CARDINAL A)
(ADD1 (CARDINAL (CDR B)))))),
which again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (SUBSET (CDR B) (DELETE (CAR B) A))
(EQUAL (CARDINAL A)
(ADD1 (CARDINAL (DELETE (CAR B) A))))
(NOT (LISTP B)))
(NOT (LESSP (CARDINAL A) 0))),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
CARDINAL-INEQUALITY
(PROVE-LEMMA CARDINAL-SUBSET
(REWRITE)
(IMPLIES (AND (SET-STANDARD A)
(SET-STANDARD B)
(SUBSET B A))
(EQUAL (CARDINAL (SET-MINUS A B))
(DIFFERENCE (CARDINAL A)
(CARDINAL B))))
((USE (CARDINAL-EQUALITY (B (CDR B))
(C (CAR B)))
(CARDINAL-INEQUALITY (B (CDR B))
(A A)))
(INDUCT (SUBSET B A))))
This conjecture simplifies, appealing to the lemmas CONS-CAR-CDR, CDR-NLISTP,
and SUB1-ADD1, and unfolding NOT, AND, IMPLIES, SET-STANDARD, SUBSET, CARDINAL,
OR, LISTP, EQUAL, LESSP, and DIFFERENCE, to the following ten new formulas:
Case 10.(IMPLIES (AND (MEMBER (CAR B) (CDR B))
(NOT (SET-STANDARD (CDR B)))
(NOT (LISTP B))
(SET-STANDARD A))
(EQUAL (CARDINAL (SET-MINUS A B))
(DIFFERENCE (CARDINAL A) 0))).
But this again simplifies, applying CAR-NLISTP and CDR-NLISTP, and expanding
MEMBER, to:
T.
Case 9. (IMPLIES (AND (MEMBER (CAR B) (CDR B))
(NOT (SUBSET (CDR B) A))
(NOT (LISTP B))
(SET-STANDARD A))
(EQUAL (CARDINAL (SET-MINUS A B))
(DIFFERENCE (CARDINAL A) 0))).
But this again simplifies, appealing to the lemmas CAR-NLISTP and CDR-NLISTP,
and opening up the definition of MEMBER, to:
T.
Case 8. (IMPLIES (AND (MEMBER (CAR B) (CDR B))
(NOT (LESSP (CARDINAL A)
(CARDINAL (CDR B))))
(NOT (LISTP B))
(SET-STANDARD A))
(EQUAL (CARDINAL (SET-MINUS A B))
(DIFFERENCE (CARDINAL A) 0))),
which again simplifies, applying CAR-NLISTP and CDR-NLISTP, and opening up
MEMBER, to:
T.
Case 7. (IMPLIES (AND (NOT (MEMBER (CAR B) A))
(NOT (SET-STANDARD (CDR B)))
(NOT (LISTP B))
(SET-STANDARD A))
(EQUAL (CARDINAL (SET-MINUS A B))
(DIFFERENCE (CARDINAL A) 0))).
However this again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
expanding SET-STANDARD, to:
T.
Case 6. (IMPLIES (AND (NOT (MEMBER (CAR B) A))
(NOT (SUBSET (CDR B) A))
(NOT (LISTP B))
(SET-STANDARD A))
(EQUAL (CARDINAL (SET-MINUS A B))
(DIFFERENCE (CARDINAL A) 0))).
But this again simplifies, applying CAR-NLISTP and CDR-NLISTP, and unfolding
the definitions of LISTP and SUBSET, to:
T.
Case 5. (IMPLIES (AND (NOT (MEMBER (CAR B) A))
(NOT (LESSP (CARDINAL A)
(CARDINAL (CDR B))))
(NOT (LISTP B))
(SET-STANDARD A))
(EQUAL (CARDINAL (SET-MINUS A B))
(DIFFERENCE (CARDINAL A) 0))).
This again simplifies, appealing to the lemmas CAR-NLISTP and CDR-NLISTP,
and expanding the definitions of CARDINAL, EQUAL, LESSP, and DIFFERENCE, to
two new goals:
Case 5.2.
(IMPLIES (AND (NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))),
which we will name *1.
Case 5.1.
(IMPLIES (AND (NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)).
Name the above subgoal *2.
Case 4. (IMPLIES (AND (NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A (CDR B)))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)).
But this again simplifies, rewriting with CDR-NLISTP, to:
(IMPLIES (AND (NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)),
which we will name *3.
Case 3. (IMPLIES (AND (NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A (CDR B)))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
This again simplifies, applying the lemma CDR-NLISTP, to:
(IMPLIES (AND (NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
Give the above formula the name *4.
Case 2. (IMPLIES (AND (LISTP B)
(EQUAL (CARDINAL (SET-MINUS A (CDR B)))
(ADD1 (CARDINAL (SET-MINUS A B))))
(NOT (LESSP (CARDINAL A)
(CARDINAL (CDR B))))
(SET-STANDARD A)
(SET-STANDARD (CDR B))
(SUBSET (CDR B) A)
(EQUAL (ADD1 (CARDINAL (SET-MINUS A B)))
(DIFFERENCE (CARDINAL A)
(CARDINAL (CDR B))))
(NOT (MEMBER (CAR B) (CDR B)))
(MEMBER (CAR B) A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(DIFFERENCE (SUB1 (CARDINAL A))
(CARDINAL (CDR B))))).
However this again simplifies, using linear arithmetic, to the conjecture:
(IMPLIES (AND (LESSP (SUB1 (CARDINAL A))
(CARDINAL (CDR B)))
(LISTP B)
(EQUAL (CARDINAL (SET-MINUS A (CDR B)))
(ADD1 (CARDINAL (SET-MINUS A B))))
(NOT (LESSP (CARDINAL A)
(CARDINAL (CDR B))))
(SET-STANDARD A)
(SET-STANDARD (CDR B))
(SUBSET (CDR B) A)
(EQUAL (ADD1 (CARDINAL (SET-MINUS A B)))
(DIFFERENCE (CARDINAL A)
(CARDINAL (CDR B))))
(NOT (MEMBER (CAR B) (CDR B)))
(MEMBER (CAR B) A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(DIFFERENCE (SUB1 (CARDINAL A))
(CARDINAL (CDR B))))).
But this again simplifies, using linear arithmetic, to:
T.
Case 1. (IMPLIES (AND (LISTP B)
(EQUAL (CARDINAL (SET-MINUS A (CDR B)))
(ADD1 (CARDINAL (SET-MINUS A B))))
(NOT (LESSP (CARDINAL A)
(CARDINAL (CDR B))))
(SET-STANDARD A)
(SET-STANDARD (CDR B))
(SUBSET (CDR B) A)
(EQUAL (ADD1 (CARDINAL (SET-MINUS A B)))
(DIFFERENCE (CARDINAL A)
(CARDINAL (CDR B))))
(NOT (MEMBER (CAR B) (CDR B)))
(MEMBER (CAR B) A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)),
which again simplifies, using linear arithmetic, to:
T.
So next consider:
(IMPLIES (AND (NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))),
which we named *4 above. Let us appeal to the induction principle. There are
six plausible inductions. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP A)
(MEMBER (CAR A) 0)
(p (CDR A) B))
(p A B))
(IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) 0))
(p (CDR A) B))
(p A B))
(IMPLIES (NOT (LISTP A)) (p A B))).
Linear arithmetic and the lemma CDR-LESSP can be used to establish that the
measure (COUNT A) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme leads to the
following nine new goals:
Case 9. (IMPLIES
(AND (LISTP A)
(MEMBER (CAR A) 0)
(NOT (EQUAL (CARDINAL (SET-MINUS (CDR A) 0))
(ADD1 (CARDINAL (SET-MINUS (CDR A) '(0 . 0))))))
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
This simplifies, unfolding LISTP and MEMBER, to:
T.
Case 8. (IMPLIES (AND (LISTP A)
(MEMBER (CAR A) 0)
(NOT (SET-STANDARD (CDR A)))
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
This simplifies, expanding the definitions of LISTP and MEMBER, to:
T.
Case 7. (IMPLIES (AND (LISTP A)
(MEMBER (CAR A) 0)
(EQUAL (CARDINAL (CDR A)) 0)
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
This simplifies, unfolding LISTP and MEMBER, to:
T.
Case 6. (IMPLIES (AND (LISTP A)
(MEMBER (CAR A) 0)
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(CARDINAL (CDR A)))
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
This simplifies, opening up LISTP and MEMBER, to:
T.
Case 5. (IMPLIES
(AND (LISTP A)
(NOT (MEMBER (CAR A) 0))
(NOT (EQUAL (CARDINAL (SET-MINUS (CDR A) 0))
(ADD1 (CARDINAL (SET-MINUS (CDR A) '(0 . 0))))))
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
This simplifies, rewriting with CDR-CONS and ADD1-EQUAL, and unfolding the
definitions of LISTP, MEMBER, SET-MINUS, CARDINAL, CDR, CAR, and
SET-STANDARD, to two new goals:
Case 5.2.
(IMPLIES
(AND (LISTP A)
(NOT (EQUAL (CARDINAL (SET-MINUS (CDR A) 0))
(ADD1 (CARDINAL (SET-MINUS (CDR A) '(0 . 0))))))
(NOT (LISTP B))
(NOT (EQUAL (CAR A) 0))
(EQUAL (CARDINAL (SET-MINUS (CDR A) 0))
(CARDINAL (CONS (CAR A)
(SET-MINUS (CDR A) '(0 . 0)))))
(NOT (MEMBER (CAR A) (CDR A)))
(SET-STANDARD (CDR A)))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(CARDINAL (CDR A)))),
which again simplifies, applying the lemma CDR-CONS, and unfolding the
definition of CARDINAL, to:
T.
Case 5.1.
(IMPLIES
(AND (LISTP A)
(NOT (EQUAL (CARDINAL (SET-MINUS (CDR A) 0))
(ADD1 (CARDINAL (SET-MINUS (CDR A) '(0 . 0))))))
(NOT (LISTP B))
(EQUAL (CAR A) 0)
(EQUAL (CARDINAL (SET-MINUS (CDR A) 0))
(CARDINAL (SET-MINUS (CDR A) '(0 . 0))))
(NOT (MEMBER 0 (CDR A)))
(SET-STANDARD (CDR A)))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(CARDINAL (CDR A)))),
which again simplifies, trivially, to:
(IMPLIES (AND (LISTP A)
(NOT (LISTP B))
(EQUAL (CAR A) 0)
(EQUAL (CARDINAL (SET-MINUS (CDR A) 0))
(CARDINAL (SET-MINUS (CDR A) '(0 . 0))))
(NOT (MEMBER 0 (CDR A)))
(SET-STANDARD (CDR A)))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(CARDINAL (CDR A)))),
which further simplifies, rewriting with SET-MINUS-LEMMA2, to the new
conjecture:
(IMPLIES (AND (LISTP A)
(NOT (LISTP B))
(EQUAL (CAR A) 0)
(NOT (MEMBER 0 (CDR A)))
(SET-STANDARD (CDR A)))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(CARDINAL (CDR A)))).
Applying the lemma CAR-CDR-ELIM, replace A by (CONS X Z) to eliminate
(CAR A) and (CDR A). We would thus like to prove:
(IMPLIES (AND (NOT (LISTP B))
(EQUAL X 0)
(NOT (MEMBER 0 Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B))
(CARDINAL Z))),
which further simplifies, clearly, to:
(IMPLIES (AND (NOT (LISTP B))
(NOT (MEMBER 0 Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B))
(CARDINAL Z))),
which we will finally name *4.1.
Case 4. (IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) 0))
(NOT (SET-STANDARD (CDR A)))
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
This simplifies, rewriting with CDR-CONS and ADD1-EQUAL, and expanding the
functions LISTP, MEMBER, SET-MINUS, CARDINAL, CDR, CAR, and SET-STANDARD, to:
T.
Case 3. (IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) 0))
(EQUAL (CARDINAL (CDR A)) 0)
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))),
which simplifies, rewriting with CDR-CONS and ADD1-EQUAL, and unfolding the
functions LISTP, MEMBER, SET-MINUS, CARDINAL, CDR, CAR, SET-STANDARD, ADD1,
EQUAL, and NUMBERP, to the following two new formulas:
Case 3.2.
(IMPLIES
(AND (LISTP A)
(EQUAL (CARDINAL (CDR A)) 0)
(NOT (LISTP B))
(NOT (EQUAL (CAR A) 0))
(EQUAL (CARDINAL (SET-MINUS (CDR A) 0))
(CARDINAL (CONS (CAR A)
(SET-MINUS (CDR A) '(0 . 0)))))
(NOT (MEMBER (CAR A) (CDR A)))
(SET-STANDARD (CDR A)))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
0)).
But this again simplifies, applying CDR-CONS, and opening up CARDINAL, to:
(IMPLIES
(AND (LISTP A)
(EQUAL (CARDINAL (CDR A)) 0)
(NOT (LISTP B))
(NOT (EQUAL (CAR A) 0))
(EQUAL (CARDINAL (SET-MINUS (CDR A) 0))
(ADD1 (CARDINAL (SET-MINUS (CDR A) '(0 . 0)))))
(NOT (MEMBER (CAR A) (CDR A)))
(SET-STANDARD (CDR A)))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
0)).
Applying the lemma CAR-CDR-ELIM, replace A by (CONS Z X) to eliminate
(CDR A) and (CAR A). This produces:
(IMPLIES (AND (EQUAL (CARDINAL X) 0)
(NOT (LISTP B))
(NOT (EQUAL Z 0))
(EQUAL (CARDINAL (SET-MINUS X 0))
(ADD1 (CARDINAL (SET-MINUS X '(0 . 0)))))
(NOT (MEMBER Z X))
(SET-STANDARD X))
(EQUAL (CARDINAL (SET-MINUS X B)) 0)),
which we will name *4.2.
Case 3.1.
(IMPLIES (AND (LISTP A)
(EQUAL (CARDINAL (CDR A)) 0)
(NOT (LISTP B))
(EQUAL (CAR A) 0)
(EQUAL (CARDINAL (SET-MINUS (CDR A) 0))
(CARDINAL (SET-MINUS (CDR A) '(0 . 0))))
(NOT (MEMBER 0 (CDR A)))
(SET-STANDARD (CDR A)))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
0)).
But this further simplifies, applying SET-MINUS-LEMMA2, to:
(IMPLIES (AND (LISTP A)
(EQUAL (CARDINAL (CDR A)) 0)
(NOT (LISTP B))
(EQUAL (CAR A) 0)
(NOT (MEMBER 0 (CDR A)))
(SET-STANDARD (CDR A)))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
0)).
Applying the lemma CAR-CDR-ELIM, replace A by (CONS Z X) to eliminate
(CDR A) and (CAR A). This produces the new formula:
(IMPLIES (AND (EQUAL (CARDINAL X) 0)
(NOT (LISTP B))
(EQUAL Z 0)
(NOT (MEMBER 0 X))
(SET-STANDARD X))
(EQUAL (CARDINAL (SET-MINUS X B)) 0)),
which further simplifies, trivially, to:
(IMPLIES (AND (EQUAL (CARDINAL X) 0)
(NOT (LISTP B))
(NOT (MEMBER 0 X))
(SET-STANDARD X))
(EQUAL (CARDINAL (SET-MINUS X B)) 0)),
which we will name *4.3.
Case 2. (IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) 0))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(CARDINAL (CDR A)))
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
This simplifies, rewriting with CDR-CONS and ADD1-EQUAL, and expanding LISTP,
MEMBER, SET-MINUS, CARDINAL, CDR, CAR, and SET-STANDARD, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP A))
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))),
which simplifies, applying SET-MINUS-LEMMA2, and expanding the functions
SET-MINUS, CARDINAL, MEMBER, ADD1, and EQUAL, to:
T.
So next consider:
(IMPLIES (AND (EQUAL (CARDINAL X) 0)
(NOT (LISTP B))
(NOT (MEMBER 0 X))
(SET-STANDARD X))
(EQUAL (CARDINAL (SET-MINUS X B)) 0)),
named *4.3 above. What luck! This conjecture is subsumed by the subgoal we
named *2 above.
So let us turn our attention to:
(IMPLIES (AND (EQUAL (CARDINAL X) 0)
(NOT (LISTP B))
(NOT (EQUAL Z 0))
(EQUAL (CARDINAL (SET-MINUS X 0))
(ADD1 (CARDINAL (SET-MINUS X '(0 . 0)))))
(NOT (MEMBER Z X))
(SET-STANDARD X))
(EQUAL (CARDINAL (SET-MINUS X B)) 0)),
named *4.2 above. Ah ha! This conjecture is subsumed by formula *3 above.
So we now return to:
(IMPLIES (AND (NOT (LISTP B))
(NOT (MEMBER 0 Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B))
(CARDINAL Z))),
which is formula *4.1 above. We will appeal to induction. The recursive
terms in the conjecture suggest four inductions. However, they merge into one
likely candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP Z) (p Z B))
(IMPLIES (AND (NOT (NLISTP Z))
(EQUAL 0 (CAR Z)))
(p Z B))
(IMPLIES (AND (NOT (NLISTP Z))
(NOT (EQUAL 0 (CAR Z)))
(p (CDR Z) B))
(p Z B))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP inform us that the measure (COUNT Z) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme produces the following five new formulas:
Case 5. (IMPLIES (AND (NLISTP Z)
(NOT (LISTP B))
(NOT (MEMBER 0 Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B))
(CARDINAL Z))).
This simplifies, opening up NLISTP, MEMBER, SET-STANDARD, SET-MINUS,
CARDINAL, and EQUAL, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP Z))
(EQUAL 0 (CAR Z))
(NOT (LISTP B))
(NOT (MEMBER 0 Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B))
(CARDINAL Z))).
This simplifies, opening up the definitions of NLISTP, MEMBER, and EQUAL, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP Z))
(NOT (EQUAL 0 (CAR Z)))
(MEMBER 0 (CDR Z))
(NOT (LISTP B))
(NOT (MEMBER 0 Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B))
(CARDINAL Z))).
This simplifies, unfolding the definitions of NLISTP and MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP Z))
(NOT (EQUAL 0 (CAR Z)))
(NOT (SET-STANDARD (CDR Z)))
(NOT (LISTP B))
(NOT (MEMBER 0 Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B))
(CARDINAL Z))).
This simplifies, unfolding NLISTP, MEMBER, and SET-STANDARD, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP Z))
(NOT (EQUAL 0 (CAR Z)))
(EQUAL (CARDINAL (SET-MINUS (CDR Z) B))
(CARDINAL (CDR Z)))
(NOT (LISTP B))
(NOT (MEMBER 0 Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B))
(CARDINAL Z))).
This simplifies, rewriting with the lemma CDR-CONS, and unfolding the
definitions of NLISTP, MEMBER, SET-STANDARD, SET-MINUS, and CARDINAL, to:
T.
That finishes the proof of *4.1, which, consequently, also finishes the
proof of *4.
So let us turn our attention to:
(IMPLIES (AND (NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)),
named *3 above. We will appeal to induction. Five inductions are suggested
by terms in the conjecture. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP A)
(MEMBER (CAR A) 0)
(p (CDR A) B))
(p A B))
(IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) 0))
(p (CDR A) B))
(p A B))
(IMPLIES (NOT (LISTP A)) (p A B))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT A)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme leads to the following nine new
formulas:
Case 9. (IMPLIES
(AND (LISTP A)
(MEMBER (CAR A) 0)
(NOT (EQUAL (CARDINAL (SET-MINUS (CDR A) 0))
(ADD1 (CARDINAL (SET-MINUS (CDR A) '(0 . 0))))))
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)).
This simplifies, expanding LISTP and MEMBER, to:
T.
Case 8. (IMPLIES (AND (LISTP A)
(MEMBER (CAR A) 0)
(NOT (SET-STANDARD (CDR A)))
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)).
This simplifies, opening up the definitions of LISTP and MEMBER, to:
T.
Case 7. (IMPLIES (AND (LISTP A)
(MEMBER (CAR A) 0)
(NOT (EQUAL (CARDINAL (CDR A)) 0))
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)).
This simplifies, expanding LISTP and MEMBER, to:
T.
Case 6. (IMPLIES (AND (LISTP A)
(MEMBER (CAR A) 0)
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
0)
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)).
This simplifies, expanding the functions LISTP and MEMBER, to:
T.
Case 5. (IMPLIES
(AND (LISTP A)
(NOT (MEMBER (CAR A) 0))
(NOT (EQUAL (CARDINAL (SET-MINUS (CDR A) 0))
(ADD1 (CARDINAL (SET-MINUS (CDR A) '(0 . 0))))))
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)).
This simplifies, appealing to the lemmas CDR-CONS and ADD1-EQUAL, and
unfolding LISTP, MEMBER, SET-MINUS, CARDINAL, CDR, CAR, and SET-STANDARD, to:
T.
Case 4. (IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) 0))
(NOT (SET-STANDARD (CDR A)))
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)).
This simplifies, rewriting with the lemmas CDR-CONS and ADD1-EQUAL, and
unfolding the definitions of LISTP, MEMBER, SET-MINUS, CARDINAL, CDR, CAR,
and SET-STANDARD, to:
T.
Case 3. (IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) 0))
(NOT (EQUAL (CARDINAL (CDR A)) 0))
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)).
This simplifies, rewriting with CDR-CONS and ADD1-EQUAL, and expanding LISTP,
MEMBER, SET-MINUS, CARDINAL, CDR, CAR, and SET-STANDARD, to:
T.
Case 2. (IMPLIES (AND (LISTP A)
(NOT (MEMBER (CAR A) 0))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
0)
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)),
which simplifies, rewriting with CDR-CONS and ADD1-EQUAL, and opening up
LISTP, MEMBER, SET-MINUS, CARDINAL, CDR, CAR, and SET-STANDARD, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP A))
(NOT (LISTP B))
(EQUAL (CARDINAL (SET-MINUS A 0))
(ADD1 (CARDINAL (SET-MINUS A '(0 . 0)))))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)).
This simplifies, applying SET-MINUS-LEMMA2, and opening up the functions
SET-MINUS, CARDINAL, MEMBER, ADD1, and EQUAL, to:
T.
That finishes the proof of *3.
So next consider:
(IMPLIES (AND (NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)),
which is formula *2 above. We will try to prove it by induction. The
recursive terms in the conjecture suggest four inductions. However, they
merge into one likely candidate induction. We will induct according to the
following scheme:
(AND (IMPLIES (NLISTP A) (p A B))
(IMPLIES (AND (NOT (NLISTP A))
(EQUAL 0 (CAR A)))
(p A B))
(IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL 0 (CAR A)))
(p (CDR A) B))
(p A B))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP establish that the measure (COUNT A) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme generates six new goals:
Case 6. (IMPLIES (AND (NLISTP A)
(NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)),
which simplifies, opening up NLISTP, MEMBER, SET-STANDARD, CARDINAL, EQUAL,
and SET-MINUS, to:
T.
Case 5. (IMPLIES (AND (NOT (NLISTP A))
(EQUAL 0 (CAR A))
(NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)),
which simplifies, opening up NLISTP, MEMBER, and EQUAL, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL 0 (CAR A)))
(MEMBER 0 (CDR A))
(NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)),
which simplifies, unfolding NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL 0 (CAR A)))
(NOT (SET-STANDARD (CDR A)))
(NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)),
which simplifies, expanding the definitions of NLISTP, MEMBER, and
SET-STANDARD, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL 0 (CAR A)))
(NOT (EQUAL (CARDINAL (CDR A)) 0))
(NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)),
which simplifies, unfolding the definitions of NLISTP, MEMBER, SET-STANDARD,
and CARDINAL, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL 0 (CAR A)))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
0)
(NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(EQUAL (CARDINAL A) 0))
(EQUAL (CARDINAL (SET-MINUS A B)) 0)),
which simplifies, opening up NLISTP, MEMBER, SET-STANDARD, and CARDINAL, to:
T.
That finishes the proof of *2.
So next consider:
(IMPLIES (AND (NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))),
which we named *1 above. We will try to prove it by induction. There are
five plausible inductions. However, they merge into one likely candidate
induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP A) (p A B))
(IMPLIES (AND (NOT (NLISTP A))
(EQUAL 0 (CAR A)))
(p A B))
(IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL 0 (CAR A)))
(p (CDR A) B))
(p A B))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to establish that the measure (COUNT A) decreases according
to the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme leads to the following six new goals:
Case 6. (IMPLIES (AND (NLISTP A)
(NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
This simplifies, expanding the functions NLISTP, MEMBER, SET-STANDARD,
CARDINAL, and EQUAL, to:
T.
Case 5. (IMPLIES (AND (NOT (NLISTP A))
(EQUAL 0 (CAR A))
(NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
This simplifies, opening up NLISTP, MEMBER, and EQUAL, to:
T.
Case 4. (IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL 0 (CAR A)))
(MEMBER 0 (CDR A))
(NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
This simplifies, unfolding the functions NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL 0 (CAR A)))
(NOT (SET-STANDARD (CDR A)))
(NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
This simplifies, opening up NLISTP, MEMBER, and SET-STANDARD, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL 0 (CAR A)))
(EQUAL (CARDINAL (CDR A)) 0)
(NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
This simplifies, rewriting with CDR-CONS and ADD1-EQUAL, and unfolding
NLISTP, MEMBER, SET-STANDARD, CARDINAL, ADD1, EQUAL, SET-MINUS, and NUMBERP,
to the conjecture:
(IMPLIES (AND (LISTP A)
(NOT (EQUAL 0 (CAR A)))
(EQUAL (CARDINAL (CDR A)) 0)
(NOT (MEMBER 0 (CDR A)))
(NOT (LISTP B))
(NOT (MEMBER (CAR A) (CDR A)))
(SET-STANDARD (CDR A)))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
0)).
Appealing to the lemma CAR-CDR-ELIM, we now replace A by (CONS X Z) to
eliminate (CAR A) and (CDR A). The result is the goal:
(IMPLIES (AND (NOT (EQUAL 0 X))
(EQUAL (CARDINAL Z) 0)
(NOT (MEMBER 0 Z))
(NOT (LISTP B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B)) 0)).
Call the above conjecture *1.1.
Case 1. (IMPLIES (AND (NOT (NLISTP A))
(NOT (EQUAL 0 (CAR A)))
(EQUAL (CARDINAL (SET-MINUS (CDR A) B))
(CARDINAL (CDR A)))
(NOT (MEMBER 0 A))
(NOT (LISTP B))
(SET-STANDARD A)
(NOT (EQUAL (CARDINAL A) 0)))
(EQUAL (CARDINAL (SET-MINUS A B))
(CARDINAL A))).
This simplifies, rewriting with the lemma CDR-CONS, and opening up NLISTP,
MEMBER, SET-STANDARD, CARDINAL, and SET-MINUS, to:
T.
So let us turn our attention to:
(IMPLIES (AND (NOT (EQUAL 0 X))
(EQUAL (CARDINAL Z) 0)
(NOT (MEMBER 0 Z))
(NOT (LISTP B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B)) 0)),
which we named *1.1 above. Perhaps we can prove it by induction. The
recursive terms in the conjecture suggest five inductions. However, they
merge into one likely candidate induction. We will induct according to the
following scheme:
(AND (IMPLIES (AND (LISTP Z) (p (CDR Z) B X))
(p Z B X))
(IMPLIES (NOT (LISTP Z)) (p Z B X))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT Z)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme produces the following six new
formulas:
Case 6. (IMPLIES (AND (LISTP Z)
(NOT (EQUAL (CARDINAL (CDR Z)) 0))
(NOT (EQUAL 0 X))
(EQUAL (CARDINAL Z) 0)
(NOT (MEMBER 0 Z))
(NOT (LISTP B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B)) 0)).
This simplifies, unfolding the function CARDINAL, to:
T.
Case 5. (IMPLIES (AND (LISTP Z)
(MEMBER 0 (CDR Z))
(NOT (EQUAL 0 X))
(EQUAL (CARDINAL Z) 0)
(NOT (MEMBER 0 Z))
(NOT (LISTP B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B)) 0)).
This simplifies, opening up the function CARDINAL, to:
T.
Case 4. (IMPLIES (AND (LISTP Z)
(MEMBER X (CDR Z))
(NOT (EQUAL 0 X))
(EQUAL (CARDINAL Z) 0)
(NOT (MEMBER 0 Z))
(NOT (LISTP B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B)) 0)).
This simplifies, opening up the definition of CARDINAL, to:
T.
Case 3. (IMPLIES (AND (LISTP Z)
(NOT (SET-STANDARD (CDR Z)))
(NOT (EQUAL 0 X))
(EQUAL (CARDINAL Z) 0)
(NOT (MEMBER 0 Z))
(NOT (LISTP B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B)) 0)).
This simplifies, unfolding the function CARDINAL, to:
T.
Case 2. (IMPLIES (AND (LISTP Z)
(EQUAL (CARDINAL (SET-MINUS (CDR Z) B))
0)
(NOT (EQUAL 0 X))
(EQUAL (CARDINAL Z) 0)
(NOT (MEMBER 0 Z))
(NOT (LISTP B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B)) 0)).
This simplifies, opening up the function CARDINAL, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP Z))
(NOT (EQUAL 0 X))
(EQUAL (CARDINAL Z) 0)
(NOT (MEMBER 0 Z))
(NOT (LISTP B))
(NOT (MEMBER X Z))
(SET-STANDARD Z))
(EQUAL (CARDINAL (SET-MINUS Z B)) 0)).
This simplifies, opening up the definitions of CARDINAL, EQUAL, MEMBER,
SET-STANDARD, and SET-MINUS, to:
T.
That finishes the proof of *1.1, which also finishes the proof of *1.
Q.E.D.
[ 0.0 0.2 0.2 ]
CARDINAL-SUBSET
(DCL OP (X Y))
[ 0.0 0.0 0.0 ]
OP
(DEFN-SK GROUP-OP
(G)
(AND
(FORALL (X Y)
(IMPLIES (AND (MEMBER X G) (MEMBER Y G))
(MEMBER (OP X Y) G)))
(FORALL (X Y Z)
(IMPLIES (AND (MEMBER X G)
(MEMBER Y G)
(MEMBER Z G))
(EQUAL (OP (OP X Y) Z)
(OP X (OP Y Z)))))
(EXISTS ID
(AND (MEMBER ID G)
(FORALL X
(IMPLIES (MEMBER X G)
(AND (EQUAL (OP ID X) X)
(EQUAL (OP X ID) X)
(EXISTS INV
(AND (MEMBER INV G)
(EQUAL (OP INV X) ID)
(EQUAL (OP X INV) ID))))))))))
Adding the Skolem axiom:
(AND (IMPLIES (AND (IMPLIES (AND (MEMBER (X G) G)
(MEMBER (Y G) G))
(MEMBER (OP (X G) (Y G)) G))
(IMPLIES (AND (MEMBER (X-1 G) G)
(MEMBER (Y-1 G) G)
(MEMBER (Z G) G))
(EQUAL (OP (OP (X-1 G) (Y-1 G)) (Z G))
(OP (X-1 G) (OP (Y-1 G) (Z G)))))
(MEMBER ID G)
(IMPLIES (MEMBER (X-2 G ID) G)
(AND (EQUAL (OP ID (X-2 G ID)) (X-2 G ID))
(EQUAL (OP (X-2 G ID) ID) (X-2 G ID))
(MEMBER INV G)
(EQUAL (OP INV (X-2 G ID)) ID)
(EQUAL (OP (X-2 G ID) INV) ID))))
(GROUP-OP G))
(IMPLIES (NOT (AND (IMPLIES (AND (MEMBER X G) (MEMBER Y G))
(MEMBER (OP X Y) G))
(IMPLIES (AND (MEMBER X G)
(MEMBER Y G)
(MEMBER Z G))
(EQUAL (OP (OP X Y) Z)
(OP X (OP Y Z))))
(MEMBER (ID G) G)
(IMPLIES (MEMBER X G)
(AND (EQUAL (OP (ID G) X) X)
(EQUAL (OP X (ID G)) X)
(MEMBER (INV G X) G)
(EQUAL (OP (INV G X) X) (ID G))
(EQUAL (OP X (INV G X)) (ID G))))))
(NOT (GROUP-OP G)))).
As this is a DEFN-SK we can conclude that:
(OR (TRUEP (GROUP-OP G))
(FALSEP (GROUP-OP G)))
is a theorem.
[ 0.0 0.0 0.0 ]
GROUP-OP
(PROVE-LEMMA GROUP-OP-CLOSED
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(MEMBER X G)
(MEMBER Y G))
(MEMBER (OP X Y) G))
((USE (GROUP-OP))))
This conjecture simplifies, expanding the functions AND, IMPLIES, and NOT, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GROUP-OP-CLOSED
(PROVE-LEMMA GROUP-OP-ASSOCIATIVITY
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(MEMBER X G)
(MEMBER Y G)
(MEMBER Z G))
(EQUAL (OP (OP X Y) Z)
(OP X (OP Y Z))))
((USE (GROUP-OP))))
WARNING: Note that GROUP-OP-ASSOCIATIVITY contains the free variable G which
will be chosen by instantiating the hypothesis (GROUP-OP G).
This formula simplifies, rewriting with GROUP-OP-CLOSED, and expanding the
functions AND, IMPLIES, and NOT, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GROUP-OP-ASSOCIATIVITY
(PROVE-LEMMA GROUP-OP-ASSOCIATIVITY1
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(MEMBER X G)
(MEMBER Y G)
(MEMBER Z G))
(EQUAL (OP X (OP Y Z))
(OP (OP X Y) Z)))
((USE (GROUP-OP))))
WARNING: Note that GROUP-OP-ASSOCIATIVITY1 contains the free variable G which
will be chosen by instantiating the hypothesis (GROUP-OP G).
This formula simplifies, rewriting with GROUP-OP-CLOSED and
GROUP-OP-ASSOCIATIVITY, and expanding the functions AND, IMPLIES, and NOT, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GROUP-OP-ASSOCIATIVITY1
(PROVE-LEMMA GROUP-OP-IDENTITY
(REWRITE)
(IMPLIES (GROUP-OP G)
(AND (MEMBER (ID G) G)
(IMPLIES (MEMBER X G)
(AND (EQUAL (OP (ID G) X) X)
(EQUAL (OP X (ID G)) X)))))
((USE (GROUP-OP))))
WARNING: Note that the proposed lemma GROUP-OP-IDENTITY is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and three replacement rules.
This formula simplifies, unfolding the definitions of AND, IMPLIES, and NOT,
to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GROUP-OP-IDENTITY
(PROVE-LEMMA GROUP-OP-INVERSE
(REWRITE)
(IMPLIES (AND (GROUP-OP G) (MEMBER X G))
(AND (MEMBER (INV G X) G)
(EQUAL (OP (INV G X) X) (ID G))
(EQUAL (OP X (INV G X)) (ID G))))
((USE (GROUP-OP))))
WARNING: Note that the proposed lemma GROUP-OP-INVERSE is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and three replacement rules.
This conjecture simplifies, rewriting with GROUP-OP-IDENTITY, and expanding
AND, IMPLIES, and NOT, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GROUP-OP-INVERSE
(DEFN RIGHT-COSET
(S A)
(IF (LISTP S)
(CONS (OP (CAR S) A)
(RIGHT-COSET (CDR S) A))
NIL))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT S) decreases according to the well-founded relation LESSP in each
recursive call. Hence, RIGHT-COSET is accepted under the principle of
definition. Note that:
(OR (LITATOM (RIGHT-COSET S A))
(LISTP (RIGHT-COSET S A)))
is a theorem.
[ 0.0 0.0 0.0 ]
RIGHT-COSET
(PROVE-LEMMA RIGHT-COSET-CARDINAL
(REWRITE)
(EQUAL (CARDINAL (RIGHT-COSET S A))
(CARDINAL S)))
Call the conjecture *1.
We will try to prove it by induction. The recursive terms in the
conjecture suggest two inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP S) (p (CDR S) A))
(p S A))
(IMPLIES (NOT (LISTP S)) (p S A))).
Linear arithmetic and the lemma CDR-LESSP can be used to establish that the
measure (COUNT S) decreases according to the well-founded relation LESSP in
each induction step of the scheme. The above induction scheme generates the
following two new formulas:
Case 2. (IMPLIES (AND (LISTP S)
(EQUAL (CARDINAL (RIGHT-COSET (CDR S) A))
(CARDINAL (CDR S))))
(EQUAL (CARDINAL (RIGHT-COSET S A))
(CARDINAL S))).
This simplifies, applying CDR-CONS, and expanding the functions RIGHT-COSET
and CARDINAL, to:
T.
Case 1. (IMPLIES (NOT (LISTP S))
(EQUAL (CARDINAL (RIGHT-COSET S A))
(CARDINAL S))),
which simplifies, opening up the functions RIGHT-COSET, CARDINAL, and EQUAL,
to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
RIGHT-COSET-CARDINAL
(PROVE-LEMMA RIGHT-COSET-NEMPTY
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(MEMBER X G)
(SUBSET S G)
(MEMBER (ID G) S))
(MEMBER X (RIGHT-COSET S X))))
WARNING: Note that RIGHT-COSET-NEMPTY contains the free variable G which will
be chosen by instantiating the hypothesis (GROUP-OP G).
Give the conjecture the name *1.
Perhaps we can prove it by induction. There are three plausible
inductions. However, they merge into one likely candidate induction. We will
induct according to the following scheme:
(AND (IMPLIES (AND (LISTP S) (p X (CDR S) G))
(p X S G))
(IMPLIES (NOT (LISTP S)) (p X S G))).
Linear arithmetic and the lemma CDR-LESSP can be used to show that the measure
(COUNT S) decreases according to the well-founded relation LESSP in each
induction step of the scheme. The above induction scheme generates four new
conjectures:
Case 4. (IMPLIES (AND (LISTP S)
(NOT (SUBSET (CDR S) G))
(GROUP-OP G)
(MEMBER X G)
(SUBSET S G)
(MEMBER (ID G) S))
(MEMBER X (RIGHT-COSET S X))),
which simplifies, unfolding the definition of SUBSET, to:
T.
Case 3. (IMPLIES (AND (LISTP S)
(NOT (MEMBER (ID G) (CDR S)))
(GROUP-OP G)
(MEMBER X G)
(SUBSET S G)
(MEMBER (ID G) S))
(MEMBER X (RIGHT-COSET S X))),
which simplifies, rewriting with CDR-CONS and CAR-CONS, and expanding the
definitions of SUBSET, MEMBER, and RIGHT-COSET, to:
(IMPLIES (AND (LISTP S)
(NOT (MEMBER (ID G) (CDR S)))
(GROUP-OP G)
(MEMBER X G)
(MEMBER (CAR S) G)
(SUBSET (CDR S) G)
(EQUAL (ID G) (CAR S))
(NOT (EQUAL X (OP (CAR S) X))))
(MEMBER X (RIGHT-COSET (CDR S) X))),
which further simplifies, obviously, to:
(IMPLIES (AND (LISTP S)
(NOT (MEMBER (CAR S) (CDR S)))
(GROUP-OP G)
(MEMBER X G)
(MEMBER (CAR S) G)
(SUBSET (CDR S) G)
(EQUAL (ID G) (CAR S))
(NOT (EQUAL X (OP (CAR S) X))))
(MEMBER X (RIGHT-COSET (CDR S) X))).
Applying the lemma CAR-CDR-ELIM, replace S by (CONS Z V) to eliminate
(CAR S) and (CDR S). We thus obtain the new goal:
(IMPLIES (AND (NOT (MEMBER Z V))
(GROUP-OP G)
(MEMBER X G)
(MEMBER Z G)
(SUBSET V G)
(EQUAL (ID G) Z)
(NOT (EQUAL X (OP Z X))))
(MEMBER X (RIGHT-COSET V X))),
which further simplifies, applying GROUP-OP-IDENTITY, to:
T.
Case 2. (IMPLIES (AND (LISTP S)
(MEMBER X (RIGHT-COSET (CDR S) X))
(GROUP-OP G)
(MEMBER X G)
(SUBSET S G)
(MEMBER (ID G) S))
(MEMBER X (RIGHT-COSET S X))).
This simplifies, rewriting with CDR-CONS and CAR-CONS, and expanding the
functions SUBSET, MEMBER, and RIGHT-COSET, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP S))
(GROUP-OP G)
(MEMBER X G)
(SUBSET S G)
(MEMBER (ID G) S))
(MEMBER X (RIGHT-COSET S X))),
which simplifies, expanding the definitions of SUBSET and MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.1 0.0 ]
RIGHT-COSET-NEMPTY
(PROVE-LEMMA OP-EQUALITY1 NIL
(IMPLIES (AND (GROUP-OP G)
(MEMBER X G)
(MEMBER Y G)
(MEMBER A G)
(MEMBER B G)
(EQUAL (OP X A) (OP Y B)))
(EQUAL X (OP Y (OP B (INV G A))))))
This formula simplifies, applying GROUP-OP-INVERSE, GROUP-OP-IDENTITY,
GROUP-OP-ASSOCIATIVITY, and GROUP-OP-ASSOCIATIVITY1, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OP-EQUALITY1
(PROVE-LEMMA OP-EQUALITY2 NIL
(IMPLIES (AND (GROUP-OP G)
(MEMBER X G)
(MEMBER Y G)
(MEMBER A G)
(MEMBER B G)
(EQUAL (OP X A) (OP Y B)))
(EQUAL A (OP (OP (INV G X) Y) B))))
This formula simplifies, applying GROUP-OP-INVERSE, GROUP-OP-IDENTITY,
GROUP-OP-ASSOCIATIVITY1, and GROUP-OP-ASSOCIATIVITY, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OP-EQUALITY2
(PROVE-LEMMA CANCELLATION NIL
(IMPLIES (AND (GROUP-OP G)
(MEMBER X G)
(MEMBER Y G)
(MEMBER A G)
(EQUAL (OP X A) (OP Y A)))
(EQUAL X Y))
((USE (OP-EQUALITY1 (B A)))))
This conjecture simplifies, applying GROUP-OP-INVERSE and GROUP-OP-IDENTITY,
and unfolding AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
CANCELLATION
(PROVE-LEMMA OP-EQUALITY3 NIL
(IMPLIES (AND (GROUP-OP G)
(MEMBER X G)
(MEMBER A G)
(EQUAL (OP X A) (ID G)))
(EQUAL A (INV G X)))
((USE (OP-EQUALITY2 (Y (ID G))
(B (ID G))))))
This conjecture simplifies, rewriting with GROUP-OP-IDENTITY and
GROUP-OP-INVERSE, and expanding the definitions of AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OP-EQUALITY3
(PROVE-LEMMA OP-EQUALITY4 NIL
(IMPLIES (AND (GROUP-OP G)
(MEMBER X G)
(EQUAL (OP X X) X))
(EQUAL X (ID G)))
((USE (OP-EQUALITY1 (A X)
(Y X)
(B (ID G))))))
This simplifies, applying GROUP-OP-IDENTITY and GROUP-OP-INVERSE, and
unfolding the functions AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OP-EQUALITY4
(DEFN SUBGROUP-OP
(H G)
(AND (GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)))
Note that (OR (FALSEP (SUBGROUP-OP H G)) (TRUEP (SUBGROUP-OP H G))) is a
theorem.
[ 0.0 0.0 0.0 ]
SUBGROUP-OP
(PROVE-LEMMA OP-IDENTITY-SAME NIL
(IMPLIES (SUBGROUP-OP H G)
(EQUAL (ID G) (ID H)))
((USE (OP-EQUALITY4 (X (ID H))))))
This conjecture can be simplified, using the abbreviations SUBGROUP-OP and
IMPLIES, to:
(IMPLIES (AND (IMPLIES (AND (GROUP-OP G)
(MEMBER (ID H) G)
(EQUAL (OP (ID H) (ID H)) (ID H)))
(EQUAL (ID H) (ID G)))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G))
(EQUAL (ID G) (ID H))).
This simplifies, applying GROUP-OP-IDENTITY and SUBSET-LEMMA0, and expanding
the definitions of AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OP-IDENTITY-SAME
(PROVE-LEMMA OP-IDENTITY-IN-SUBGROUP
(REWRITE)
(IMPLIES (SUBGROUP-OP H G)
(MEMBER (ID G) H))
((USE (OP-IDENTITY-SAME)
(GROUP-OP-IDENTITY (G H)))))
This formula can be simplified, using the abbreviations SUBGROUP-OP, IMPLIES,
and AND, to:
(IMPLIES (AND (IMPLIES (SUBGROUP-OP H G)
(EQUAL (ID G) (ID H)))
(IMPLIES (GROUP-OP H)
(AND (MEMBER (ID H) H)
(IMPLIES (MEMBER X H)
(AND (EQUAL (OP (ID H) X) X)
(EQUAL (OP X (ID H)) X)))))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G))
(MEMBER (ID G) H)),
which simplifies, applying SUBSET-TRANSITIVITY and SUBSET-REFLEXIVITY, and
unfolding the definitions of SUBGROUP-OP, IMPLIES, and AND, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OP-IDENTITY-IN-SUBGROUP
(PROVE-LEMMA OP-INVERSE-SAME NIL
(IMPLIES (AND (SUBGROUP-OP H G) (MEMBER X H))
(EQUAL (INV H X) (INV G X)))
((USE (OP-EQUALITY3 (A (INV H X)))
(OP-IDENTITY-SAME))))
This conjecture can be simplified, using the abbreviations SUBGROUP-OP,
IMPLIES, and AND, to:
(IMPLIES (AND (IMPLIES (AND (GROUP-OP G)
(MEMBER X G)
(MEMBER (INV H X) G)
(EQUAL (OP X (INV H X)) (ID G)))
(EQUAL (INV H X) (INV G X)))
(IMPLIES (SUBGROUP-OP H G)
(EQUAL (ID G) (ID H)))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(MEMBER X H))
(EQUAL (INV H X) (INV G X))).
This simplifies, applying SUBSET-LEMMA0, GROUP-OP-INVERSE, SUBSET-TRANSITIVITY,
and SUBSET-REFLEXIVITY, and expanding AND, IMPLIES, and SUBGROUP-OP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OP-INVERSE-SAME
(PROVE-LEMMA OP-INVERSE-IN-SUBGROUP
(REWRITE)
(IMPLIES (AND (SUBGROUP-OP H G) (MEMBER X H))
(MEMBER (INV G X) H))
((USE (OP-INVERSE-SAME)
(GROUP-OP-INVERSE (G H)))))
This formula can be simplified, using the abbreviations SUBGROUP-OP, IMPLIES,
and AND, to:
(IMPLIES (AND (IMPLIES (AND (SUBGROUP-OP H G) (MEMBER X H))
(EQUAL (INV H X) (INV G X)))
(IMPLIES (AND (GROUP-OP H) (MEMBER X H))
(AND (MEMBER (INV H X) H)
(EQUAL (OP (INV H X) X) (ID H))
(EQUAL (OP X (INV H X)) (ID H))))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(MEMBER X H))
(MEMBER (INV G X) H)),
which simplifies, rewriting with SUBSET-TRANSITIVITY, SUBSET-REFLEXIVITY,
SUBSET-LEMMA0, and GROUP-OP-INVERSE, and unfolding SUBGROUP-OP, AND, and
IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OP-INVERSE-IN-SUBGROUP
(PROVE-LEMMA GROUP-OP-ORDER NIL
(IMPLIES (GROUP-OP G)
(LEQ 1 (CARDINAL G)))
((USE (CARDINAL-LEMMA (S G) (X (ID G))))))
This simplifies, applying the lemmas SUBSET-REFLEXIVITY and
OP-IDENTITY-IN-SUBGROUP, and opening up the functions SUBGROUP-OP and IMPLIES,
to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GROUP-OP-ORDER
(DISABLE GROUP-OP)
[ 0.0 0.0 0.0 ]
GROUP-OP-OFF
(DISABLE GROUP-OP-ASSOCIATIVITY1)
[ 0.0 0.0 0.0 ]
GROUP-OP-ASSOCIATIVITY1-OFF
(DCL OP1 (X Y))
[ 0.0 0.0 0.0 ]
OP1
(DEFN-SK GROUP-OP1
(H)
(AND
(FORALL (X Y)
(IMPLIES (AND (MEMBER X H) (MEMBER Y H))
(MEMBER (OP1 X Y) H)))
(FORALL (X Y Z)
(IMPLIES (AND (MEMBER X H)
(MEMBER Y H)
(MEMBER Z H))
(EQUAL (OP1 (OP1 X Y) Z)
(OP1 X (OP1 Y Z)))))
(EXISTS ID
(AND (MEMBER ID H)
(FORALL X
(IMPLIES (MEMBER X H)
(AND (EQUAL (OP1 ID X) X)
(EQUAL (OP1 X ID) X)
(EXISTS INV
(AND (MEMBER INV H)
(EQUAL (OP1 INV X) ID)
(EQUAL (OP1 X INV) ID))))))))))
Adding the Skolem axiom:
(AND
(IMPLIES (AND (IMPLIES (AND (MEMBER (X-3 H) H)
(MEMBER (Y-2 H) H))
(MEMBER (OP1 (X-3 H) (Y-2 H)) H))
(IMPLIES (AND (MEMBER (X-4 H) H)
(MEMBER (Y-3 H) H)
(MEMBER (Z-1 H) H))
(EQUAL (OP1 (OP1 (X-4 H) (Y-3 H)) (Z-1 H))
(OP1 (X-4 H) (OP1 (Y-3 H) (Z-1 H)))))
(MEMBER ID H)
(IMPLIES (MEMBER (X-5 H ID) H)
(AND (EQUAL (OP1 ID (X-5 H ID)) (X-5 H ID))
(EQUAL (OP1 (X-5 H ID) ID) (X-5 H ID))
(MEMBER INV H)
(EQUAL (OP1 INV (X-5 H ID)) ID)
(EQUAL (OP1 (X-5 H ID) INV) ID))))
(GROUP-OP1 H))
(IMPLIES (NOT (AND (IMPLIES (AND (MEMBER X H) (MEMBER Y H))
(MEMBER (OP1 X Y) H))
(IMPLIES (AND (MEMBER X H)
(MEMBER Y H)
(MEMBER Z H))
(EQUAL (OP1 (OP1 X Y) Z)
(OP1 X (OP1 Y Z))))
(MEMBER (ID-1 H) H)
(IMPLIES (MEMBER X H)
(AND (EQUAL (OP1 (ID-1 H) X) X)
(EQUAL (OP1 X (ID-1 H)) X)
(MEMBER (INV-1 H X) H)
(EQUAL (OP1 (INV-1 H X) X) (ID-1 H))
(EQUAL (OP1 X (INV-1 H X))
(ID-1 H))))))
(NOT (GROUP-OP1 H)))).
As this is a DEFN-SK we can conclude that:
(OR (TRUEP (GROUP-OP1 H))
(FALSEP (GROUP-OP1 H)))
is a theorem.
[ 0.0 0.0 0.0 ]
GROUP-OP1
(PROVE-LEMMA GROUP-OP1-CLOSED
(REWRITE)
(IMPLIES (AND (GROUP-OP1 H)
(MEMBER X H)
(MEMBER Y H))
(MEMBER (OP1 X Y) H))
((USE (GROUP-OP1))))
This conjecture simplifies, expanding the functions AND, IMPLIES, and NOT, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GROUP-OP1-CLOSED
(PROVE-LEMMA GROUP-OP1-ASSOCIATIVITY
(REWRITE)
(IMPLIES (AND (GROUP-OP1 H)
(MEMBER X H)
(MEMBER Y H)
(MEMBER Z H))
(EQUAL (OP1 (OP1 X Y) Z)
(OP1 X (OP1 Y Z))))
((USE (GROUP-OP1))))
WARNING: Note that GROUP-OP1-ASSOCIATIVITY contains the free variable H which
will be chosen by instantiating the hypothesis (GROUP-OP1 H).
This formula simplifies, rewriting with GROUP-OP1-CLOSED, and expanding the
functions AND, IMPLIES, and NOT, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GROUP-OP1-ASSOCIATIVITY
(PROVE-LEMMA GROUP-OP1-ASSOCIATIVITY1
(REWRITE)
(IMPLIES (AND (GROUP-OP1 H)
(MEMBER X H)
(MEMBER Y H)
(MEMBER Z H))
(EQUAL (OP1 X (OP1 Y Z))
(OP1 (OP1 X Y) Z)))
((USE (GROUP-OP1))))
WARNING: Note that GROUP-OP1-ASSOCIATIVITY1 contains the free variable H
which will be chosen by instantiating the hypothesis (GROUP-OP1 H).
This formula simplifies, rewriting with GROUP-OP1-CLOSED and
GROUP-OP1-ASSOCIATIVITY, and expanding the functions AND, IMPLIES, and NOT, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GROUP-OP1-ASSOCIATIVITY1
(PROVE-LEMMA GROUP-OP1-IDENTITY
(REWRITE)
(IMPLIES (GROUP-OP1 H)
(AND (MEMBER (ID-1 H) H)
(IMPLIES (MEMBER X H)
(AND (EQUAL (OP1 (ID-1 H) X) X)
(EQUAL (OP1 X (ID-1 H)) X)))))
((USE (GROUP-OP1))))
WARNING: Note that the proposed lemma GROUP-OP1-IDENTITY is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and three replacement rules.
This formula simplifies, unfolding the definitions of AND, IMPLIES, and NOT,
to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GROUP-OP1-IDENTITY
(PROVE-LEMMA GROUP-OP1-INVERSE
(REWRITE)
(IMPLIES (AND (GROUP-OP1 H) (MEMBER X H))
(AND (MEMBER (INV-1 H X) H)
(EQUAL (OP1 (INV-1 H X) X) (ID-1 H))
(EQUAL (OP1 X (INV-1 H X)) (ID-1 H))))
((USE (GROUP-OP1))))
WARNING: Note that the proposed lemma GROUP-OP1-INVERSE is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and three replacement rules.
This conjecture simplifies, rewriting with GROUP-OP1-IDENTITY, and expanding
AND, IMPLIES, and NOT, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
GROUP-OP1-INVERSE
(PROVE-LEMMA OP1-EQUALITY1 NIL
(IMPLIES (AND (GROUP-OP1 H)
(MEMBER X H)
(MEMBER Y H)
(MEMBER A H)
(MEMBER B H)
(EQUAL (OP1 X A) (OP1 Y B)))
(EQUAL X
(OP1 Y (OP1 B (INV-1 H A))))))
This formula simplifies, applying GROUP-OP1-INVERSE, GROUP-OP1-IDENTITY,
GROUP-OP1-ASSOCIATIVITY, and GROUP-OP1-ASSOCIATIVITY1, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OP1-EQUALITY1
(PROVE-LEMMA OP1-EQUALITY2 NIL
(IMPLIES (AND (GROUP-OP1 H)
(MEMBER X H)
(MEMBER Y H)
(MEMBER A H)
(MEMBER B H)
(EQUAL (OP1 X A) (OP1 Y B)))
(EQUAL A
(OP1 (OP1 (INV-1 H X) Y) B))))
This formula simplifies, applying GROUP-OP1-INVERSE, GROUP-OP1-IDENTITY,
GROUP-OP1-ASSOCIATIVITY1, and GROUP-OP1-ASSOCIATIVITY, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OP1-EQUALITY2
(PROVE-LEMMA OP1-EQUALITY3 NIL
(IMPLIES (AND (GROUP-OP1 H)
(MEMBER X H)
(MEMBER A H)
(EQUAL (OP1 X A) (ID-1 H)))
(EQUAL A (INV-1 H X)))
((USE (OP1-EQUALITY2 (Y (ID-1 H))
(B (ID-1 H))))))
This conjecture simplifies, rewriting with GROUP-OP1-IDENTITY and
GROUP-OP1-INVERSE, and expanding the definitions of AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OP1-EQUALITY3
(PROVE-LEMMA OP1-EQUALITY4 NIL
(IMPLIES (AND (GROUP-OP1 H)
(MEMBER X H)
(EQUAL (OP1 X X) X))
(EQUAL X (ID-1 H)))
((USE (OP1-EQUALITY1 (A X)
(Y X)
(B (ID-1 H))))))
This simplifies, applying GROUP-OP1-IDENTITY and GROUP-OP1-INVERSE, and
unfolding the functions AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OP1-EQUALITY4
(PROVE-LEMMA OP1-CANCELLATION NIL
(IMPLIES (AND (GROUP-OP1 H)
(MEMBER X H)
(MEMBER Y H)
(MEMBER A H)
(EQUAL (OP1 X A) (OP1 Y A)))
(EQUAL X Y))
((USE (OP1-EQUALITY1 (B A)))))
This conjecture simplifies, applying GROUP-OP1-INVERSE and GROUP-OP1-IDENTITY,
and unfolding AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
OP1-CANCELLATION
(DCL PHI (X))
[ 0.0 0.0 0.0 ]
PHI
(DEFN-SK HOMO-PHI
(G H)
(FORALL (X Y)
(IMPLIES (AND (MEMBER X G) (MEMBER Y G))
(AND (MEMBER (PHI X) H)
(MEMBER (PHI Y) H)
(EQUAL (PHI (OP X Y))
(OP1 (PHI X) (PHI Y)))))))
Adding the Skolem axiom:
(AND (IMPLIES (IMPLIES (AND (MEMBER (X-6 G H) G)
(MEMBER (Y-4 G H) G))
(AND (MEMBER (PHI (X-6 G H)) H)
(MEMBER (PHI (Y-4 G H)) H)
(EQUAL (PHI (OP (X-6 G H) (Y-4 G H)))
(OP1 (PHI (X-6 G H))
(PHI (Y-4 G H))))))
(HOMO-PHI G H))
(IMPLIES (NOT (IMPLIES (AND (MEMBER X G) (MEMBER Y G))
(AND (MEMBER (PHI X) H)
(MEMBER (PHI Y) H)
(EQUAL (PHI (OP X Y))
(OP1 (PHI X) (PHI Y))))))
(NOT (HOMO-PHI G H)))).
As this is a DEFN-SK we can conclude that:
(OR (TRUEP (HOMO-PHI G H))
(FALSEP (HOMO-PHI G H)))
is a theorem.
[ 0.0 0.0 0.0 ]
HOMO-PHI
(PROVE-LEMMA HOMOMORPHISM-PHI
(REWRITE)
(IMPLIES (AND (HOMO-PHI G H)
(MEMBER X G)
(MEMBER Y G))
(AND (MEMBER (PHI X) H)
(MEMBER (PHI Y) H)
(EQUAL (PHI (OP X Y))
(OP1 (PHI X) (PHI Y)))))
((USE (HOMO-PHI))))
WARNING: Note that HOMOMORPHISM-PHI contains the free variables Y and G which
will be chosen by instantiating the hypotheses (HOMO-PHI G H) and (MEMBER Y G).
WARNING: Note that HOMOMORPHISM-PHI contains the free variables X and G which
will be chosen by instantiating the hypotheses (HOMO-PHI G H) and (MEMBER X G).
WARNING: Note that HOMOMORPHISM-PHI contains the free variables H and G which
will be chosen by instantiating the hypothesis (HOMO-PHI G H).
WARNING: Note that the proposed lemma HOMOMORPHISM-PHI is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and three replacement rules.
This formula simplifies, opening up AND, IMPLIES, and NOT, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
HOMOMORPHISM-PHI
(DEFN PHI-INV
(G A)
(IF (LISTP G)
(IF (EQUAL (PHI (CAR G)) A)
(CONS (CAR G) (PHI-INV (CDR G) A))
(PHI-INV (CDR G) A))
NIL))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT G) decreases according to the well-founded relation LESSP in each
recursive call. Hence, PHI-INV is accepted under the definitional principle.
Note that (OR (LITATOM (PHI-INV G A)) (LISTP (PHI-INV G A))) is a theorem.
[ 0.0 0.0 0.0 ]
PHI-INV
(PROVE-LEMMA BASIC-MAPPING1
(REWRITE)
(IMPLIES (AND (MEMBER X G) (EQUAL (PHI X) A))
(MEMBER X (PHI-INV G A))))
Give the conjecture the name *1.
Let us appeal to the induction principle. The recursive terms in the
conjecture suggest two inductions. However, they merge into one likely
candidate induction. We will induct according to the following scheme:
(AND (IMPLIES (NLISTP G) (p X G))
(IMPLIES (AND (NOT (NLISTP G))
(EQUAL X (CAR G)))
(p X G))
(IMPLIES (AND (NOT (NLISTP G))
(NOT (EQUAL X (CAR G)))
(p X (CDR G)))
(p X G))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to show that the measure (COUNT G) decreases according to
the well-founded relation LESSP in each induction step of the scheme. The
above induction scheme generates the following four new conjectures:
Case 4. (IMPLIES (AND (NLISTP G) (MEMBER X G))
(MEMBER X (PHI-INV G (PHI X)))).
This simplifies, opening up the functions NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP G))
(EQUAL X (CAR G))
(MEMBER X G))
(MEMBER X (PHI-INV G (PHI X)))).
This simplifies, unfolding the functions NLISTP and MEMBER, to:
(IMPLIES (LISTP G)
(MEMBER (CAR G)
(PHI-INV G (PHI (CAR G))))).
Applying the lemma CAR-CDR-ELIM, replace G by (CONS Z V) to eliminate
(CAR G) and (CDR G). This produces the new goal:
(MEMBER Z
(PHI-INV (CONS Z V) (PHI Z))),
which further simplifies, appealing to the lemmas CDR-CONS and CAR-CONS, and
opening up PHI-INV and MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP G))
(NOT (EQUAL X (CAR G)))
(NOT (MEMBER X (CDR G)))
(MEMBER X G))
(MEMBER X (PHI-INV G (PHI X)))),
which simplifies, unfolding the functions NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP G))
(NOT (EQUAL X (CAR G)))
(MEMBER X (PHI-INV (CDR G) (PHI X)))
(MEMBER X G))
(MEMBER X (PHI-INV G (PHI X)))),
which simplifies, unfolding the functions NLISTP, MEMBER, and PHI-INV, to:
(IMPLIES (AND (LISTP G)
(NOT (EQUAL X (CAR G)))
(MEMBER X (PHI-INV (CDR G) (PHI X)))
(MEMBER X (CDR G))
(EQUAL (PHI (CAR G)) (PHI X)))
(MEMBER X
(CONS (CAR G)
(PHI-INV (CDR G) (PHI X))))).
This again simplifies, applying CDR-CONS and CAR-CONS, and expanding the
definition of MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
BASIC-MAPPING1
(PROVE-LEMMA BASIC-MAPPING2
(REWRITE)
(IMPLIES (MEMBER X (PHI-INV G A))
(EQUAL (PHI X) A)))
WARNING: Note that BASIC-MAPPING2 contains the free variables A and G which
will be chosen by instantiating the hypothesis (MEMBER X (PHI-INV G A)).
Give the conjecture the name *1.
We will try to prove it by induction. There is only one suggested
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP G)
(EQUAL (PHI (CAR G)) A)
(p X A (CDR G)))
(p X A G))
(IMPLIES (AND (LISTP G)
(NOT (EQUAL (PHI (CAR G)) A))
(p X A (CDR G)))
(p X A G))
(IMPLIES (NOT (LISTP G)) (p X A G))).
Linear arithmetic and the lemma CDR-LESSP inform us that the measure (COUNT G)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates three new goals:
Case 3. (IMPLIES (AND (LISTP G)
(EQUAL (PHI (CAR G)) A)
(NOT (MEMBER X (PHI-INV (CDR G) A)))
(MEMBER X (PHI-INV G A)))
(EQUAL (PHI X) A)),
which simplifies, applying CDR-CONS and CAR-CONS, and unfolding the
functions PHI-INV and MEMBER, to:
T.
Case 2. (IMPLIES (AND (LISTP G)
(NOT (EQUAL (PHI (CAR G)) A))
(NOT (MEMBER X (PHI-INV (CDR G) A)))
(MEMBER X (PHI-INV G A)))
(EQUAL (PHI X) A)).
This simplifies, opening up PHI-INV, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP G))
(MEMBER X (PHI-INV G A)))
(EQUAL (PHI X) A)).
This simplifies, expanding PHI-INV, LISTP, and MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
BASIC-MAPPING2
(PROVE-LEMMA PHI-INV-SUBSET
(REWRITE)
(SUBSET (PHI-INV G A) G))
Give the conjecture the name *1.
We will try to prove it by induction. There is only one suggested
induction. We will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP G)
(EQUAL (PHI (CAR G)) A)
(p (CDR G) A))
(p G A))
(IMPLIES (AND (LISTP G)
(NOT (EQUAL (PHI (CAR G)) A))
(p (CDR G) A))
(p G A))
(IMPLIES (NOT (LISTP G)) (p G A))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT G)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme leads to three new formulas:
Case 3. (IMPLIES (AND (LISTP G)
(EQUAL (PHI (CAR G)) A)
(SUBSET (PHI-INV (CDR G) A) (CDR G)))
(SUBSET (PHI-INV G A) G)),
which simplifies, applying CDR-CONS and CAR-CONS, and opening up the
definitions of PHI-INV, MEMBER, and SUBSET, to:
(IMPLIES (AND (LISTP G)
(SUBSET (PHI-INV (CDR G) (PHI (CAR G)))
(CDR G)))
(SUBSET (PHI-INV (CDR G) (PHI (CAR G)))
G)).
Applying the lemma CAR-CDR-ELIM, replace G by (CONS Z X) to eliminate
(CDR G) and (CAR G). This produces:
(IMPLIES (SUBSET (PHI-INV X (PHI Z)) X)
(SUBSET (PHI-INV X (PHI Z))
(CONS Z X))),
which further simplifies, appealing to the lemma SUBSET-LEMMA1, to:
T.
Case 2. (IMPLIES (AND (LISTP G)
(NOT (EQUAL (PHI (CAR G)) A))
(SUBSET (PHI-INV (CDR G) A) (CDR G)))
(SUBSET (PHI-INV G A) G)),
which simplifies, opening up the definition of PHI-INV, to the conjecture:
(IMPLIES (AND (LISTP G)
(NOT (EQUAL (PHI (CAR G)) A))
(SUBSET (PHI-INV (CDR G) A) (CDR G)))
(SUBSET (PHI-INV (CDR G) A) G)).
Appealing to the lemma CAR-CDR-ELIM, we now replace G by (CONS X Z) to
eliminate (CAR G) and (CDR G). This generates:
(IMPLIES (AND (NOT (EQUAL (PHI X) A))
(SUBSET (PHI-INV Z A) Z))
(SUBSET (PHI-INV Z A) (CONS X Z))).
This further simplifies, rewriting with the lemma SUBSET-LEMMA1, to:
T.
Case 1. (IMPLIES (NOT (LISTP G))
(SUBSET (PHI-INV G A) G)),
which simplifies, unfolding PHI-INV, LISTP, and SUBSET, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
PHI-INV-SUBSET
(PROVE-LEMMA ID-TO-ID NIL
(IMPLIES (AND (GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(EQUAL (PHI (ID G)) (ID-1 H)))
((USE (HOMOMORPHISM-PHI (X (ID G))
(Y (ID G)))
(OP1-EQUALITY4 (G H)
(X (PHI (ID G)))))))
This conjecture simplifies, rewriting with SUBSET-REFLEXIVITY,
OP-IDENTITY-IN-SUBGROUP, and GROUP-OP-IDENTITY, and opening up SUBGROUP-OP,
AND, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
ID-TO-ID
(PROVE-LEMMA INV-TO-INV NIL
(IMPLIES (AND (GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H)
(MEMBER X G))
(EQUAL (PHI (INV G X))
(INV-1 H (PHI X))))
((USE (HOMOMORPHISM-PHI (Y (INV G X)))
(OP1-EQUALITY2 (X (PHI X))
(A (PHI (INV G X)))
(Y (ID-1 H))
(B (ID-1 H))
(G H))
(ID-TO-ID))))
This conjecture simplifies, applying SUBSET-REFLEXIVITY,
OP-INVERSE-IN-SUBGROUP, HOMOMORPHISM-PHI, GROUP-OP-INVERSE, GROUP-OP1-IDENTITY,
and GROUP-OP1-INVERSE, and expanding the functions SUBGROUP-OP, AND, and
IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
INV-TO-INV
(PROVE-LEMMA KER-CLOSED
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H)
(MEMBER X (PHI-INV G (ID-1 H)))
(MEMBER Y (PHI-INV G (ID-1 H))))
(MEMBER (OP X Y)
(PHI-INV G (ID-1 H))))
((USE (SUBSET-LEMMA0 (S1 (PHI-INV G (ID-1 H)))
(S G))
(SUBSET-LEMMA0 (X Y)
(S1 (PHI-INV G (ID-1 H)))
(S G)))))
This conjecture simplifies, appealing to the lemmas PHI-INV-SUBSET,
HOMOMORPHISM-PHI, GROUP-OP1-IDENTITY, BASIC-MAPPING2, GROUP-OP-CLOSED, and
BASIC-MAPPING1, and unfolding the functions AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
KER-CLOSED
(PROVE-LEMMA KER-ASSOCIATIVITY
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(MEMBER X (PHI-INV G A))
(MEMBER Y (PHI-INV G A))
(MEMBER Z (PHI-INV G A)))
(EQUAL (OP (OP X Y) Z)
(OP X (OP Y Z))))
((USE (SUBSET-LEMMA0 (S1 (PHI-INV G A))
(S G))
(SUBSET-LEMMA0 (X Y)
(S1 (PHI-INV G A))
(S G))
(SUBSET-LEMMA0 (X Z)
(S1 (PHI-INV G A))
(S G)))))
WARNING: Note that KER-ASSOCIATIVITY contains the free variables A and G
which will be chosen by instantiating the hypotheses (GROUP-OP G) and
(MEMBER X (PHI-INV G A)).
This conjecture simplifies, applying PHI-INV-SUBSET and GROUP-OP-ASSOCIATIVITY,
and expanding the functions AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
KER-ASSOCIATIVITY
(PROVE-LEMMA KER-IDENTITY
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(MEMBER (ID G) (PHI-INV G (ID-1 H))))
((USE (BASIC-MAPPING1 (X (ID G))
(A (ID-1 H)))
(ID-TO-ID))))
This simplifies, applying SUBSET-REFLEXIVITY and OP-IDENTITY-IN-SUBGROUP, and
unfolding the functions SUBGROUP-OP, AND, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
KER-IDENTITY
(PROVE-LEMMA ID-INV-ID
(REWRITE)
(IMPLIES (GROUP-OP1 H)
(EQUAL (INV-1 H (ID-1 H)) (ID-1 H)))
((USE (OP1-CANCELLATION (X (INV-1 H (ID-1 H)))
(Y (ID-1 H))
(A (ID-1 H))
(B (ID-1 H))))))
This conjecture simplifies, rewriting with GROUP-OP1-IDENTITY and
GROUP-OP1-INVERSE, and unfolding the functions AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.2 ]
ID-INV-ID
(PROVE-LEMMA KER-INVERSE
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H)
(MEMBER X (PHI-INV G (ID-1 H))))
(MEMBER (INV G X)
(PHI-INV G (ID-1 H))))
((USE (BASIC-MAPPING1 (X (INV G X))
(A (ID-1 H)))
(INV-TO-INV)
(SUBSET-LEMMA0 (S1 (PHI-INV G (ID-1 H)))
(S G)))))
This simplifies, applying BASIC-MAPPING2, ID-INV-ID, and PHI-INV-SUBSET, and
unfolding the functions AND and IMPLIES, to:
(IMPLIES (AND (NOT (MEMBER (INV G X) G))
(EQUAL (PHI (INV G X)) (ID-1 H))
(MEMBER X G)
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H)
(MEMBER X (PHI-INV G (ID-1 H))))
(MEMBER (INV G X)
(PHI-INV G (ID-1 H)))).
But this again simplifies, appealing to the lemmas SUBSET-REFLEXIVITY and
OP-INVERSE-IN-SUBGROUP, and expanding the definition of SUBGROUP-OP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
KER-INVERSE
(PROVE-LEMMA KER-IDENTITY-INVERSE
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(IMPLIES (MEMBER X (PHI-INV G (ID-1 H)))
(AND (EQUAL (OP (ID G) X) X)
(EQUAL (OP X (ID G)) X)
(MEMBER (INV G X)
(PHI-INV G (ID-1 H)))
(EQUAL (OP (INV G X) X) (ID G))
(EQUAL (OP X (INV G X)) (ID G)))))
((USE (SUBSET-LEMMA0 (S1 (PHI-INV G (ID-1 H)))
(S G)))))
WARNING: Note that KER-IDENTITY-INVERSE contains the free variable H which
will be chosen by instantiating the hypothesis (GROUP-OP1 H).
WARNING: Note that KER-IDENTITY-INVERSE contains the free variable H which
will be chosen by instantiating the hypothesis (GROUP-OP1 H).
WARNING: the previously added lemma, KER-INVERSE, could be applied whenever
the newly proposed KER-IDENTITY-INVERSE could!
WARNING: Note that KER-IDENTITY-INVERSE contains the free variable H which
will be chosen by instantiating the hypothesis (GROUP-OP1 H).
WARNING: Note that KER-IDENTITY-INVERSE contains the free variable H which
will be chosen by instantiating the hypothesis (GROUP-OP1 H).
WARNING: Note that the proposed lemma KER-IDENTITY-INVERSE is to be stored as
zero type prescription rules, zero compound recognizer rules, zero linear
rules, and five replacement rules.
This conjecture simplifies, rewriting with PHI-INV-SUBSET, GROUP-OP-IDENTITY,
KER-INVERSE, and GROUP-OP-INVERSE, and expanding AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
KER-IDENTITY-INVERSE
(PROVE-LEMMA KER-SUBGROUP
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H))))
((USE (GROUP-OP (G (PHI-INV G (ID-1 H)))
(ID (ID G))
(INV (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))))
(KER-CLOSED (X (X (PHI-INV G (ID-1 H))))
(Y (Y (PHI-INV G (ID-1 H)))))
(KER-ASSOCIATIVITY (X (X-1 (PHI-INV G (ID-1 H))))
(Y (Y-1 (PHI-INV G (ID-1 H))))
(Z (Z (PHI-INV G (ID-1 H))))
(A (ID-1 H)))
(KER-IDENTITY-INVERSE (X (X-2 (PHI-INV G (ID-1 H)) (ID G)))))))
This conjecture simplifies, appealing to the lemmas KER-IDENTITY, KER-CLOSED,
KER-ASSOCIATIVITY, and KER-IDENTITY-INVERSE, and expanding AND, IMPLIES, and
NOT, to the following 74 new conjectures:
Case 74.(IMPLIES (AND (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, applying KER-CLOSED, to:
T.
Case 73.(IMPLIES (AND (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H)))
(EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G))
(EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, applying KER-CLOSED, to:
T.
Case 72.(IMPLIES (AND (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, appealing to the lemma KER-CLOSED, to:
T.
Case 71.(IMPLIES (AND (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H)))
(EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G))
(EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, applying KER-CLOSED, to:
T.
Case 70.(IMPLIES (AND (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, applying KER-CLOSED, to:
T.
Case 69.(IMPLIES (AND (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H)))
(EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G))
(EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, rewriting with KER-CLOSED, to:
T.
Case 68.(IMPLIES (AND (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(NOT (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, applying KER-CLOSED, to:
T.
Case 67.(IMPLIES (AND (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H)))
(EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G))
(EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, rewriting with KER-CLOSED, to:
T.
Case 66.(IMPLIES (AND (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H)))))))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, rewriting with KER-ASSOCIATIVITY, to:
T.
Case 65.(IMPLIES (AND (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H)))))))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H)))
(EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G))
(EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, appealing to the lemma KER-ASSOCIATIVITY, to:
T.
Case 64.(IMPLIES (AND (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H)))))))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, rewriting with KER-ASSOCIATIVITY, to:
T.
Case 63.(IMPLIES (AND (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H)))))))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H)))
(EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G))
(EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, applying the lemma KER-ASSOCIATIVITY, to:
T.
Case 62.(IMPLIES (AND (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H)))))))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, applying KER-ASSOCIATIVITY, to:
T.
Case 61.(IMPLIES (AND (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H)))))))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H)))
(EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G))
(EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, rewriting with KER-ASSOCIATIVITY, to:
T.
Case 60.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G)))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 59.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G)))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 58.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G)))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, appealing to the lemma KER-IDENTITY-INVERSE,
to:
T.
Case 57.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G)))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 56.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G)))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 55.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G)))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 54.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G)))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, appealing to the lemma KER-IDENTITY-INVERSE, to:
T.
Case 53.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G)))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 52.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G)))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 51.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G)))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, appealing to the lemma KER-IDENTITY-INVERSE, to:
T.
Case 50.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G)))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 49.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(ID G)))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, applying the lemma KER-IDENTITY-INVERSE, to:
T.
Case 48.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G)))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, appealing to the lemma KER-IDENTITY-INVERSE, to:
T.
Case 47.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G)))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 46.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G)))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, appealing to the lemma KER-IDENTITY-INVERSE,
to:
T.
Case 45.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G)))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 44.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G)))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 43.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G)))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 42.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G)))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 41.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G)))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 40.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G)))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 39.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G)))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 38.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G)))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 37.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(ID G)))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 36.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 35.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 34.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, applying the lemma KER-IDENTITY-INVERSE, to:
T.
Case 33.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, applying the lemma KER-IDENTITY-INVERSE, to:
T.
Case 32.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, applying the lemma KER-IDENTITY-INVERSE, to:
T.
Case 31.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, applying the lemma KER-IDENTITY-INVERSE, to:
T.
Case 30.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 29.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 28.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H))))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 27.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H))))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 26.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H))))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 25.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (INV G
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(PHI-INV G (ID-1 H))))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 24.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 23.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 22.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 21.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 20.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, rewriting with the lemma KER-IDENTITY-INVERSE, to:
T.
Case 19.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, applying the lemma KER-IDENTITY-INVERSE, to:
T.
Case 18.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 17.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Case 16.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 15.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
This again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 14.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 13.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (X-2 (PHI-INV G (ID-1 H)) (ID G))
(ID G))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 12.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, appealing to the lemma KER-IDENTITY-INVERSE,
to:
T.
Case 11.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, appealing to the lemma KER-IDENTITY-INVERSE, to:
T.
Case 10.(IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, rewriting with the lemma KER-IDENTITY-INVERSE, to:
T.
Case 9. (IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (X (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 8. (IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, applying the lemma KER-IDENTITY-INVERSE, to:
T.
Case 7. (IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, applying the lemma KER-IDENTITY-INVERSE, to:
T.
Case 6. (IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 5. (IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(NOT (MEMBER (Y (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 4. (IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (X-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
However this again simplifies, applying the lemma KER-IDENTITY-INVERSE, to:
T.
Case 3. (IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (Y-1 (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))),
which again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 2. (IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(NOT (MEMBER (Z (PHI-INV G (ID-1 H)))
(PHI-INV G (ID-1 H))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, applying KER-IDENTITY-INVERSE, to:
T.
Case 1. (IMPLIES (AND (MEMBER (X-2 (PHI-INV G (ID-1 H)) (ID G))
(PHI-INV G (ID-1 H)))
(NOT (EQUAL (OP (ID G)
(X-2 (PHI-INV G (ID-1 H)) (ID G)))
(X-2 (PHI-INV G (ID-1 H)) (ID G))))
(MEMBER (OP (X (PHI-INV G (ID-1 H)))
(Y (PHI-INV G (ID-1 H))))
(PHI-INV G (ID-1 H)))
(EQUAL (OP (OP (X-1 (PHI-INV G (ID-1 H)))
(Y-1 (PHI-INV G (ID-1 H))))
(Z (PHI-INV G (ID-1 H))))
(OP (X-1 (PHI-INV G (ID-1 H)))
(OP (Y-1 (PHI-INV G (ID-1 H)))
(Z (PHI-INV G (ID-1 H))))))
(GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(GROUP-OP (PHI-INV G (ID-1 H)))).
But this again simplifies, rewriting with KER-IDENTITY-INVERSE, to:
T.
Q.E.D.
[ 0.0 2.5 0.1 ]
KER-SUBGROUP
(DEFN-SK OP-NORMALP
(G N)
(FORALL (X Y)
(IMPLIES (AND (MEMBER X G) (MEMBER Y N))
(MEMBER (OP (OP X Y) (INV G X)) N))))
Adding the Skolem axiom:
(AND (IMPLIES (IMPLIES (AND (MEMBER (X-7 G N) G)
(MEMBER (Y-5 G N) N))
(MEMBER (OP (OP (X-7 G N) (Y-5 G N))
(INV G (X-7 G N)))
N))
(OP-NORMALP G N))
(IMPLIES (NOT (IMPLIES (AND (MEMBER X G) (MEMBER Y N))
(MEMBER (OP (OP X Y) (INV G X)) N)))
(NOT (OP-NORMALP G N)))).
As this is a DEFN-SK we can conclude that:
(OR (TRUEP (OP-NORMALP G N))
(FALSEP (OP-NORMALP G N)))
is a theorem.
[ 0.0 0.0 0.0 ]
OP-NORMALP
(DEFN NORMAL-SUBGROUP-OP
(G N)
(AND (GROUP-OP G)
(GROUP-OP N)
(SUBSET N G)
(OP-NORMALP G N)))
From the definition we can conclude that:
(OR (FALSEP (NORMAL-SUBGROUP-OP G N))
(TRUEP (NORMAL-SUBGROUP-OP G N)))
is a theorem.
[ 0.0 0.0 0.0 ]
NORMAL-SUBGROUP-OP
(PROVE-LEMMA NORMAL-LEMMA
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H)
(MEMBER X G)
(MEMBER Y (PHI-INV G (ID-1 H))))
(MEMBER (OP (OP X Y) (INV G X))
(PHI-INV G (ID-1 H))))
((USE (BASIC-MAPPING1 (X (OP (OP X Y) (INV G X)))
(A (ID-1 H)))
(SUBSET-LEMMA0 (X Y)
(S1 (PHI-INV G (ID-1 H)))
(S G))
(INV-TO-INV))))
This formula simplifies, rewriting with the lemmas PHI-INV-SUBSET,
OP-INVERSE-IN-SUBGROUP, SUBSET-REFLEXIVITY, GROUP-OP-ASSOCIATIVITY,
GROUP-OP1-IDENTITY, HOMOMORPHISM-PHI, GROUP-OP1-INVERSE, BASIC-MAPPING2,
GROUP-OP-CLOSED, and BASIC-MAPPING1, and opening up AND, IMPLIES, and
SUBGROUP-OP, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
NORMAL-LEMMA
(PROVE-LEMMA KER-NORMAL
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(OP-NORMALP G (PHI-INV G (ID-1 H))))
((USE (OP-NORMALP (H (PHI-INV G (ID-1 H))))
(NORMAL-LEMMA (X (X-7 G (PHI-INV G (ID-1 H))))
(Y (Y-5 G (PHI-INV G (ID-1 H))))))))
This simplifies, opening up the functions AND, IMPLIES, NOT, and OP-NORMALP,
to:
T.
Q.E.D.
[ 0.0 0.5 0.0 ]
KER-NORMAL
(PROVE-LEMMA KER-NORMAL-SUBGROUP
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(GROUP-OP1 H)
(HOMO-PHI G H))
(NORMAL-SUBGROUP-OP G
(PHI-INV G (ID-1 H)))))
WARNING: Note that the rewrite rule KER-NORMAL-SUBGROUP will be stored so as
to apply only to terms with the nonrecursive function symbol
NORMAL-SUBGROUP-OP.
This simplifies, appealing to the lemmas KER-NORMAL, PHI-INV-SUBSET, and
KER-SUBGROUP, and opening up the function NORMAL-SUBGROUP-OP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
KER-NORMAL-SUBGROUP
(ENABLE GROUP-OP-ASSOCIATIVITY1)
[ 0.0 0.0 0.0 ]
GROUP-OP-ASSOCIATIVITY1-ON
(PROVE-LEMMA RIGHT-COSET-STANDARD-1
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(SUBSET S G)
(MEMBER A G)
(MEMBER X G)
(NOT (MEMBER X S)))
(NOT (MEMBER (OP X A) (RIGHT-COSET S A))))
((USE (CANCELLATION (Y (CAR S))))
(INDUCT (RIGHT-COSET S A))))
WARNING: Note that RIGHT-COSET-STANDARD-1 contains the free variable G which
will be chosen by instantiating the hypothesis (GROUP-OP G).
This simplifies, unfolding the definitions of AND, IMPLIES, NOT, SUBSET,
MEMBER, RIGHT-COSET, and OR, to four new conjectures:
Case 4. (IMPLIES (AND (NOT (MEMBER (CAR S) G))
(NOT (LISTP S))
(GROUP-OP G)
(MEMBER A G)
(MEMBER X G))
(NOT (MEMBER (OP X A) NIL))),
which again simplifies, appealing to the lemma CAR-NLISTP, and unfolding the
definitions of LISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (EQUAL (OP X A) (OP (CAR S) A)))
(LISTP S)
(GROUP-OP G)
(SUBSET (CDR S) G)
(MEMBER A G)
(MEMBER X G)
(NOT (MEMBER X (CDR S)))
(NOT (MEMBER (OP X A)
(RIGHT-COSET (CDR S) A)))
(MEMBER (CAR S) G)
(NOT (EQUAL X (CAR S))))
(NOT (MEMBER (OP X A)
(CONS (OP (CAR S) A)
(RIGHT-COSET (CDR S) A))))),
which again simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding
the function MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL (OP X A) (OP (CAR S) A)))
(NOT (LISTP S))
(GROUP-OP G)
(MEMBER A G)
(MEMBER X G))
(NOT (MEMBER (OP X A) NIL))).
However this again simplifies, rewriting with the lemma CAR-NLISTP, and
expanding the definitions of LISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (EQUAL X (CAR S))
(NOT (LISTP S))
(GROUP-OP G)
(MEMBER A G)
(MEMBER X G))
(NOT (MEMBER (OP X A) NIL))),
which again simplifies, rewriting with CAR-NLISTP, and expanding the
definitions of LISTP and MEMBER, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
RIGHT-COSET-STANDARD-1
(PROVE-LEMMA RIGHT-COSET-STANDARD-2
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(SUBSET S G)
(SET-STANDARD S)
(MEMBER A G))
(SET-STANDARD (RIGHT-COSET S A)))
((USE (RIGHT-COSET-STANDARD-1 (X (CAR S))
(S (CDR S))))
(INDUCT (SET-STANDARD S))))
WARNING: Note that RIGHT-COSET-STANDARD-2 contains the free variable G which
will be chosen by instantiating the hypothesis (GROUP-OP G).
This conjecture simplifies, expanding NOT, AND, IMPLIES, SUBSET, SET-STANDARD,
RIGHT-COSET, and OR, to the following five new formulas:
Case 5. (IMPLIES (AND (NOT (SUBSET (CDR S) G))
(NOT (LISTP S))
(GROUP-OP G)
(MEMBER A G))
(SET-STANDARD NIL)).
But this again simplifies, rewriting with CDR-NLISTP, and expanding LISTP
and SUBSET, to:
T.
Case 4. (IMPLIES (AND (NOT (MEMBER (CAR S) G))
(NOT (LISTP S))
(GROUP-OP G)
(MEMBER A G))
(SET-STANDARD NIL)).
This again simplifies, rewriting with the lemma CAR-NLISTP, and opening up
the function SET-STANDARD, to:
T.
Case 3. (IMPLIES (AND (MEMBER (CAR S) (CDR S))
(NOT (LISTP S))
(GROUP-OP G)
(MEMBER A G))
(SET-STANDARD NIL)),
which again simplifies, rewriting with CAR-NLISTP and CDR-NLISTP, and
unfolding the function MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (MEMBER (OP (CAR S) A)
(RIGHT-COSET (CDR S) A)))
(LISTP S)
(GROUP-OP G)
(SUBSET (CDR S) G)
(SET-STANDARD (CDR S))
(MEMBER A G)
(SET-STANDARD (RIGHT-COSET (CDR S) A))
(MEMBER (CAR S) G)
(NOT (MEMBER (CAR S) (CDR S))))
(SET-STANDARD (CONS (OP (CAR S) A)
(RIGHT-COSET (CDR S) A)))).
However this again simplifies, applying RIGHT-COSET-STANDARD-1, CDR-CONS,
and CAR-CONS, and unfolding the definition of SET-STANDARD, to:
T.
Case 1. (IMPLIES (AND (NOT (MEMBER (OP (CAR S) A)
(RIGHT-COSET (CDR S) A)))
(NOT (LISTP S))
(GROUP-OP G)
(MEMBER A G))
(SET-STANDARD NIL)).
This again simplifies, applying the lemmas CAR-NLISTP and CDR-NLISTP, and
expanding LISTP, RIGHT-COSET, MEMBER, and SET-STANDARD, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
RIGHT-COSET-STANDARD-2
(PROVE-LEMMA RIGHT-COSET-STANDARD
(REWRITE)
(IMPLIES (AND (SUBGROUP-OP H G)
(SET-STANDARD H)
(MEMBER A G))
(SET-STANDARD (RIGHT-COSET H A)))
((USE (RIGHT-COSET-STANDARD-2 (S H)))))
WARNING: Note that RIGHT-COSET-STANDARD contains the free variable G which
will be chosen by instantiating the hypothesis (SUBGROUP-OP H G).
This formula can be simplified, using the abbreviations SUBGROUP-OP, AND, and
IMPLIES, to:
(IMPLIES (AND (IMPLIES (AND (GROUP-OP G)
(SUBSET H G)
(SET-STANDARD H)
(MEMBER A G))
(SET-STANDARD (RIGHT-COSET H A)))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SET-STANDARD H)
(MEMBER A G))
(SET-STANDARD (RIGHT-COSET H A))),
which simplifies, rewriting with SUBSET-REFLEXIVITY and SUBSET-TRANSITIVITY,
and opening up AND and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
RIGHT-COSET-STANDARD
(PROVE-LEMMA RIGHT-COSET-DISJOINT-LEMMA
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(SUBSET S G)
(MEMBER X G)
(MEMBER Y G)
(MEMBER A G)
(MEMBER B G)
(MEMBER (OP (INV G X) Y) S)
(NOT (MEMBER A (RIGHT-COSET S B))))
(NOT (EQUAL (OP X A) (OP Y B)))))
WARNING: Note that RIGHT-COSET-DISJOINT-LEMMA contains the free variables S
and G which will be chosen by instantiating the hypotheses (GROUP-OP G) and
(SUBSET S G).
Name the conjecture *1.
We will appeal to induction. Three inductions are suggested by terms in
the conjecture. However, they merge into one likely candidate induction. We
will induct according to the following scheme:
(AND (IMPLIES (AND (LISTP S) (p X A Y B (CDR S) G))
(p X A Y B S G))
(IMPLIES (NOT (LISTP S))
(p X A Y B S G))).
Linear arithmetic and the lemma CDR-LESSP establish that the measure (COUNT S)
decreases according to the well-founded relation LESSP in each induction step
of the scheme. The above induction scheme generates the following four new
formulas:
Case 4. (IMPLIES (AND (LISTP S)
(NOT (SUBSET (CDR S) G))
(GROUP-OP G)
(SUBSET S G)
(MEMBER X G)
(MEMBER Y G)
(MEMBER A G)
(MEMBER B G)
(MEMBER (OP (INV G X) Y) S)
(NOT (MEMBER A (RIGHT-COSET S B))))
(NOT (EQUAL (OP X A) (OP Y B)))).
This simplifies, opening up the definition of SUBSET, to:
T.
Case 3. (IMPLIES (AND (LISTP S)
(NOT (MEMBER (OP (INV G X) Y) (CDR S)))
(GROUP-OP G)
(SUBSET S G)
(MEMBER X G)
(MEMBER Y G)
(MEMBER A G)
(MEMBER B G)
(MEMBER (OP (INV G X) Y) S)
(NOT (MEMBER A (RIGHT-COSET S B))))
(NOT (EQUAL (OP X A) (OP Y B)))).
This simplifies, applying CDR-CONS and CAR-CONS, and unfolding the functions
SUBSET, MEMBER, and RIGHT-COSET, to:
(IMPLIES (AND (LISTP S)
(NOT (MEMBER (OP (INV G X) Y) (CDR S)))
(GROUP-OP G)
(MEMBER (CAR S) G)
(SUBSET (CDR S) G)
(MEMBER X G)
(MEMBER Y G)
(MEMBER A G)
(MEMBER B G)
(EQUAL (OP (INV G X) Y) (CAR S))
(NOT (EQUAL A (OP (CAR S) B)))
(NOT (MEMBER A (RIGHT-COSET (CDR S) B))))
(NOT (EQUAL (OP X A) (OP Y B)))).
This further simplifies, trivially, to:
(IMPLIES (AND (LISTP S)
(NOT (MEMBER (CAR S) (CDR S)))
(GROUP-OP G)
(MEMBER (CAR S) G)
(SUBSET (CDR S) G)
(MEMBER X G)
(MEMBER Y G)
(MEMBER A G)
(MEMBER B G)
(EQUAL (OP (INV G X) Y) (CAR S))
(NOT (EQUAL A (OP (CAR S) B)))
(NOT (MEMBER A (RIGHT-COSET (CDR S) B))))
(NOT (EQUAL (OP X A) (OP Y B)))).
Applying the lemma CAR-CDR-ELIM, replace S by (CONS Z V) to eliminate
(CAR S) and (CDR S). This produces the new formula:
(IMPLIES (AND (NOT (MEMBER Z V))
(GROUP-OP G)
(MEMBER Z G)
(SUBSET V G)
(MEMBER X G)
(MEMBER Y G)
(MEMBER A G)
(MEMBER B G)
(EQUAL (OP (INV G X) Y) Z)
(NOT (EQUAL A (OP Z B)))
(NOT (MEMBER A (RIGHT-COSET V B))))
(NOT (EQUAL (OP X A) (OP Y B)))),
which further simplifies, applying OP-INVERSE-IN-SUBGROUP,
SUBSET-REFLEXIVITY, GROUP-OP-CLOSED, GROUP-OP-INVERSE, GROUP-OP-IDENTITY,
GROUP-OP-ASSOCIATIVITY1, and GROUP-OP-ASSOCIATIVITY, and opening up the
definition of SUBGROUP-OP, to:
T.
Case 2. (IMPLIES (AND (LISTP S)
(MEMBER A (RIGHT-COSET (CDR S) B))
(GROUP-OP G)
(SUBSET S G)
(MEMBER X G)
(MEMBER Y G)
(MEMBER A G)
(MEMBER B G)
(MEMBER (OP (INV G X) Y) S)
(NOT (MEMBER A (RIGHT-COSET S B))))
(NOT (EQUAL (OP X A) (OP Y B)))).
This simplifies, rewriting with CDR-CONS and CAR-CONS, and unfolding SUBSET,
MEMBER, and RIGHT-COSET, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP S))
(GROUP-OP G)
(SUBSET S G)
(MEMBER X G)
(MEMBER Y G)
(MEMBER A G)
(MEMBER B G)
(MEMBER (OP (INV G X) Y) S)
(NOT (MEMBER A (RIGHT-COSET S B))))
(NOT (EQUAL (OP X A) (OP Y B)))),
which simplifies, opening up the definitions of SUBSET and MEMBER, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.1 ]
RIGHT-COSET-DISJOINT-LEMMA
(PROVE-LEMMA RIGHT-COSET-DISJOINT-1
(REWRITE)
(IMPLIES (AND (SUBGROUP-OP H G)
(SUBSET S H)
(MEMBER X H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(NOT (MEMBER (OP X A) (RIGHT-COSET S B))))
((USE (RIGHT-COSET-DISJOINT-LEMMA (Y (CAR S))
(S H)))
(INDUCT (SUBSET S H))))
WARNING: Note that RIGHT-COSET-DISJOINT-1 contains the free variables G and H
which will be chosen by instantiating the hypothesis (SUBGROUP-OP H G).
This conjecture simplifies, opening up the functions NOT, AND, IMPLIES,
SUBGROUP-OP, SUBSET, RIGHT-COSET, and OR, to the following eight new
conjectures:
Case 8. (IMPLIES (AND (NOT (MEMBER X G))
(LISTP S)
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SUBSET (CDR S) H)
(MEMBER X H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B)))
(NOT (MEMBER (OP X A)
(RIGHT-COSET (CDR S) B)))
(MEMBER (CAR S) H))
(NOT (MEMBER (OP X A)
(CONS (OP (CAR S) B)
(RIGHT-COSET (CDR S) B))))).
But this again simplifies, applying SUBSET-LEMMA0, to:
T.
Case 7. (IMPLIES (AND (NOT (MEMBER X G))
(NOT (LISTP S))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(MEMBER X H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(NOT (MEMBER (OP X A) NIL))).
This again simplifies, applying the lemma SUBSET-LEMMA0, to:
T.
Case 6. (IMPLIES (AND (NOT (MEMBER (CAR S) G))
(LISTP S)
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SUBSET (CDR S) H)
(MEMBER X H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B)))
(NOT (MEMBER (OP X A)
(RIGHT-COSET (CDR S) B)))
(MEMBER (CAR S) H))
(NOT (MEMBER (OP X A)
(CONS (OP (CAR S) B)
(RIGHT-COSET (CDR S) B))))),
which again simplifies, applying SUBSET-LEMMA0, to:
T.
Case 5. (IMPLIES (AND (NOT (MEMBER (CAR S) G))
(NOT (LISTP S))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(MEMBER X H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(NOT (MEMBER (OP X A) NIL))).
This again simplifies, rewriting with CAR-NLISTP, and expanding LISTP and
MEMBER, to:
T.
Case 4. (IMPLIES (AND (NOT (MEMBER (OP (INV G X) (CAR S)) H))
(LISTP S)
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SUBSET (CDR S) H)
(MEMBER X H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B)))
(NOT (MEMBER (OP X A)
(RIGHT-COSET (CDR S) B)))
(MEMBER (CAR S) H))
(NOT (MEMBER (OP X A)
(CONS (OP (CAR S) B)
(RIGHT-COSET (CDR S) B))))).
This again simplifies, appealing to the lemmas OP-INVERSE-IN-SUBGROUP,
SUBSET-TRANSITIVITY, SUBSET-REFLEXIVITY, and GROUP-OP-CLOSED, and unfolding
the function SUBGROUP-OP, to:
T.
Case 3. (IMPLIES (AND (NOT (MEMBER (OP (INV G X) (CAR S)) H))
(NOT (LISTP S))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(MEMBER X H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(NOT (MEMBER (OP X A) NIL))),
which again simplifies, applying CAR-NLISTP, and expanding the definitions
of LISTP and MEMBER, to:
T.
Case 2. (IMPLIES (AND (NOT (EQUAL (OP X A) (OP (CAR S) B)))
(LISTP S)
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SUBSET (CDR S) H)
(MEMBER X H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B)))
(NOT (MEMBER (OP X A)
(RIGHT-COSET (CDR S) B)))
(MEMBER (CAR S) H))
(NOT (MEMBER (OP X A)
(CONS (OP (CAR S) B)
(RIGHT-COSET (CDR S) B))))).
This again simplifies, applying CDR-CONS and CAR-CONS, and expanding MEMBER,
to:
T.
Case 1. (IMPLIES (AND (NOT (EQUAL (OP X A) (OP (CAR S) B)))
(NOT (LISTP S))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(MEMBER X H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(NOT (MEMBER (OP X A) NIL))).
But this again simplifies, applying CAR-NLISTP, and unfolding the functions
LISTP and MEMBER, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
RIGHT-COSET-DISJOINT-1
(PROVE-LEMMA RIGHT-COSET-DISJOINT-2
(REWRITE)
(IMPLIES (AND (SUBGROUP-OP H G)
(MEMBER X H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(NOT (MEMBER (OP X A) (RIGHT-COSET H B))))
((USE (RIGHT-COSET-DISJOINT-1 (S H)))))
WARNING: Note that RIGHT-COSET-DISJOINT-2 contains the free variable G which
will be chosen by instantiating the hypothesis (SUBGROUP-OP H G).
This conjecture can be simplified, using the abbreviations NOT, SUBGROUP-OP,
AND, and IMPLIES, to:
(IMPLIES (AND (IMPLIES (AND (SUBGROUP-OP H G)
(SUBSET H H)
(MEMBER X H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(NOT (MEMBER (OP X A) (RIGHT-COSET H B))))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(MEMBER X H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(NOT (MEMBER (OP X A) (RIGHT-COSET H B)))).
This simplifies, rewriting with the lemmas SUBSET-TRANSITIVITY and
SUBSET-REFLEXIVITY, and unfolding the functions SUBGROUP-OP, NOT, AND, and
IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
RIGHT-COSET-DISJOINT-2
(PROVE-LEMMA RIGHT-COSET-DISJOINT-3
(REWRITE)
(IMPLIES (AND (SUBGROUP-OP H G)
(SUBSET S H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(SET-DISJOINT (RIGHT-COSET S A)
(RIGHT-COSET H B)))
((USE (RIGHT-COSET-DISJOINT-2 (X (CAR S))))
(INDUCT (RIGHT-COSET S A))))
WARNING: Note that RIGHT-COSET-DISJOINT-3 contains the free variable G which
will be chosen by instantiating the hypothesis (SUBGROUP-OP H G).
This formula simplifies, expanding the definitions of SUBGROUP-OP, NOT, AND,
IMPLIES, SUBSET, RIGHT-COSET, and OR, to three new goals:
Case 3. (IMPLIES (AND (NOT (MEMBER (CAR S) H))
(NOT (LISTP S))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(SET-DISJOINT NIL (RIGHT-COSET H B))),
which again simplifies, rewriting with the lemma CAR-NLISTP, and expanding
LISTP and SET-DISJOINT, to:
T.
Case 2. (IMPLIES (AND (NOT (MEMBER (OP (CAR S) A)
(RIGHT-COSET H B)))
(LISTP S)
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SUBSET (CDR S) H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B)))
(SET-DISJOINT (RIGHT-COSET (CDR S) A)
(RIGHT-COSET H B))
(MEMBER (CAR S) H))
(SET-DISJOINT (CONS (OP (CAR S) A)
(RIGHT-COSET (CDR S) A))
(RIGHT-COSET H B))),
which again simplifies, applying the lemmas CDR-CONS and CAR-CONS, and
opening up the definition of SET-DISJOINT, to:
T.
Case 1. (IMPLIES (AND (NOT (MEMBER (OP (CAR S) A)
(RIGHT-COSET H B)))
(NOT (LISTP S))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(SET-DISJOINT NIL (RIGHT-COSET H B))),
which again simplifies, applying CAR-NLISTP, and unfolding the functions
LISTP and SET-DISJOINT, to:
T.
Q.E.D.
[ 0.0 0.3 0.0 ]
RIGHT-COSET-DISJOINT-3
(PROVE-LEMMA RIGHT-COSET-DISJOINT
(REWRITE)
(IMPLIES (AND (SUBGROUP-OP H G)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(SET-DISJOINT (RIGHT-COSET H A)
(RIGHT-COSET H B)))
((USE (RIGHT-COSET-DISJOINT-3 (S H)))))
WARNING: Note that RIGHT-COSET-DISJOINT contains the free variable G which
will be chosen by instantiating the hypothesis (SUBGROUP-OP H G).
This conjecture can be simplified, using the abbreviations NOT, SUBGROUP-OP,
AND, and IMPLIES, to the formula:
(IMPLIES (AND (IMPLIES (AND (SUBGROUP-OP H G)
(SUBSET H H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(SET-DISJOINT (RIGHT-COSET H A)
(RIGHT-COSET H B)))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(SET-DISJOINT (RIGHT-COSET H A)
(RIGHT-COSET H B))).
This simplifies, applying SUBSET-TRANSITIVITY and SUBSET-REFLEXIVITY, and
unfolding the definitions of SUBGROUP-OP, NOT, AND, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
RIGHT-COSET-DISJOINT
(DISABLE GROUP-OP)
[ 0.0 0.0 0.0 ]
GROUP-OP-OFF1
(DEFN-SK OP-CLOSED
(S1 S2)
(FORALL (X Y)
(IMPLIES (AND (MEMBER X S1) (MEMBER Y S2))
(MEMBER (OP X Y) S2))))
Adding the Skolem axiom:
(AND (IMPLIES (IMPLIES (AND (MEMBER (X-8 S1 S2) S1)
(MEMBER (Y-6 S1 S2) S2))
(MEMBER (OP (X-8 S1 S2) (Y-6 S1 S2))
S2))
(OP-CLOSED S1 S2))
(IMPLIES (NOT (IMPLIES (AND (MEMBER X S1) (MEMBER Y S2))
(MEMBER (OP X Y) S2)))
(NOT (OP-CLOSED S1 S2)))).
As this is a DEFN-SK we can conclude that:
(OR (TRUEP (OP-CLOSED S1 S2))
(FALSEP (OP-CLOSED S1 S2)))
is a theorem.
[ 0.0 0.0 0.0 ]
OP-CLOSED
(PROVE-LEMMA LA-LEMMA1
(REWRITE)
(IMPLIES (AND (MEMBER B S)
(SUBSET H1 H)
(OP-CLOSED H S))
(SUBSET (RIGHT-COSET H1 B) S))
((USE (OP-CLOSED (S1 H)
(S2 S)
(X (CAR H1))
(Y B)))
(INDUCT (RIGHT-COSET H1 B))))
WARNING: Note that LA-LEMMA1 contains the free variable H which will be
chosen by instantiating the hypothesis (SUBSET H1 H).
This formula simplifies, opening up AND, IMPLIES, NOT, SUBSET, RIGHT-COSET,
and OR, to the following six new formulas:
Case 6. (IMPLIES (AND (MEMBER (X-8 H S) H)
(MEMBER (Y-6 H S) S)
(NOT (MEMBER (OP (X-8 H S) (Y-6 H S)) S))
(NOT (MEMBER (CAR H1) H))
(NOT (LISTP H1))
(MEMBER B S)
(OP-CLOSED H S))
(SUBSET NIL S)).
However this again simplifies, applying the lemma CAR-NLISTP, and unfolding
the functions LISTP and SUBSET, to:
T.
Case 5. (IMPLIES (AND (MEMBER (X-8 H S) H)
(MEMBER (Y-6 H S) S)
(NOT (MEMBER (OP (X-8 H S) (Y-6 H S)) S))
(MEMBER (OP (CAR H1) B) S)
(LISTP H1)
(MEMBER B S)
(SUBSET (CDR H1) H)
(OP-CLOSED H S)
(SUBSET (RIGHT-COSET (CDR H1) B) S)
(MEMBER (CAR H1) H))
(SUBSET (CONS (OP (CAR H1) B)
(RIGHT-COSET (CDR H1) B))
S)),
which again simplifies, rewriting with SUBSET-TRANSITIVITY,
SUBSET-REFLEXIVITY, CDR-CONS, and CAR-CONS, and expanding the function
SUBSET, to:
T.
Case 4. (IMPLIES (AND (MEMBER (X-8 H S) H)
(MEMBER (Y-6 H S) S)
(NOT (MEMBER (OP (X-8 H S) (Y-6 H S)) S))
(MEMBER (OP (CAR H1) B) S)
(NOT (LISTP H1))
(MEMBER B S)
(OP-CLOSED H S))
(SUBSET NIL S)).
This again simplifies, applying CAR-NLISTP, and opening up the definitions
of LISTP and SUBSET, to:
T.
Case 3. (IMPLIES (AND (OP-CLOSED H S)
(NOT (MEMBER (CAR H1) H))
(NOT (LISTP H1))
(MEMBER B S))
(SUBSET NIL S)).
But this again simplifies, applying CAR-NLISTP, and opening up the functions
LISTP and SUBSET, to:
T.
Case 2. (IMPLIES (AND (OP-CLOSED H S)
(MEMBER (OP (CAR H1) B) S)
(LISTP H1)
(MEMBER B S)
(SUBSET (CDR H1) H)
(SUBSET (RIGHT-COSET (CDR H1) B) S)
(MEMBER (CAR H1) H))
(SUBSET (CONS (OP (CAR H1) B)
(RIGHT-COSET (CDR H1) B))
S)).
However this again simplifies, applying SUBSET-TRANSITIVITY,
SUBSET-REFLEXIVITY, CDR-CONS, and CAR-CONS, and unfolding the function
SUBSET, to:
T.
Case 1. (IMPLIES (AND (OP-CLOSED H S)
(MEMBER (OP (CAR H1) B) S)
(NOT (LISTP H1))
(MEMBER B S))
(SUBSET NIL S)).
But this again simplifies, applying CAR-NLISTP, and unfolding LISTP and
SUBSET, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
LA-LEMMA1
(PROVE-LEMMA LA-LEMMA2
(REWRITE)
(IMPLIES (AND (SUBGROUP-OP H G)
(SUBSET S G)
(MEMBER B G)
(OP-CLOSED H S))
(IMPLIES (AND (MEMBER X H)
(MEMBER A
(SET-MINUS S (RIGHT-COSET H B))))
(MEMBER (OP X A)
(SET-MINUS S (RIGHT-COSET H B)))))
((USE (OP-CLOSED (S1 H) (S2 S) (Y A))
(RIGHT-COSET-DISJOINT-2)
(SET-MINUS-LEMMA3 (X A)
(S1 (RIGHT-COSET H B)))
(SET-MINUS-LEMMA3 (X (OP X A))
(S1 (RIGHT-COSET H B))))
(DO-NOT-INDUCT T)))
WARNING: Note that LA-LEMMA2 contains the free variable G which will be
chosen by instantiating the hypothesis (SUBGROUP-OP H G).
This formula can be simplified, using the abbreviations SUBGROUP-OP, IMPLIES,
and AND, to the new conjecture:
(IMPLIES (AND (IMPLIES (IMPLIES (AND (MEMBER (X-8 H S) H)
(MEMBER (Y-6 H S) S))
(MEMBER (OP (X-8 H S) (Y-6 H S)) S))
(OP-CLOSED H S))
(IMPLIES (NOT (IMPLIES (AND (MEMBER X H) (MEMBER A S))
(MEMBER (OP X A) S)))
(NOT (OP-CLOSED H S)))
(IMPLIES (AND (SUBGROUP-OP H G)
(MEMBER X H)
(MEMBER A G)
(MEMBER B G)
(NOT (MEMBER A (RIGHT-COSET H B))))
(NOT (MEMBER (OP X A) (RIGHT-COSET H B))))
(EQUAL (MEMBER A
(SET-MINUS S (RIGHT-COSET H B)))
(AND (MEMBER A S)
(NOT (MEMBER A (RIGHT-COSET H B)))))
(EQUAL (MEMBER (OP X A)
(SET-MINUS S (RIGHT-COSET H B)))
(AND (MEMBER (OP X A) S)
(NOT (MEMBER (OP X A) (RIGHT-COSET H B)))))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SUBSET S G)
(MEMBER B G)
(OP-CLOSED H S)
(MEMBER X H)
(MEMBER A
(SET-MINUS S (RIGHT-COSET H B))))
(MEMBER (OP X A)
(SET-MINUS S (RIGHT-COSET H B)))),
which simplifies, rewriting with SUBSET-TRANSITIVITY and SUBSET-REFLEXIVITY,
and unfolding AND, IMPLIES, NOT, SUBGROUP-OP, and EQUAL, to:
(IMPLIES (AND (MEMBER (OP X A) S)
(NOT (MEMBER A G))
(MEMBER A S)
(NOT (MEMBER A (RIGHT-COSET H B)))
(MEMBER (OP X A) (RIGHT-COSET H B))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SUBSET S G)
(MEMBER B G)
(OP-CLOSED H S)
(MEMBER X H)
(MEMBER A
(SET-MINUS S (RIGHT-COSET H B))))
(MEMBER (OP X A)
(SET-MINUS S (RIGHT-COSET H B)))),
which again simplifies, appealing to the lemma SUBSET-LEMMA0, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
LA-LEMMA2
(PROVE-LEMMA LA-LEMMA3
(REWRITE)
(IMPLIES (AND (SUBGROUP-OP H G)
(SUBSET S G)
(MEMBER B G)
(OP-CLOSED H S))
(OP-CLOSED H
(SET-MINUS S (RIGHT-COSET H B))))
((USE (OP-CLOSED (S1 H)
(S2 (SET-MINUS S (RIGHT-COSET H B)))
(X (X-8 H
(SET-MINUS S (RIGHT-COSET H B))))
(Y (Y-6 H
(SET-MINUS S (RIGHT-COSET H B)))))
(LA-LEMMA2 (X (X-8 H
(SET-MINUS S (RIGHT-COSET H B))))
(A (Y-6 H
(SET-MINUS S (RIGHT-COSET H B))))))))
WARNING: Note that LA-LEMMA3 contains the free variable G which will be
chosen by instantiating the hypothesis (SUBGROUP-OP H G).
This formula can be simplified, using the abbreviations SUBGROUP-OP, IMPLIES,
and AND, to the new conjecture:
(IMPLIES
(AND
(IMPLIES (IMPLIES (AND (MEMBER (X-8 H
(SET-MINUS S (RIGHT-COSET H B)))
H)
(MEMBER (Y-6 H
(SET-MINUS S (RIGHT-COSET H B)))
(SET-MINUS S (RIGHT-COSET H B))))
(MEMBER (OP (X-8 H
(SET-MINUS S (RIGHT-COSET H B)))
(Y-6 H
(SET-MINUS S (RIGHT-COSET H B))))
(SET-MINUS S (RIGHT-COSET H B))))
(OP-CLOSED H
(SET-MINUS S (RIGHT-COSET H B))))
(IMPLIES
(NOT (IMPLIES (AND (MEMBER (X-8 H
(SET-MINUS S (RIGHT-COSET H B)))
H)
(MEMBER (Y-6 H
(SET-MINUS S (RIGHT-COSET H B)))
(SET-MINUS S (RIGHT-COSET H B))))
(MEMBER (OP (X-8 H
(SET-MINUS S (RIGHT-COSET H B)))
(Y-6 H
(SET-MINUS S (RIGHT-COSET H B))))
(SET-MINUS S (RIGHT-COSET H B)))))
(NOT (OP-CLOSED H
(SET-MINUS S (RIGHT-COSET H B)))))
(IMPLIES (AND (SUBGROUP-OP H G)
(SUBSET S G)
(MEMBER B G)
(OP-CLOSED H S))
(IMPLIES (AND (MEMBER (X-8 H
(SET-MINUS S (RIGHT-COSET H B)))
H)
(MEMBER (Y-6 H
(SET-MINUS S (RIGHT-COSET H B)))
(SET-MINUS S (RIGHT-COSET H B))))
(MEMBER (OP (X-8 H
(SET-MINUS S (RIGHT-COSET H B)))
(Y-6 H
(SET-MINUS S (RIGHT-COSET H B))))
(SET-MINUS S (RIGHT-COSET H B)))))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SUBSET S G)
(MEMBER B G)
(OP-CLOSED H S))
(OP-CLOSED H
(SET-MINUS S (RIGHT-COSET H B)))),
which simplifies, rewriting with SUBSET-TRANSITIVITY and SUBSET-REFLEXIVITY,
and expanding AND, IMPLIES, NOT, and SUBGROUP-OP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LA-LEMMA3
(PROVE-LEMMA LAGRANGE-INDUCT-MEASURE
(REWRITE)
(IMPLIES (AND (GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SUBSET S G)
(LISTP S))
(LESSP (COUNT (SET-MINUS S (RIGHT-COSET H (CAR S))))
(COUNT S)))
((USE (SET-MINUS-LEMMA (S1 (RIGHT-COSET H (CAR S)))
(X (CAR S)))
(RIGHT-COSET-NEMPTY (X (CAR S)) (S H))
(SUBSET-LEMMA0 (X (CAR S))
(S G)
(S1 H)))
(DO-NOT-INDUCT T)))
WARNING: When the linear lemma LAGRANGE-INDUCT-MEASURE is stored under:
(COUNT (SET-MINUS S (RIGHT-COSET H (CAR S))))
it contains the free variable G which will be chosen by instantiating the
hypothesis (GROUP-OP G).
WARNING: Note that the proposed lemma LAGRANGE-INDUCT-MEASURE is to be stored
as zero type prescription rules, zero compound recognizer rules, one linear
rule, and zero replacement rules.
This formula simplifies, rewriting with SUBSET-LEMMA0, SUBSET-REFLEXIVITY,
SUBSET-TRANSITIVITY, and OP-IDENTITY-IN-SUBGROUP, and opening up the
definitions of MEMBER, AND, IMPLIES, and SUBGROUP-OP, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LAGRANGE-INDUCT-MEASURE
(PROVE-LEMMA LA-LEMMA4 NIL
(IMPLIES (AND (LEQ Y X)
(LEQ 1 Y)
(EQUAL (REMAINDER (DIFFERENCE X Y) Y)
0))
(EQUAL (REMAINDER X Y) 0)))
This conjecture simplifies, expanding the definition of REMAINDER, to two new
conjectures:
Case 2. (IMPLIES (AND (NOT (LESSP X Y))
(NOT (LESSP Y 1))
(EQUAL (REMAINDER (DIFFERENCE X Y) Y)
0)
(NOT (NUMBERP Y))
(NUMBERP X))
(EQUAL X 0)),
which again simplifies, expanding the functions LESSP, NUMBERP, and EQUAL,
to:
T.
Case 1. (IMPLIES (AND (NOT (LESSP X Y))
(NOT (LESSP Y 1))
(EQUAL (REMAINDER (DIFFERENCE X Y) Y)
0)
(EQUAL Y 0)
(NUMBERP X))
(EQUAL X 0)),
which again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LA-LEMMA4
(PROVE-LEMMA LA-LEMMA5
(REWRITE)
(IMPLIES
(AND (SUBGROUP-OP H G)
(SET-STANDARD H)
(SUBSET S G)
(SET-STANDARD S)
(OP-CLOSED H S)
(EQUAL (REMAINDER (CARDINAL (SET-MINUS S (RIGHT-COSET H (CAR S))))
(CARDINAL H))
0))
(EQUAL (REMAINDER (CARDINAL S) (CARDINAL H))
0))
((USE (CARDINAL-INEQUALITY (A S)
(B (RIGHT-COSET H (CAR S))))
(CARDINAL-SUBSET (A S)
(B (RIGHT-COSET H (CAR S))))
(LA-LEMMA4 (X (CARDINAL S))
(Y (CARDINAL H)))
(RIGHT-COSET-STANDARD (A (CAR S)))
(RIGHT-COSET-CARDINAL (S H)
(A (CAR S)))
(LA-LEMMA1 (H1 H) (B (CAR S)))
(GROUP-OP-ORDER))
(DO-NOT-INDUCT T)))
WARNING: Note that LA-LEMMA5 contains the free variable G which will be
chosen by instantiating the hypothesis (SUBGROUP-OP H G).
This formula can be simplified, using the abbreviations SUBGROUP-OP, IMPLIES,
AND, and RIGHT-COSET-CARDINAL, to the new goal:
(IMPLIES
(AND
(IMPLIES (AND (SET-STANDARD (RIGHT-COSET H (CAR S)))
(SUBSET (RIGHT-COSET H (CAR S)) S))
(IF (LESSP (CARDINAL S) (CARDINAL H))
F T))
(IMPLIES (AND (SET-STANDARD S)
(SET-STANDARD (RIGHT-COSET H (CAR S)))
(SUBSET (RIGHT-COSET H (CAR S)) S))
(EQUAL (CARDINAL (SET-MINUS S (RIGHT-COSET H (CAR S))))
(DIFFERENCE (CARDINAL S)
(CARDINAL H))))
(IMPLIES (AND (IF (LESSP (CARDINAL S) (CARDINAL H))
F T)
(IF (LESSP (CARDINAL H) 1) F T)
(EQUAL (REMAINDER (DIFFERENCE (CARDINAL S) (CARDINAL H))
(CARDINAL H))
0))
(EQUAL (REMAINDER (CARDINAL S) (CARDINAL H))
0))
(IMPLIES (AND (SUBGROUP-OP H G)
(SET-STANDARD H)
(MEMBER (CAR S) G))
(SET-STANDARD (RIGHT-COSET H (CAR S))))
(EQUAL (CARDINAL H) (CARDINAL H))
(IMPLIES (AND (MEMBER (CAR S) S)
(SUBSET H H)
(OP-CLOSED H S))
(SUBSET (RIGHT-COSET H (CAR S)) S))
(IMPLIES (GROUP-OP G)
(IF (LESSP (CARDINAL G) 1) F T))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SET-STANDARD H)
(SUBSET S G)
(SET-STANDARD S)
(OP-CLOSED H S)
(EQUAL (REMAINDER (CARDINAL (SET-MINUS S (RIGHT-COSET H (CAR S))))
(CARDINAL H))
0))
(EQUAL (REMAINDER (CARDINAL S) (CARDINAL H))
0)),
which simplifies, rewriting with SUBSET-TRANSITIVITY, SUBSET-REFLEXIVITY,
CAR-NLISTP, RIGHT-COSET-CARDINAL, and CARDINAL-SUBSET, and opening up AND,
IMPLIES, REMAINDER, SUBGROUP-OP, MEMBER, SUBSET, SET-STANDARD, OP-CLOSED,
SET-MINUS, CARDINAL, LESSP, EQUAL, NUMBERP, and DIFFERENCE, to:
(IMPLIES (AND (NOT (LESSP (CARDINAL S) (CARDINAL H)))
(EQUAL (CARDINAL (SET-MINUS S (RIGHT-COSET H (CAR S))))
(DIFFERENCE (CARDINAL S)
(CARDINAL H)))
(LESSP (CARDINAL H) 1)
(SET-STANDARD (RIGHT-COSET H (CAR S)))
(SUBSET (RIGHT-COSET H (CAR S)) S)
(NOT (LESSP (CARDINAL G) 1))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SET-STANDARD H)
(SUBSET S G)
(SET-STANDARD S)
(OP-CLOSED H S)
(EQUAL (REMAINDER (DIFFERENCE (CARDINAL S) (CARDINAL H))
(CARDINAL H))
0)
(EQUAL (CARDINAL H) 0))
(EQUAL (CARDINAL S) 0)),
which again simplifies, applying RIGHT-COSET-CARDINAL and CARDINAL-SUBSET, and
opening up the functions EQUAL, LESSP, DIFFERENCE, and REMAINDER, to:
T.
Q.E.D.
[ 0.0 0.6 0.0 ]
LA-LEMMA5
(DEFN LAGRANGE-INDUCT
(G H S)
(IF (AND (SUBGROUP-OP H G)
(SUBSET S G)
(LISTP S))
(LAGRANGE-INDUCT G H
(SET-MINUS S (RIGHT-COSET H (CAR S))))
T)
((LESSP (COUNT S))))
Linear arithmetic, the lemma LAGRANGE-INDUCT-MEASURE, and the definitions
of AND and SUBGROUP-OP inform us that the measure (COUNT S) decreases
according to the well-founded relation LESSP in each recursive call. Hence,
LAGRANGE-INDUCT is accepted under the definitional principle. Observe that:
(TRUEP (LAGRANGE-INDUCT G H S))
is a theorem.
[ 0.0 0.0 0.0 ]
LAGRANGE-INDUCT
(PROVE-LEMMA LAGRANGE-GENERALIZED NIL
(IMPLIES (AND (SUBGROUP-OP H G)
(SET-STANDARD H)
(SUBSET S G)
(SET-STANDARD S)
(OP-CLOSED H S))
(EQUAL (REMAINDER (CARDINAL S) (CARDINAL H))
0))
((USE (LA-LEMMA3 (B (CAR S)))
(SET-STANDARD-LEMMA (A S)
(B (RIGHT-COSET H (CAR S))))
(SUBSET-LEMMA2 (A S)
(B G)
(C (RIGHT-COSET H (CAR S))))
(LA-LEMMA5))
(INDUCT (LAGRANGE-INDUCT G H S))))
This formula simplifies, rewriting with SUBSET-REFLEXIVITY and
SUBSET-TRANSITIVITY, and expanding the functions SUBGROUP-OP, AND, IMPLIES,
NOT, OR, SUBSET, and EQUAL, to two new goals:
Case 2. (IMPLIES
(AND
(NOT (MEMBER (CAR S) G))
(SET-STANDARD (SET-MINUS S (RIGHT-COSET H (CAR S))))
(SUBSET (SET-MINUS S (RIGHT-COSET H (CAR S)))
G)
(NOT
(EQUAL (REMAINDER (CARDINAL (SET-MINUS S (RIGHT-COSET H (CAR S))))
(CARDINAL H))
0))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SET-STANDARD H)
(NOT (LISTP S))
(SET-STANDARD S)
(OP-CLOSED H S))
(EQUAL (REMAINDER (CARDINAL S) (CARDINAL H))
0)),
which again simplifies, applying CAR-NLISTP, and expanding the functions
SET-MINUS, SET-STANDARD, SUBSET, CARDINAL, LESSP, EQUAL, NUMBERP, and
REMAINDER, to:
T.
Case 1. (IMPLIES
(AND
(OP-CLOSED H
(SET-MINUS S (RIGHT-COSET H (CAR S))))
(SET-STANDARD (SET-MINUS S (RIGHT-COSET H (CAR S))))
(SUBSET (SET-MINUS S (RIGHT-COSET H (CAR S)))
G)
(NOT
(EQUAL (REMAINDER (CARDINAL (SET-MINUS S (RIGHT-COSET H (CAR S))))
(CARDINAL H))
0))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SUBSET S G)
(NOT (LISTP S))
(SET-STANDARD H)
(SET-STANDARD S)
(OP-CLOSED H S))
(EQUAL (REMAINDER (CARDINAL S) (CARDINAL H))
0)).
However this again simplifies, applying CAR-NLISTP, SUBSET-REFLEXIVITY, and
SUBSET-TRANSITIVITY, and opening up SET-MINUS, IMPLIES, AND, MEMBER,
OP-CLOSED, SET-STANDARD, CARDINAL, LESSP, EQUAL, NUMBERP, and REMAINDER, to:
T.
Q.E.D.
[ 0.0 1.2 0.0 ]
LAGRANGE-GENERALIZED
(DEFN DIVIDES
(M N)
(EQUAL (REMAINDER N M) 0))
From the definition we can conclude that:
(OR (FALSEP (DIVIDES M N))
(TRUEP (DIVIDES M N)))
is a theorem.
[ 0.0 0.0 0.0 ]
DIVIDES
(PROVE-LEMMA SUBSET-OP-CLOSED
(REWRITE)
(IMPLIES (AND (GROUP-OP G) (SUBSET H G))
(OP-CLOSED H G))
((USE (GROUP-OP-CLOSED (X (X-8 H G))
(Y (Y-6 H G)))
(OP-CLOSED (S1 H) (S2 G)))))
This conjecture simplifies, unfolding the functions AND, IMPLIES, NOT, and
OP-CLOSED, to:
(IMPLIES (AND (NOT (MEMBER (X-8 H G) G))
(MEMBER (X-8 H G) H)
(MEMBER (Y-6 H G) G)
(NOT (MEMBER (OP (X-8 H G) (Y-6 H G)) G))
(GROUP-OP G)
(SUBSET H G))
(OP-CLOSED H G)),
which again simplifies, rewriting with SUBSET-LEMMA0, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
SUBSET-OP-CLOSED
(PROVE-LEMMA LAGRANGE NIL
(IMPLIES (AND (SUBGROUP-OP H G)
(SET-STANDARD G)
(SET-STANDARD H))
(DIVIDES (CARDINAL H) (CARDINAL G)))
((USE (LAGRANGE-GENERALIZED (S G)))))
This formula can be simplified, using the abbreviations SUBGROUP-OP, AND,
IMPLIES, and DIVIDES, to the new conjecture:
(IMPLIES (AND (IMPLIES (AND (SUBGROUP-OP H G)
(SET-STANDARD H)
(SUBSET G G)
(SET-STANDARD G)
(OP-CLOSED H G))
(EQUAL (REMAINDER (CARDINAL G) (CARDINAL H))
0))
(GROUP-OP G)
(GROUP-OP H)
(SUBSET H G)
(SET-STANDARD G)
(SET-STANDARD H))
(EQUAL (REMAINDER (CARDINAL G) (CARDINAL H))
0)),
which simplifies, rewriting with SUBSET-TRANSITIVITY, SUBSET-REFLEXIVITY, and
SUBSET-OP-CLOSED, and opening up SUBGROUP-OP, AND, and IMPLIES, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
LAGRANGE