JumpPart (halt SCM) is empty by Lm2, RECDEF_2:def 2;
then halt SCM is ins-loc-free by COMPOS_1:def 16;
hence SCM is proper-halt by COMPOS_1:def 18; :: thesis: SCM is IC-Ins-separated
IC = NAT by AMI_2:22, FUNCT_7:def 1;
then ObjectKind (IC ) = NAT by AMI_2:def 4;
hence SCM is IC-Ins-separated by MEMSTR_0:def 3; :: thesis: verum