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