:: deftheorem Def9 defines Result TURING_1:def 9 :
for T being TuringStr
for s being All-State of T st s is Accept-Halt holds
for b₃ being All-State of T holds
( b₃ = Result s iff ex k being Nat st
( b₃ = (Computation s) . k & ((Computation s) . k) `1_3 = the AcceptS of T ) );