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

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 omega st

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

hence
SuccTuring computes 1 succ 1
; :: thesis: verumfor 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 omega st

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

set sc = 1 succ 1;

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 omega st

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_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 omega st

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_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 omega st

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_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 omega st

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) ) )

assume that

A1: x in dom (1 succ 1) and

A2: s = [ the InitS of SuccTuring,h,t] and

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

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

A4: s = [0,h,t] by A2, Def17;

A5: dom (1 succ 1) = 1 -tuples_on NAT by COMPUT_1:def 7;

then x is Tuple of 1, NAT by A1, FINSEQ_2:131;

then consider i being Element of NAT such that

A6: x = <*i*> by FINSEQ_2:97;

A7: <*h*> ^ x = <*h,i*> by A6;

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

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

take h2 = h; :: thesis: ex y being Element of omega st

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

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

thus (Result s) `2_3 = h2 by A3, A4, A7, Th31; :: thesis: ( y = (1 succ 1) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

thus y = (x /. 1) + 1 by A6, FINSEQ_4:16

.= (1 succ 1) . x by A1, A5, COMPUT_1:def 7 ; :: thesis: (Result s) `3_3 storeData <*h2*> ^ <*y*>

(Result s) `3_3 storeData <*h2,(i + 1)*> by A3, A4, A7, Th31;

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

end;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 omega st

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_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 omega st

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_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 omega st

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_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 omega st

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) ) )

assume that

A1: x in dom (1 succ 1) and

A2: s = [ the InitS of SuccTuring,h,t] and

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

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

A4: s = [0,h,t] by A2, Def17;

A5: dom (1 succ 1) = 1 -tuples_on NAT by COMPUT_1:def 7;

then x is Tuple of 1, NAT by A1, FINSEQ_2:131;

then consider i being Element of NAT such that

A6: x = <*i*> by FINSEQ_2:97;

A7: <*h*> ^ x = <*h,i*> by A6;

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

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

take h2 = h; :: thesis: ex y being Element of omega st

( (Result s) `2_3 = h2 & y = (1 succ 1) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

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

thus (Result s) `2_3 = h2 by A3, A4, A7, Th31; :: thesis: ( y = (1 succ 1) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

thus y = (x /. 1) + 1 by A6, FINSEQ_4:16

.= (1 succ 1) . x by A1, A5, COMPUT_1:def 7 ; :: thesis: (Result s) `3_3 storeData <*h2*> ^ <*y*>

(Result s) `3_3 storeData <*h2,(i + 1)*> by A3, A4, A7, Th31;

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