for T being TuringStr
for s being All-State of T holds (Computation s) . 1 = Following s