timeline · one strip per step · width = formula length · bright = what the step produced
Feed it a formula. It rewrites it one rule at a time, live, and tells you whether it is a tautology.
if C then X else Y · && ∧ and · || ∨ or · ! ¬ not · -> → (right-assoc) · <-> ↔ · true false 0 1 · keys: ← → space