Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
WolframInstitute`TuringMachine`InductiveProofs`
inductionProofGraph  |
|
| | ||||
▪
p is a proof association as returned by , , or .
FindInductiveProof
mergedProofFor
cachedProofFor
▪
Base-case and step-case token-event graphs are laid out side by side and joined through an induction node and a universally-quantified goal node.
▪
The following options can be given:
option | default | description | |
"GraftDerived" | True | graft each derived-axiom sub-proof onto its use site; False | |
"MergeAsAxiom" | False | color grafted use sites as axioms rather than derived theorems | |
"LemmaComponents" | All | which lemma-case components to include |
▪
Vertices carry equation-box or event-disc shapes; use for a laid-out, styled rendering.
proofGraph
Examples
(1)
Basic Examples
(1)
Build the proof graph for the binary-incrementer machine 453:
In[1]:=
 | inductionProofGraph |
 | cachedProofFor |
Out[1]=
 |
|
""