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_3 = head & (Result s) `3_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_3 = head & (Result s) `3_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_3 = h & (Result s) `3_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_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; :: thesis: ( (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; :: thesis: (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; :: thesis: verum

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; :: 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_3 = head & (Result s) `3_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_3 = h & (Result s) `3_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_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; :: thesis: ( (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; :: thesis: (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; :: thesis: verum