let s be All-State of (ZeroTuring ';' SuccTuring); 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_3 = head & (Result s) `3_3 storeData <*head,1*> )
let t be 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_3 = head & (Result s) `3_3 storeData <*head,1*> )
let h, n be Element of NAT ; ( s = [[0,0],h,t] & t storeData <*h,n*> implies ( s is Accept-Halt & (Result s) `2_3 = h & (Result s) `3_3 storeData <*h,1*> ) )
assume that
A1:
s = [[0,0],h,t]
and
A2:
t storeData <*h,n*>
; ( s is Accept-Halt & (Result s) `2_3 = h & (Result s) `3_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 Def19;
then A4:
( [ the InitS of ZeroTuring,h1,t] is Accept-Halt & (Result [ the InitS of ZeroTuring,h1,t]) `2_3 = h )
by A2, Lm15;
the Symbols of ZeroTuring =
{0,1}
by Def19
.=
the Symbols of SuccTuring
by Def17
;
then reconsider t2 = (Result [ the InitS of ZeroTuring,h1,t]) `3_3 as Tape of SuccTuring ;
set s2 = [ the InitS of SuccTuring,h1,t2];
A5:
0 = the InitS of SuccTuring
by Def17;
then A6:
s = [ the InitS of (ZeroTuring ';' SuccTuring),h,t]
by A1, A3, Def31;
(Result [ the InitS of ZeroTuring,h1,t]) `3_3 storeData <*h,0*>
by A2, A3, Lm15;
then A7:
t2 storeData <*h,0*>
by Th48;
then A8:
(Result [ the InitS of SuccTuring,h1,t2]) `3_3 storeData <*h,(0 + 1)*>
by A5, Th31;
A9:
[ the InitS of SuccTuring,h1,t2] is Accept-Halt
by A7, A5, Th31;
hence
s is Accept-Halt
by A4, A6, Th45; ( (Result s) `2_3 = h & (Result s) `3_3 storeData <*h,1*> )
(Result [ the InitS of SuccTuring,h1,t2]) `2_3 = h
by A7, A5, Th31;
hence
(Result s) `2_3 = h
by A4, A9, A6, Th45; (Result s) `3_3 storeData <*h,1*>
(Result s) `3_3 = (Result [ the InitS of SuccTuring,h1,t2]) `3_3
by A4, A9, A6, Th45;
hence
(Result s) `3_3 storeData <*h,1*>
by A8, Th48; verum