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 = head & (Result s) `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 = head & (Result s) `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 = h & (Result s) `3 storeData <*h,0 *> ) )
assume that
A1: s = [0 ,h,t] and
A2: t storeData <*h,n*> ; :: thesis: ( s is Accept-Halt & (Result s) `2 = h & (Result s) `3 storeData <*h,0 *> )
set f = <*n*>;
A3: len <*n*> = 1 by FINSEQ_1:56;
t storeData <*h*> ^ <*n*> by A2, FINSEQ_1:def 9;
hence ( s is Accept-Halt & (Result s) `2 = h & (Result s) `3 storeData <*h,0 *> ) by A1, A3, Th39; :: thesis: verum