let s be All-State of ZeroTuring; :: thesis: for t being Tape of ZeroTuring
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,0*> )
let t be Tape of ZeroTuring; :: thesis: 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,0*> )
let h, n be Element of NAT ; :: thesis: ( s = [0,h,t] & t storeData <*h,n*> implies ( s is Accept-Halt & (Result s) `2_3 = h & (Result s) `3_3 storeData <*h,0*> ) )
len <*n*> = 1 by FINSEQ_1:39;
hence ( s = [0,h,t] & t storeData <*h,n*> implies ( s is Accept-Halt & (Result s) `2_3 = h & (Result s) `3_3 storeData <*h,0*> ) ) by Th34; :: thesis: verum