now

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, y being Element of NAT st
( (Result s) `2 = h2 & y = [+] . x & (Result s) `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, y being Element of NAT st
( (Result s) `2 = h2 & y = [+] . x & (Result s) `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, y being Element of NAT st
( (Result s) `2 = h2 & y = [+] . x & (Result s) `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, y being Element of NAT st
( (Result s) `2 = h2 & y = [+] . x & (Result s) `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, y being Element of NAT st
( (Result s) `2 = h2 & y = [+] . x & (Result s) `3 storeData <*h2*> ^ <*y*> ) )
x is Tuple of 2, NAT by A1, Th32, FINSEQ_2:151;
then consider i, j being Element of NAT such that
A4: x = <*i,j*> by A1, Th32, FINSEQ_2:120;
A5: s = [0 ,h1,t] by A2, Def15;
A6: <*h1*> ^ x = <*h1,i,j*> by A4, FINSEQ_1:60;
hence s is Accept-Halt by A3, A5, Th31; :: thesis: ex h2, y being Element of NAT st
( (Result s) `2 = h2 & y = [+] . x & (Result s) `3 storeData <*h2*> ^ <*y*> )
take h2 = 1 + h1; :: thesis: ex y being Element of NAT st
( (Result s) `2 = h2 & y = [+] . x & (Result s) `3 storeData <*h2*> ^ <*y*> )
take y = i + j; :: thesis: ( (Result s) `2 = h2 & y = [+] . x & (Result s) `3 storeData <*h2*> ^ <*y*> )
t storeData <*h1,i,j*> by A3, A4, FINSEQ_1:60;
hence (Result s) `2 = h2 by A5, Th31; :: thesis: ( y = [+] . x & (Result s) `3 storeData <*h2*> ^ <*y*> )
thus y = [+] . x by A4, COMPUT_1:89; :: thesis: (Result s) `3 storeData <*h2*> ^ <*y*>
(Result s) `3 storeData <*(1 + h1),(i + j)*> by A3, A5, A6, Th31;
hence (Result s) `3 storeData <*h2*> ^ <*y*> by FINSEQ_1:def 9; :: thesis: verum

end;

hence SumTuring computes [+] by Def16; :: thesis: verum