now

let s be All-State of SuccTuring ; :: thesis: for t being Tape of SuccTuring
for h being Element of NAT
for x being FinSequence of NAT st x in dom (1 succ 1) & s = [the InitS of SuccTuring ,h,t] & t storeData <*h*> ^ x holds
( s is Accept-Halt & ex h2 being Element of NAT ex y being Element of NAT st
( (Result s) `2 = h2 & y = (1 succ 1) . x & (Result s) `3 storeData <*h2*> ^ <*y*> ) )
let t be Tape of SuccTuring ; :: thesis: for h being Element of NAT
for x being FinSequence of NAT st x in dom (1 succ 1) & s = [the InitS of SuccTuring ,h,t] & t storeData <*h*> ^ x holds
( s is Accept-Halt & ex h2 being Element of NAT ex y being Element of NAT st
( (Result s) `2 = h2 & y = (1 succ 1) . x & (Result s) `3 storeData <*h2*> ^ <*y*> ) )
let h be Element of NAT ; :: thesis: for x being FinSequence of NAT st x in dom (1 succ 1) & s = [the InitS of SuccTuring ,h,t] & t storeData <*h*> ^ x holds
( s is Accept-Halt & ex h2 being Element of NAT ex y being Element of NAT st
( (Result s) `2 = h2 & y = (1 succ 1) . x & (Result s) `3 storeData <*h2*> ^ <*y*> ) )
let x be FinSequence of NAT ; :: thesis: ( x in dom (1 succ 1) & s = [the InitS of SuccTuring ,h,t] & t storeData <*h*> ^ x implies ( s is Accept-Halt & ex h2 being Element of NAT ex y being Element of NAT st
( (Result s) `2 = h2 & y = (1 succ 1) . x & (Result s) `3 storeData <*h2*> ^ <*y*> ) ) )
set sc = 1 succ 1;
assume A1: ( x in dom (1 succ 1) & s = [the InitS of SuccTuring ,h,t] & t storeData <*h*> ^ x ) ; :: thesis: ( s is Accept-Halt & ex h2 being Element of NAT ex y being Element of NAT st
( (Result s) `2 = h2 & y = (1 succ 1) . x & (Result s) `3 storeData <*h2*> ^ <*y*> ) )
A2: dom (1 succ 1) = 1 -tuples_on NAT by COMPUT_1:def 10;
then consider i being Element of NAT such that
A3: x = <*i*> by A1, FINSEQ_2:117;
A4: s = [0 ,h,t] by A1, Def18;
A5: <*h*> ^ x = <*h,i*> by A3, FINSEQ_1:def 9;
hence s is Accept-Halt by A1, A4, Th36; :: thesis: ex h2 being Element of NAT ex y being Element of NAT st
( (Result s) `2 = h2 & y = (1 succ 1) . x & (Result s) `3 storeData <*h2*> ^ <*y*> )
take h2 = h; :: thesis: ex y being Element of NAT st
( (Result s) `2 = h2 & y = (1 succ 1) . x & (Result s) `3 storeData <*h2*> ^ <*y*> )
take y = i + 1; :: thesis: ( (Result s) `2 = h2 & y = (1 succ 1) . x & (Result s) `3 storeData <*h2*> ^ <*y*> )
thus (Result s) `2 = h2 by A1, A4, A5, Th36; :: thesis: ( y = (1 succ 1) . x & (Result s) `3 storeData <*h2*> ^ <*y*> )
thus y = (x /. 1) + 1 by A3, FINSEQ_4:25
.= (1 succ 1) . x by A1, A2, COMPUT_1:def 10 ; :: thesis: (Result s) `3 storeData <*h2*> ^ <*y*>
(Result s) `3 storeData <*h2,(i + 1)*> by A1, A4, A5, Th36;
hence (Result s) `3 storeData <*h2*> ^ <*y*> by FINSEQ_1:def 9; :: thesis: verum

end;

hence SuccTuring computes 1 succ 1 by Def16; :: thesis: verum