for s being All-State of (ZeroTuring ';' SuccTuring)
for t being Tape of ZeroTuring
for head, n being Element of NAT st s = [[0,0],head,t] & t storeData <*head,n*> holds
( s is Accept-Halt & (Result s) `2_3 = head & (Result s) `3_3 storeData <*head,1*> )