Automata
0s and 1s01s and 10s.
0101 \(\notin C\)0110 \(\in C\)\[ \begin{aligned} &\forall A :\exists p \in \mathbb{N} : \\ &\exists xyz \in A : |xyz| \geq p \implies \\ &\forall i \in \mathbb{N} : xy^iz \in A \land \\ &|y| > 0 \land \\ &|xy| \leq p \end{aligned} \] - That is, \(\{xz, xyz, xyyz\} \in A\)
y# assume S as a list of states.
S : List[states]
x : str
y : str
z : str
assert(states(x + z) == S[:i] + S[j:])
assert(states(x + y + z) == S == S[:i]+S[i:j]+S[j:])
assert(states(x + y + y + z) == S[:i] + S[i:j] + S[i:j] + S[j:])
assert(states(x + y * 2 + z) == S[:i] + S[i:j] * 2 + S[j:])
# This can't run - it's infinite
assert(all((states(x+y*n+z) == A[:i]+A[i:j]*n+A[j:]) for n in count()))\[ \begin{aligned} &\forall A :\exists p \in \mathbb{N} : \\ &\exists xyz \in A : |xyz| \geq p \implies \\ &\forall i \in \mathbb{N} : xy^iz \in A \land \\ &|y| > 0 \land \\ &|xy| \leq p \end{aligned} \]
Proof
0s and 1s”