theorem Th31: :: TURING_1:31

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