theorem Th34: :: TURING_1:34

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