action sets Sections AutomataTheory Doc

Def n0n1(n) == ([0]n) @ ([1]n)

Thm* S:ActionSet(), s,q:S.car. (n:. #(S.car)=n ) & (k:. (S:n0n1(k)s) = q) (L:*. (S:Ls) = q & (k:. L = n0n1(k))) n0n1_irregular