Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
WolframInstitute`TuringMachine`InductiveProofs`
mergedProofFor  |
|
| | ||||
▪
ru is a machine number; its state/color shape is looked up internally.
▪
Each strategy derives its own behavioral lemmas (carry, absorb, tail-peel, scan, flip) rather than assuming them, and hands the assembled goal and axioms to .
FindInductiveProof
▪
The result is the same association shape returned by , extended with a key holding the sub-proofs. If no strategy succeeds, the last failure is returned.
FindInductiveProof
"LemmaProofs"
▪
cachedProofFor
Examples
(1)
Basic Examples
(1)
Derive the proof for the binary-incrementer machine 453:
In[1]:=
 | mergedProofFor |
Out[1]=
True
 |
|
 |
|
""