Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
WolframInstitute`TuringMachine`InductiveProofs`
MultiwayInductiveProofPanel  |
|
| | ||||
▪
The proof graph (from ) is placed inside the sub-proof cones (from ) so the proof is shown as a path through the surrounding rewrite space.
inductionProofGraph
multiwaySubProofCones
▪
The following options can be given:
option | default | description | |
"GraftDerived" | True | graft each derived-axiom sub-proof into the proof graph | |
"PinProof" | True | pin the proof at its own layout while the cloud arranges around it | |
"BackgroundOpacity" | 0.25 | opacity of the faded cloud | |
"CloudCore" | 2 | keep only the k-core of the cloud, dropping splaying tendrils | |
"MaxStates" | 500 | total cloud-state cap | |
"DirectOverlap" | False | grow "MaxStates" | |
"SizeBound" | Automatic | confine the cloud to the proof's term-size regime | |
"Labeled" | False | draw labelled proof vertices instead of discs | |
"Layout" | "SpringElectricalEmbedding" | cloud layout | |
"Width" | Automatic | image width |
▪
With the default the layout loads the paclet.
"PinProof"True
WolframInstitute`Z3Link`
▪
The sub-proof-cone options of (such as , , , and ) are also accepted and passed through to the surrounding cloud.
multiwaySubProofCones
"Beam"
"MaxNew"
"Oriented"
"WellFormedOnly"
Examples
(2)
Basic Examples
(1)
The proof for the binary-incrementer machine 453, embedded in its multiway cloud:
In[1]:=
 | MultiwayInductiveProofPanel |
Out[1]=
Options
(1)
 |
|
""