the haltF of (SCM R) = [0,{},{}] by Def1;
then JumpPart (halt (SCM R)) is empty by RECDEF_2:def 2;
then halt (SCM R) is ins-loc-free by COMPOS_1:def 16;
hence SCM R is proper-halt by COMPOS_1:def 18; :: thesis: SCM R is IC-Ins-separated
thus ObjectKind (IC ) = (SCM-OK R) . (IC ) by Def1
.= (SCM-OK R) . NAT by Def1
.= NAT by AMI_2:22, SCMRING1:def 3 ; :: according to MEMSTR_0:def 3 :: thesis: verum