let k1 be Integer; :: thesis: ( k1 <> 0 implies not goto k1 is halting )
assume A1: k1 <> 0 ; :: thesis: not goto k1 is halting
set n = |.k1.|;
reconsider loc = |.k1.| + 1 as Element of NAT ;
consider s being State of SCMPDS such that
A2: s . NAT = loc and
for d being Int_position holds s . d = 0 by Th58;
- |.k1.| <= k1 by ABSVALUE:4;
then 0 - |.k1.| <= k1 ;
then A3: (|.k1.| + k1) * 1 >= 0 by XREAL_1:20;
ex m being Element of NAT st
( m = IC s & ICplusConst (s,k1) = |.(m + k1).| ) by Def17;
then A4: (Exec ((goto k1),s)) . (IC ) = |.((|.k1.| + k1) + 1).| by A2, Th1, Th51
.= |.(|.k1.| + k1).| + |.1.| by A3, ABSVALUE:11
.= |.(|.k1.| + k1).| + 1 by ABSVALUE:def 1
.= (|.k1.| + k1) + 1 by A3, ABSVALUE:def 1
.= (|.k1.| + 1) + k1 ;
assume goto k1 is halting ; :: thesis: contradiction
then (Exec ((goto k1),s)) . (IC ) = |.k1.| + 1 by A2, Th1;
hence contradiction by A1, A4; :: thesis: verum