let s be All-State of (ZeroTuring ';' SuccTuring ); :: thesis: for t being Tape of ZeroTuring
for head, n being Element of NAT st s = [[0 ,0 ],head,t] & t storeData <*head,n*> holds
( s is Accept-Halt & (Result s) `2 = head & (Result s) `3 storeData <*head,1*> )
let t be Tape of ZeroTuring ; :: thesis: for head, n being Element of NAT st s = [[0 ,0 ],head,t] & t storeData <*head,n*> holds
( s is Accept-Halt & (Result s) `2 = head & (Result s) `3 storeData <*head,1*> )
let h, n be Element of NAT ; :: thesis: ( s = [[0 ,0 ],h,t] & t storeData <*h,n*> implies ( s is Accept-Halt & (Result s) `2 = h & (Result s) `3 storeData <*h,1*> ) )
assume that
A1: s = [[0 ,0 ],h,t] and
A2: t storeData <*h,n*> ; :: thesis: ( s is Accept-Halt & (Result s) `2 = h & (Result s) `3 storeData <*h,1*> )
reconsider h1 = h as Element of INT by INT_1:def 2;
set s1 = [the InitS of ZeroTuring ,h1,t];
A3: 0 = the InitS of ZeroTuring by Def20;
then A4: ( [the InitS of ZeroTuring ,h1,t] is Accept-Halt & (Result [the InitS of ZeroTuring ,h1,t]) `2 = h ) by A2, Lm15;
the Symbols of ZeroTuring = {0 ,1} by Def20
.= the Symbols of SuccTuring by Def18 ;
then reconsider t2 = (Result [the InitS of ZeroTuring ,h1,t]) `3 as Tape of SuccTuring ;
set s2 = [the InitS of SuccTuring ,h1,t2];
A5: 0 = the InitS of SuccTuring by Def18;
then A6: s = [the InitS of (ZeroTuring ';' SuccTuring ),h,t] by A1, A3, Def32;
(Result [the InitS of ZeroTuring ,h1,t]) `3 storeData <*h,0 *> by A2, A3, Lm15;
then A7: t2 storeData <*h,0 *> by Th53;
then A8: (Result [the InitS of SuccTuring ,h1,t2]) `3 storeData <*h,(0 + 1)*> by A5, Th36;
A9: [the InitS of SuccTuring ,h1,t2] is Accept-Halt by A7, A5, Th36;
hence s is Accept-Halt by A4, A6, Th50; :: thesis: ( (Result s) `2 = h & (Result s) `3 storeData <*h,1*> )
(Result [the InitS of SuccTuring ,h1,t2]) `2 = h by A7, A5, Th36;
hence (Result s) `2 = h by A4, A9, A6, Th50; :: thesis: (Result s) `3 storeData <*h,1*>
(Result s) `3 = (Result [the InitS of SuccTuring ,h1,t2]) `3 by A4, A9, A6, Th50;
hence (Result s) `3 storeData <*h,1*> by A8, Th53; :: thesis: verum