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, SUBSET_1:def 8;
consider s being State of SCMPDS such that
A2: s . NAT = loc and
A3: for d being Int_position holds s . d = 0 by Th58;
(Exec ((return a),s)) . (IC ) = |.(s . (DataLoc ((s . a),RetIC))).| + 2 by Th55
.= |.0.| + 2 by A3
.= 0 + 2 by ABSVALUE:def 1
.= (IC s) + 1 by A2, A1 ;
hence not return a is halting by Th60; :: thesis: verum