:: deftheorem Def7 defines Computation TURING_1:def 7 :
for T being TuringStr
for s being All-State of T
for b₃ being sequence of [: the FStates of T,INT,(Funcs (INT, the Symbols of T)):] holds
( b₃ = Computation s iff ( b₃ . 0 = s & ( for i being Nat holds b₃ . (i + 1) = Following (b₃ . i) ) ) );