(BOOT-STRAP NQTHM)
[ 0.1 0.1 0.0 ]
GROUND-ZERO
(CONSTRAIN AC-FN-INTRO
(REWRITE)
(AND (EQUAL (AC-FN X Y) (AC-FN Y X))
(EQUAL (AC-FN (AC-FN X Y) Z)
(AC-FN X (AC-FN Y Z))))
((AC-FN PLUS)))
WARNING: Note that the proposed lemma AC-FN-INTRO is to be stored as zero
type prescription rules, zero compound recognizer rules, zero linear rules,
and two replacement rules.
We will verify the consistency and the conservative nature of this constraint
by attempting to prove:
(AND (EQUAL (PLUS X Y) (PLUS Y X))
(EQUAL (PLUS (PLUS X Y) Z)
(PLUS X Y Z))).
This formula can be simplified, using the abbreviation AND, to the following
two new goals:
Case 2. (EQUAL (PLUS X Y) (PLUS Y X)).
This simplifies, using linear arithmetic, to:
T.
Case 1. (EQUAL (PLUS (PLUS X Y) Z)
(PLUS X Y Z)).
This simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
AC-FN-INTRO
(DEFN FOLDR
(LST ROOT)
(IF (LISTP LST)
(AC-FN (CAR LST)
(FOLDR (CDR LST) ROOT))
ROOT))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT LST) decreases according to the well-founded relation LESSP in each
recursive call. Hence, FOLDR is accepted under the definitional principle.
[ 0.0 0.0 0.0 ]
FOLDR
(DEFN REMOVE1
(A X)
(IF (LISTP X)
(IF (EQUAL A (CAR X))
(CDR X)
(CONS (CAR X) (REMOVE1 A (CDR X))))
X))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT X) decreases according to the well-founded relation LESSP in each
recursive call. Hence, REMOVE1 is accepted under the principle of definition.
[ 0.0 0.0 0.0 ]
REMOVE1
(DEFN PERMUTATION-P
(X1 X2)
(IF (LISTP X1)
(AND (MEMBER (CAR X1) X2)
(PERMUTATION-P (CDR X1)
(REMOVE1 (CAR X1) X2)))
(NLISTP X2)))
Linear arithmetic and the lemma CDR-LESSP establish that the measure
(COUNT X1) decreases according to the well-founded relation LESSP in each
recursive call. Hence, PERMUTATION-P is accepted under the definitional
principle. From the definition we can conclude that:
(OR (FALSEP (PERMUTATION-P X1 X2))
(TRUEP (PERMUTATION-P X1 X2)))
is a theorem.
[ 0.0 0.0 0.0 ]
PERMUTATION-P
(PROVE-LEMMA AC-FN-ASSOC-REVERSED
(REWRITE)
(EQUAL (AC-FN X (AC-FN Y Z))
(AC-FN (AC-FN X Y) Z)))
WARNING: the previously added lemma, AC-FN-INTRO, could be applied whenever
the newly proposed AC-FN-ASSOC-REVERSED could!
This formula can be simplified, using the abbreviation AC-FN-INTRO, to:
(EQUAL (AC-FN X (AC-FN Y Z))
(AC-FN X (AC-FN Y Z))),
which simplifies, trivially, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
AC-FN-ASSOC-REVERSED
(PROVE-LEMMA AC-FN-COMM NIL
(EQUAL (AC-FN X Z) (AC-FN Z X)))
This formula simplifies, rewriting with AC-FN-INTRO, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
AC-FN-COMM
(PROVE-LEMMA AC-FN-COMMUTATIVITY-2
(REWRITE)
(EQUAL (AC-FN Z (AC-FN X A))
(AC-FN X (AC-FN Z A)))
((DISABLE AC-FN-INTRO)
(USE (AC-FN-COMM))))
WARNING: the previously added lemma, AC-FN-ASSOC-REVERSED, could be applied
whenever the newly proposed AC-FN-COMMUTATIVITY-2 could!
WARNING: the previously added lemma, AC-FN-INTRO, could be applied whenever
the newly proposed AC-FN-COMMUTATIVITY-2 could!
This conjecture can be simplified, using the abbreviation AC-FN-ASSOC-REVERSED,
to the formula:
(IMPLIES (EQUAL (AC-FN X Z) (AC-FN Z X))
(EQUAL (AC-FN (AC-FN Z X) A)
(AC-FN (AC-FN X Z) A))).
This simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
AC-FN-COMMUTATIVITY-2
(DISABLE AC-FN-ASSOC-REVERSED)
[ 0.0 0.0 0.0 ]
AC-FN-ASSOC-REVERSED-OFF
(PROVE-LEMMA FOLDR-REMOVE1
(REWRITE)
(IMPLIES (MEMBER Z X2)
(EQUAL (AC-FN Z (FOLDR (REMOVE1 Z X2) ROOT))
(FOLDR X2 ROOT))))
WARNING: the previously added lemma, AC-FN-INTRO, could be applied whenever
the newly proposed FOLDR-REMOVE1 could!
Call the conjecture *1.
We will appeal to 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 X2) (p Z X2 ROOT))
(IMPLIES (AND (NOT (NLISTP X2))
(EQUAL Z (CAR X2)))
(p Z X2 ROOT))
(IMPLIES (AND (NOT (NLISTP X2))
(NOT (EQUAL Z (CAR X2)))
(p Z (CDR X2) ROOT))
(p Z X2 ROOT))).
Linear arithmetic, the lemmas CDR-LESSEQP and CDR-LESSP, and the definition of
NLISTP can be used to establish that the measure (COUNT X2) 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 X2) (MEMBER Z X2))
(EQUAL (AC-FN Z (FOLDR (REMOVE1 Z X2) ROOT))
(FOLDR X2 ROOT))),
which simplifies, expanding the definitions of NLISTP and MEMBER, to:
T.
Case 3. (IMPLIES (AND (NOT (NLISTP X2))
(EQUAL Z (CAR X2))
(MEMBER Z X2))
(EQUAL (AC-FN Z (FOLDR (REMOVE1 Z X2) ROOT))
(FOLDR X2 ROOT))),
which simplifies, opening up the definitions of NLISTP, MEMBER, REMOVE1, and
FOLDR, to:
T.
Case 2. (IMPLIES (AND (NOT (NLISTP X2))
(NOT (EQUAL Z (CAR X2)))
(NOT (MEMBER Z (CDR X2)))
(MEMBER Z X2))
(EQUAL (AC-FN Z (FOLDR (REMOVE1 Z X2) ROOT))
(FOLDR X2 ROOT))),
which simplifies, opening up the definitions of NLISTP and MEMBER, to:
T.
Case 1. (IMPLIES (AND (NOT (NLISTP X2))
(NOT (EQUAL Z (CAR X2)))
(EQUAL (AC-FN Z
(FOLDR (REMOVE1 Z (CDR X2)) ROOT))
(FOLDR (CDR X2) ROOT))
(MEMBER Z X2))
(EQUAL (AC-FN Z (FOLDR (REMOVE1 Z X2) ROOT))
(FOLDR X2 ROOT))),
which simplifies, rewriting with CDR-CONS and CAR-CONS, and expanding the
definitions of NLISTP, MEMBER, REMOVE1, and FOLDR, to:
(IMPLIES (AND (LISTP X2)
(NOT (EQUAL Z (CAR X2)))
(EQUAL (AC-FN Z
(FOLDR (REMOVE1 Z (CDR X2)) ROOT))
(FOLDR (CDR X2) ROOT))
(MEMBER Z (CDR X2)))
(EQUAL (AC-FN Z
(AC-FN (CAR X2)
(FOLDR (REMOVE1 Z (CDR X2)) ROOT)))
(AC-FN (CAR X2)
(FOLDR (CDR X2) ROOT)))).
Applying the lemma CAR-CDR-ELIM, replace X2 by (CONS X V) to eliminate
(CAR X2) and (CDR X2). We thus obtain the new conjecture:
(IMPLIES (AND (NOT (EQUAL Z X))
(EQUAL (AC-FN Z (FOLDR (REMOVE1 Z V) ROOT))
(FOLDR V ROOT))
(MEMBER Z V))
(EQUAL (AC-FN Z
(AC-FN X (FOLDR (REMOVE1 Z V) ROOT)))
(AC-FN X (FOLDR V ROOT)))),
which further simplifies, rewriting with the lemma AC-FN-COMMUTATIVITY-2, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
FOLDR-REMOVE1
(PROVE-LEMMA FOLDR-PERMUTATION-P
(REWRITE)
(IMPLIES (PERMUTATION-P X1 X2)
(EQUAL (FOLDR X1 ROOT)
(FOLDR X2 ROOT))))
WARNING: Note that FOLDR-PERMUTATION-P contains the free variable X2 which
will be chosen by instantiating the hypothesis (PERMUTATION-P X1 X2).
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 X1)
(p (CDR X1)
ROOT
(REMOVE1 (CAR X1) X2)))
(p X1 ROOT X2))
(IMPLIES (NOT (LISTP X1))
(p X1 ROOT X2))).
Linear arithmetic and the lemma CDR-LESSP can be used to prove that the
measure (COUNT X1) decreases according to the well-founded relation LESSP in
each induction step of the scheme. Note, however, the inductive instance
chosen for X2. The above induction scheme leads to three new goals:
Case 3. (IMPLIES (AND (LISTP X1)
(NOT (PERMUTATION-P (CDR X1)
(REMOVE1 (CAR X1) X2)))
(PERMUTATION-P X1 X2))
(EQUAL (FOLDR X1 ROOT)
(FOLDR X2 ROOT))),
which simplifies, opening up the definition of PERMUTATION-P, to:
T.
Case 2. (IMPLIES (AND (LISTP X1)
(EQUAL (FOLDR (CDR X1) ROOT)
(FOLDR (REMOVE1 (CAR X1) X2) ROOT))
(PERMUTATION-P X1 X2))
(EQUAL (FOLDR X1 ROOT)
(FOLDR X2 ROOT))),
which simplifies, expanding PERMUTATION-P and FOLDR, to:
(IMPLIES (AND (LISTP X1)
(EQUAL (FOLDR (CDR X1) ROOT)
(FOLDR (REMOVE1 (CAR X1) X2) ROOT))
(MEMBER (CAR X1) X2)
(PERMUTATION-P (CDR X1)
(REMOVE1 (CAR X1) X2)))
(EQUAL (AC-FN (CAR X1) (FOLDR (CDR X1) ROOT))
(FOLDR X2 ROOT))).
Appealing to the lemma CAR-CDR-ELIM, we now replace X1 by (CONS Z X) to
eliminate (CDR X1) and (CAR X1). The result is the formula:
(IMPLIES (AND (EQUAL (FOLDR X ROOT)
(FOLDR (REMOVE1 Z X2) ROOT))
(MEMBER Z X2)
(PERMUTATION-P X (REMOVE1 Z X2)))
(EQUAL (AC-FN Z (FOLDR X ROOT))
(FOLDR X2 ROOT))).
We use the above equality hypothesis by substituting:
(FOLDR (REMOVE1 Z X2) ROOT)
for (FOLDR X ROOT) and throwing away the equality. We thus obtain:
(IMPLIES (AND (MEMBER Z X2)
(PERMUTATION-P X (REMOVE1 Z X2)))
(EQUAL (AC-FN Z (FOLDR (REMOVE1 Z X2) ROOT))
(FOLDR X2 ROOT))),
which further simplifies, applying FOLDR-REMOVE1, to:
T.
Case 1. (IMPLIES (AND (NOT (LISTP X1))
(PERMUTATION-P X1 X2))
(EQUAL (FOLDR X1 ROOT)
(FOLDR X2 ROOT))).
This simplifies, expanding the functions PERMUTATION-P and FOLDR, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
FOLDR-PERMUTATION-P
(DEFN SUMLIST
(LST)
(IF (LISTP LST)
(PLUS (CAR LST) (SUMLIST (CDR LST)))
0))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT LST) decreases according to the well-founded relation LESSP in each
recursive call. Hence, SUMLIST is accepted under the definitional principle.
From the definition we can conclude that (NUMBERP (SUMLIST LST)) is a theorem.
[ 0.0 0.0 0.0 ]
SUMLIST
(FUNCTIONALLY-INSTANTIATE SUMLIST-PERMUTATION-P-LEMMA NIL *AUTO*
FOLDR-PERMUTATION-P
((AC-FN PLUS)
(FOLDR (LAMBDA (LST ROOT)
(IF (LISTP LST)
(PLUS ROOT (SUMLIST LST))
ROOT)))))
The functional instantiation of FOLDR-PERMUTATION-P under:
((AC-FN PLUS)
(FOLDR (LAMBDA (LST ROOT)
(IF (LISTP LST)
(PLUS ROOT (SUMLIST LST))
ROOT))))
requires us to prove:
(AND (EQUAL (IF (LISTP LST)
(PLUS ROOT (SUMLIST LST))
ROOT)
(IF (LISTP LST)
(PLUS (CAR LST)
(IF (LISTP (CDR LST))
(PLUS ROOT (SUMLIST (CDR LST)))
ROOT))
ROOT))
(EQUAL (PLUS X Y) (PLUS Y X))
(EQUAL (PLUS (PLUS X Y) Z)
(PLUS X Y Z))).
This conjecture can be simplified, using the abbreviation AND, to three new
formulas:
Case 3. (EQUAL (IF (LISTP LST)
(PLUS ROOT (SUMLIST LST))
ROOT)
(IF (LISTP LST)
(PLUS (CAR LST)
(IF (LISTP (CDR LST))
(PLUS ROOT (SUMLIST (CDR LST)))
ROOT))
ROOT)),
which simplifies, unfolding the function SUMLIST, to two new formulas:
Case 3.2.
(IMPLIES (AND (LISTP LST) (LISTP (CDR LST)))
(EQUAL (PLUS ROOT
(CAR LST)
(SUMLIST (CDR LST)))
(PLUS (CAR LST)
ROOT
(SUMLIST (CDR LST))))),
which again simplifies, using linear arithmetic, to:
T.
Case 3.1.
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST))))
(EQUAL (PLUS ROOT
(CAR LST)
(SUMLIST (CDR LST)))
(PLUS (CAR LST) ROOT))),
which again simplifies, unfolding the definition of SUMLIST, to the
formula:
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST))))
(EQUAL (PLUS ROOT (CAR LST) 0)
(PLUS (CAR LST) ROOT))).
However this again simplifies, using linear arithmetic, to:
T.
Case 2. (EQUAL (PLUS X Y) (PLUS Y X)),
which simplifies, using linear arithmetic, to:
T.
Case 1. (EQUAL (PLUS (PLUS X Y) Z)
(PLUS X Y Z)),
which simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
SUMLIST-PERMUTATION-P-LEMMA
(PROVE-LEMMA SUMLIST-PERMUTATION-P
(REWRITE)
(IMPLIES (PERMUTATION-P X1 X2)
(EQUAL (SUMLIST X1) (SUMLIST X2)))
((USE (SUMLIST-PERMUTATION-P-LEMMA (ROOT 0)))))
WARNING: Note that SUMLIST-PERMUTATION-P contains the free variable X2 which
will be chosen by instantiating the hypothesis (PERMUTATION-P X1 X2).
This conjecture simplifies, expanding the functions EQUAL, PLUS, IMPLIES,
PERMUTATION-P, SUMLIST, and MEMBER, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
SUMLIST-PERMUTATION-P
(PROVE-LEMMA TIMES-ASSOC
(REWRITE)
(EQUAL (TIMES (TIMES X Y) Z)
(TIMES X (TIMES Y Z))))
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 (ZEROP X) (p X Y Z))
(IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Y Z))
(p X Y Z))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to prove that the measure (COUNT X) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme leads to two new goals:
Case 2. (IMPLIES (ZEROP X)
(EQUAL (TIMES (TIMES X Y) Z)
(TIMES X Y Z))),
which simplifies, opening up the definitions of ZEROP, EQUAL, and TIMES, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP X))
(EQUAL (TIMES (TIMES (SUB1 X) Y) Z)
(TIMES (SUB1 X) Y Z)))
(EQUAL (TIMES (TIMES X Y) Z)
(TIMES X Y Z))),
which simplifies, expanding ZEROP and TIMES, to:
(IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL (TIMES (TIMES (SUB1 X) Y) Z)
(TIMES (SUB1 X) Y Z)))
(EQUAL (TIMES (PLUS Y (TIMES (SUB1 X) Y)) Z)
(PLUS (TIMES Y Z)
(TIMES (SUB1 X) Y Z)))).
Appealing to the lemma SUB1-ELIM, we now replace X by (ADD1 V) to eliminate
(SUB1 X). We rely upon the type restriction lemma noted when SUB1 was
introduced to constrain the new variable. This generates:
(IMPLIES (AND (NUMBERP V)
(NOT (EQUAL (ADD1 V) 0))
(EQUAL (TIMES (TIMES V Y) Z)
(TIMES V Y Z)))
(EQUAL (TIMES (PLUS Y (TIMES V Y)) Z)
(PLUS (TIMES Y Z) (TIMES V Y Z)))).
This further simplifies, trivially, to:
(IMPLIES (AND (NUMBERP V)
(EQUAL (TIMES (TIMES V Y) Z)
(TIMES V Y Z)))
(EQUAL (TIMES (PLUS Y (TIMES V Y)) Z)
(PLUS (TIMES Y Z) (TIMES V Y Z)))).
We use the above equality hypothesis by substituting (TIMES (TIMES V Y) Z)
for (TIMES V Y Z) and throwing away the equality. This generates the goal:
(IMPLIES (NUMBERP V)
(EQUAL (TIMES (PLUS Y (TIMES V Y)) Z)
(PLUS (TIMES Y Z)
(TIMES (TIMES V Y) Z)))).
We will try to prove the above formula by generalizing it, replacing
(TIMES V Y) by A. We restrict the new variable by recalling the type
restriction lemma noted when TIMES was introduced. We thus obtain:
(IMPLIES (AND (NUMBERP A) (NUMBERP V))
(EQUAL (TIMES (PLUS Y A) Z)
(PLUS (TIMES Y Z) (TIMES A Z)))),
which has an irrelevant term in it. By eliminating the term we get:
(IMPLIES (NUMBERP A)
(EQUAL (TIMES (PLUS Y A) Z)
(PLUS (TIMES Y Z) (TIMES A Z)))),
which we will finally name *1.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 (ZEROP Y) (p Y A Z))
(IMPLIES (AND (NOT (ZEROP Y)) (p (SUB1 Y) A Z))
(p Y A Z))).
Linear arithmetic, the lemmas SUB1-LESSEQP and SUB1-LESSP, and the definition
of ZEROP establish that the measure (COUNT Y) decreases according to the
well-founded relation LESSP in each induction step of the scheme. The above
induction scheme leads to the following two new formulas:
Case 2. (IMPLIES (AND (ZEROP Y) (NUMBERP A))
(EQUAL (TIMES (PLUS Y A) Z)
(PLUS (TIMES Y Z) (TIMES A Z)))).
This simplifies, unfolding ZEROP, EQUAL, PLUS, and TIMES, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP Y))
(EQUAL (TIMES (PLUS (SUB1 Y) A) Z)
(PLUS (TIMES (SUB1 Y) Z) (TIMES A Z)))
(NUMBERP A))
(EQUAL (TIMES (PLUS Y A) Z)
(PLUS (TIMES Y Z) (TIMES A Z)))).
This simplifies, applying SUB1-ADD1, and opening up the functions ZEROP,
PLUS, and TIMES, to the formula:
(IMPLIES (AND (NOT (EQUAL Y 0))
(NUMBERP Y)
(EQUAL (TIMES (PLUS (SUB1 Y) A) Z)
(PLUS (TIMES (SUB1 Y) Z) (TIMES A Z)))
(NUMBERP A))
(EQUAL (PLUS Z (TIMES (PLUS (SUB1 Y) A) Z))
(PLUS (PLUS Z (TIMES (SUB1 Y) Z))
(TIMES A Z)))).
This again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1.1, which finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
TIMES-ASSOC
(PROVE-LEMMA TIMES-1
(REWRITE)
(EQUAL (TIMES X 1) (FIX X)))
This simplifies, unfolding FIX, to two new formulas:
Case 2. (IMPLIES (NOT (NUMBERP X))
(EQUAL (TIMES X 1) 0)),
which again simplifies, unfolding TIMES and EQUAL, to:
T.
Case 1. (IMPLIES (NUMBERP X)
(EQUAL (TIMES X 1) X)),
which we will name *1.
We will appeal to induction. There is only one plausible induction. We
will induct according to the following scheme:
(AND (IMPLIES (ZEROP X) (p X))
(IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X)))
(p X))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us 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 the following two new goals:
Case 2. (IMPLIES (AND (ZEROP X) (NUMBERP X))
(EQUAL (TIMES X 1) X)).
This simplifies, opening up the definitions of ZEROP, NUMBERP, TIMES, and
EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP X))
(EQUAL (TIMES (SUB1 X) 1) (SUB1 X))
(NUMBERP X))
(EQUAL (TIMES X 1) X)).
This simplifies, expanding the definitions of ZEROP and TIMES, to:
(IMPLIES (AND (NOT (EQUAL X 0))
(EQUAL (TIMES (SUB1 X) 1) (SUB1 X))
(NUMBERP X))
(EQUAL (PLUS 1 (SUB1 X)) X)),
which again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1. Q.E.D.
[ 0.0 0.0 0.0 ]
TIMES-1
(PROVE-LEMMA TIMES-COMM
(REWRITE)
(EQUAL (TIMES X Z) (TIMES Z X)))
WARNING: the newly proposed lemma, TIMES-COMM, could be applied whenever the
previously added lemma TIMES-1 could.
WARNING: the newly proposed lemma, TIMES-COMM, could be applied whenever the
previously added lemma TIMES-ASSOC could.
Give the conjecture the name *1.
We will appeal to induction. Two inductions are suggested by terms in
the conjecture, both of which are flawed. We limit our consideration to the
two suggested by the largest number of nonprimitive recursive functions in the
conjecture. Since both of these are equally likely, we will choose
arbitrarily. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP X) (p X Z))
(IMPLIES (AND (NOT (ZEROP X)) (p (SUB1 X) Z))
(p X Z))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP inform
us that the measure (COUNT X) decreases according to the well-founded relation
LESSP in each induction step of the scheme. The above induction scheme
produces the following two new conjectures:
Case 2. (IMPLIES (ZEROP X)
(EQUAL (TIMES X Z) (TIMES Z X))).
This simplifies, expanding the functions ZEROP, EQUAL, and TIMES, to the
following two new conjectures:
Case 2.2.
(IMPLIES (EQUAL X 0)
(EQUAL 0 (TIMES Z 0))).
This again simplifies, obviously, to:
(EQUAL 0 (TIMES Z 0)),
which we will name *1.1.
Case 2.1.
(IMPLIES (NOT (NUMBERP X))
(EQUAL 0 (TIMES Z X))).
Name the above subgoal *1.2.
Case 1. (IMPLIES (AND (NOT (ZEROP X))
(EQUAL (TIMES (SUB1 X) Z)
(TIMES Z (SUB1 X))))
(EQUAL (TIMES X Z) (TIMES Z X))).
This simplifies, opening up ZEROP and TIMES, to the new conjecture:
(IMPLIES (AND (NOT (EQUAL X 0))
(NUMBERP X)
(EQUAL (TIMES (SUB1 X) Z)
(TIMES Z (SUB1 X))))
(EQUAL (PLUS Z (TIMES Z (SUB1 X)))
(TIMES Z X))).
Applying the lemma SUB1-ELIM, replace X by (ADD1 V) to eliminate (SUB1 X).
We employ the type restriction lemma noted when SUB1 was introduced to
restrict the new variable. This produces the new conjecture:
(IMPLIES (AND (NUMBERP V)
(NOT (EQUAL (ADD1 V) 0))
(EQUAL (TIMES V Z) (TIMES Z V)))
(EQUAL (PLUS Z (TIMES Z V))
(TIMES Z (ADD1 V)))),
which further simplifies, obviously, to:
(IMPLIES (AND (NUMBERP V)
(EQUAL (TIMES V Z) (TIMES Z V)))
(EQUAL (PLUS Z (TIMES V Z))
(TIMES Z (ADD1 V)))).
We now use the above equality hypothesis by substituting (TIMES Z V) for
(TIMES V Z) and throwing away the equality. This generates:
(IMPLIES (NUMBERP V)
(EQUAL (PLUS Z (TIMES Z V))
(TIMES Z (ADD1 V)))).
Name the above subgoal *1.3.
We will appeal to induction. There are three plausible inductions.
However, they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (ZEROP Z) (p Z V))
(IMPLIES (AND (NOT (ZEROP Z)) (p (SUB1 Z) V))
(p Z V))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
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 leads to the following two new formulas:
Case 2. (IMPLIES (AND (ZEROP Z) (NUMBERP V))
(EQUAL (PLUS Z (TIMES Z V))
(TIMES Z (ADD1 V)))).
This simplifies, expanding the functions ZEROP, EQUAL, TIMES, PLUS, and
NUMBERP, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP Z))
(EQUAL (PLUS (SUB1 Z) (TIMES (SUB1 Z) V))
(TIMES (SUB1 Z) (ADD1 V)))
(NUMBERP V))
(EQUAL (PLUS Z (TIMES Z V))
(TIMES Z (ADD1 V)))).
This simplifies, applying SUB1-ADD1, and opening up ZEROP, TIMES, and PLUS,
to the formula:
(IMPLIES (AND (NOT (EQUAL Z 0))
(NUMBERP Z)
(EQUAL (PLUS (SUB1 Z) (TIMES (SUB1 Z) V))
(TIMES (SUB1 Z) (ADD1 V)))
(NUMBERP V))
(EQUAL (PLUS Z V (TIMES (SUB1 Z) V))
(ADD1 (PLUS V (TIMES (SUB1 Z) (ADD1 V)))))).
This again simplifies, using linear arithmetic, to:
T.
That finishes the proof of *1.3.
So let us turn our attention to:
(IMPLIES (NOT (NUMBERP X))
(EQUAL 0 (TIMES Z X))),
named *1.2 above. We will try to prove it by induction. There is only one
suggested induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP Z) (p Z X))
(IMPLIES (AND (NOT (ZEROP Z)) (p (SUB1 Z) X))
(p Z X))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP can be
used to 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 leads to the following two new formulas:
Case 2. (IMPLIES (AND (ZEROP Z) (NOT (NUMBERP X)))
(EQUAL 0 (TIMES Z X))).
This simplifies, opening up the definitions of ZEROP, EQUAL, and TIMES, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP Z))
(EQUAL 0 (TIMES (SUB1 Z) X))
(NOT (NUMBERP X)))
(EQUAL 0 (TIMES Z X))).
This simplifies, unfolding the definitions of ZEROP, TIMES, NUMBERP, PLUS,
and EQUAL, to:
T.
That finishes the proof of *1.2.
So we now return to:
(EQUAL 0 (TIMES Z 0)),
named *1.1 above. We will appeal to induction. There is only one plausible
induction. We will induct according to the following scheme:
(AND (IMPLIES (ZEROP Z) (p Z))
(IMPLIES (AND (NOT (ZEROP Z)) (p (SUB1 Z)))
(p Z))).
Linear arithmetic, the lemma COUNT-NUMBERP, and the definition of ZEROP
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 generates the following two new formulas:
Case 2. (IMPLIES (ZEROP Z)
(EQUAL 0 (TIMES Z 0))).
This simplifies, opening up the definitions of ZEROP, TIMES, and EQUAL, to:
T.
Case 1. (IMPLIES (AND (NOT (ZEROP Z))
(EQUAL 0 (TIMES (SUB1 Z) 0)))
(EQUAL 0 (TIMES Z 0))).
This simplifies, expanding the definitions of ZEROP, TIMES, PLUS, and EQUAL,
to:
T.
That finishes the proof of *1.1, which also finishes the proof of *1.
Q.E.D.
[ 0.0 0.0 0.0 ]
TIMES-COMM
(DEFN TIMESLIST
(LST)
(IF (LISTP LST)
(TIMES (CAR LST)
(TIMESLIST (CDR LST)))
1))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT LST) decreases according to the well-founded relation LESSP in each
recursive call. Hence, TIMESLIST is accepted under the definitional principle.
From the definition we can conclude that (NUMBERP (TIMESLIST LST)) is a
theorem.
[ 0.0 0.0 0.0 ]
TIMESLIST
(FUNCTIONALLY-INSTANTIATE TIMES-COMMUTATIVITY-2
(REWRITE)
*AUTO* AC-FN-COMMUTATIVITY-2
((AC-FN TIMES)))
WARNING: the previously added lemma, TIMES-COMM, could be applied whenever
the newly proposed TIMES-COMMUTATIVITY-2 could!
The functional instantiation of AC-FN-COMMUTATIVITY-2 under ((AC-FN TIMES))
requires us to prove:
(AND (EQUAL (TIMES X Y) (TIMES Y X))
(EQUAL (TIMES (TIMES X Y) Z)
(TIMES X Y Z))).
This formula can be simplified, using the abbreviations AND and TIMES-ASSOC,
to the following two new goals:
Case 2. (EQUAL (TIMES X Y) (TIMES Y X)).
This simplifies, rewriting with TIMES-COMM, to:
T.
Case 1. (EQUAL (TIMES X Y Z) (TIMES X Y Z)),
which simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
TIMES-COMMUTATIVITY-2
(FUNCTIONALLY-INSTANTIATE TIMESLIST-PERMUTATION-P-LEMMA NIL *AUTO*
FOLDR-PERMUTATION-P
((AC-FN TIMES)
(FOLDR (LAMBDA (LST ROOT)
(IF (LISTP LST)
(TIMES ROOT (TIMESLIST LST))
ROOT)))))
The functional instantiation of FOLDR-PERMUTATION-P under:
((AC-FN TIMES)
(FOLDR (LAMBDA (LST ROOT)
(IF (LISTP LST)
(TIMES ROOT (TIMESLIST LST))
ROOT))))
requires us to prove:
(EQUAL (IF (LISTP LST)
(TIMES ROOT (TIMESLIST LST))
ROOT)
(IF (LISTP LST)
(TIMES (CAR LST)
(IF (LISTP (CDR LST))
(TIMES ROOT (TIMESLIST (CDR LST)))
ROOT))
ROOT)).
Note that we are using the following earlier FUNCTIONALLY-INSTANTIATE
event in order to satisfy part of the proof obligation: TIMES-COMMUTATIVITY-2.
This simplifies, expanding TIMESLIST, to two new formulas:
Case 2. (IMPLIES (AND (LISTP LST) (LISTP (CDR LST)))
(EQUAL (TIMES ROOT
(CAR LST)
(TIMESLIST (CDR LST)))
(TIMES (CAR LST)
ROOT
(TIMESLIST (CDR LST))))),
which again simplifies, applying TIMES-COMMUTATIVITY-2, to:
T.
Case 1. (IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST))))
(EQUAL (TIMES ROOT
(CAR LST)
(TIMESLIST (CDR LST)))
(TIMES (CAR LST) ROOT))).
However this again simplifies, rewriting with the lemmas TIMES-COMM and
TIMES-COMMUTATIVITY-2, and opening up TIMESLIST, to the conjecture:
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST))))
(EQUAL (TIMES 1 ROOT (CAR LST))
(TIMES ROOT (CAR LST)))).
But this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
TIMESLIST-PERMUTATION-P-LEMMA
(PROVE-LEMMA TIMESLIST-PERMUTATION-P
(REWRITE)
(IMPLIES (PERMUTATION-P X1 X2)
(EQUAL (TIMESLIST X1) (TIMESLIST X2)))
((USE (TIMESLIST-PERMUTATION-P-LEMMA (ROOT 1)))))
WARNING: Note that TIMESLIST-PERMUTATION-P contains the free variable X2
which will be chosen by instantiating the hypothesis (PERMUTATION-P X1 X2).
This conjecture simplifies, expanding the functions IMPLIES, PERMUTATION-P,
TIMESLIST, EQUAL, and MEMBER, to:
(IMPLIES (AND (LISTP X2)
(LISTP X1)
(EQUAL (TIMES 1 (TIMESLIST X1))
(TIMES 1 (TIMESLIST X2)))
(PERMUTATION-P X1 X2))
(EQUAL (TIMESLIST X1)
(TIMESLIST X2))).
However this again simplifies, using linear arithmetic, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
TIMESLIST-PERMUTATION-P
(DEFN OR2
(A B)
(IF (EQUAL A 'Z)
B
(IF (EQUAL B 'Z) A 'X)))
Observe that:
(OR (LITATOM (OR2 A B))
(EQUAL (OR2 A B) A)
(EQUAL (OR2 A B) B))
is a theorem.
[ 0.0 0.0 0.0 ]
OR2
(DEFN WIRED-OR
(LST)
(IF (LISTP LST)
(OR2 (CAR LST) (WIRED-OR (CDR LST)))
'Z))
Linear arithmetic and the lemma CDR-LESSP inform us that the measure
(COUNT LST) decreases according to the well-founded relation LESSP in each
recursive call. Hence, WIRED-OR is accepted under the definitional principle.
[ 0.0 0.0 0.0 ]
WIRED-OR
(FUNCTIONALLY-INSTANTIATE WIRED-OR-PERMUTATION-P-LEMMA NIL *AUTO*
FOLDR-PERMUTATION-P
((AC-FN OR2)
(FOLDR (LAMBDA (LST ROOT)
(IF (LISTP LST)
(OR2 ROOT (WIRED-OR LST))
ROOT)))))
The functional instantiation of FOLDR-PERMUTATION-P under:
((AC-FN OR2)
(FOLDR (LAMBDA (LST ROOT)
(IF (LISTP LST)
(OR2 ROOT (WIRED-OR LST))
ROOT))))
requires us to prove:
(AND (EQUAL (IF (LISTP LST)
(OR2 ROOT (WIRED-OR LST))
ROOT)
(IF (LISTP LST)
(OR2 (CAR LST)
(IF (LISTP (CDR LST))
(OR2 ROOT (WIRED-OR (CDR LST)))
ROOT))
ROOT))
(EQUAL (OR2 X Y) (OR2 Y X))
(EQUAL (OR2 (OR2 X Y) Z)
(OR2 X (OR2 Y Z)))).
This conjecture can be simplified, using the abbreviation AND, to three new
formulas:
Case 3. (EQUAL (IF (LISTP LST)
(OR2 ROOT (WIRED-OR LST))
ROOT)
(IF (LISTP LST)
(OR2 (CAR LST)
(IF (LISTP (CDR LST))
(OR2 ROOT (WIRED-OR (CDR LST)))
ROOT))
ROOT)),
which simplifies, unfolding the functions OR2 and WIRED-OR, to ten new
formulas:
Case 3.10.
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(EQUAL (CAR LST) 'Z))
(EQUAL (OR2 ROOT (WIRED-OR (CDR LST)))
(OR2 (CAR LST) ROOT))),
which again simplifies, unfolding the definitions of WIRED-OR, EQUAL, and
OR2, to:
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(EQUAL (CAR LST) 'Z)
(EQUAL ROOT 'Z))
(EQUAL 'Z ROOT)).
This again simplifies, obviously, to:
T.
Case 3.9.
(IMPLIES (AND (LISTP LST)
(NOT (EQUAL ROOT 'Z))
(EQUAL (WIRED-OR (CDR LST)) 'Z)
(EQUAL (CAR LST) 'Z))
(EQUAL (OR2 ROOT (WIRED-OR (CDR LST)))
(OR2 (CAR LST) ROOT))).
However this again simplifies, unfolding the definitions of EQUAL and OR2,
to:
T.
Case 3.8.
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(NOT (EQUAL (CAR LST) 'Z))
(EQUAL (WIRED-OR (CDR LST)) 'Z))
(EQUAL (OR2 ROOT (CAR LST))
(OR2 (CAR LST) ROOT))),
which again simplifies, expanding the definitions of WIRED-OR, EQUAL, and
OR2, to:
T.
Case 3.7.
(IMPLIES (AND (LISTP LST)
(NOT (EQUAL ROOT 'Z))
(EQUAL (WIRED-OR (CDR LST)) 'Z)
(NOT (EQUAL (CAR LST) 'Z)))
(EQUAL (OR2 ROOT (CAR LST))
(OR2 (CAR LST) ROOT))),
which again simplifies, opening up the functions OR2 and EQUAL, to:
T.
Case 3.6.
(IMPLIES (AND (LISTP LST)
(LISTP (CDR LST))
(NOT (EQUAL ROOT 'Z))
(NOT (EQUAL (WIRED-OR (CDR LST)) 'Z))
(EQUAL (CAR LST) 'Z))
(EQUAL (OR2 ROOT (WIRED-OR (CDR LST)))
(OR2 (CAR LST) 'X))),
which again simplifies, expanding OR2 and EQUAL, to:
T.
Case 3.5.
(IMPLIES (AND (LISTP LST)
(LISTP (CDR LST))
(NOT (EQUAL ROOT 'Z))
(NOT (EQUAL (WIRED-OR (CDR LST)) 'Z))
(NOT (EQUAL (CAR LST) 'Z)))
(EQUAL (OR2 ROOT 'X)
(OR2 (CAR LST) 'X))),
which again simplifies, opening up EQUAL and OR2, to:
T.
Case 3.4.
(IMPLIES (AND (LISTP LST)
(LISTP (CDR LST))
(EQUAL ROOT 'Z)
(EQUAL (CAR LST) 'Z))
(EQUAL (OR2 ROOT (WIRED-OR (CDR LST)))
(OR2 (CAR LST)
(WIRED-OR (CDR LST))))),
which again simplifies, clearly, to:
T.
Case 3.3.
(IMPLIES (AND (LISTP LST)
(LISTP (CDR LST))
(EQUAL ROOT 'Z)
(NOT (EQUAL (CAR LST) 'Z))
(NOT (EQUAL (WIRED-OR (CDR LST)) 'Z)))
(EQUAL (OR2 ROOT 'X)
(OR2 (CAR LST)
(WIRED-OR (CDR LST))))).
This again simplifies, expanding the functions OR2 and EQUAL, to:
T.
Case 3.2.
(IMPLIES (AND (LISTP LST)
(LISTP (CDR LST))
(EQUAL ROOT 'Z)
(NOT (EQUAL (CAR LST) 'Z))
(EQUAL (WIRED-OR (CDR LST)) 'Z))
(EQUAL (OR2 ROOT (CAR LST))
(OR2 (CAR LST)
(WIRED-OR (CDR LST))))),
which again simplifies, expanding the functions EQUAL and OR2, to:
T.
Case 3.1.
(IMPLIES (AND (LISTP LST)
(NOT (LISTP (CDR LST)))
(NOT (EQUAL (CAR LST) 'Z))
(NOT (EQUAL (WIRED-OR (CDR LST)) 'Z)))
(EQUAL (OR2 ROOT 'X)
(OR2 (CAR LST) ROOT))),
which again simplifies, unfolding the definitions of WIRED-OR and EQUAL,
to:
T.
Case 2. (EQUAL (OR2 X Y) (OR2 Y X)),
which simplifies, expanding the function OR2, to:
(IMPLIES (AND (EQUAL Y 'Z) (EQUAL X 'Z))
(EQUAL Y X)).
This again simplifies, clearly, to:
T.
Case 1. (EQUAL (OR2 (OR2 X Y) Z)
(OR2 X (OR2 Y Z))).
This simplifies, unfolding the function OR2, to the following five new
conjectures:
Case 1.5.
(IMPLIES (AND (NOT (EQUAL Y 'Z))
(EQUAL Z 'Z)
(NOT (EQUAL X 'Z)))
(EQUAL (OR2 'X Z) (OR2 X Y))).
This again simplifies, unfolding the definitions of OR2 and EQUAL, to:
T.
Case 1.4.
(IMPLIES (AND (NOT (EQUAL Y 'Z))
(EQUAL Z 'Z)
(EQUAL X 'Z))
(EQUAL (OR2 Y Z) (OR2 X Y))),
which again simplifies, unfolding the functions EQUAL and OR2, to:
T.
Case 1.3.
(IMPLIES (AND (NOT (EQUAL Y 'Z))
(NOT (EQUAL Z 'Z))
(NOT (EQUAL X 'Z)))
(EQUAL (OR2 'X Z) (OR2 X 'X))),
which again simplifies, opening up EQUAL and OR2, to:
T.
Case 1.2.
(IMPLIES (AND (NOT (EQUAL Y 'Z))
(NOT (EQUAL Z 'Z))
(EQUAL X 'Z))
(EQUAL (OR2 Y Z) (OR2 X 'X))),
which again simplifies, expanding the definitions of OR2 and EQUAL, to:
T.
Case 1.1.
(IMPLIES (AND (EQUAL Y 'Z) (EQUAL X 'Z))
(EQUAL (OR2 Y Z) (OR2 X Z))),
which again simplifies, clearly, to:
T.
Q.E.D.
[ 0.0 0.1 0.0 ]
WIRED-OR-PERMUTATION-P-LEMMA
(PROVE-LEMMA WIRED-OR-PERMUTATION-P
(REWRITE)
(IMPLIES (PERMUTATION-P X1 X2)
(EQUAL (WIRED-OR X1) (WIRED-OR X2)))
((USE (WIRED-OR-PERMUTATION-P-LEMMA (ROOT 'Z)))))
WARNING: Note that WIRED-OR-PERMUTATION-P contains the free variable X2 which
will be chosen by instantiating the hypothesis (PERMUTATION-P X1 X2).
This conjecture simplifies, expanding the functions EQUAL, OR2, IMPLIES,
PERMUTATION-P, WIRED-OR, and MEMBER, to:
T.
Q.E.D.
[ 0.0 0.0 0.0 ]
WIRED-OR-PERMUTATION-P