let a be Int_position ; :: thesis: not return a is halting
reconsider loc = 1 as Instruction-Location of SCMPDS by AMI_1:def 4;
consider s being State of SCMPDS such that
A1: ( s . NAT = loc & ( for d being Int_position holds s . d = 0 ) ) by Th74;
X: In NAT ,SCM-Memory = NAT by AMI_2:30, FUNCT_7:def 1;
(Exec (return a),s) . (IC SCMPDS ) = (abs (s . (DataLoc (s . a),RetIC ))) + 2 by Th70
.= (abs 0 ) + 2 by A1
.= 0 + 2 by ABSVALUE:def 1
.= Next (IC s) by A1, X ;
hence not return a is halting by Th76; :: thesis: verum