Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
WolframInstitute`TuringMachine`InductiveProofs`
FindInductiveProof  |
| | |||||
|
| | ||||
▪
goal is an between two tape terms mentioning the induction variable ; axioms is a list of equational axioms (each an or a over one).
Equal
n
Equal
ForAll
▪
The base case () and the step case (, with goal itself added as the induction hypothesis) are each proved with the built-in .
nzero
nsucc[n]
FindEquationalProof
▪
The result is an association with keys , , , , , , , , and . is only when both cases produced a .
"Valid"
"Goal"
"InductionVariable"
"Axioms"
"BaseGoal"
"StepGoal"
"IH"
"BaseProof"
"StepProof"
"Valid"
True
ProofObject
▪
t defaults to 30 seconds.
Examples
(2)
Basic Examples
(1)
Prove that a one-cell-longer run of ones equals the run with a appended:
s1
In[1]:=
proof=
[ones[succ[n],y]seq[ones[n,y],s1],{ForAll[y,ones[zero,y]y],ForAll[{m,y},ones[succ[m],y]seq[ones[m,y],s1]]},20];proof["Valid"]
 | FindInductiveProof |
Out[1]=
True
Scope
(1)
 |
|
 |
|
""