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

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