let n be Nat; :: thesis: ( n >= 1 implies ZeroTuring computes n const 0 )

assume A1: n >= 1 ; :: thesis: ZeroTuring computes n const 0

assume A1: n >= 1 ; :: thesis: ZeroTuring computes n const 0

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

for t being Tape of ZeroTuring

for h being Element of NAT

for x being FinSequence of NAT st x in dom (n const 0) & s = [ the InitS of ZeroTuring,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 = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

hence
ZeroTuring computes n const 0
; :: thesis: verumfor t being Tape of ZeroTuring

for h being Element of NAT

for x being FinSequence of NAT st x in dom (n const 0) & s = [ the InitS of ZeroTuring,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 = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

set cs = n const 0;

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

for h being Element of NAT

for x being FinSequence of NAT st x in dom (n const 0) & s = [ the InitS of ZeroTuring,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 = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

let t be Tape of ZeroTuring; :: thesis: for h being Element of NAT

for x being FinSequence of NAT st x in dom (n const 0) & s = [ the InitS of ZeroTuring,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 = (n const 0) . 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 (n const 0) & s = [ the InitS of ZeroTuring,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 = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

let x be FinSequence of NAT ; :: thesis: ( x in dom (n const 0) & s = [ the InitS of ZeroTuring,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 = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) ) )

assume that

A2: x in dom (n const 0) and

A3: s = [ the InitS of ZeroTuring,h,t] and

A4: 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 = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

x in n -tuples_on NAT by A2;

then x in { f where f is Element of NAT * : len f = n } by FINSEQ_2:def 4;

then A6: ex f being Element of NAT * st

( x = f & len f = n ) ;

A7: s = [0,h,t] by A3, Def19;

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

( (Result s) `2_3 = h2 & y = (n const 0) . 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 = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

take y = 0 ; :: thesis: ( (Result s) `2_3 = h2 & y = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

thus (Result s) `2_3 = h2 by A1, A4, A6, A7, Th34; :: thesis: ( y = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

thus y = (n const 0) . x by A2, FUNCOP_1:7; :: thesis: (Result s) `3_3 storeData <*h2*> ^ <*y*>

(Result s) `3_3 storeData <*h2,0*> by A1, A4, A6, A7, Th34;

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

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

for h being Element of NAT

for x being FinSequence of NAT st x in dom (n const 0) & s = [ the InitS of ZeroTuring,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 = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

let t be Tape of ZeroTuring; :: thesis: for h being Element of NAT

for x being FinSequence of NAT st x in dom (n const 0) & s = [ the InitS of ZeroTuring,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 = (n const 0) . 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 (n const 0) & s = [ the InitS of ZeroTuring,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 = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

let x be FinSequence of NAT ; :: thesis: ( x in dom (n const 0) & s = [ the InitS of ZeroTuring,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 = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) ) )

assume that

A2: x in dom (n const 0) and

A3: s = [ the InitS of ZeroTuring,h,t] and

A4: 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 = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> ) )

x in n -tuples_on NAT by A2;

then x in { f where f is Element of NAT * : len f = n } by FINSEQ_2:def 4;

then A6: ex f being Element of NAT * st

( x = f & len f = n ) ;

A7: s = [0,h,t] by A3, Def19;

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

( (Result s) `2_3 = h2 & y = (n const 0) . 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 = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

take y = 0 ; :: thesis: ( (Result s) `2_3 = h2 & y = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

thus (Result s) `2_3 = h2 by A1, A4, A6, A7, Th34; :: thesis: ( y = (n const 0) . x & (Result s) `3_3 storeData <*h2*> ^ <*y*> )

thus y = (n const 0) . x by A2, FUNCOP_1:7; :: thesis: (Result s) `3_3 storeData <*h2*> ^ <*y*>

(Result s) `3_3 storeData <*h2,0*> by A1, A4, A6, A7, Th34;

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