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