Command:fixleadzero and fixtrailzero - Walnut-Theorem-Prover/Walnut GitHub Wiki

One can now "fix" leading and trailing zeroes for Automata (not Word Automata) using the fixleadzero and fixtrailzero commands.

These commands have similar syntax and behavior.

fixleadzero

For leading zeroes, the syntax is as follows: for an automaton foo saved in "Automata Library/", one writes fixleadzero bar foo;

The resulting automaton bar accepts an input 0* x' if and only if foo accepts an input x, where x' is x with its leading zeroes removed. bar will be saved in the "Automata Library/" directory.

fixtrailzero

For trailing zeroes, the syntax is as follows: for an automaton foo saved in "Automata Library/", one writes fixtrailzero bar foo;

The resulting automaton bar accepts an input x' 0* if and only if foo accepts an input x, where x' is x with its trailing zeroes removed. bar will be saved in the "Automata Library/" directory.