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 = abs k1;
reconsider loc = (abs 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 Th74;
- (abs k1) <= k1 by ABSVALUE:11;
then 0 - (abs k1) <= k1 ;
then A3: ((abs k1) + k1) * 1 >= 0 by XREAL_1:22;
ex m being Element of NAT st
( m = IC s & ICplusConst s,k1 = abs (m + k1) ) by Def20;
then A4: (Exec (goto k1),s) . (IC SCMPDS ) = abs (((abs k1) + k1) + 1) by A2, Th6, Th66
.= (abs ((abs k1) + k1)) + (abs 1) by A3, ABSVALUE:24
.= (abs ((abs k1) + k1)) + 1 by ABSVALUE:def 1
.= ((abs k1) + k1) + 1 by A3, ABSVALUE:def 1
.= ((abs k1) + 1) + k1 ;
assume goto k1 is halting ; :: thesis: contradiction
then (Exec (goto k1),s) . (IC SCMPDS ) = (abs k1) + 1 by A2, Th6, AMI_1:def 8;
hence contradiction by A1, A4; :: thesis: verum