(49) Induction-Processor (SOUND transformation)
This DP could be deleted by the Induction-Processor:IF2(
true,
s(
z0'),
s(
z1')) →
DIV(
if(
gt(
z0',
z1'),
z0',
s(
z1')),
s(
z1'))
This order was computed:Polynomial interpretation [POLO]:
POL(0) = 0
POL(DIV(x1, x2)) = x1
POL(IF1(x1, x2, x3)) = x2
POL(IF2(x1, x2, x3)) = x2
POL(false) = 1
POL(ge(x1, x2)) = 1 + x1 + x2
POL(gt(x1, x2)) = 1
POL(if(x1, x2, x3)) = x1 + x2
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
POL(true) = 1
At least one of these decreasing rules is always used after the deleted DP:if(
false,
x683,
y503) →
0The following formula is valid:z0':sort[a23],z1':sort[a23].
if'(
gt(
z0' ,
z1' ),
z0' ,
s(
z1' ))=
trueThe transformed set:minus'(
s(
x41),
y29) →
if'(
gt(
s(
x41),
y29),
x41,
y29)
if'(
true,
x59,
y43) →
minus'(
x59,
y43)
if'(
false,
x68,
y50) →
trueminus'(
0,
x1) →
falsegt(
0,
y) →
falsegt(
s(
x5),
0) →
truege(
x14,
0) →
truege(
0,
s(
x23)) →
falsege(
s(
x32),
s(
y22)) →
ge(
x32,
y22)
minus(
s(
x41),
y29) →
if(
gt(
s(
x41),
y29),
x41,
y29)
gt(
s(
x50),
s(
y36)) →
gt(
x50,
y36)
if(
true,
x59,
y43) →
s(
minus(
x59,
y43))
if(
false,
x68,
y50) →
0minus(
0,
x1) →
0equal_bool(
true,
false) →
falseequal_bool(
false,
true) →
falseequal_bool(
true,
true) →
trueequal_bool(
false,
false) →
trueand(
true,
x) →
xand(
false,
x) →
falseor(
true,
x) →
trueor(
false,
x) →
xnot(
false) →
truenot(
true) →
falseisa_true(
true) →
trueisa_true(
false) →
falseisa_false(
true) →
falseisa_false(
false) →
trueequal_sort[a23](
0,
0) →
trueequal_sort[a23](
0,
s(
x0)) →
falseequal_sort[a23](
s(
x0),
0) →
falseequal_sort[a23](
s(
x0),
s(
x1)) →
equal_sort[a23](
x0,
x1)
equal_sort[a40](
witness_sort[a40],
witness_sort[a40]) →
trueThe proof given by the theorem prover:The following input was given to ACL2:
(set-ruler-extenders :all)
(defun trs_isbool (x)
(or
(and
(consp
x
)
(eq
'trs_true
(car
x
)
)
(eq
(cdr
x
)
'nil
)
)
(and
(consp
x
)
(eq
'trs_false
(car
x
)
)
(eq
(cdr
x
)
'nil
)
)
)
)
(defun trs_issort[a23] (x)
(or
(and
(consp
x
)
(eq
'trs_0
(car
x
)
)
(eq
(cdr
x
)
'nil
)
)
(and
(consp
x
)
(consp
(cdr
x
)
)
(eq
'trs_s
(car
x
)
)
(trs_issort[a23]
(car
(cdr
x
)
)
)
(eq
(cdr
(cdr
x
)
)
'nil
)
)
)
)
(defun trs_issort[a40] (x)
(or
(and
(consp
x
)
(eq
'trs_witness_sort[a40]
(car
x
)
)
(eq
(cdr
x
)
'nil
)
)
)
)
(defun trs_ge (x0 x1)
(if
(and
(trs_issort[a23]
x0
)
(trs_issort[a23]
x1
)
)
(if
(and
(eq
(car
x1
)
'trs_0
)
)
(list 'trs_true
)
(if
(and
(eq
(car
x0
)
'trs_0
)
(eq
(car
x1
)
'trs_s
)
)
(list 'trs_false
)
(if
(and
)
(trs_ge
(car
(cdr
x0
)
)
(car
(cdr
x1
)
)
)
(list 'trs_true
)
)
)
)
(list 'trs_true
)
)
)
(defun trs_gt (x0 x1)
(if
(and
(trs_issort[a23]
x0
)
(trs_issort[a23]
x1
)
)
(if
(and
(eq
(car
x0
)
'trs_0
)
)
(list 'trs_false
)
(if
(and
(eq
(car
x0
)
'trs_s
)
(eq
(car
x1
)
'trs_0
)
)
(list 'trs_true
)
(if
(and
)
(trs_gt
(car
(cdr
x0
)
)
(car
(cdr
x1
)
)
)
(list 'trs_true
)
)
)
)
(list 'trs_true
)
)
)
(defun trs_equal_sort[a40] (x0 x1)
(if
(and
(trs_issort[a40]
x0
)
(trs_issort[a40]
x1
)
)
(if
(and
)
(list 'trs_true
)
(list 'trs_true
)
)
(list 'trs_true
)
)
)
(defun trs_equal_sort[a23] (x0 x1)
(if
(and
(trs_issort[a23]
x0
)
(trs_issort[a23]
x1
)
)
(if
(and
(eq
(car
x0
)
'trs_0
)
(eq
(car
x1
)
'trs_0
)
)
(list 'trs_true
)
(if
(and
(eq
(car
x0
)
'trs_0
)
(eq
(car
x1
)
'trs_s
)
)
(list 'trs_false
)
(if
(and
(eq
(car
x0
)
'trs_s
)
(eq
(car
x1
)
'trs_0
)
)
(list 'trs_false
)
(if
(and
)
(trs_equal_sort[a23]
(car
(cdr
x0
)
)
(car
(cdr
x1
)
)
)
(list 'trs_true
)
)
)
)
)
(list 'trs_true
)
)
)
(defun trs_isa_false (x0)
(if
(and
(trs_isbool
x0
)
)
(if
(and
(eq
(car
x0
)
'trs_true
)
)
(list 'trs_false
)
(if
(and
)
(list 'trs_true
)
(list 'trs_true
)
)
)
(list 'trs_true
)
)
)
(defun trs_isa_true (x0)
(if
(and
(trs_isbool
x0
)
)
(if
(and
(eq
(car
x0
)
'trs_true
)
)
(list 'trs_true
)
(if
(and
)
(list 'trs_false
)
(list 'trs_true
)
)
)
(list 'trs_true
)
)
)
(defun trs_not (x0)
(if
(and
(trs_isbool
x0
)
)
(if
(and
(eq
(car
x0
)
'trs_false
)
)
(list 'trs_true
)
(if
(and
)
(list 'trs_false
)
(list 'trs_true
)
)
)
(list 'trs_true
)
)
)
(defun trs_or (x0 x1)
(if
(and
(trs_isbool
x0
)
(trs_isbool
x1
)
)
(if
(and
(eq
(car
x0
)
'trs_true
)
)
(list 'trs_true
)
(if
(and
)
x1
(list 'trs_true
)
)
)
(list 'trs_true
)
)
)
(defun trs_and (x0 x1)
(if
(and
(trs_isbool
x0
)
(trs_isbool
x1
)
)
(if
(and
(eq
(car
x0
)
'trs_true
)
)
x1
(if
(and
)
(list 'trs_false
)
(list 'trs_true
)
)
)
(list 'trs_true
)
)
)
(defun trs_equal_bool (x0 x1)
(if
(and
(trs_isbool
x0
)
(trs_isbool
x1
)
)
(if
(and
(eq
(car
x0
)
'trs_true
)
(eq
(car
x1
)
'trs_false
)
)
(list 'trs_false
)
(if
(and
(eq
(car
x0
)
'trs_false
)
(eq
(car
x1
)
'trs_true
)
)
(list 'trs_false
)
(if
(and
(eq
(car
x0
)
'trs_true
)
(eq
(car
x1
)
'trs_true
)
)
(list 'trs_true
)
(if
(and
)
(list 'trs_true
)
(list 'trs_true
)
)
)
)
)
(list 'trs_true
)
)
)
(defun trs_if (x0 x1 x2)
(if
(and
(trs_isbool
x0
)
(trs_issort[a23]
x1
)
(trs_issort[a23]
x2
)
)
(if
(and
(eq
(car
x0
)
'trs_false
)
)
(list 'trs_0
)
(if
(and
(eq
(car
x0
)
'trs_true
)
(eq
(car
x1
)
'trs_s
)
)
(list 'trs_s
(trs_if
(trs_gt
(list 'trs_s
(car
(cdr
x1
)
)
)
x2
)
(car
(cdr
x1
)
)
x2
)
)
(if
(and
)
(list 'trs_s
(list 'trs_0
)
)
(list 'trs_0
)
)
)
)
(list 'trs_0
)
)
)
(defun trs_ifprime (x0 x1 x2)
(if
(and
(trs_isbool
x0
)
(trs_issort[a23]
x1
)
(trs_issort[a23]
x2
)
)
(if
(and
(eq
(car
x0
)
'trs_false
)
)
(list 'trs_true
)
(if
(and
(eq
(car
x0
)
'trs_true
)
(eq
(car
x1
)
'trs_s
)
)
(trs_ifprime
(trs_gt
(list 'trs_s
(car
(cdr
x1
)
)
)
x2
)
(car
(cdr
x1
)
)
x2
)
(if
(and
)
(list 'trs_false
)
(list 'trs_true
)
)
)
)
(list 'trs_true
)
)
)
(defun trs_minus (x0 x1)
(if
(and
(trs_issort[a23]
x0
)
(trs_issort[a23]
x1
)
)
(if
(and
(eq
(car
x0
)
'trs_0
)
)
(list 'trs_0
)
(if
(and
(eq
(car
x0
)
'trs_s
)
(eq
(trs_equal_bool
(trs_gt
(list 'trs_s
(car
(cdr
x0
)
)
)
x1
)
(list 'trs_true
)
)
(list 'trs_true
)
)
)
(list 'trs_s
(trs_minus
(car
(cdr
x0
)
)
x1
)
)
(if
(and
(eq
(trs_equal_bool
(trs_gt
(list 'trs_s
(car
(cdr
x0
)
)
)
x1
)
(list 'trs_true
)
)
(list 'trs_false
)
)
)
(list 'trs_0
)
(list 'trs_0
)
)
)
)
(list 'trs_0
)
)
)
(defun trs_minusprime (x0 x1)
(if
(and
(trs_issort[a23]
x0
)
(trs_issort[a23]
x1
)
)
(if
(and
(eq
(car
x0
)
'trs_0
)
)
(list 'trs_false
)
(if
(and
(eq
(car
x0
)
'trs_s
)
(eq
(trs_equal_bool
(trs_gt
(list 'trs_s
(car
(cdr
x0
)
)
)
x1
)
(list 'trs_true
)
)
(list 'trs_true
)
)
)
(trs_minusprime
(car
(cdr
x0
)
)
x1
)
(if
(and
(eq
(trs_equal_bool
(trs_gt
(list 'trs_s
(car
(cdr
x0
)
)
)
x1
)
(list 'trs_true
)
)
(list 'trs_false
)
)
)
(list 'trs_true
)
(list 'trs_true
)
)
)
)
(list 'trs_true
)
)
)
(with-prover-time-limit 3
(defthm test
(implies
(and
(trs_issort[a23] trs_z0prime)
(trs_issort[a23] trs_z1prime)
)
(eq
(trs_ifprime
(trs_gt
trs_z0prime
trs_z1prime
)
trs_z0prime
(list 'trs_s
trs_z1prime
)
)
(list 'trs_true
)
)
)
)
)The following output was given by ACL2:
This is SBCL 1.0.29.11.debian, an implementation of ANSI Common Lisp.
More information about SBCL is available at .
SBCL is free software, provided as is, with absolutely no warranty.
It is mostly in the public domain; some portions are provided under
BSD-style licenses. See the CREDITS and COPYING files in the
distribution for more information.
ACL2 Version 3.6 built February 12, 2010 14:59:57.
Copyright (C) 2009 University of Texas at Austin
ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you
are welcome to redistribute it under certain conditions. For details,
see the GNU General Public License.
Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*).
See the documentation topic note-3-6 for recent changes.
Note: We have modified the prompt in some underlying Lisps to further
distinguish it from the ACL2 prompt.
ACL2 Version 3.6. Level 1. Cbd "/home/petersk/workspace/benchmark/".
Distributed books directory "/home/petersk/download/acl2-sources/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.
ACL2 !> :ALL
ACL2 !>
Since TRS_ISBOOL is non-recursive, its admission is trivial. We observe
that the type of TRS_ISBOOL is described by the theorem
(OR (EQUAL (TRS_ISBOOL X) T) (EQUAL (TRS_ISBOOL X) NIL)). We used
the :executable-counterpart of EQUAL and primitive type reasoning.
Summary
Form: ( DEFUN TRS_ISBOOL ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TRS_ISBOOL
ACL2 !>
For the admission of TRS_ISSORT[A23] we will use the relation O< (which
is known to be well-founded on the domain recognized by O-P) and the
measure (ACL2-COUNT X). The non-trivial part of the measure conjecture
is
Goal
(IMPLIES (AND (NOT (AND (CONSP X)
(EQ 'TRS_0 (CAR X))
(EQ (CDR X) NIL)))
(CONSP X)
(CONSP (CDR X))
(EQ 'TRS_S (CAR X)))
(O< (ACL2-COUNT (CADR X))
(ACL2-COUNT X))).
By the simple :definition EQ we reduce the conjecture to
Goal'
(IMPLIES (AND (NOT (AND (CONSP X)
(EQUAL 'TRS_0 (CAR X))
(EQUAL (CDR X) NIL)))
(CONSP X)
(CONSP (CDR X))
(EQUAL 'TRS_S (CAR X)))
(O< (ACL2-COUNT (CADR X))
(ACL2-COUNT X))).
This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP and
O<, the :executable-counterparts of ACL2-COUNT and EQUAL, primitive
type reasoning, the :rewrite rule UNICITY-OF-0 and the :type-prescription
rule ACL2-COUNT, to
Goal''
(IMPLIES (AND (CONSP X)
(CONSP (CDR X))
(EQUAL 'TRS_S (CAR X)))
(< (ACL2-COUNT (CADR X))
(+ 1 (ACL2-COUNT (CDR X))))).
The destructor terms (CAR X) and (CDR X) can be eliminated. Furthermore,
those terms are at the root of a chain of two rounds of destructor
elimination. (1) Use CAR-CDR-ELIM to replace X by (CONS X1 X2), (CAR X)
by X1 and (CDR X) by X2 and restrict the type of the new variable X1
to be that of the term it replaces. (2) Use CAR-CDR-ELIM, again, to
replace X2 by (CONS X3 X4), (CAR X2) by X3 and (CDR X2) by X4. These
steps produce the following goal.
Goal'''
(IMPLIES (AND (CONSP (CONS X3 X4))
(SYMBOLP X1)
(NOT (EQUAL X1 T))
(NOT (EQUAL X1 NIL))
(CONSP (LIST* X1 X3 X4))
(EQUAL 'TRS_S X1))
(< (ACL2-COUNT X3)
(+ 1 (ACL2-COUNT (CONS X3 X4))))).
By case analysis we reduce the conjecture to
Goal'4'
(IMPLIES (AND (CONSP (CONS X3 X4))
(SYMBOLP X1)
(NOT (EQUAL X1 T))
X1 (CONSP (LIST* X1 X3 X4))
(EQUAL 'TRS_S X1))
(< (ACL2-COUNT X3)
(+ 1 (ACL2-COUNT (CONS X3 X4))))).
This simplifies, using the :definition ACL2-COUNT, the :executable-
counterparts of EQUAL, NOT and SYMBOLP, primitive type reasoning and
the :rewrite rules CAR-CONS and CDR-CONS, to
Goal'5'
(< (ACL2-COUNT X3)
(+ 1 1 (ACL2-COUNT X3)
(ACL2-COUNT X4))).
But simplification reduces this to T, using linear arithmetic, primitive
type reasoning and the :type-prescription rule ACL2-COUNT.
Q.E.D.
That completes the proof of the measure theorem for TRS_ISSORT[A23].
Thus, we admit this function under the principle of definition. We
observe that the type of TRS_ISSORT[A23] is described by the theorem
(OR (EQUAL (TRS_ISSORT[A23] X) T) (EQUAL (TRS_ISSORT[A23] X) NIL)).
We used the :executable-counterpart of EQUAL and primitive type reasoning.
Summary
Form: ( DEFUN TRS_ISSORT[A23] ...)
Rules: ((:DEFINITION ACL2-COUNT)
(:DEFINITION EQ)
(:DEFINITION FIX)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O<)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART ACL2-COUNT)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART SYMBOLP)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION ACL2-COUNT))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
TRS_ISSORT[A23]
ACL2 !>
Since TRS_ISSORT[A40] is non-recursive, its admission is trivial.
We observe that the type of TRS_ISSORT[A40] is described by the theorem
(OR (EQUAL (TRS_ISSORT[A40] X) T) (EQUAL (TRS_ISSORT[A40] X) NIL)).
We used primitive type reasoning.
Summary
Form: ( DEFUN TRS_ISSORT[A40] ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TRS_ISSORT[A40]
ACL2 !>
For the admission of TRS_GE we will use the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X0). The non-trivial part of the measure conjecture is
Goal
(IMPLIES (AND (AND (TRS_ISSORT[A23] X0)
(TRS_ISSORT[A23] X1))
(NOT (EQ (CAR X1) 'TRS_0))
(NOT (AND (EQ (CAR X0) 'TRS_0)
(EQ (CAR X1) 'TRS_S)))
T)
(O< (ACL2-COUNT (CADR X0))
(ACL2-COUNT X0))).
By the simple :definition EQ we reduce the conjecture to
Goal'
(IMPLIES (AND (TRS_ISSORT[A23] X0)
(TRS_ISSORT[A23] X1)
(NOT (EQUAL (CAR X1) 'TRS_0))
(NOT (AND (EQUAL (CAR X0) 'TRS_0)
(EQUAL (CAR X1) 'TRS_S))))
(O< (ACL2-COUNT (CADR X0))
(ACL2-COUNT X0))).
This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O<
and TRS_ISSORT[A23], the :executable-counterparts of ACL2-COUNT and
EQUAL, primitive type reasoning, the :rewrite rules COMMUTATIVITY-OF-+
and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to
Goal''
(IMPLIES (AND (CONSP X0)
(CONSP (CDR X0))
(EQUAL 'TRS_S (CAR X0))
(TRS_ISSORT[A23] (CADR X0))
(NOT (CDDR X0))
(TRS_ISSORT[A23] X1)
(NOT (EQUAL (CAR X1) 'TRS_0)))
(< (ACL2-COUNT (CADR X0))
(+ 1 1 (ACL2-COUNT (CADR X0))))).
But simplification reduces this to T, using linear arithmetic, primitive
type reasoning and the :type-prescription rule ACL2-COUNT.
Q.E.D.
That completes the proof of the measure theorem for TRS_GE. Thus,
we admit this function under the principle of definition. We observe
that the type of TRS_GE is described by the theorem
(AND (CONSP (TRS_GE X0 X1)) (TRUE-LISTP (TRS_GE X0 X1))).
Summary
Form: ( DEFUN TRS_GE ...)
Rules: ((:DEFINITION ACL2-COUNT)
(:DEFINITION EQ)
(:DEFINITION FIX)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O<)
(:DEFINITION TRS_ISSORT[A23])
(:EXECUTABLE-COUNTERPART ACL2-COUNT)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION ACL2-COUNT))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
TRS_GE
ACL2 !>
For the admission of TRS_GT we will use the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X0). The non-trivial part of the measure conjecture is
Goal
(IMPLIES (AND (AND (TRS_ISSORT[A23] X0)
(TRS_ISSORT[A23] X1))
(NOT (EQ (CAR X0) 'TRS_0))
(NOT (AND (EQ (CAR X0) 'TRS_S)
(EQ (CAR X1) 'TRS_0)))
T)
(O< (ACL2-COUNT (CADR X0))
(ACL2-COUNT X0))).
By the simple :definition EQ we reduce the conjecture to
Goal'
(IMPLIES (AND (TRS_ISSORT[A23] X0)
(TRS_ISSORT[A23] X1)
(NOT (EQUAL (CAR X0) 'TRS_0))
(NOT (AND (EQUAL (CAR X0) 'TRS_S)
(EQUAL (CAR X1) 'TRS_0))))
(O< (ACL2-COUNT (CADR X0))
(ACL2-COUNT X0))).
This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O<
and TRS_ISSORT[A23], the :executable-counterparts of ACL2-COUNT and
EQUAL, primitive type reasoning, the :rewrite rules COMMUTATIVITY-OF-+
and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to
Goal''
(IMPLIES (AND (CONSP X0)
(CONSP (CDR X0))
(EQUAL 'TRS_S (CAR X0))
(TRS_ISSORT[A23] (CADR X0))
(NOT (CDDR X0))
(TRS_ISSORT[A23] X1)
(NOT (EQUAL (CAR X1) 'TRS_0)))
(< (ACL2-COUNT (CADR X0))
(+ 1 1 (ACL2-COUNT (CADR X0))))).
But simplification reduces this to T, using linear arithmetic, primitive
type reasoning and the :type-prescription rule ACL2-COUNT.
Q.E.D.
That completes the proof of the measure theorem for TRS_GT. Thus,
we admit this function under the principle of definition. We observe
that the type of TRS_GT is described by the theorem
(AND (CONSP (TRS_GT X0 X1)) (TRUE-LISTP (TRS_GT X0 X1))).
Summary
Form: ( DEFUN TRS_GT ...)
Rules: ((:DEFINITION ACL2-COUNT)
(:DEFINITION EQ)
(:DEFINITION FIX)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O<)
(:DEFINITION TRS_ISSORT[A23])
(:EXECUTABLE-COUNTERPART ACL2-COUNT)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION ACL2-COUNT))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
TRS_GT
ACL2 !>
Since TRS_EQUAL_SORT[A40] is non-recursive, its admission is trivial.
We observe that the type of TRS_EQUAL_SORT[A40] is described by the
theorem
(AND (CONSP (TRS_EQUAL_SORT[A40] X0 X1))
(TRUE-LISTP (TRS_EQUAL_SORT[A40] X0 X1))).
Summary
Form: ( DEFUN TRS_EQUAL_SORT[A40] ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TRS_EQUAL_SORT[A40]
ACL2 !>
For the admission of TRS_EQUAL_SORT[A23] we will use the relation O<
(which is known to be well-founded on the domain recognized by O-P)
and the measure (ACL2-COUNT X0). The non-trivial part of the measure
conjecture is
Goal
(IMPLIES (AND (AND (TRS_ISSORT[A23] X0)
(TRS_ISSORT[A23] X1))
(NOT (AND (EQ (CAR X0) 'TRS_0)
(EQ (CAR X1) 'TRS_0)))
(NOT (AND (EQ (CAR X0) 'TRS_0)
(EQ (CAR X1) 'TRS_S)))
(NOT (AND (EQ (CAR X0) 'TRS_S)
(EQ (CAR X1) 'TRS_0)))
T)
(O< (ACL2-COUNT (CADR X0))
(ACL2-COUNT X0))).
By the simple :definition EQ we reduce the conjecture to
Goal'
(IMPLIES (AND (TRS_ISSORT[A23] X0)
(TRS_ISSORT[A23] X1)
(NOT (AND (EQUAL (CAR X0) 'TRS_0)
(EQUAL (CAR X1) 'TRS_0)))
(NOT (AND (EQUAL (CAR X0) 'TRS_0)
(EQUAL (CAR X1) 'TRS_S)))
(NOT (AND (EQUAL (CAR X0) 'TRS_S)
(EQUAL (CAR X1) 'TRS_0))))
(O< (ACL2-COUNT (CADR X0))
(ACL2-COUNT X0))).
This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O<
and TRS_ISSORT[A23], the :executable-counterparts of ACL2-COUNT and
EQUAL, primitive type reasoning, the :rewrite rules COMMUTATIVITY-OF-+
and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to
Goal''
(IMPLIES (AND (CONSP X0)
(CONSP (CDR X0))
(EQUAL 'TRS_S (CAR X0))
(TRS_ISSORT[A23] (CADR X0))
(NOT (CDDR X0))
(TRS_ISSORT[A23] X1)
(NOT (EQUAL (CAR X1) 'TRS_0)))
(< (ACL2-COUNT (CADR X0))
(+ 1 1 (ACL2-COUNT (CADR X0))))).
But simplification reduces this to T, using linear arithmetic, primitive
type reasoning and the :type-prescription rule ACL2-COUNT.
Q.E.D.
That completes the proof of the measure theorem for TRS_EQUAL_SORT[A23].
Thus, we admit this function under the principle of definition. We
observe that the type of TRS_EQUAL_SORT[A23] is described by the theorem
(AND (CONSP (TRS_EQUAL_SORT[A23] X0 X1))
(TRUE-LISTP (TRS_EQUAL_SORT[A23] X0 X1))).
We used the :executable-counterpart of EQUAL and primitive type reasoning.
Summary
Form: ( DEFUN TRS_EQUAL_SORT[A23] ...)
Rules: ((:DEFINITION ACL2-COUNT)
(:DEFINITION EQ)
(:DEFINITION FIX)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O<)
(:DEFINITION TRS_ISSORT[A23])
(:EXECUTABLE-COUNTERPART ACL2-COUNT)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION ACL2-COUNT))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
TRS_EQUAL_SORT[A23]
ACL2 !>
Since TRS_ISA_FALSE is non-recursive, its admission is trivial. We
observe that the type of TRS_ISA_FALSE is described by the theorem
(AND (CONSP (TRS_ISA_FALSE X0)) (TRUE-LISTP (TRS_ISA_FALSE X0))).
Summary
Form: ( DEFUN TRS_ISA_FALSE ...)
Rules: NIL
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
TRS_ISA_FALSE
ACL2 !>
Since TRS_ISA_TRUE is non-recursive, its admission is trivial. We
observe that the type of TRS_ISA_TRUE is described by the theorem
(AND (CONSP (TRS_ISA_TRUE X0)) (TRUE-LISTP (TRS_ISA_TRUE X0))).
Summary
Form: ( DEFUN TRS_ISA_TRUE ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TRS_ISA_TRUE
ACL2 !>
Since TRS_NOT is non-recursive, its admission is trivial. We observe
that the type of TRS_NOT is described by the theorem
(AND (CONSP (TRS_NOT X0)) (TRUE-LISTP (TRS_NOT X0))).
Summary
Form: ( DEFUN TRS_NOT ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TRS_NOT
ACL2 !>
Since TRS_OR is non-recursive, its admission is trivial. We observe
that the type of TRS_OR is described by the theorem
(OR (AND (CONSP (TRS_OR X0 X1))
(TRUE-LISTP (TRS_OR X0 X1)))
(EQUAL (TRS_OR X0 X1) X1)).
Summary
Form: ( DEFUN TRS_OR ...)
Rules: NIL
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
TRS_OR
ACL2 !>
Since TRS_AND is non-recursive, its admission is trivial. We observe
that the type of TRS_AND is described by the theorem
(OR (AND (CONSP (TRS_AND X0 X1))
(TRUE-LISTP (TRS_AND X0 X1)))
(EQUAL (TRS_AND X0 X1) X1)).
Summary
Form: ( DEFUN TRS_AND ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TRS_AND
ACL2 !>
Since TRS_EQUAL_BOOL is non-recursive, its admission is trivial. We
observe that the type of TRS_EQUAL_BOOL is described by the theorem
(AND (CONSP (TRS_EQUAL_BOOL X0 X1)) (TRUE-LISTP (TRS_EQUAL_BOOL X0 X1))).
We used the :executable-counterpart of EQUAL and primitive type reasoning.
Summary
Form: ( DEFUN TRS_EQUAL_BOOL ...)
Rules: ((:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
TRS_EQUAL_BOOL
ACL2 !>
For the admission of TRS_IF we will use the relation O< (which is known
to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X1). The non-trivial part of the measure conjecture is
Goal
(IMPLIES (AND (AND (TRS_ISBOOL X0)
(TRS_ISSORT[A23] X1)
(TRS_ISSORT[A23] X2))
(NOT (EQ (CAR X0) 'TRS_FALSE))
(AND (EQ (CAR X0) 'TRS_TRUE)
(EQ (CAR X1) 'TRS_S)))
(O< (ACL2-COUNT (CADR X1))
(ACL2-COUNT X1))).
By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture
to
Goal'
(IMPLIES (AND (CONSP X0)
(COND ((EQUAL 'TRS_TRUE (CAR X0))
(EQUAL (CDR X0) NIL))
((EQUAL 'TRS_FALSE (CAR X0))
(EQUAL (CDR X0) NIL))
(T NIL))
(TRS_ISSORT[A23] X1)
(TRS_ISSORT[A23] X2)
(NOT (EQUAL (CAR X0) 'TRS_FALSE))
(EQUAL (CAR X0) 'TRS_TRUE)
(EQUAL (CAR X1) 'TRS_S))
(O< (ACL2-COUNT (CADR X1))
(ACL2-COUNT X1))).
This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O<
and TRS_ISSORT[A23], the :executable-counterparts of ACL2-COUNT and
EQUAL, primitive type reasoning, the :rewrite rules COMMUTATIVITY-OF-+
and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to
Goal''
(IMPLIES (AND (CONSP X0)
(NOT (CDR X0))
(CONSP X1)
(CONSP (CDR X1))
(TRS_ISSORT[A23] (CADR X1))
(NOT (CDDR X1))
(TRS_ISSORT[A23] X2)
(EQUAL (CAR X0) 'TRS_TRUE)
(EQUAL (CAR X1) 'TRS_S))
(< (ACL2-COUNT (CADR X1))
(+ 1 1 (ACL2-COUNT (CADR X1))))).
But simplification reduces this to T, using linear arithmetic, primitive
type reasoning and the :type-prescription rule ACL2-COUNT.
Q.E.D.
That completes the proof of the measure theorem for TRS_IF. Thus,
we admit this function under the principle of definition. We observe
that the type of TRS_IF is described by the theorem
(AND (CONSP (TRS_IF X0 X1 X2)) (TRUE-LISTP (TRS_IF X0 X1 X2))). We
used primitive type reasoning.
Summary
Form: ( DEFUN TRS_IF ...)
Rules: ((:DEFINITION ACL2-COUNT)
(:DEFINITION EQ)
(:DEFINITION FIX)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O<)
(:DEFINITION TRS_ISBOOL)
(:DEFINITION TRS_ISSORT[A23])
(:EXECUTABLE-COUNTERPART ACL2-COUNT)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION ACL2-COUNT))
Warnings: None
Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00)
TRS_IF
ACL2 !>
For the admission of TRS_IFPRIME we will use the relation O< (which
is known to be well-founded on the domain recognized by O-P) and the
measure (ACL2-COUNT X1). The non-trivial part of the measure conjecture
is
Goal
(IMPLIES (AND (AND (TRS_ISBOOL X0)
(TRS_ISSORT[A23] X1)
(TRS_ISSORT[A23] X2))
(NOT (EQ (CAR X0) 'TRS_FALSE))
(AND (EQ (CAR X0) 'TRS_TRUE)
(EQ (CAR X1) 'TRS_S)))
(O< (ACL2-COUNT (CADR X1))
(ACL2-COUNT X1))).
By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture
to
Goal'
(IMPLIES (AND (CONSP X0)
(COND ((EQUAL 'TRS_TRUE (CAR X0))
(EQUAL (CDR X0) NIL))
((EQUAL 'TRS_FALSE (CAR X0))
(EQUAL (CDR X0) NIL))
(T NIL))
(TRS_ISSORT[A23] X1)
(TRS_ISSORT[A23] X2)
(NOT (EQUAL (CAR X0) 'TRS_FALSE))
(EQUAL (CAR X0) 'TRS_TRUE)
(EQUAL (CAR X1) 'TRS_S))
(O< (ACL2-COUNT (CADR X1))
(ACL2-COUNT X1))).
This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O<
and TRS_ISSORT[A23], the :executable-counterparts of ACL2-COUNT and
EQUAL, primitive type reasoning, the :rewrite rules COMMUTATIVITY-OF-+
and UNICITY-OF-0 and the :type-prescription rule ACL2-COUNT, to
Goal''
(IMPLIES (AND (CONSP X0)
(NOT (CDR X0))
(CONSP X1)
(CONSP (CDR X1))
(TRS_ISSORT[A23] (CADR X1))
(NOT (CDDR X1))
(TRS_ISSORT[A23] X2)
(EQUAL (CAR X0) 'TRS_TRUE)
(EQUAL (CAR X1) 'TRS_S))
(< (ACL2-COUNT (CADR X1))
(+ 1 1 (ACL2-COUNT (CADR X1))))).
But simplification reduces this to T, using linear arithmetic, primitive
type reasoning and the :type-prescription rule ACL2-COUNT.
Q.E.D.
That completes the proof of the measure theorem for TRS_IFPRIME. Thus,
we admit this function under the principle of definition. We observe
that the type of TRS_IFPRIME is described by the theorem
(AND (CONSP (TRS_IFPRIME X0 X1 X2)) (TRUE-LISTP (TRS_IFPRIME X0 X1 X2))).
Summary
Form: ( DEFUN TRS_IFPRIME ...)
Rules: ((:DEFINITION ACL2-COUNT)
(:DEFINITION EQ)
(:DEFINITION FIX)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O<)
(:DEFINITION TRS_ISBOOL)
(:DEFINITION TRS_ISSORT[A23])
(:EXECUTABLE-COUNTERPART ACL2-COUNT)
(:EXECUTABLE-COUNTERPART EQUAL)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION ACL2-COUNT))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
TRS_IFPRIME
ACL2 !>
For the admission of TRS_MINUS we will use the relation O< (which is
known to be well-founded on the domain recognized by O-P) and the measure
(ACL2-COUNT X0). The non-trivial part of the measure conjecture is
Goal
(IMPLIES (AND (AND (TRS_ISSORT[A23] X0)
(TRS_ISSORT[A23] X1))
(NOT (EQ (CAR X0) 'TRS_0))
(AND (EQ (CAR X0) 'TRS_S)
(EQ (TRS_EQUAL_BOOL (TRS_GT (LIST 'TRS_S (CADR X0)) X1)
'(TRS_TRUE))
'(TRS_TRUE))))
(O< (ACL2-COUNT (CADR X0))
(ACL2-COUNT X0))).
By the simple :definition EQ we reduce the conjecture to
Goal'
(IMPLIES (AND (TRS_ISSORT[A23] X0)
(TRS_ISSORT[A23] X1)
(NOT (EQUAL (CAR X0) 'TRS_0))
(EQUAL (CAR X0) 'TRS_S)
(EQUAL (TRS_EQUAL_BOOL (TRS_GT (LIST 'TRS_S (CADR X0)) X1)
'(TRS_TRUE))
'(TRS_TRUE)))
(O< (ACL2-COUNT (CADR X0))
(ACL2-COUNT X0))).
This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O<,
TRS_GT and TRS_ISSORT[A23], the :executable-counterparts of ACL2-COUNT
and EQUAL, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS,
COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type-prescription rules
ACL2-COUNT and TRS_ISSORT[A23], to the following two conjectures.
Subgoal 2
(IMPLIES (AND (CONSP X0)
(CONSP (CDR X0))
(TRS_ISSORT[A23] (CADR X0))
(NOT (CDDR X0))
(TRS_ISSORT[A23] X1)
(EQUAL (CAR X0) 'TRS_S)
(EQUAL (CAR X1) 'TRS_0)
(EQUAL (TRS_EQUAL_BOOL '(TRS_TRUE) '(TRS_TRUE))
'(TRS_TRUE)))
(< (ACL2-COUNT (CADR X0))
(+ 1 1 (ACL2-COUNT (CADR X0))))).
By the :executable-counterparts of EQUAL and TRS_EQUAL_BOOL we reduce
the conjecture to
Subgoal 2'
(IMPLIES (AND (CONSP X0)
(CONSP (CDR X0))
(TRS_ISSORT[A23] (CADR X0))
(NOT (CDDR X0))
(TRS_ISSORT[A23] X1)
(EQUAL (CAR X0) 'TRS_S)
(EQUAL (CAR X1) 'TRS_0))
(< (ACL2-COUNT (CADR X0))
(+ 1 1 (ACL2-COUNT (CADR X0))))).
But simplification reduces this to T, using linear arithmetic, primitive
type reasoning and the :type-prescription rule ACL2-COUNT.
Subgoal 1
(IMPLIES (AND (CONSP X0)
(CONSP (CDR X0))
(TRS_ISSORT[A23] (CADR X0))
(NOT (CDDR X0))
(TRS_ISSORT[A23] X1)
(EQUAL (CAR X0) 'TRS_S)
(NOT (EQUAL (CAR X1) 'TRS_0))
(EQUAL (TRS_EQUAL_BOOL (TRS_GT (CADR X0) (CADR X1))
'(TRS_TRUE))
'(TRS_TRUE)))
(< (ACL2-COUNT (CADR X0))
(+ 1 1 (ACL2-COUNT (CADR X0))))).
But simplification reduces this to T, using linear arithmetic, primitive
type reasoning and the :type-prescription rule ACL2-COUNT.
Q.E.D.
That completes the proof of the measure theorem for TRS_MINUS. Thus,
we admit this function under the principle of definition. We observe
that the type of TRS_MINUS is described by the theorem
(AND (CONSP (TRS_MINUS X0 X1)) (TRUE-LISTP (TRS_MINUS X0 X1))). We
used primitive type reasoning.
Summary
Form: ( DEFUN TRS_MINUS ...)
Rules: ((:DEFINITION ACL2-COUNT)
(:DEFINITION EQ)
(:DEFINITION FIX)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O<)
(:DEFINITION TRS_GT)
(:DEFINITION TRS_ISSORT[A23])
(:EXECUTABLE-COUNTERPART ACL2-COUNT)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART TRS_EQUAL_BOOL)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION ACL2-COUNT)
(:TYPE-PRESCRIPTION TRS_ISSORT[A23]))
Warnings: None
Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)
TRS_MINUS
ACL2 !>
For the admission of TRS_MINUSPRIME we will use the relation O< (which
is known to be well-founded on the domain recognized by O-P) and the
measure (ACL2-COUNT X0). The non-trivial part of the measure conjecture
is
Goal
(IMPLIES (AND (AND (TRS_ISSORT[A23] X0)
(TRS_ISSORT[A23] X1))
(NOT (EQ (CAR X0) 'TRS_0))
(AND (EQ (CAR X0) 'TRS_S)
(EQ (TRS_EQUAL_BOOL (TRS_GT (LIST 'TRS_S (CADR X0)) X1)
'(TRS_TRUE))
'(TRS_TRUE))))
(O< (ACL2-COUNT (CADR X0))
(ACL2-COUNT X0))).
By the simple :definition EQ we reduce the conjecture to
Goal'
(IMPLIES (AND (TRS_ISSORT[A23] X0)
(TRS_ISSORT[A23] X1)
(NOT (EQUAL (CAR X0) 'TRS_0))
(EQUAL (CAR X0) 'TRS_S)
(EQUAL (TRS_EQUAL_BOOL (TRS_GT (LIST 'TRS_S (CADR X0)) X1)
'(TRS_TRUE))
'(TRS_TRUE)))
(O< (ACL2-COUNT (CADR X0))
(ACL2-COUNT X0))).
This simplifies, using the :definitions ACL2-COUNT, FIX, O-FINP, O<,
TRS_GT and TRS_ISSORT[A23], the :executable-counterparts of ACL2-COUNT
and EQUAL, primitive type reasoning, the :rewrite rules CAR-CONS, CDR-CONS,
COMMUTATIVITY-OF-+ and UNICITY-OF-0 and the :type-prescription rules
ACL2-COUNT and TRS_ISSORT[A23], to the following two conjectures.
Subgoal 2
(IMPLIES (AND (CONSP X0)
(CONSP (CDR X0))
(TRS_ISSORT[A23] (CADR X0))
(NOT (CDDR X0))
(TRS_ISSORT[A23] X1)
(EQUAL (CAR X0) 'TRS_S)
(EQUAL (CAR X1) 'TRS_0)
(EQUAL (TRS_EQUAL_BOOL '(TRS_TRUE) '(TRS_TRUE))
'(TRS_TRUE)))
(< (ACL2-COUNT (CADR X0))
(+ 1 1 (ACL2-COUNT (CADR X0))))).
By the :executable-counterparts of EQUAL and TRS_EQUAL_BOOL we reduce
the conjecture to
Subgoal 2'
(IMPLIES (AND (CONSP X0)
(CONSP (CDR X0))
(TRS_ISSORT[A23] (CADR X0))
(NOT (CDDR X0))
(TRS_ISSORT[A23] X1)
(EQUAL (CAR X0) 'TRS_S)
(EQUAL (CAR X1) 'TRS_0))
(< (ACL2-COUNT (CADR X0))
(+ 1 1 (ACL2-COUNT (CADR X0))))).
But simplification reduces this to T, using linear arithmetic, primitive
type reasoning and the :type-prescription rule ACL2-COUNT.
Subgoal 1
(IMPLIES (AND (CONSP X0)
(CONSP (CDR X0))
(TRS_ISSORT[A23] (CADR X0))
(NOT (CDDR X0))
(TRS_ISSORT[A23] X1)
(EQUAL (CAR X0) 'TRS_S)
(NOT (EQUAL (CAR X1) 'TRS_0))
(EQUAL (TRS_EQUAL_BOOL (TRS_GT (CADR X0) (CADR X1))
'(TRS_TRUE))
'(TRS_TRUE)))
(< (ACL2-COUNT (CADR X0))
(+ 1 1 (ACL2-COUNT (CADR X0))))).
But simplification reduces this to T, using linear arithmetic, primitive
type reasoning and the :type-prescription rule ACL2-COUNT.
Q.E.D.
That completes the proof of the measure theorem for TRS_MINUSPRIME.
Thus, we admit this function under the principle of definition. We
observe that the type of TRS_MINUSPRIME is described by the theorem
(AND (CONSP (TRS_MINUSPRIME X0 X1)) (TRUE-LISTP (TRS_MINUSPRIME X0 X1))).
Summary
Form: ( DEFUN TRS_MINUSPRIME ...)
Rules: ((:DEFINITION ACL2-COUNT)
(:DEFINITION EQ)
(:DEFINITION FIX)
(:DEFINITION NOT)
(:DEFINITION O-FINP)
(:DEFINITION O<)
(:DEFINITION TRS_GT)
(:DEFINITION TRS_ISSORT[A23])
(:EXECUTABLE-COUNTERPART ACL2-COUNT)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART TRS_EQUAL_BOOL)
(:FAKE-RUNE-FOR-LINEAR NIL)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:REWRITE COMMUTATIVITY-OF-+)
(:REWRITE UNICITY-OF-0)
(:TYPE-PRESCRIPTION ACL2-COUNT)
(:TYPE-PRESCRIPTION TRS_ISSORT[A23]))
Warnings: None
Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.01)
TRS_MINUSPRIME
ACL2 !>
By the simple :definition EQ we reduce the conjecture to
Goal'
(IMPLIES (AND (TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] TRS_Z1PRIME))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
Name the formula above *1.
Perhaps we can prove *1 by induction. Four induction schemes are suggested
by this conjecture. These merge into one derived induction scheme.
We will induct according to a scheme suggested by
(TRS_IFPRIME (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)
TRS_Z0PRIME
(CONS 'TRS_S (CONS TRS_Z1PRIME 'NIL))),
but modified to accommodate (TRS_ISSORT[A23] TRS_Z1PRIME) and
(TRS_GT TRS_Z0PRIME TRS_Z1PRIME). These suggestions were produced
using the :induction rules TRS_GT, TRS_IFPRIME and TRS_ISSORT[A23].
If we let (:P TRS_Z0PRIME TRS_Z1PRIME) denote *1 above then the induction
scheme we'll use is
(AND (IMPLIES (NOT (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME))))
(:P TRS_Z0PRIME TRS_Z1PRIME))
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME)))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_FALSE))
(NOT (AND (EQ (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME) 'TRS_S)))
T)
(:P TRS_Z0PRIME TRS_Z1PRIME))
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME)))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_FALSE))
(AND (EQ (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME) 'TRS_S))
(:P (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME)))
(:P TRS_Z0PRIME TRS_Z1PRIME))
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME)))
(EQ (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_FALSE))
(:P TRS_Z0PRIME TRS_Z1PRIME))).
This induction is justified by the same argument used to admit TRS_IFPRIME.
Note, however, that the unmeasured variable TRS_Z1PRIME is being instantiated.
When applied to the goal at hand the above induction scheme produces
six nontautological subgoals.
Subgoal *1/6
(IMPLIES (AND (NOT (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME))))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] TRS_Z1PRIME))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME and
TRS_ISSORT[A23], the :executable-counterparts of CAR, EQUAL and TRS_ISBOOL,
primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS
and the :type-prescription rules TRS_ISBOOL and TRS_ISSORT[A23], to
the following two conjectures.
Subgoal *1/6.2
(IMPLIES (AND (EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (CAR TRS_Z1PRIME) 'TRS_0)
(NOT (TRS_ISBOOL '(TRS_TRUE)))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(CONSP TRS_Z1PRIME)
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
But we reduce the conjecture to T, by the :executable-counterpart of
TRS_ISBOOL.
Subgoal *1/6.1
(IMPLIES (AND (NOT (TRS_ISBOOL (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(EQUAL 'TRS_S (CAR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(CONSP TRS_Z1PRIME)
(CONSP (CDR TRS_Z1PRIME))
(EQUAL 'TRS_S (CAR TRS_Z1PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z1PRIME))
(NOT (CDDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
But simplification reduces this to T, using the :definitions TRS_IFPRIME
and TRS_ISBOOL, the :executable-counterpart of EQUAL, primitive type
reasoning and the :type-prescription rule TRS_GT.
Subgoal *1/5
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME)))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_FALSE))
(NOT (AND (EQ (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME) 'TRS_S)))
T (TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] TRS_Z1PRIME))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture
to
Subgoal *1/5'
(IMPLIES (AND (CONSP (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(COND ((EQUAL 'TRS_TRUE
(CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
NIL))
((EQUAL 'TRS_FALSE
(CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
NIL))
(T NIL))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME))
(NOT (EQUAL (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_FALSE))
(NOT (AND (EQUAL (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)))
(TRS_ISSORT[A23] TRS_Z1PRIME))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
But simplification reduces this to T, using the :definitions TRS_GT
and TRS_ISSORT[A23], the :executable-counterparts of CAR and EQUAL,
primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS
and the :type-prescription rules TRS_GT and TRS_ISSORT[A23].
Subgoal *1/4
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME)))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_FALSE))
(AND (EQ (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME) 'TRS_S))
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))
(CADR TRS_Z0PRIME)
(LIST 'TRS_S (CADR TRS_Z1PRIME)))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] TRS_Z1PRIME))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture
to
Subgoal *1/4'
(IMPLIES (AND (CONSP (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(COND ((EQUAL 'TRS_TRUE
(CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
NIL))
((EQUAL 'TRS_FALSE
(CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
NIL))
(T NIL))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME))
(NOT (EQUAL (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_FALSE))
(EQUAL (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))
(CADR TRS_Z0PRIME)
(LIST 'TRS_S (CADR TRS_Z1PRIME)))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT and TRS_ISSORT[A23],
the :executable-counterparts of CAR and EQUAL, primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rules TRS_GT and TRS_ISSORT[A23], to the following ten conjectures.
Subgoal *1/4.10
(IMPLIES (AND (EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))
(CADR TRS_Z0PRIME)
(LIST 'TRS_S (CADR TRS_Z1PRIME)))
'(TRS_TRUE))
(CONSP TRS_Z1PRIME)
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT and TRS_IFPRIME, the
:executable-counterparts of CAR, CONS, EQUAL, TRS_ISBOOL and TRS_ISSORT[A23]
and the :type-prescription rule TRS_ISSORT[A23], to
Subgoal *1/4.10'
(IMPLIES (AND (EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(CONSP TRS_Z1PRIME)
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z1PRIME) and (CDR TRS_Z1PRIME) can be
eliminated by using CAR-CDR-ELIM to replace TRS_Z1PRIME by
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2), (CAR TRS_Z1PRIME) by TRS_Z1PRIME1
and (CDR TRS_Z1PRIME) by TRS_Z1PRIME2 and restrict the type of the
new variable TRS_Z1PRIME1 to be that of the term it replaces. This
produces the following goal.
Subgoal *1/4.10''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
(NOT (EQUAL TRS_Z1PRIME1 NIL))
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.10'''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
TRS_Z1PRIME1
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
This simplifies, using the :executable-counterparts of CONS, CONSP,
EQUAL, NOT and SYMBOLP, to
Subgoal *1/4.10'4'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME '(TRS_S (TRS_0)))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z0PRIME) and (CDR TRS_Z0PRIME) can be
eliminated. Furthermore, those terms are at the root of a chain of
two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace
TRS_Z0PRIME by (CONS TRS_Z0PRIME1 TRS_Z0PRIME2), (CAR TRS_Z0PRIME)
by TRS_Z0PRIME1 and (CDR TRS_Z0PRIME) by TRS_Z0PRIME2 and restrict
the type of the new variable TRS_Z0PRIME1 to be that of the term it
replaces. (2) Use CAR-CDR-ELIM, again, to replace TRS_Z0PRIME2 by
(CONS TRS_Z0PRIME3 TRS_Z0PRIME4), (CAR TRS_Z0PRIME2) by TRS_Z0PRIME3
and (CDR TRS_Z0PRIME2) by TRS_Z0PRIME4. These steps produce the
following goal.
Subgoal *1/4.10'5'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
(NOT (EQUAL TRS_Z0PRIME1 NIL))
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.10'6'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
TRS_Z0PRIME1
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME and
TRS_ISSORT[A23], the :executable-counterparts of CAR, CDR, EQUAL, NOT,
SYMBOLP, TRS_ISBOOL and TRS_ISSORT[A23], primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule TRS_ISSORT[A23], to
Subgoal *1/4.10'7'
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
Name the formula above *1.1.
Subgoal *1/4.9
(IMPLIES (AND (NOT (CONSP (CDR TRS_Z1PRIME)))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))
(CADR TRS_Z0PRIME)
(LIST 'TRS_S (CADR TRS_Z1PRIME)))
'(TRS_TRUE))
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT and TRS_IFPRIME, the
:executable-counterparts of CAR, CONS, CONSP, EQUAL, TRS_ISBOOL and
TRS_ISSORT[A23] and the :type-prescription rule TRS_ISSORT[A23], to
Subgoal *1/4.9'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z1PRIME) and (CDR TRS_Z1PRIME) can be
eliminated by using CAR-CDR-ELIM to replace TRS_Z1PRIME by
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2), (CAR TRS_Z1PRIME) by TRS_Z1PRIME1
and (CDR TRS_Z1PRIME) by TRS_Z1PRIME2 and restrict the type of the
new variable TRS_Z1PRIME1 to be that of the term it replaces. This
produces the following goal.
Subgoal *1/4.9''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
(NOT (EQUAL TRS_Z1PRIME1 NIL))
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.9'''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
TRS_Z1PRIME1
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
This simplifies, using the :executable-counterparts of CONS, CONSP,
EQUAL, NOT and SYMBOLP, to
Subgoal *1/4.9'4'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME '(TRS_S (TRS_0)))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z0PRIME) and (CDR TRS_Z0PRIME) can be
eliminated. Furthermore, those terms are at the root of a chain of
two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace
TRS_Z0PRIME by (CONS TRS_Z0PRIME1 TRS_Z0PRIME2), (CAR TRS_Z0PRIME)
by TRS_Z0PRIME1 and (CDR TRS_Z0PRIME) by TRS_Z0PRIME2 and restrict
the type of the new variable TRS_Z0PRIME1 to be that of the term it
replaces. (2) Use CAR-CDR-ELIM, again, to replace TRS_Z0PRIME2 by
(CONS TRS_Z0PRIME3 TRS_Z0PRIME4), (CAR TRS_Z0PRIME2) by TRS_Z0PRIME3
and (CDR TRS_Z0PRIME2) by TRS_Z0PRIME4. These steps produce the
following goal.
Subgoal *1/4.9'5'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
(NOT (EQUAL TRS_Z0PRIME1 NIL))
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.9'6'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
TRS_Z0PRIME1
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME and
TRS_ISSORT[A23], the :executable-counterparts of CAR, CDR, EQUAL, NOT,
SYMBOLP, TRS_ISBOOL and TRS_ISSORT[A23], primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule TRS_ISSORT[A23], to
Subgoal *1/4.9'7'
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
Name the formula above *1.2.
Subgoal *1/4.8
(IMPLIES (AND (NOT (CDR (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))
(CADR TRS_Z0PRIME)
(LIST 'TRS_S (CADR TRS_Z1PRIME)))
'(TRS_TRUE))
(CONSP TRS_Z1PRIME)
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT and TRS_IFPRIME, the
:executable-counterparts of CAR, CDR, CONS, EQUAL, TRS_ISBOOL and
TRS_ISSORT[A23] and the :type-prescription rule TRS_ISSORT[A23], to
Subgoal *1/4.8'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(CONSP TRS_Z1PRIME)
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z1PRIME) and (CDR TRS_Z1PRIME) can be
eliminated by using CAR-CDR-ELIM to replace TRS_Z1PRIME by
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2), (CAR TRS_Z1PRIME) by TRS_Z1PRIME1
and (CDR TRS_Z1PRIME) by TRS_Z1PRIME2 and restrict the type of the
new variable TRS_Z1PRIME1 to be that of the term it replaces. This
produces the following goal.
Subgoal *1/4.8''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
(NOT (EQUAL TRS_Z1PRIME1 NIL))
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.8'''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
TRS_Z1PRIME1
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
This simplifies, using the :executable-counterparts of CONS, CONSP,
EQUAL, NOT and SYMBOLP, to
Subgoal *1/4.8'4'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME '(TRS_S (TRS_0)))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z0PRIME) and (CDR TRS_Z0PRIME) can be
eliminated. Furthermore, those terms are at the root of a chain of
two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace
TRS_Z0PRIME by (CONS TRS_Z0PRIME1 TRS_Z0PRIME2), (CAR TRS_Z0PRIME)
by TRS_Z0PRIME1 and (CDR TRS_Z0PRIME) by TRS_Z0PRIME2 and restrict
the type of the new variable TRS_Z0PRIME1 to be that of the term it
replaces. (2) Use CAR-CDR-ELIM, again, to replace TRS_Z0PRIME2 by
(CONS TRS_Z0PRIME3 TRS_Z0PRIME4), (CAR TRS_Z0PRIME2) by TRS_Z0PRIME3
and (CDR TRS_Z0PRIME2) by TRS_Z0PRIME4. These steps produce the
following goal.
Subgoal *1/4.8'5'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
(NOT (EQUAL TRS_Z0PRIME1 NIL))
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.8'6'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
TRS_Z0PRIME1
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME and
TRS_ISSORT[A23], the :executable-counterparts of CAR, CDR, EQUAL, NOT,
SYMBOLP, TRS_ISBOOL and TRS_ISSORT[A23], primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule TRS_ISSORT[A23], to
Subgoal *1/4.8'7'
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
Name the formula above *1.3.
Subgoal *1/4.7
(IMPLIES (AND (NOT (CDR (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(NOT (TRS_ISSORT[A23] (CADR TRS_Z1PRIME)))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))
(CADR TRS_Z0PRIME)
(LIST 'TRS_S (CADR TRS_Z1PRIME)))
'(TRS_TRUE))
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT and TRS_IFPRIME, the
:executable-counterparts of CAR, CDR, CONS, EQUAL, TRS_ISBOOL and
TRS_ISSORT[A23] and the :type-prescription rule TRS_ISSORT[A23], to
Subgoal *1/4.7'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z1PRIME) and (CDR TRS_Z1PRIME) can be
eliminated by using CAR-CDR-ELIM to replace TRS_Z1PRIME by
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2), (CAR TRS_Z1PRIME) by TRS_Z1PRIME1
and (CDR TRS_Z1PRIME) by TRS_Z1PRIME2 and restrict the type of the
new variable TRS_Z1PRIME1 to be that of the term it replaces. This
produces the following goal.
Subgoal *1/4.7''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
(NOT (EQUAL TRS_Z1PRIME1 NIL))
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.7'''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
TRS_Z1PRIME1
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
This simplifies, using the :executable-counterparts of CONS, CONSP,
EQUAL, NOT and SYMBOLP, to
Subgoal *1/4.7'4'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME '(TRS_S (TRS_0)))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z0PRIME) and (CDR TRS_Z0PRIME) can be
eliminated. Furthermore, those terms are at the root of a chain of
two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace
TRS_Z0PRIME by (CONS TRS_Z0PRIME1 TRS_Z0PRIME2), (CAR TRS_Z0PRIME)
by TRS_Z0PRIME1 and (CDR TRS_Z0PRIME) by TRS_Z0PRIME2 and restrict
the type of the new variable TRS_Z0PRIME1 to be that of the term it
replaces. (2) Use CAR-CDR-ELIM, again, to replace TRS_Z0PRIME2 by
(CONS TRS_Z0PRIME3 TRS_Z0PRIME4), (CAR TRS_Z0PRIME2) by TRS_Z0PRIME3
and (CDR TRS_Z0PRIME2) by TRS_Z0PRIME4. These steps produce the
following goal.
Subgoal *1/4.7'5'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
(NOT (EQUAL TRS_Z0PRIME1 NIL))
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.7'6'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
TRS_Z0PRIME1
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME and
TRS_ISSORT[A23], the :executable-counterparts of CAR, CDR, EQUAL, NOT,
SYMBOLP, TRS_ISBOOL and TRS_ISSORT[A23], primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule TRS_ISSORT[A23], to
Subgoal *1/4.7'7'
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
Name the formula above *1.4.
Subgoal *1/4.6
(IMPLIES (AND (NOT (CDR (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))
(CADR TRS_Z0PRIME)
(LIST 'TRS_S (CADR TRS_Z1PRIME)))
'(TRS_TRUE))
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT and TRS_IFPRIME, the
:executable-counterparts of CAR, CDR, CONS, EQUAL, TRS_ISBOOL and
TRS_ISSORT[A23] and the :type-prescription rule TRS_ISSORT[A23], to
Subgoal *1/4.6'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z1PRIME) and (CDR TRS_Z1PRIME) can be
eliminated by using CAR-CDR-ELIM to replace TRS_Z1PRIME by
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2), (CAR TRS_Z1PRIME) by TRS_Z1PRIME1
and (CDR TRS_Z1PRIME) by TRS_Z1PRIME2 and restrict the type of the
new variable TRS_Z1PRIME1 to be that of the term it replaces. This
produces the following goal.
Subgoal *1/4.6''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
(NOT (EQUAL TRS_Z1PRIME1 NIL))
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.6'''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
TRS_Z1PRIME1
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
This simplifies, using the :executable-counterparts of CONS, CONSP,
EQUAL, NOT and SYMBOLP, to
Subgoal *1/4.6'4'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME '(TRS_S (TRS_0)))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z0PRIME) and (CDR TRS_Z0PRIME) can be
eliminated. Furthermore, those terms are at the root of a chain of
two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace
TRS_Z0PRIME by (CONS TRS_Z0PRIME1 TRS_Z0PRIME2), (CAR TRS_Z0PRIME)
by TRS_Z0PRIME1 and (CDR TRS_Z0PRIME) by TRS_Z0PRIME2 and restrict
the type of the new variable TRS_Z0PRIME1 to be that of the term it
replaces. (2) Use CAR-CDR-ELIM, again, to replace TRS_Z0PRIME2 by
(CONS TRS_Z0PRIME3 TRS_Z0PRIME4), (CAR TRS_Z0PRIME2) by TRS_Z0PRIME3
and (CDR TRS_Z0PRIME2) by TRS_Z0PRIME4. These steps produce the
following goal.
Subgoal *1/4.6'5'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
(NOT (EQUAL TRS_Z0PRIME1 NIL))
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.6'6'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
TRS_Z0PRIME1
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME and
TRS_ISSORT[A23], the :executable-counterparts of CAR, CDR, EQUAL, NOT,
SYMBOLP, TRS_ISBOOL and TRS_ISSORT[A23], primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule TRS_ISSORT[A23], to
Subgoal *1/4.6'7'
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
Name the formula above *1.5.
Subgoal *1/4.5
(IMPLIES (AND (NOT (CDR (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME)))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))
(CADR TRS_Z0PRIME)
(LIST 'TRS_S (CADR TRS_Z1PRIME)))
'(TRS_TRUE))
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT and TRS_IFPRIME, the
:executable-counterparts of CAR, CDR, CONS, EQUAL, TRS_ISBOOL and
TRS_ISSORT[A23] and the :type-prescription rule TRS_ISSORT[A23], to
Subgoal *1/4.5'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z1PRIME) and (CDR TRS_Z1PRIME) can be
eliminated by using CAR-CDR-ELIM to replace TRS_Z1PRIME by
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2), (CAR TRS_Z1PRIME) by TRS_Z1PRIME1
and (CDR TRS_Z1PRIME) by TRS_Z1PRIME2 and restrict the type of the
new variable TRS_Z1PRIME1 to be that of the term it replaces. This
produces the following goal.
Subgoal *1/4.5''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
(NOT (EQUAL TRS_Z1PRIME1 NIL))
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.5'''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
TRS_Z1PRIME1
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
This simplifies, using the :executable-counterparts of CONS, CONSP,
EQUAL, NOT and SYMBOLP, to
Subgoal *1/4.5'4'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME '(TRS_S (TRS_0)))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z0PRIME) and (CDR TRS_Z0PRIME) can be
eliminated. Furthermore, those terms are at the root of a chain of
two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace
TRS_Z0PRIME by (CONS TRS_Z0PRIME1 TRS_Z0PRIME2), (CAR TRS_Z0PRIME)
by TRS_Z0PRIME1 and (CDR TRS_Z0PRIME) by TRS_Z0PRIME2 and restrict
the type of the new variable TRS_Z0PRIME1 to be that of the term it
replaces. (2) Use CAR-CDR-ELIM, again, to replace TRS_Z0PRIME2 by
(CONS TRS_Z0PRIME3 TRS_Z0PRIME4), (CAR TRS_Z0PRIME2) by TRS_Z0PRIME3
and (CDR TRS_Z0PRIME2) by TRS_Z0PRIME4. These steps produce the
following goal.
Subgoal *1/4.5'5'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
(NOT (EQUAL TRS_Z0PRIME1 NIL))
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.5'6'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
TRS_Z0PRIME1
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME and
TRS_ISSORT[A23], the :executable-counterparts of CAR, CDR, EQUAL, NOT,
SYMBOLP, TRS_ISBOOL and TRS_ISSORT[A23], primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule TRS_ISSORT[A23], to
Subgoal *1/4.5'7'
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
Name the formula above *1.6.
Subgoal *1/4.4
(IMPLIES (AND (NOT (CDR (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME)))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))
(CADR TRS_Z0PRIME)
(LIST 'TRS_S (CADR TRS_Z1PRIME)))
'(TRS_TRUE))
(CONSP TRS_Z1PRIME)
(CONSP (CDR TRS_Z1PRIME))
(EQUAL 'TRS_S (CAR TRS_Z1PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z1PRIME))
(NOT (CDDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z1PRIME) and (CDR TRS_Z1PRIME) can be
eliminated. Furthermore, those terms are at the root of a chain of
two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace
TRS_Z1PRIME by (CONS TRS_Z1PRIME1 TRS_Z1PRIME2), (CAR TRS_Z1PRIME)
by TRS_Z1PRIME1 and (CDR TRS_Z1PRIME) by TRS_Z1PRIME2 and restrict
the type of the new variable TRS_Z1PRIME1 to be that of the term it
replaces. (2) Use CAR-CDR-ELIM, again, to replace TRS_Z1PRIME2 by
(CONS TRS_Z1PRIME3 TRS_Z1PRIME4), (CAR TRS_Z1PRIME2) by TRS_Z1PRIME3
and (CDR TRS_Z1PRIME2) by TRS_Z1PRIME4. These steps produce the
following goal.
Subgoal *1/4.4'
(IMPLIES (AND (CONSP (CONS TRS_Z1PRIME3 TRS_Z1PRIME4))
(SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
(NOT (EQUAL TRS_Z1PRIME1 NIL))
(CONSP (LIST* TRS_Z1PRIME1 TRS_Z1PRIME3 TRS_Z1PRIME4))
(NOT (CDR (TRS_GT (CADR TRS_Z0PRIME)
TRS_Z1PRIME3)))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR (TRS_GT (CADR TRS_Z0PRIME)
TRS_Z1PRIME3))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME) TRS_Z1PRIME3)
(CADR TRS_Z0PRIME)
(LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(EQUAL 'TRS_S TRS_Z1PRIME1)
(TRS_ISSORT[A23] TRS_Z1PRIME3)
(NOT TRS_Z1PRIME4))
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME) TRS_Z1PRIME3)
TRS_Z0PRIME
(LIST 'TRS_S
(LIST* TRS_Z1PRIME1
TRS_Z1PRIME3 TRS_Z1PRIME4)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.4''
(IMPLIES (AND (CONSP (CONS TRS_Z1PRIME3 TRS_Z1PRIME4))
(SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
TRS_Z1PRIME1
(CONSP (LIST* TRS_Z1PRIME1 TRS_Z1PRIME3 TRS_Z1PRIME4))
(NOT (CDR (TRS_GT (CADR TRS_Z0PRIME)
TRS_Z1PRIME3)))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR (TRS_GT (CADR TRS_Z0PRIME)
TRS_Z1PRIME3))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME) TRS_Z1PRIME3)
(CADR TRS_Z0PRIME)
(LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(EQUAL 'TRS_S TRS_Z1PRIME1)
(TRS_ISSORT[A23] TRS_Z1PRIME3)
(NOT TRS_Z1PRIME4))
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME) TRS_Z1PRIME3)
TRS_Z0PRIME
(LIST 'TRS_S
(LIST* TRS_Z1PRIME1
TRS_Z1PRIME3 TRS_Z1PRIME4)))
'(TRS_TRUE))).
This simplifies, using the :executable-counterparts of EQUAL, NOT and
SYMBOLP and primitive type reasoning, to
Subgoal *1/4.4'''
(IMPLIES (AND (NOT (CDR (TRS_GT (CADR TRS_Z0PRIME)
TRS_Z1PRIME3)))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR (TRS_GT (CADR TRS_Z0PRIME)
TRS_Z1PRIME3))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME) TRS_Z1PRIME3)
(CADR TRS_Z0PRIME)
(LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME) TRS_Z1PRIME3)
TRS_Z0PRIME
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z0PRIME) and (CDR TRS_Z0PRIME) can be
eliminated. Furthermore, those terms are at the root of a chain of
two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace
TRS_Z0PRIME by (CONS TRS_Z0PRIME1 TRS_Z0PRIME2), (CAR TRS_Z0PRIME)
by TRS_Z0PRIME1 and (CDR TRS_Z0PRIME) by TRS_Z0PRIME2 and restrict
the type of the new variable TRS_Z0PRIME1 to be that of the term it
replaces. (2) Use CAR-CDR-ELIM, again, to replace TRS_Z0PRIME2 by
(CONS TRS_Z0PRIME3 TRS_Z0PRIME4), (CAR TRS_Z0PRIME2) by TRS_Z0PRIME3
and (CDR TRS_Z0PRIME2) by TRS_Z0PRIME4. These steps produce the
following goal.
Subgoal *1/4.4'4'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
(NOT (EQUAL TRS_Z0PRIME1 NIL))
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(NOT (CDR (TRS_GT TRS_Z0PRIME3 TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL (CAR (TRS_GT TRS_Z0PRIME3 TRS_Z1PRIME3))
'TRS_TRUE)
(EQUAL TRS_Z0PRIME1 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 TRS_Z1PRIME3)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 TRS_Z1PRIME3)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.4'5'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
TRS_Z0PRIME1
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(NOT (CDR (TRS_GT TRS_Z0PRIME3 TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL (CAR (TRS_GT TRS_Z0PRIME3 TRS_Z1PRIME3))
'TRS_TRUE)
(EQUAL TRS_Z0PRIME1 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 TRS_Z1PRIME3)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 TRS_Z1PRIME3)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME, TRS_ISBOOL
and TRS_ISSORT[A23], the :executable-counterparts of EQUAL, NOT and
SYMBOLP, primitive type reasoning, the :rewrite rules CAR-CONS and
CDR-CONS and the :type-prescription rules TRS_GT and TRS_ISSORT[A23],
to
Subgoal *1/4.4'6'
(IMPLIES (AND (NOT (CDR (TRS_GT TRS_Z0PRIME3 TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (CAR (TRS_GT TRS_Z0PRIME3 TRS_Z1PRIME3))
'TRS_TRUE)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 TRS_Z1PRIME3)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
We generalize this conjecture, replacing (TRS_GT TRS_Z0PRIME3 TRS_Z1PRIME3)
by L and restricting the type of the new variable L to be that of the
term it replaces, as established by TRS_GT. This produces
Subgoal *1/4.4'7'
(IMPLIES (AND (CONSP L)
(TRUE-LISTP L)
(NOT (CDR L))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (CAR L) 'TRS_TRUE)
(EQUAL (TRS_IFPRIME L
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
This simplifies, using the :definition TRUE-LISTP and the :executable-
counterpart of TRUE-LISTP, to
Subgoal *1/4.4'8'
(IMPLIES (AND (CONSP L)
(NOT (CDR L))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (CAR L) 'TRS_TRUE)
(EQUAL (TRS_IFPRIME L
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
The destructor terms (CAR L) and (CDR L) can be eliminated by using
CAR-CDR-ELIM to replace L by (CONS L1 L2), (CAR L) by L1 and (CDR L)
by L2 and restrict the type of the new variable L1 to be that of the
term it replaces. This produces the following goal.
Subgoal *1/4.4'9'
(IMPLIES (AND (SYMBOLP L1)
(NOT (EQUAL L1 T))
(NOT (EQUAL L1 NIL))
(CONSP (CONS L1 L2))
(NOT L2)
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL L1 'TRS_TRUE)
(EQUAL (TRS_IFPRIME (CONS L1 L2)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.4'10'
(IMPLIES (AND (SYMBOLP L1)
(NOT (EQUAL L1 T))
L1 (CONSP (CONS L1 L2))
(NOT L2)
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL L1 'TRS_TRUE)
(EQUAL (TRS_IFPRIME (CONS L1 L2)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
This simplifies, using the :executable-counterparts of CONS, CONSP,
EQUAL, NOT and SYMBOLP, to
Subgoal *1/4.4'11'
(IMPLIES (AND (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
Name the formula above *1.7.
Subgoal *1/4.3
(IMPLIES (AND (NOT (CDR (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(NOT (CONSP (CDR TRS_Z1PRIME)))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))
(CADR TRS_Z0PRIME)
(LIST 'TRS_S (CADR TRS_Z1PRIME)))
'(TRS_TRUE))
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT and TRS_IFPRIME, the
:executable-counterparts of CAR, CDR, CONS, CONSP, EQUAL, TRS_ISBOOL
and TRS_ISSORT[A23] and the :type-prescription rule TRS_ISSORT[A23],
to
Subgoal *1/4.3'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z1PRIME) and (CDR TRS_Z1PRIME) can be
eliminated by using CAR-CDR-ELIM to replace TRS_Z1PRIME by
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2), (CAR TRS_Z1PRIME) by TRS_Z1PRIME1
and (CDR TRS_Z1PRIME) by TRS_Z1PRIME2 and restrict the type of the
new variable TRS_Z1PRIME1 to be that of the term it replaces. This
produces the following goal.
Subgoal *1/4.3''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
(NOT (EQUAL TRS_Z1PRIME1 NIL))
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.3'''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
TRS_Z1PRIME1
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
This simplifies, using the :executable-counterparts of CONS, CONSP,
EQUAL, NOT and SYMBOLP, to
Subgoal *1/4.3'4'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME '(TRS_S (TRS_0)))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z0PRIME) and (CDR TRS_Z0PRIME) can be
eliminated. Furthermore, those terms are at the root of a chain of
two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace
TRS_Z0PRIME by (CONS TRS_Z0PRIME1 TRS_Z0PRIME2), (CAR TRS_Z0PRIME)
by TRS_Z0PRIME1 and (CDR TRS_Z0PRIME) by TRS_Z0PRIME2 and restrict
the type of the new variable TRS_Z0PRIME1 to be that of the term it
replaces. (2) Use CAR-CDR-ELIM, again, to replace TRS_Z0PRIME2 by
(CONS TRS_Z0PRIME3 TRS_Z0PRIME4), (CAR TRS_Z0PRIME2) by TRS_Z0PRIME3
and (CDR TRS_Z0PRIME2) by TRS_Z0PRIME4. These steps produce the
following goal.
Subgoal *1/4.3'5'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
(NOT (EQUAL TRS_Z0PRIME1 NIL))
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.3'6'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
TRS_Z0PRIME1
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME and
TRS_ISSORT[A23], the :executable-counterparts of CAR, CDR, EQUAL, NOT,
SYMBOLP, TRS_ISBOOL and TRS_ISSORT[A23], primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule TRS_ISSORT[A23], to
Subgoal *1/4.3'7'
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
Name the formula above *1.8.
Subgoal *1/4.2
(IMPLIES (AND (NOT (TRS_ISSORT[A23] (CADR TRS_Z1PRIME)))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))
(CADR TRS_Z0PRIME)
(LIST 'TRS_S (CADR TRS_Z1PRIME)))
'(TRS_TRUE))
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT and TRS_IFPRIME, the
:executable-counterparts of CAR, CONS, EQUAL, TRS_ISBOOL and TRS_ISSORT[A23]
and the :type-prescription rule TRS_ISSORT[A23], to
Subgoal *1/4.2'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z1PRIME) and (CDR TRS_Z1PRIME) can be
eliminated by using CAR-CDR-ELIM to replace TRS_Z1PRIME by
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2), (CAR TRS_Z1PRIME) by TRS_Z1PRIME1
and (CDR TRS_Z1PRIME) by TRS_Z1PRIME2 and restrict the type of the
new variable TRS_Z1PRIME1 to be that of the term it replaces. This
produces the following goal.
Subgoal *1/4.2''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
(NOT (EQUAL TRS_Z1PRIME1 NIL))
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.2'''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
TRS_Z1PRIME1
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
This simplifies, using the :executable-counterparts of CONS, CONSP,
EQUAL, NOT and SYMBOLP, to
Subgoal *1/4.2'4'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME '(TRS_S (TRS_0)))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z0PRIME) and (CDR TRS_Z0PRIME) can be
eliminated. Furthermore, those terms are at the root of a chain of
two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace
TRS_Z0PRIME by (CONS TRS_Z0PRIME1 TRS_Z0PRIME2), (CAR TRS_Z0PRIME)
by TRS_Z0PRIME1 and (CDR TRS_Z0PRIME) by TRS_Z0PRIME2 and restrict
the type of the new variable TRS_Z0PRIME1 to be that of the term it
replaces. (2) Use CAR-CDR-ELIM, again, to replace TRS_Z0PRIME2 by
(CONS TRS_Z0PRIME3 TRS_Z0PRIME4), (CAR TRS_Z0PRIME2) by TRS_Z0PRIME3
and (CDR TRS_Z0PRIME2) by TRS_Z0PRIME4. These steps produce the
following goal.
Subgoal *1/4.2'5'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
(NOT (EQUAL TRS_Z0PRIME1 NIL))
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.2'6'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
TRS_Z0PRIME1
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME and
TRS_ISSORT[A23], the :executable-counterparts of CAR, CDR, EQUAL, NOT,
SYMBOLP, TRS_ISBOOL and TRS_ISSORT[A23], primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule TRS_ISSORT[A23], to
Subgoal *1/4.2'7'
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
Name the formula above *1.9.
Subgoal *1/4.1
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME)
(CADR TRS_Z1PRIME))
(CADR TRS_Z0PRIME)
(LIST 'TRS_S (CADR TRS_Z1PRIME)))
'(TRS_TRUE))
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT and TRS_IFPRIME, the
:executable-counterparts of CAR, CONS, EQUAL, TRS_ISBOOL and TRS_ISSORT[A23]
and the :type-prescription rule TRS_ISSORT[A23], to
Subgoal *1/4.1'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z1PRIME) and (CDR TRS_Z1PRIME) can be
eliminated by using CAR-CDR-ELIM to replace TRS_Z1PRIME by
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2), (CAR TRS_Z1PRIME) by TRS_Z1PRIME1
and (CDR TRS_Z1PRIME) by TRS_Z1PRIME2 and restrict the type of the
new variable TRS_Z1PRIME1 to be that of the term it replaces. This
produces the following goal.
Subgoal *1/4.1''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
(NOT (EQUAL TRS_Z1PRIME1 NIL))
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.1'''
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
TRS_Z1PRIME1
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
This simplifies, using the :executable-counterparts of CONS, CONSP,
EQUAL, NOT and SYMBOLP, to
Subgoal *1/4.1'4'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME '(TRS_S (TRS_0)))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z0PRIME) and (CDR TRS_Z0PRIME) can be
eliminated. Furthermore, those terms are at the root of a chain of
two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace
TRS_Z0PRIME by (CONS TRS_Z0PRIME1 TRS_Z0PRIME2), (CAR TRS_Z0PRIME)
by TRS_Z0PRIME1 and (CDR TRS_Z0PRIME) by TRS_Z0PRIME2 and restrict
the type of the new variable TRS_Z0PRIME1 to be that of the term it
replaces. (2) Use CAR-CDR-ELIM, again, to replace TRS_Z0PRIME2 by
(CONS TRS_Z0PRIME3 TRS_Z0PRIME4), (CAR TRS_Z0PRIME2) by TRS_Z0PRIME3
and (CDR TRS_Z0PRIME2) by TRS_Z0PRIME4. These steps produce the
following goal.
Subgoal *1/4.1'5'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
(NOT (EQUAL TRS_Z0PRIME1 NIL))
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/4.1'6'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
TRS_Z0PRIME1
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME and
TRS_ISSORT[A23], the :executable-counterparts of CAR, CDR, EQUAL, NOT,
SYMBOLP, TRS_ISBOOL and TRS_ISSORT[A23], primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule TRS_ISSORT[A23], to
Subgoal *1/4.1'7'
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
Name the formula above *1.10.
Subgoal *1/3
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME)))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_FALSE))
(AND (EQ (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME) 'TRS_S))
(NOT (TRS_ISSORT[A23] (CADR TRS_Z1PRIME)))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] TRS_Z1PRIME))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture
to
Subgoal *1/3'
(IMPLIES (AND (CONSP (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(COND ((EQUAL 'TRS_TRUE
(CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
NIL))
((EQUAL 'TRS_FALSE
(CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
NIL))
(T NIL))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME))
(NOT (EQUAL (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_FALSE))
(EQUAL (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(NOT (TRS_ISSORT[A23] (CADR TRS_Z1PRIME)))
(TRS_ISSORT[A23] TRS_Z1PRIME))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT and TRS_ISSORT[A23],
the :executable-counterparts of CAR, CDR, CONSP and EQUAL, primitive
type reasoning, the :rewrite rules CAR-CONS and CDR-CONS and the :type-
prescription rule TRS_ISSORT[A23], to
Subgoal *1/3''
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(NOT (TRS_ISSORT[A23] (CADR TRS_Z1PRIME)))
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
This simplifies, using the :executable-counterparts of CAR and
TRS_ISSORT[A23], to
Subgoal *1/3'''
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(CONSP TRS_Z1PRIME)
(EQUAL 'TRS_0 (CAR TRS_Z1PRIME))
(NOT (CDR TRS_Z1PRIME)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z1PRIME) and (CDR TRS_Z1PRIME) can be
eliminated by using CAR-CDR-ELIM to replace TRS_Z1PRIME by
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2), (CAR TRS_Z1PRIME) by TRS_Z1PRIME1
and (CDR TRS_Z1PRIME) by TRS_Z1PRIME2 and restrict the type of the
new variable TRS_Z1PRIME1 to be that of the term it replaces. This
produces the following goal.
Subgoal *1/3'4'
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
(NOT (EQUAL TRS_Z1PRIME1 NIL))
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/3'5'
(IMPLIES (AND (SYMBOLP TRS_Z1PRIME1)
(NOT (EQUAL TRS_Z1PRIME1 T))
TRS_Z1PRIME1
(CONSP (CONS TRS_Z1PRIME1 TRS_Z1PRIME2))
(CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(EQUAL 'TRS_0 TRS_Z1PRIME1)
(NOT TRS_Z1PRIME2))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME
(LIST 'TRS_S
(CONS TRS_Z1PRIME1 TRS_Z1PRIME2)))
'(TRS_TRUE))).
This simplifies, using the :executable-counterparts of CONS, CONSP,
EQUAL, NOT and SYMBOLP, to
Subgoal *1/3'6'
(IMPLIES (AND (CONSP TRS_Z0PRIME)
(CONSP (CDR TRS_Z0PRIME))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME))
(NOT (CDDR TRS_Z0PRIME))
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME '(TRS_S (TRS_0)))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z0PRIME) and (CDR TRS_Z0PRIME) can be
eliminated. Furthermore, those terms are at the root of a chain of
two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace
TRS_Z0PRIME by (CONS TRS_Z0PRIME1 TRS_Z0PRIME2), (CAR TRS_Z0PRIME)
by TRS_Z0PRIME1 and (CDR TRS_Z0PRIME) by TRS_Z0PRIME2 and restrict
the type of the new variable TRS_Z0PRIME1 to be that of the term it
replaces. (2) Use CAR-CDR-ELIM, again, to replace TRS_Z0PRIME2 by
(CONS TRS_Z0PRIME3 TRS_Z0PRIME4), (CAR TRS_Z0PRIME2) by TRS_Z0PRIME3
and (CDR TRS_Z0PRIME2) by TRS_Z0PRIME4. These steps produce the
following goal.
Subgoal *1/3'7'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
(NOT (EQUAL TRS_Z0PRIME1 NIL))
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1/3'8'
(IMPLIES (AND (CONSP (CONS TRS_Z0PRIME3 TRS_Z0PRIME4))
(SYMBOLP TRS_Z0PRIME1)
(NOT (EQUAL TRS_Z0PRIME1 T))
TRS_Z0PRIME1
(CONSP (LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT TRS_Z0PRIME4)
(EQUAL TRS_Z0PRIME1 'TRS_S))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
(LIST* TRS_Z0PRIME1 TRS_Z0PRIME3 TRS_Z0PRIME4)
'(TRS_S (TRS_0)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME and
TRS_ISSORT[A23], the :executable-counterparts of CAR, CDR, EQUAL, NOT,
SYMBOLP, TRS_ISBOOL and TRS_ISSORT[A23], primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule TRS_ISSORT[A23], to
Subgoal *1/3'9'
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
Name the formula above *1.11.
Subgoal *1/2
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME)))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_FALSE))
(AND (EQ (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME) 'TRS_S))
(NOT (TRS_ISSORT[A23] (CADR TRS_Z0PRIME)))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] TRS_Z1PRIME))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture
to
Subgoal *1/2'
(IMPLIES (AND (CONSP (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(COND ((EQUAL 'TRS_TRUE
(CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
NIL))
((EQUAL 'TRS_FALSE
(CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
NIL))
(T NIL))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME))
(NOT (EQUAL (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_FALSE))
(EQUAL (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME) 'TRS_S)
(NOT (TRS_ISSORT[A23] (CADR TRS_Z0PRIME)))
(TRS_ISSORT[A23] TRS_Z1PRIME))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
But simplification reduces this to T, using the :definitions TRS_GT
and TRS_ISSORT[A23] and the :executable-counterparts of CDR, CONSP
and EQUAL.
Subgoal *1/1
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME)))
(EQ (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_FALSE)
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] TRS_Z1PRIME))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture
to
Subgoal *1/1'
(IMPLIES (AND (CONSP (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
(COND ((EQUAL 'TRS_TRUE
(CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
NIL))
((EQUAL 'TRS_FALSE
(CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
NIL))
(T NIL))
(TRS_ISSORT[A23] TRS_Z0PRIME)
(TRS_ISSORT[A23] (LIST 'TRS_S TRS_Z1PRIME))
(EQUAL (CAR (TRS_GT TRS_Z0PRIME TRS_Z1PRIME))
'TRS_FALSE)
(TRS_ISSORT[A23] TRS_Z1PRIME))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME TRS_Z1PRIME)
TRS_Z0PRIME (LIST 'TRS_S TRS_Z1PRIME))
'(TRS_TRUE))).
But simplification reduces this to T, using the :definitions TRS_GT,
TRS_IFPRIME, TRS_ISBOOL and TRS_ISSORT[A23], the :executable-counterparts
of CAR, EQUAL and TRS_ISBOOL, primitive type reasoning, the :rewrite
rules CAR-CONS and CDR-CONS and the :type-prescription rules TRS_GT
and TRS_ISSORT[A23].
So we now return to *1.11, which is
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
But the formula above is subsumed by *1.10, which we'll try to prove
later. We therefore regard *1.11 as proved (pending the proof of the
more general *1.10).
We next consider *1.10, which is
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
But the formula above is subsumed by *1.9, which we'll try to prove
later. We therefore regard *1.10 as proved (pending the proof of the
more general *1.9).
We next consider *1.9, which is
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
But the formula above is subsumed by *1.8, which we'll try to prove
later. We therefore regard *1.9 as proved (pending the proof of the
more general *1.8).
We next consider *1.8, which is
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
But the formula above is subsumed by *1.6, which we'll try to prove
later. We therefore regard *1.8 as proved (pending the proof of the
more general *1.6).
We next consider *1.7, which is
(IMPLIES (AND (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
Perhaps we can prove *1.7 by induction. Five induction schemes are
suggested by this conjecture. These merge into two derived induction
schemes. By considering those suggested by the largest number of non-
primitive recursive functions, we narrow the field to one.
We will induct according to a scheme suggested by
(TRS_IFPRIME (TRS_GT TRS_Z0PRIME3
(CONS 'TRS_S (CONS TRS_Z1PRIME3 'NIL)))
TRS_Z0PRIME3
(CONS 'TRS_S
(CONS (CONS 'TRS_S (CONS TRS_Z1PRIME3 'NIL))
'NIL))).
This suggestion was produced using the :induction rules TRS_GT,
TRS_IFPRIME and TRS_ISSORT[A23]. If we let (:P TRS_Z0PRIME3 TRS_Z1PRIME3)
denote *1.7 above then the induction scheme we'll use is
(AND (IMPLIES (NOT (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))))
(:P TRS_Z0PRIME3 TRS_Z1PRIME3))
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3))))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_FALSE))
(NOT (AND (EQ (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME3) 'TRS_S)))
T)
(:P TRS_Z0PRIME3 TRS_Z1PRIME3))
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3))))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_FALSE))
(AND (EQ (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME3) 'TRS_S))
(:P (CADR TRS_Z0PRIME3) TRS_Z1PRIME3))
(:P TRS_Z0PRIME3 TRS_Z1PRIME3))
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3))))
(EQ (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_FALSE))
(:P TRS_Z0PRIME3 TRS_Z1PRIME3))).
This induction is justified by the same argument used to admit TRS_IFPRIME.
When applied to the goal at hand the above induction scheme produces
six nontautological subgoals.
Subgoal *1.7/6
(IMPLIES (AND (NOT (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME and
TRS_ISSORT[A23], the :executable-counterparts of CAR, EQUAL and TRS_ISBOOL,
primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS
and the :type-prescription rules TRS_ISBOOL and TRS_ISSORT[A23], to
Subgoal *1.7/6'
(IMPLIES (AND (NOT (TRS_ISBOOL (TRS_GT (CADR TRS_Z0PRIME3)
TRS_Z1PRIME3)))
(CONSP TRS_Z0PRIME3)
(CONSP (CDR TRS_Z0PRIME3))
(EQUAL 'TRS_S (CAR TRS_Z0PRIME3))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME3))
(NOT (CDDR TRS_Z0PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME3)
TRS_Z1PRIME3)
(CADR TRS_Z0PRIME3)
(LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME3)
TRS_Z1PRIME3)
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
But simplification reduces this to T, using the :definitions TRS_IFPRIME
and TRS_ISBOOL, the :executable-counterpart of EQUAL, primitive type
reasoning and the :type-prescription rule TRS_GT.
Subgoal *1.7/5
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3))))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_FALSE))
(NOT (AND (EQ (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME3) 'TRS_S)))
T (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture
to
Subgoal *1.7/5'
(IMPLIES (AND (CONSP (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(COND ((EQUAL 'TRS_TRUE
(CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
NIL))
((EQUAL 'TRS_FALSE
(CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
NIL))
(T NIL))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
(NOT (EQUAL (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_FALSE))
(NOT (AND (EQUAL (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME3) 'TRS_S)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
But simplification reduces this to T, using the :definitions TRS_GT
and TRS_ISSORT[A23], the :executable-counterparts of CAR and EQUAL,
primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS
and the :type-prescription rules TRS_GT and TRS_ISSORT[A23].
Subgoal *1.7/4
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3))))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_FALSE))
(AND (EQ (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME3) 'TRS_S))
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME3)
(LIST 'TRS_S TRS_Z1PRIME3))
(CADR TRS_Z0PRIME3)
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture
to
Subgoal *1.7/4'
(IMPLIES (AND (CONSP (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(COND ((EQUAL 'TRS_TRUE
(CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
NIL))
((EQUAL 'TRS_FALSE
(CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
NIL))
(T NIL))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
(NOT (EQUAL (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_FALSE))
(EQUAL (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME3) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME3)
(LIST 'TRS_S TRS_Z1PRIME3))
(CADR TRS_Z0PRIME3)
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
But simplification reduces this to T, using the :definitions TRS_GT,
TRS_IFPRIME, TRS_ISBOOL and TRS_ISSORT[A23], the :executable-counterparts
of CAR, EQUAL and TRS_ISBOOL, primitive type reasoning, the :rewrite
rules CAR-CONS and CDR-CONS and the :type-prescription rules TRS_GT
and TRS_ISSORT[A23].
Subgoal *1.7/3
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3))))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_FALSE))
(AND (EQ (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME3) 'TRS_S))
(NOT (EQUAL (TRS_IFPRIME '(TRS_TRUE)
(CADR TRS_Z0PRIME3)
(LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture
to
Subgoal *1.7/3'
(IMPLIES (AND (CONSP (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(COND ((EQUAL 'TRS_TRUE
(CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
NIL))
((EQUAL 'TRS_FALSE
(CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
NIL))
(T NIL))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
(NOT (EQUAL (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_FALSE))
(EQUAL (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME3) 'TRS_S)
(NOT (EQUAL (TRS_IFPRIME '(TRS_TRUE)
(CADR TRS_Z0PRIME3)
(LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME and
TRS_ISSORT[A23], the :executable-counterparts of CAR, EQUAL and TRS_ISBOOL,
primitive type reasoning, the :rewrite rules CAR-CONS and CDR-CONS
and the :type-prescription rules TRS_GT and TRS_ISSORT[A23], to
Subgoal *1.7/3''
(IMPLIES (AND (NOT (CDR (TRS_GT (CADR TRS_Z0PRIME3)
TRS_Z1PRIME3)))
(CONSP TRS_Z0PRIME3)
(CONSP (CDR TRS_Z0PRIME3))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME3))
(NOT (CDDR TRS_Z0PRIME3))
(EQUAL (CAR (TRS_GT (CADR TRS_Z0PRIME3)
TRS_Z1PRIME3))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME3) 'TRS_S)
(NOT (EQUAL (TRS_IFPRIME '(TRS_TRUE)
(CADR TRS_Z0PRIME3)
(LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE)))
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME3)
TRS_Z1PRIME3)
(CADR TRS_Z0PRIME3)
(LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME3)
TRS_Z1PRIME3)
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
The destructor terms (CAR TRS_Z0PRIME3) and (CDR TRS_Z0PRIME3) can
be eliminated. Furthermore, those terms are at the root of a chain
of two rounds of destructor elimination. (1) Use CAR-CDR-ELIM to replace
TRS_Z0PRIME3 by (CONS TRS_Z0PRIME4 TRS_Z0PRIME5), (CAR TRS_Z0PRIME3)
by TRS_Z0PRIME4 and (CDR TRS_Z0PRIME3) by TRS_Z0PRIME5 and restrict
the type of the new variable TRS_Z0PRIME4 to be that of the term it
replaces. (2) Use CAR-CDR-ELIM, again, to replace TRS_Z0PRIME5 by
(CONS TRS_Z0PRIME6 TRS_Z0PRIME7), (CAR TRS_Z0PRIME5) by TRS_Z0PRIME6
and (CDR TRS_Z0PRIME5) by TRS_Z0PRIME7. These steps produce the
following goal.
Subgoal *1.7/3'''
(IMPLIES
(AND (CONSP (CONS TRS_Z0PRIME6 TRS_Z0PRIME7))
(SYMBOLP TRS_Z0PRIME4)
(NOT (EQUAL TRS_Z0PRIME4 T))
(NOT (EQUAL TRS_Z0PRIME4 NIL))
(CONSP (LIST* TRS_Z0PRIME4 TRS_Z0PRIME6 TRS_Z0PRIME7))
(NOT (CDR (TRS_GT TRS_Z0PRIME6 TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME6)
(NOT TRS_Z0PRIME7)
(EQUAL (CAR (TRS_GT TRS_Z0PRIME6 TRS_Z1PRIME3))
'TRS_TRUE)
(EQUAL TRS_Z0PRIME4 'TRS_S)
(NOT (EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE)))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME6 TRS_Z1PRIME3)
TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME6 TRS_Z1PRIME3)
(LIST* TRS_Z0PRIME4 TRS_Z0PRIME6 TRS_Z0PRIME7)
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1.7/3'4'
(IMPLIES
(AND (CONSP (CONS TRS_Z0PRIME6 TRS_Z0PRIME7))
(SYMBOLP TRS_Z0PRIME4)
(NOT (EQUAL TRS_Z0PRIME4 T))
TRS_Z0PRIME4
(CONSP (LIST* TRS_Z0PRIME4 TRS_Z0PRIME6 TRS_Z0PRIME7))
(NOT (CDR (TRS_GT TRS_Z0PRIME6 TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME6)
(NOT TRS_Z0PRIME7)
(EQUAL (CAR (TRS_GT TRS_Z0PRIME6 TRS_Z1PRIME3))
'TRS_TRUE)
(EQUAL TRS_Z0PRIME4 'TRS_S)
(NOT (EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE)))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME6 TRS_Z1PRIME3)
TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME6 TRS_Z1PRIME3)
(LIST* TRS_Z0PRIME4 TRS_Z0PRIME6 TRS_Z0PRIME7)
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME, TRS_ISBOOL
and TRS_ISSORT[A23], the :executable-counterparts of EQUAL, NOT and
SYMBOLP, primitive type reasoning, the :rewrite rules CAR-CONS and
CDR-CONS and the :type-prescription rules TRS_GT and TRS_ISSORT[A23],
to
Subgoal *1.7/3'5'
(IMPLIES
(AND (NOT (CDR (TRS_GT TRS_Z0PRIME6 TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME6)
(EQUAL (CAR (TRS_GT TRS_Z0PRIME6 TRS_Z1PRIME3))
'TRS_TRUE)
(NOT (EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE)))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME6 TRS_Z1PRIME3)
TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME6
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
We generalize this conjecture, replacing (TRS_GT TRS_Z0PRIME6 TRS_Z1PRIME3)
by L and restricting the type of the new variable L to be that of the
term it replaces, as established by TRS_GT. This produces
Subgoal *1.7/3'6'
(IMPLIES
(AND (CONSP L)
(TRUE-LISTP L)
(NOT (CDR L))
(TRS_ISSORT[A23] TRS_Z0PRIME6)
(EQUAL (CAR L) 'TRS_TRUE)
(NOT (EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE)))
(EQUAL (TRS_IFPRIME L
TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME6
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
This simplifies, using the :definition TRUE-LISTP and the :executable-
counterpart of TRUE-LISTP, to
Subgoal *1.7/3'7'
(IMPLIES
(AND (CONSP L)
(NOT (CDR L))
(TRS_ISSORT[A23] TRS_Z0PRIME6)
(EQUAL (CAR L) 'TRS_TRUE)
(NOT (EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE)))
(EQUAL (TRS_IFPRIME L
TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME6
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
The destructor terms (CAR L) and (CDR L) can be eliminated by using
CAR-CDR-ELIM to replace L by (CONS L1 L2), (CAR L) by L1 and (CDR L)
by L2 and restrict the type of the new variable L1 to be that of the
term it replaces. This produces the following goal.
Subgoal *1.7/3'8'
(IMPLIES
(AND (SYMBOLP L1)
(NOT (EQUAL L1 T))
(NOT (EQUAL L1 NIL))
(CONSP (CONS L1 L2))
(NOT L2)
(TRS_ISSORT[A23] TRS_Z0PRIME6)
(EQUAL L1 'TRS_TRUE)
(NOT (EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE)))
(EQUAL (TRS_IFPRIME (CONS L1 L2)
TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME6
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
By case analysis we reduce the conjecture to
Subgoal *1.7/3'9'
(IMPLIES
(AND (SYMBOLP L1)
(NOT (EQUAL L1 T))
L1 (CONSP (CONS L1 L2))
(NOT L2)
(TRS_ISSORT[A23] TRS_Z0PRIME6)
(EQUAL L1 'TRS_TRUE)
(NOT (EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE)))
(EQUAL (TRS_IFPRIME (CONS L1 L2)
TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME6 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME6
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
But simplification reduces this to T, using the :executable-counterparts
of CONS, CONSP, EQUAL, NOT and SYMBOLP.
Subgoal *1.7/2
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3))))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_FALSE))
(AND (EQ (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME3) 'TRS_S))
(NOT (TRS_ISSORT[A23] (CADR TRS_Z0PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture
to
Subgoal *1.7/2'
(IMPLIES (AND (CONSP (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(COND ((EQUAL 'TRS_TRUE
(CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
NIL))
((EQUAL 'TRS_FALSE
(CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
NIL))
(T NIL))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
(NOT (EQUAL (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_FALSE))
(EQUAL (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME3) 'TRS_S)
(NOT (TRS_ISSORT[A23] (CADR TRS_Z0PRIME3)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
But simplification reduces this to T, using the :definitions TRS_GT
and TRS_ISSORT[A23] and the :executable-counterparts of CDR, CONSP
and EQUAL.
Subgoal *1.7/1
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3))))
(EQ (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_FALSE)
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
By the simple :definitions EQ and TRS_ISBOOL we reduce the conjecture
to
Subgoal *1.7/1'
(IMPLIES (AND (CONSP (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
(COND ((EQUAL 'TRS_TRUE
(CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
NIL))
((EQUAL 'TRS_FALSE
(CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
NIL))
(T NIL))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] (LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
(EQUAL (CAR (TRS_GT TRS_Z0PRIME3
(LIST 'TRS_S TRS_Z1PRIME3)))
'TRS_FALSE)
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z1PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 (LIST 'TRS_S TRS_Z1PRIME3))
TRS_Z0PRIME3
(LIST 'TRS_S
(LIST 'TRS_S TRS_Z1PRIME3)))
'(TRS_TRUE))).
But simplification reduces this to T, using the :definitions TRS_GT,
TRS_IFPRIME, TRS_ISBOOL and TRS_ISSORT[A23], the :executable-counterparts
of CAR, EQUAL and TRS_ISBOOL, primitive type reasoning, the :rewrite
rules CAR-CONS and CDR-CONS and the :type-prescription rules TRS_GT
and TRS_ISSORT[A23].
That completes the proof of *1.7.
We therefore turn our attention to *1.6, which is
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
But the formula above is subsumed by *1.5, which we'll try to prove
later. We therefore regard *1.6 as proved (pending the proof of the
more general *1.5).
We next consider *1.5, which is
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
But the formula above is subsumed by *1.4, which we'll try to prove
later. We therefore regard *1.5 as proved (pending the proof of the
more general *1.4).
We next consider *1.4, which is
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
But the formula above is subsumed by *1.3, which we'll try to prove
later. We therefore regard *1.4 as proved (pending the proof of the
more general *1.3).
We next consider *1.3, which is
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
But the formula above is subsumed by *1.2, which we'll try to prove
later. We therefore regard *1.3 as proved (pending the proof of the
more general *1.2).
We next consider *1.2, which is
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
But the formula above is subsumed by *1.1, which we'll try to prove
later. We therefore regard *1.2 as proved (pending the proof of the
more general *1.1).
We next consider *1.1, which is
(IMPLIES (TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
Perhaps we can prove *1.1 by induction. Three induction schemes are
suggested by this conjecture. These merge into one derived induction
scheme.
We will induct according to a scheme suggested by
(TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0)) TRS_Z0PRIME3 '(TRS_S (TRS_0))).
This suggestion was produced using the :induction rules TRS_GT, TRS_IFPRIME
and TRS_ISSORT[A23]. If we let (:P TRS_Z0PRIME3) denote *1.1 above
then the induction scheme we'll use is
(AND (IMPLIES (NOT (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] '(TRS_S (TRS_0)))))
(:P TRS_Z0PRIME3))
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] '(TRS_S (TRS_0))))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_FALSE))
(NOT (AND (EQ (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME3) 'TRS_S)))
T)
(:P TRS_Z0PRIME3))
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] '(TRS_S (TRS_0))))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_FALSE))
(AND (EQ (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME3) 'TRS_S))
(:P (CADR TRS_Z0PRIME3)))
(:P TRS_Z0PRIME3))
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] '(TRS_S (TRS_0))))
(EQ (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_FALSE))
(:P TRS_Z0PRIME3))).
This induction is justified by the same argument used to admit TRS_IFPRIME.
When applied to the goal at hand the above induction scheme produces
five nontautological subgoals.
Subgoal *1.1/5
(IMPLIES (AND (NOT (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] '(TRS_S (TRS_0)))))
(TRS_ISSORT[A23] TRS_Z0PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
By the :executable-counterpart of TRS_ISSORT[A23] we reduce the conjecture
to
Subgoal *1.1/5'
(IMPLIES (AND (NOT (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
This simplifies, using the :definitions TRS_GT, TRS_IFPRIME and
TRS_ISSORT[A23], the :executable-counterparts of CAR, CDR, EQUAL, TRS_ISBOOL
and TRS_ISSORT[A23], primitive type reasoning and the :type-prescription
rules TRS_ISBOOL and TRS_ISSORT[A23], to
Subgoal *1.1/5''
(IMPLIES (AND (NOT (TRS_ISBOOL '(TRS_TRUE)))
(CONSP TRS_Z0PRIME3)
(CONSP (CDR TRS_Z0PRIME3))
(EQUAL 'TRS_S (CAR TRS_Z0PRIME3))
(TRS_ISSORT[A23] (CADR TRS_Z0PRIME3))
(NOT (CDDR TRS_Z0PRIME3)))
(EQUAL (TRS_IFPRIME '(TRS_TRUE)
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
But we reduce the conjecture to T, by the :executable-counterpart of
TRS_ISBOOL.
Subgoal *1.1/4
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] '(TRS_S (TRS_0))))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_FALSE))
(NOT (AND (EQ (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME3) 'TRS_S)))
T (TRS_ISSORT[A23] TRS_Z0PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
By the simple :definitions EQ and TRS_ISBOOL and the :executable-counterpart
of TRS_ISSORT[A23] we reduce the conjecture to
Subgoal *1.1/4'
(IMPLIES (AND (CONSP (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
(COND ((EQUAL 'TRS_TRUE
(CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
NIL))
((EQUAL 'TRS_FALSE
(CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
NIL))
(T NIL))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT (EQUAL (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_FALSE))
(NOT (AND (EQUAL (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME3) 'TRS_S))))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
But simplification reduces this to T, using the :definitions TRS_GT
and TRS_ISSORT[A23], the :executable-counterparts of CAR, CDR, EQUAL
and TRS_ISSORT[A23], primitive type reasoning and the :type-prescription
rule TRS_ISSORT[A23].
Subgoal *1.1/3
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] '(TRS_S (TRS_0))))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_FALSE))
(AND (EQ (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME3) 'TRS_S))
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME3) '(TRS_0))
(CADR TRS_Z0PRIME3)
'(TRS_S (TRS_0)))
'(TRS_TRUE))
(TRS_ISSORT[A23] TRS_Z0PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
By the simple :definitions EQ and TRS_ISBOOL and the :executable-counterpart
of TRS_ISSORT[A23] we reduce the conjecture to
Subgoal *1.1/3'
(IMPLIES (AND (CONSP (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
(COND ((EQUAL 'TRS_TRUE
(CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
NIL))
((EQUAL 'TRS_FALSE
(CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
NIL))
(T NIL))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT (EQUAL (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_FALSE))
(EQUAL (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME3) 'TRS_S)
(EQUAL (TRS_IFPRIME (TRS_GT (CADR TRS_Z0PRIME3) '(TRS_0))
(CADR TRS_Z0PRIME3)
'(TRS_S (TRS_0)))
'(TRS_TRUE)))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
But simplification reduces this to T, using the :definitions TRS_GT,
TRS_IFPRIME and TRS_ISSORT[A23], the :executable-counterparts of CAR,
CDR, CONSP, EQUAL, TRS_ISBOOL and TRS_ISSORT[A23], primitive type reasoning,
the :rewrite rules CAR-CONS and CDR-CONS and the :type-prescription
rule TRS_ISSORT[A23].
Subgoal *1.1/2
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] '(TRS_S (TRS_0))))
(NOT (EQ (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_FALSE))
(AND (EQ (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_TRUE)
(EQ (CAR TRS_Z0PRIME3) 'TRS_S))
(NOT (TRS_ISSORT[A23] (CADR TRS_Z0PRIME3)))
(TRS_ISSORT[A23] TRS_Z0PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
By the simple :definitions EQ and TRS_ISBOOL and the :executable-counterpart
of TRS_ISSORT[A23] we reduce the conjecture to
Subgoal *1.1/2'
(IMPLIES (AND (CONSP (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
(COND ((EQUAL 'TRS_TRUE
(CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
NIL))
((EQUAL 'TRS_FALSE
(CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
NIL))
(T NIL))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(NOT (EQUAL (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_FALSE))
(EQUAL (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_TRUE)
(EQUAL (CAR TRS_Z0PRIME3) 'TRS_S)
(NOT (TRS_ISSORT[A23] (CADR TRS_Z0PRIME3))))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
But simplification reduces this to T, using the :definitions TRS_GT
and TRS_ISSORT[A23] and the :executable-counterparts of CDR, CONSP
and EQUAL.
Subgoal *1.1/1
(IMPLIES (AND (AND (TRS_ISBOOL (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(TRS_ISSORT[A23] '(TRS_S (TRS_0))))
(EQ (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_FALSE)
(TRS_ISSORT[A23] TRS_Z0PRIME3))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
By the simple :definitions EQ and TRS_ISBOOL and the :executable-counterpart
of TRS_ISSORT[A23] we reduce the conjecture to
Subgoal *1.1/1'
(IMPLIES (AND (CONSP (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
(COND ((EQUAL 'TRS_TRUE
(CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
NIL))
((EQUAL 'TRS_FALSE
(CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0))))
(EQUAL (CDR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
NIL))
(T NIL))
(TRS_ISSORT[A23] TRS_Z0PRIME3)
(EQUAL (CAR (TRS_GT TRS_Z0PRIME3 '(TRS_0)))
'TRS_FALSE))
(EQUAL (TRS_IFPRIME (TRS_GT TRS_Z0PRIME3 '(TRS_0))
TRS_Z0PRIME3 '(TRS_S (TRS_0)))
'(TRS_TRUE))).
But simplification reduces this to T, using the :definitions TRS_GT,
TRS_IFPRIME and TRS_ISSORT[A23], the :executable-counterparts of CAR,
CDR, EQUAL, TRS_ISBOOL and TRS_ISSORT[A23], primitive type reasoning
and the :type-prescription rule TRS_ISSORT[A23].
That completes the proofs of *1.1 and *1.
Q.E.D.
Summary
Form: ( DEFTHM TEST ...)
Rules: ((:DEFINITION EQ)
(:DEFINITION NOT)
(:DEFINITION TRS_GT)
(:DEFINITION TRS_IFPRIME)
(:DEFINITION TRS_ISBOOL)
(:DEFINITION TRS_ISSORT[A23])
(:DEFINITION TRUE-LISTP)
(:ELIM CAR-CDR-ELIM)
(:EXECUTABLE-COUNTERPART CAR)
(:EXECUTABLE-COUNTERPART CDR)
(:EXECUTABLE-COUNTERPART CONS)
(:EXECUTABLE-COUNTERPART CONSP)
(:EXECUTABLE-COUNTERPART EQUAL)
(:EXECUTABLE-COUNTERPART NOT)
(:EXECUTABLE-COUNTERPART SYMBOLP)
(:EXECUTABLE-COUNTERPART TRS_ISBOOL)
(:EXECUTABLE-COUNTERPART TRS_ISSORT[A23])
(:EXECUTABLE-COUNTERPART TRUE-LISTP)
(:FAKE-RUNE-FOR-TYPE-SET NIL)
(:INDUCTION TRS_GT)
(:INDUCTION TRS_IFPRIME)
(:INDUCTION TRS_ISSORT[A23])
(:REWRITE CAR-CONS)
(:REWRITE CDR-CONS)
(:TYPE-PRESCRIPTION TRS_GT)
(:TYPE-PRESCRIPTION TRS_ISBOOL)
(:TYPE-PRESCRIPTION TRS_ISSORT[A23]))
Warnings: None
Time: 0.42 seconds (prove: 0.37, print: 0.05, other: 0.00)
TEST
ACL2 !>Bye.