for k being Nat
for T being TuringStr
for s being All-State of T holds (Computation s) . (k + 1) = Following ((Computation s) . k) by Def7;