Verified witness for the Challenge

The witness is the folded automaton returned by foldWords. The main theorem of the implementation proves its based-loop subgroup is precisely the subgroup generated by the input list.

def Stallings.completeStatement (S : List (List (Fin 2 × Bool))) : Prop

This definition repeats the Challenge's self-contained transition-table specification. Its value is selected by Comparator along with the theorem.

Equations

• One or more equations did not get rendered due to their size.

theorem Stallings.folded_recognizer_exists (S : List (List (Fin 2 × Bool))) : completeStatement S

The constructive finite-recognizer result, witnessed by the computed fold.