Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
WolframInstitute`TuringMachine`InductiveProofs`
boundaryAxiomsFor  |
|
| | ||||
▪
ru is a machine number (interpreted as an s=2, k=2 machine).
▪
The boundary axioms are used together with and to state the full rewrite system for the induction proof.
transitionAxiomsFor
unboundAxiom
Examples
(1)
Basic Examples
(1)
Render the boundary axioms of machine 453, together with the unbound axiom:
In[1]:=
 | RenderAxiomGrid |
 | boundaryAxiomsFor |
| unboundAxiom |
Out[1]=
s | = | s |
s | = | s |
s | = | s |
 |
|
 |
|
""