Build numbers, replay addition rules, and inspect explicitly bounded formula searches.
Every natural number is built by applying the successor function S to 0. Click S( ) to wrap another layer.
Watch addition unfold rule by rule. The successor rule peels one S from the second input. The zero rule resolves the base case.
Select a sentence and inspect its displayed finite search box. This playground is not the general Presburger decision procedure.