Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
WolframInstitute`TuringMachine`InductiveProofs`
onesRunDefinitions  |
|
| | ||||
▪
ones[n,tail]
s1
tail
▪
Together with they let a run-length-compressed configuration (see ) be expanded or matched during a proof.
zerosRunDefinitions
Examples
(1)
Basic Examples
(1)
In[1]:=
 | RenderAxiomGrid |
 | onesRunDefinitions |
| zerosRunDefinitions |
Out[1]=
s 0 | = | s |
s m+1 | = | s m |
s 0 | = | s |
s m+1 | = | s m |
 |
|
""