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 Instruction-Location of SCMPDS by AMI_1:def 4;
consider s being State of SCMPDS such that
A2: ( s . NAT = loc & ( 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;
consider m being Element of NAT such that
A4: ( m = IC s & ICplusConst s,k1 = abs (m + k1) ) by Def20;
A5: (Exec (goto k1),s) . (IC SCMPDS ) = abs (((abs k1) + k1) + 1) by A2, A4, 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, A5; :: thesis: verum