theorem Th13: :: TURING_1:13

for T being TuringStr
for s being All-State of T st s is Accept-Halt holds
ex k being Nat st
( ((Computation s) . k) `1_3 = the AcceptS of T & Result s = (Computation s) . k & ( for i being Nat st i < k holds
((Computation s) . i) `1_3 <> the AcceptS of T ) )