let a be Int_position ; :: thesis: not return a is halting
reconsider loc = 1 as Element of NAT ;
A1: In (NAT,SCM-Memory) = NAT by AMI_2:22, FUNCT_7:def 1;
consider s being State of SCMPDS such that
A2: s . NAT = loc and
A3: for d being Int_position holds s . d = 0 by Th74;
(Exec ((return a),s)) . (IC ) = (abs (s . (DataLoc ((s . a),RetIC)))) + 2 by Th70
.= (abs 0) + 2 by A3
.= 0 + 2 by ABSVALUE:def 1
.= succ (IC s) by A2, A1 ;
hence not return a is halting by Th76; :: thesis: verum