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