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