1. Introduction
This webpage describes an initial proof checker for axiomatic language.
For background see this
axiomtic language overview or this
webpage on proof.
This proof checker is defined for and is written in a
restricted form of axiomatic language
called SAL - Simplified Axiomatic Language.
Queries in SAL give the steps of a proof and their successful execution
confirms that the proof is correct.
The sections below give an overview of the system.
Future work will add some inference rules to handle proof-by-contradiction.
2. GAL / SAL / PAL - Forms of Axiomatic Language
In regular axiomatic language, called General Axiomatic Language - GAL,
string variables can occur anywhere within a sequence.
This enables one-line definitions of some common list predicates:
(member %x ($1 %x $2)).
(concat ($1) ($2) ($1 $2)).
(append1 ($) %x ($ %x)). ! append one expr to end of sequence
Example valid expressions generated by these axioms include
(member %x ($1 %x $2)), (member %x ($1a %1 $1b %x $2a $2b),
and (append1 ($1 % $2) %x ($1 % $2 %x)).
But unification with unrestricted string variables can have multiple
most-general solutions, such as unifying ($ a) with (a $) or unifying
($1 $) with ($ $2).
In SAL - Simplified Axiomatic Language, we restrict string variables
to the ends of sequences. The above list predicates would be defined
by the following SAL axioms:
(member %x (%x $)).
(member %x (% $))< (member %x ($)).
(concat () ($) ($)).
(concat (% $1) %2 (% $12))< (concat ($1) %2 ($12)).
(append1 () %x (%x)).
(append1 (% $) %x (% $'))< (append1 ($) %x ($')).
Valid expressions for these SAL axioms include (member %x (%1 %2 %x $)),
(concat (%1 %2 %3) ($2) (%1 %2 %3 $2)), and (append1 (%1 %2) %x (%1 %2 %x)).
Note that in SAL expressions, string variables are analogous to list
tail variables in Prolog:
SAL Prolog
(a %X $Z) [a, X | Z]
In SAL, unification has a single most-general result, or it fails.
This means we can have a Prolog-like top-down resolution solver for
SAL predicates, which is what has been done for this proof checker.
Note that this is *not* an implementation of (GAL) axiomatic language,
which requires automatic transformation of high-level specifications.
For example, higher-order forms in SAL axioms can easily lead to
non-termination of the solver. Axioms for a program in SAL must
be carefully written to achieve efficiency.
For internal processing of axiomatic language,
it is possible to get even simpler.
In PAL - Primitive Axiomatic Language, sequences are replaced by pairs
and there are no string variables. The PAL definition of the member
predicate is as follows:
(` (`member (%x ((` (%x %$)) `)))).
(` (`member (%x ((` (% %$)) `))))< (` (`member (%x ((` %$) `)))).
(Here we use an atom for the predicate name to avoid the complexity of
syntax extension symbols. Note our use of the atom ` when representing
SAL sequences in PAL.)
PAL is used for data representation and processing inside the proof checker.
3. Encoding Axioms and Clauses
In order to write axioms and valid clauses that must be processed
as data, we need an encoding. (To process variables, for example,
they can't be real variables. They must be ground expressions.)
The syntax extensions of axiomatic language are helpful here.
We let atoms, variables, and syntax extension symbols be
represented by syntax extension symbols with a prepended underscore:
actual tokens encoded tokens
`x _`x -- atoms
%a _%a -- expression vars
$1 _$1 -- string vars
abc _abc -- syntax extension symbols
An encoded axiom/clause is just a sequence of its encoded conclusion
and condition expressions.
An encoding of the axioms for natural numbers (with atoms for the
zero and successor symbols) is as follows:
((_num _`0))
((_num (_`s _%)) (_num _%))
4. The Check Predicate
A proof is defined in a "check" predicate which is then executed as
an SAL query.
A successful query solution indicates that the proof is correct.
The format of the check predicate is informally sketched as follows:
(check
(.. (#lbl# #ax#)..) - labeled encoded SAL axioms in "original" set
-- all valid clauses are proved wrt to these original axioms
-- this original ax set has the ax set name _ (underscore)
(..#chk_step#..) - sequence of "check steps"
-- these steps prove new valid clauses and equivalent axiom sets
(..(#lbl# #axlblseq#)..) - output list of equivalent axiom sets
-- we list each axiom set name label and the labels of its axioms
(..(#lbl# #vcP#)..) - output list of labeled valid clauses as PAL
-- (Note that valid clauses in PAL form are not very readable!)
)
#chk_step# =
(#lbl# #clause to prove# ..infer_proof..)
| (#lbl# #clause to prove# ..induc_proof..)
| (_axset #new ax set label# #lbls of axioms in new ax set#
-- axioms in new ax set must already be proved valid wrt original ax set
..(#orig ax lbl# #orig ax# ..proof..)..
-- each orig axiom not in the new set must be prove valid wrt new ax set
)
..infer_proof.. = #vc_lbl# {#cond# #vc_lbl# | #cond_perm/add#}
#vc_lbl# = label of an existing valid clause (axiom or previously proved)
-- The first #vc_lbl# initializes the "current valid clause".
Each subsequent infer_proof step modifies this clause.
#cond# = decimal symbol index of a current valid clause condition (1 .. n)
-- This condition is unfolded against the conclusion of the next #vc_lbl#,
which produces a new current valid clause.
#cond_perm/add# = sequence of permuted decimal condition numbers with an
optional _ underscore inserted for each added condition at that position.
The modified clause becomes the new current valid clause.
This inference proof step implements the inference rules that a
permutation of the conditions of a valid clause gives a valid clause
and that adding conditions to a valid clause gives a valid clause.
-- At the end of the infer_proof we check that the #clause to prove# is
an instance of the current valid clause.
..induc_proof.. = _induc #cond# #axsetlbl#
..(#lblprefix_axlbl# #resulting clause to prove# ..proof..)..
-- An induction proof step begins with the keyword '_induc'.
We unfold the #cond# condition of the #clause to prove#
against the specified set of axioms #axsetlbl#
(which would be _ to unfold against the original axiom set).
For each successful unfold, the resulting clause is given and
has a label with an arbitrary prefix followed by the label of the
axiom that produced that resulting clause. A proof of this
resulting clause is given, which may be an inference proof or
another induction proof. For an unfold step in an inference
proof, we may unfold against the #clause to prove# in addition
to already proved valid clauses.
5. Example Proofs
This section gives example proofs that are actual executions of the
check predicate using the SAL query solver.
Double-hyphen -- comments have been inserted into the query solver output
to add to the axiomatic language comments that start with !.
We use single letter predicate names n,p below in place of longer symbol names
num,plus for conciseness.
5.1. Natural Numbers
These examples give the labeled axioms n0,n1 for natural numbers:
n0 (`n `0). ! zero is a natural number
n1 (`n (`s %))< (`n %). ! if n is a nat num, so is succ(n)
Here we use atoms for all symbols to make the final valid clause PAL
output more consise.
These axioms n0,n1 are our initial valid expressions.
Replacing the variable in n1 with the atom `x gives valid clause nx,
an instance of n1:
nx (`n (`s `x))< (`n `x). ! an instance of n1, so nx is valid
Unfolding valid clause n1's condition 1 with itself gives this valid
clause n2:
n2 (`n (`s (`s %)))< (`n %). ! if n is num, then so is n+2
The complete query and its output shows these two inference proofs:
%lvcP < ! final set of valid clauses is displayed as query output
(check
( ! labeled axioms for natural numbers:
(n0 ((_`n _`0))) ! 0 is a natural number
(n1 ((_`n (_`s _%)) (_`n _%))) ! if n is nat num, n+1 is nat num
) ! - note atoms for set predicate name and zero, successor symbols
! (leading _ means atoms and vars represented by syntax extension symbols
( ! some simple valid clause inference proof steps to be checked:
(nx ((_`n (_`s _`x)) (_`n _`x)) n1)
! - clause nx is just an instance of axiom n1
(n2 ((_`n (_`s (_`s _%))) (_`n _%)) n1 1 n1) ! if n is nat num, so is n+2
! - n2 is proved by unfolding n1 (cond 1) with itself
) %laxsl %lvcP).
SOLUTIONS:
((n0 (((atom ()) ((atom "n") ((atom "0") (atom ())))))) (n1 (((atom ()) ((
atom "n") (((atom ()) ((atom "s") ((var "%") (atom ())))) (atom ())))) ((
atom ()) ((atom "n") ((var "%") (atom ())))))) (nx (((atom ()) ((atom "n")
(((atom ()) ((atom "s") ((atom "x") (atom ())))) (atom ())))) ((atom ()) ((
atom "n") ((atom "x") (atom ())))))) (n2 (((atom ()) ((atom "n") (((atom ()
) ((atom "s") (((atom ()) ((atom "s") ((var "%") (atom ())))) (atom ()))))
(atom ())))) ((atom ()) ((atom "n") ((var "%") (atom ())))))))
-- the output shows the internal PAL representation for the
valid clauses n0,n1,nx,n2
time, #solns: 0.06 1
-- execution time was .06 seconds, with just one query solution found
-- failure to get a solution would mean an error in the proof!
max stack size, max solve fn depth, # occur chks: 175257 5955 81329
-- these internal calculation parameters can be ignored
Note that the binary-tree PAL output with all its nested parentheses is
pretty much unreadable, but a user of this proof checker would really need
to deal with only encoded SAL input.
This next example uses single-letter syntax extension symbols n,0,s,
which results in a much more voluminous valid clause PAL output, since
the bit atoms for the different characters are displayed.
In this example, our inference proof unfolds n1 condition 1 with itself to
produce n2 as the "current valid clause", which then has its condition 1
unfolded with valid clause n0 to produce the unconditional valid clause
n2ve = (n (s (s 0)))., which generates the valid expression (n (s (s 0))),
or "two is a natural number".
(%laxsl %lvcP) <
(check
( ! labeled axioms for natural numbers:
(n0 ((_n _0))) ! 0 is a natural number
(n1 ((_n (_s _%)) (_n _%))) ! if n is nat num, n+1 is nat num
)
( ! a simple valid clause inference proof to be checked:
(n2ve ((_n (_s (_s _0)))) n1 1 n1 1 n0) ! 2 is a nat num
! - Successive unfolds can produce unconditional valid clauses
! representing valid expressions.
) %laxsl %lvcP).
SOLUTIONS:
(((_ (n0 n1))) ((n0 (((atom ()) (((atom ()) ((atom ()) (((atom ()) (((atom ()
) ((atom "char") (((atom ()) ((atom "0") ((atom "1") ((atom "1") ((atom "0"
) ((atom "1") ((atom "1") ((atom "1") ((atom "0") (atom ())))))))))) (atom
())))) (atom ()))) (atom ())))) (((atom ()) ((atom ()) (((atom ()) (((atom
()) ((atom "char") (((atom ()) ((atom "0") ((atom "0") ((atom "1") ((atom
"1") ((atom "0") ((atom "0") ((atom "0") ((atom "0") (atom ())))))))))) (
atom ())))) (atom ()))) (atom ())))) (atom ())))))) (n1 (((atom ()) (((atom
()) ((atom ()) (((atom ()) (((atom ()) ((atom "char") (((atom ()) ((atom
"0") ((atom "1") ((atom "1") ((atom "0") ((atom "1") ((atom "1") ((atom "1"
) ((atom "0") (atom ())))))))))) (atom ())))) (atom ()))) (atom ())))) (((
atom ()) (((atom ()) ((atom ()) (((atom ()) (((atom ()) ((atom "char") (((
atom ()) ((atom "0") ((atom "1") ((atom "1") ((atom "1") ((atom "0") ((atom
"0") ((atom "1") ((atom "1") (atom ())))))))))) (atom ())))) (atom ()))) (
atom ())))) ((var "%") (atom ())))) (atom ())))) ((atom ()) (((atom ()) ((
atom ()) (((atom ()) (((atom ()) ((atom "char") (((atom ()) ((atom "0") ((
atom "1") ((atom "1") ((atom "0") ((atom "1") ((atom "1") ((atom "1") ((
atom "0") (atom ())))))))))) (atom ())))) (atom ()))) (atom ())))) ((var
"%") (atom ())))))) (n2ve (((atom ()) (((atom ()) ((atom ()) (((atom ()) ((
(atom ()) ((atom "char") (((atom ()) ((atom "0") ((atom "1") ((atom "1") ((
atom "0") ((atom "1") ((atom "1") ((atom "1") ((atom "0") (atom ())))))))))
) (atom ())))) (atom ()))) (atom ())))) (((atom ()) (((atom ()) ((atom ())
(((atom ()) (((atom ()) ((atom "char") (((atom ()) ((atom "0") ((atom "1")
((atom "1") ((atom "1") ((atom "0") ((atom "0") ((atom "1") ((atom "1") (
atom ())))))))))) (atom ())))) (atom ()))) (atom ())))) (((atom ()) (((atom
()) ((atom ()) (((atom ()) (((atom ()) ((atom "char") (((atom ()) ((atom
"0") ((atom "1") ((atom "1") ((atom "1") ((atom "0") ((atom "0") ((atom "1"
) ((atom "1") (atom ())))))))))) (atom ())))) (atom ()))) (atom ())))) (((
atom ()) ((atom ()) (((atom ()) (((atom ()) ((atom "char") (((atom ()) ((
atom "0") ((atom "0") ((atom "1") ((atom "1") ((atom "0") ((atom "0") ((
atom "0") ((atom "0") (atom ())))))))))) (atom ())))) (atom ()))) (atom ())
))) (atom ())))) (atom ())))) (atom ()))))))))
-- The initial output gives the list of "equivalent" axiom sets.
In this case we just have the original axiom set, which has
label _ and contains axioms n0 n1.
-- After the equivalent axiom sets list we have the dump of PAL
valid clauses n0,n1,n2ve, which includes the bit atoms of
the symbol characters.
time, #solns: 0.50 1
max stack size, max solve fn depth, # occur chks: 404750 14282 1793667
5.2. "Q" Numbers
These examples give axioms for "q-numbers", where a q-number is
just a natural number with predicate name "q".
Given natural number axioms n0,n1, q-numbers can be defined by
this added qn axiom,
qn (q %)< (n %). ! every nat num is a q-num
or by these alternative axioms q0,q1:
q0 (q 0). ! zero is a q-number
q1 (q (s %))< (q %). ! if n is a q-num, so is n+1
This first example proof below starts with original
axiom set _ = n0,n1,qn,
then proves that q0,q1 are valid clauses wrt axiom set n0,n1,qn,
and then in the _axset definition step shows that original axiom qn
is a valid clause wrt alternative axiom set NQ = n0,n1,q0,q1,
which makes axiom sets _ and NQ equivalent. Note the induction proofs!
(%laxsl %vclbls) < -- we output just vc labels instead of entire clauses
(check
( ! axioms for natural numbers and "q" numbers:
(n0 ((_n _0))) ! 0 is a natural number
(n1 ((_n (_s _%)) (_n _%))) ! if n is nat num, n+1 is nat num
(qn ((_q _%) (_n _%))) ! every nat num is a "q-num"
) ! - original axioms n0,n1,qn have ax set label _
( ! some simple valid clause proof steps to be checked:
(q0 ((_q _0)) qn 1 n0) ! q0 derives from qn unfolded with n0
(q1 ((_q (_s _%)) (_q _%)) _induc 1 _ ! unfold against orig ax set n0,n1,qn
(q1_qn ((_q (_s _%)) (_n _%)) qn 1 n1)
! - q1 is proved by induction of its cond 1 against axiom qn
) ! (the resulting clause q1_qn is shown valid by unfolding qn with n1)
-- The label suffix _qn shows that this clause is the result of
unfolding with original ax set axiom qn.
(_axset NQ (n0 n1 q0 q1) ! define equivalent ax set
(qn ((_q _%) (_n _%)) _induc 1 NQ ! induction on new ax set n0,n1,q0,q1
(qn_n0 ((_q _0)) q0) ! = valid clause q0
(qn_n1 ((_q (_s _%)) (_n _%)) q1 1 qn) ! = unfold q1 with induc hyp qn
! - Note we can unfold valid clause q1 against induction hypothesis qn
! to prove qn!
)
) ! thus ax set n0,n1,qn is valid wrt new ax set n0,n1,q0,q1
-- and thus the two axiom sets are equivalent!
) %laxsl %lvcP),
(transpose %lvcP (%vclbls %vcP)). -- transpose step separates the vc labels!
SOLUTIONS:
(((_ (n0 n1 qn)) (NQ (n0 n1 q0 q1))) (n0 n1 qn q0 q1))
-- our list of equivalent axiom sets shows both sets: _ and NQ
-- following that are the labels for all the valid clauses,
which are valid with respect to both (equivalent) axiom sets
time, #solns: 4.52 1
max stack size, max solve fn depth, # occur chks: 1016492 36992 3509808
This next example proves the q-num axiom sets equivalent, but in the
other direction. That is, we start with original axioms n0,n1,q0,q1
and then show that alternative axiom set n0,n1,qn is equivalent.
(%laxsl %vclbls) <
(check
( ! axioms for natural numbers and "q" numbers:
(n0 ((_n _0))) ! 0 is a natural number
(n1 ((_n (_s _%)) (_n _%))) ! if n is nat num, n+1 is nat num
(q0 ((_q _0))) ! 0 is a q-num
(q1 ((_q (_s _%)) (_q _%))) ! if n is a q-num, n+1 is q-num
)
(
(qn ((_q _%) (_n _%)) _induc 1 _ ! induction on orig ax set n0,n1,q0,q1
(qn_n0 ((_q _0)) q0) ! = valid clause q0
(qn_n1 ((_q (_s _%)) (_n _%)) q1 1 qn) ! = unfold of q1 with induc hyp qn
! - Note that we can unfold valid clause against induction hypothesis qn
! to prove qn!
)
(_axset QN (n0 n1 qn) ! define equiv ax set
(q0 ((_q _0)) qn 1 n0)
(q1 ((_q (_s _%)) (_q _%)) _induc 1 QN
(q1_qn ((_q (_s _%)) (_n _%)) qn 1 n1) )
)
) %laxsl %lvcP),
(transpose %lvcP (%vclbls %vcP)).
SOLUTIONS:
(((_ (n0 n1 q0 q1)) (QN (n0 n1 qn))) (n0 n1 q0 q1 qn))
time, #solns: 4.54 1
max stack size, max solve fn depth, # occur chks: 1093990 40023 3491281
5.3. Natural Number Addition
Natural number addition (the "plus" function) can be defined by
the following axioms, in addition to n0,n1:
p0 (p 0 % %)< (n %). ! 0 plus n = n
p1 (p (s %1) %2 (s %3)< (p %1 %2 %3). ! n1 + n2 = n3 => n1+1 + n2 = n3+1
These axioms do induction on the first argument. An alternative definition
of plus would be axioms n0,n1,pa0,pa1, which do induction on the second
argument:
pa0 (p % 0 %)< (n %). ! n plus 0 = n
pa1 (p %1 (s %2) (s %3)< (p %1 %2 %3). ! n1 + n2 = n3 => n1 + n2+1 = n3+1
This example proves that these two axiom sets are equivalent:
(%laxsl %vclbls) < (check
( ! axioms for natural numbers and their addition:
(n0 ((_n _0)))
(n1 ((_n (_s _%)) (_n _%)))
(p0 ((_p _0 _% _%) (_n _%))) ! (induction on 1st arg)
(p1 ((_p (_s _%1) _%2 (_s _%3)) (_p _%1 _%2 _%3)))
)
( ! prove clauses pa0,pa1 valid wrt n0,n1,p0,p1:
(pa0 ((_p _% _0 _%) (_n _%)) _induc 1 _
(pa0_n0 ((_p _0 _0 _0)) p0 1 n0)
(pa0_n1 ((_p (_s _%) _0 (_s _%)) (_n _%)) p1 1 pa0)
)
(pa1 ((_p _%1 (_s _%2) (_s _%3)) (_p _%1 _%2 _%3)) _induc 1 _
(pa1_p0 ((_p _0 (_s _%) (_s _%)) (_n _%)) p0 1 n1)
(pa1_p1 ((_p (_s _%1) (_s _%2) (_s (_s _%3))) (_p _%1 _%2 _%3)) p1 1 pa1)
)
(_axset PA (n0 n1 pa0 pa1) ! define equiv ax set
! prove original axioms p0,p1 valid wrt alternate axiom set PA
(p0 ((_p _0 _% _%) (_n _%)) _induc 1 PA
(p0_n0 ((_p _0 _0 _0)) pa0 1 n0)
(p0_n1 ((_p _0 (_s _%) (_s _%)) (_n _%)) pa1 1 p0)
)
(p1 ((_p (_s _%1) _%2 (_s _%3)) (_p _%1 _%2 _%3)) _induc 1 PA
(p1_pa0 ((_p (_s _%) _0 (_s _%)) (_n _%)) pa0 1 n1)
(p1_pa1 ((_p (_s _%1) (_s _%2) (_s (_s _%3))) (_p _%1 _%2 _%3)) pa1 1 p1)
)
)
) %laxsl %lvcP),
(transpose %lvcP (%vclbls %vcP)).
SOLUTIONS:
(((_ (n0 n1 p0 p1)) (PA (n0 n1 pa0 pa1))) (n0 n1 p0 p1 pa0 pa1))
time, #solns: 10.42 1
max stack size, max solve fn depth, # occur chks: 3177582 115468 18227102
5.4. Commutativity of Addition!
To express commutativity of addition we need the following utility
predicate that asserts that two expressions are identical:
id (== % %). ! relation arguments are identical
We prove below this valid clause that asserts that if two expressions are
identical then their "successors" are identical:
ids (== (s %a) (s %b))< (== %a %b).
The commutativity of addition is expressed by proving the following
clause valid:
com (== %3a %3b)< (p %1 %2 %3a), (p %2 %1 %3b).
In order for this clause to be valid, the two additions, which have their
arguments in opposite order, must always give identical results for
all argument %1,%2 values.
Our commutativity proof below starts with original axiom set
n0,n1,p0,p1,id, then defines and proves equivalent axiom set
n0,n1,pa0,pa1,id, then proves the id "successor" valid clause,
and finally proves the commutativity valid clause.
! Proof of commutativity!
Addition_is_Commutative <
(check
( ! axioms for natural numbers and their addition:
(n0 ((_n _0)))
(n1 ((_n (_s _%)) (_n _%)))
(p0 ((_p _0 _% _%) (_n _%)))
(p1 ((_p (_s _%1) _%2 (_s _%3)) (_p _%1 _%2 _%3)))
(id ((_== _% _%))) ! identical expressions predicate
)
( ! prove commutativity of addition ...
! first we prove equivalent axioms pa0,pa1,
! then we prove id successor valid clause ids,
! finally we prove the commutativity valid clause.
! prove alternative addition clauses pa0,pa1 valid wrt n0,n1,p0,p1,id:
(pa0 ((_p _% _0 _%) (_n _%)) _induc 1 _
(pa0_n0 ((_p _0 _0 _0)) p0 1 n0)
(pa0_n1 ((_p (_s _%) _0 (_s _%)) (_n _%)) p1 1 pa0)
)
(pa1 ((_p _%1 (_s _%2) (_s _%3)) (_p _%1 _%2 _%3)) _induc 1 _
(pa1_p0 ((_p _0 (_s _%) (_s _%)) (_n _%)) p0 1 n1)
(pa1_p1 ((_p (_s _%1) (_s _%2) (_s (_s _%3))) (_p _%1 _%2 _%3)) p1 1 pa1)
)
(_axset PA (n0 n1 pa0 pa1 id) ! define alt. addition ax as equiv
! prove orig addition axioms p0,p1 valid wrt alt ax PA = n0,n1,pa0,pa1,id
(p0 ((_p _0 _% _%) (_n _%)) _induc 1 PA
(p0_n0 ((_p _0 _0 _0)) pa0 1 n0)
(p0_n1 ((_p _0 (_s _%) (_s _%)) (_n _%)) pa1 1 p0)
)
(p1 ((_p (_s _%1) _%2 (_s _%3)) (_p _%1 _%2 _%3)) _induc 1 PA
(p1_pa0 ((_p (_s _%) _0 (_s _%)) (_n _%)) pa0 1 n1)
(p1_pa1 ((_p (_s _%1) (_s _%2) (_s (_s _%3))) (_p _%1 _%2 _%3)) pa1 1 p1) )
)
! prove this "id successor" valid clause
(ids ((_== (_s _%a) (_s _%b)) (_== _%a _%b)) _induc 1 _
(ids_id ((_== (_s _%) (_s _%))) id)
)
! now prove the commutativity clause:
(com ((_== _%3a _%3b) (_p _%1 _%2 _%3a) (_p _%2 _%1 _%3b)) _induc 1 _
(com1_p0 ((_== _% _%3b) (_n _%) (_p _% _0 _%3b)) _induc 2 PA
(com12_pa0 ((_== _% _%) (_n _%) (_n _%)) id (_ _))
)
(com1_p1 ((_== (_s _%3a') _%3b)
(_p _%1' _%2 _%3a') (_p _%2 (_s _%1') _%3b)) _induc 2 PA
(com12_pa1 ((_== (_s _%3a') (_s _%3b'))
(_p _%1' _%2 _%3a') (_p _%2 _%1' _%3b')) ids 1 com)
)
)
) %laxsl %lvcP).
SOLUTIONS:
Addition_is_Commutative
time, #solns: 19.68 1
max stack size, max solve fn depth, # occur chks: 4919353 179252 28177368
back
to Axiomatic Language Home Page