for i, j being Nat
for T being TuringStr
for s being All-State of T st i <= j & ((Computation s) . i) `1_3 = the AcceptS of T holds
(Computation s) . j = (Computation s) . i