for i, k being Nat
for T being TuringStr
for s being All-State of T holds (Computation s) . (i + k) = (Computation ((Computation s) . i)) . k