The left cone grows from the base statement (P₀) and the right from the step statement (Pₘ ⟹ Pₘ₊₁); the caption states the induction schema that combines them.
▪
Options include
"BaseSteps"
(default 6),
"StepSteps"
(default 8),
"Axioms"
(
"Raw"
or the proof's axioms),
"WellFormedOnly"
,
"Oriented"
,
"FadeOpacity"
,
"MaxStates"
, and
"Height"
.
Examples
(1)
Basic Examples
(1)
The base and step cones for the binary-incrementer machine 453: