let n be Element of NAT ; :: thesis: ( n >= 1 implies ZeroTuring computes n const 0 )
assume A1: n >= 1 ; :: thesis: ZeroTuring computes n const 0

now

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 NAT st
( (Result s) `2 = h2 & y = (n const 0 ) . x & (Result s) `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 NAT st
( (Result s) `2 = h2 & y = (n const 0 ) . x & (Result s) `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 NAT st
( (Result s) `2 = h2 & y = (n const 0 ) . x & (Result s) `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 NAT st
( (Result s) `2 = h2 & y = (n const 0 ) . x & (Result s) `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 NAT st
( (Result s) `2 = h2 & y = (n const 0 ) . x & (Result s) `3 storeData <*h2*> ^ <*y*> ) )
arity (n const 0 ) = n by COMPUT_1:35;
then A5: dom (n const 0 ) c= n -tuples_on NAT by COMPUT_1:24;
then 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, Def20;
hence s is Accept-Halt by A1, A4, A6, Th39; :: thesis: ex h2 being Element of NAT ex y being Element of NAT st
( (Result s) `2 = h2 & y = (n const 0 ) . x & (Result s) `3 storeData <*h2*> ^ <*y*> )
take h2 = h; :: thesis: ex y being Element of NAT st
( (Result s) `2 = h2 & y = (n const 0 ) . x & (Result s) `3 storeData <*h2*> ^ <*y*> )
take y = 0 ; :: thesis: ( (Result s) `2 = h2 & y = (n const 0 ) . x & (Result s) `3 storeData <*h2*> ^ <*y*> )
thus (Result s) `2 = h2 by A1, A4, A6, A7, Th39; :: thesis: ( y = (n const 0 ) . x & (Result s) `3 storeData <*h2*> ^ <*y*> )
thus y = (n const 0 ) . x by A2, A5, FUNCOP_1:13; :: thesis: (Result s) `3 storeData <*h2*> ^ <*y*>
(Result s) `3 storeData <*h2,0 *> by A1, A4, A6, A7, Th39;
hence (Result s) `3 storeData <*h2*> ^ <*y*> by FINSEQ_1:def 9; :: thesis: verum

end;

hence ZeroTuring computes n const 0 by Def16; :: thesis: verum