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:30, 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 SCMPDS ) = (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