:: deftheorem defines computes TURING_1:def 15 :
for T being TuringStr
for F being Function holds
( T computes F iff for s being All-State of T
for t being Tape of T
for a being Element of NAT
for x being FinSequence of NAT st x in dom F & s = [ the InitS of T,a,t] & t storeData <*a*> ^ x holds
( s is Accept-Halt & ex b, y being Element of NAT st
( (Result s) `2_3 = b & y = F . x & (Result s) `3_3 storeData <*b*> ^ <*y*> ) ) );