for T being TuringStr
for s being All-State of T holds (Computation s) . 0 = s by Def7;