now :: thesis: for s being All-State of SumTuring

for t being Tape of SumTuring

for h1 being Element of NAT

for x being FinSequence of NAT st x in dom [+] & s = [ the InitS of SumTuring,h1,t] & t storeData <*h1*> ^ x holds

( s is Accept-Halt & ex h2 being Element of omega ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

hence
SumTuring computes [+]
; :: thesis: verumfor t being Tape of SumTuring

for h1 being Element of NAT

for x being FinSequence of NAT st x in dom [+] & s = [ the InitS of SumTuring,h1,t] & t storeData <*h1*> ^ x holds

( s is Accept-Halt & ex h2 being Element of omega ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

let s be All-State of SumTuring; :: thesis: for t being Tape of SumTuring

for h1 being Element of NAT

for x being FinSequence of NAT st x in dom [+] & s = [ the InitS of SumTuring,h1,t] & t storeData <*h1*> ^ x holds

( s is Accept-Halt & ex h2 being Element of omega ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

let t be Tape of SumTuring; :: thesis: for h1 being Element of NAT

for x being FinSequence of NAT st x in dom [+] & s = [ the InitS of SumTuring,h1,t] & t storeData <*h1*> ^ x holds

( s is Accept-Halt & ex h2 being Element of omega ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

let h1 be Element of NAT ; :: thesis: for x being FinSequence of NAT st x in dom [+] & s = [ the InitS of SumTuring,h1,t] & t storeData <*h1*> ^ x holds

( s is Accept-Halt & ex h2 being Element of omega ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

let x be FinSequence of NAT ; :: thesis: ( x in dom [+] & s = [ the InitS of SumTuring,h1,t] & t storeData <*h1*> ^ x implies ( s is Accept-Halt & ex h2 being Element of omega ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) ) )

assume that

A1: x in dom [+] and

A2: s = [ the InitS of SumTuring,h1,t] and

A3: t storeData <*h1*> ^ x ; :: thesis: ( s is Accept-Halt & ex h2 being Element of omega ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

x is Tuple of 2, NAT by A1, Th28, FINSEQ_2:131;

then consider i, j being Element of NAT such that

A4: x = <*i,j*> by FINSEQ_2:100;

A5: s = [0,h1,t] by A2, Def14;

A6: <*h1*> ^ x = <*h1,i,j*> by A4, FINSEQ_1:43;

hence s is Accept-Halt by A3, A5, Th27; :: thesis: ex h2 being Element of omega ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

take h2 = 1 + h1; :: thesis: ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

take y = i + j; :: thesis: ( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

t storeData <*h1,i,j*> by A3, A4, FINSEQ_1:43;

hence (Result s) `2_3 = h2 by A5, Th27; :: thesis: ( y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

thus y = [+] . x by A4, COMPUT_1:85; :: thesis: (Result s) `3_3 storeData <*h2*> ^ <*y*>

(Result s) `3_3 storeData <*(1 + h1),(i + j)*> by A3, A5, A6, Th27;

hence (Result s) `3_3 storeData <*h2*> ^ <*y*> ; :: thesis: verum

end;for h1 being Element of NAT

for x being FinSequence of NAT st x in dom [+] & s = [ the InitS of SumTuring,h1,t] & t storeData <*h1*> ^ x holds

( s is Accept-Halt & ex h2 being Element of omega ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

let t be Tape of SumTuring; :: thesis: for h1 being Element of NAT

for x being FinSequence of NAT st x in dom [+] & s = [ the InitS of SumTuring,h1,t] & t storeData <*h1*> ^ x holds

( s is Accept-Halt & ex h2 being Element of omega ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

let h1 be Element of NAT ; :: thesis: for x being FinSequence of NAT st x in dom [+] & s = [ the InitS of SumTuring,h1,t] & t storeData <*h1*> ^ x holds

( s is Accept-Halt & ex h2 being Element of omega ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

let x be FinSequence of NAT ; :: thesis: ( x in dom [+] & s = [ the InitS of SumTuring,h1,t] & t storeData <*h1*> ^ x implies ( s is Accept-Halt & ex h2 being Element of omega ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) ) )

assume that

A1: x in dom [+] and

A2: s = [ the InitS of SumTuring,h1,t] and

A3: t storeData <*h1*> ^ x ; :: thesis: ( s is Accept-Halt & ex h2 being Element of omega ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

x is Tuple of 2, NAT by A1, Th28, FINSEQ_2:131;

then consider i, j being Element of NAT such that

A4: x = <*i,j*> by FINSEQ_2:100;

A5: s = [0,h1,t] by A2, Def14;

A6: <*h1*> ^ x = <*h1,i,j*> by A4, FINSEQ_1:43;

hence s is Accept-Halt by A3, A5, Th27; :: thesis: ex h2 being Element of omega ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

take h2 = 1 + h1; :: thesis: ex y being Element of omega st

( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

take y = i + j; :: thesis: ( (Result s) `2_3 = h2 & y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

t storeData <*h1,i,j*> by A3, A4, FINSEQ_1:43;

hence (Result s) `2_3 = h2 by A5, Th27; :: thesis: ( y = [+] . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

thus y = [+] . x by A4, COMPUT_1:85; :: thesis: (Result s) `3_3 storeData <*h2*> ^ <*y*>

(Result s) `3_3 storeData <*(1 + h1),(i + j)*> by A3, A5, A6, Th27;

hence (Result s) `3_3 storeData <*h2*> ^ <*y*> ; :: thesis: verum