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 37;
hence SCM R is proper-halt by COMPOS_1:def 39; :: thesis: SCM R is IC-Ins-separated
thus ObjectKind (IC (SCM R)) = (SCM-OK R) . (IC (SCM R)) by Def1
.= (SCM-OK R) . NAT by Def1
.= NAT by AMI_2:30, SCMRING1:def 3 ; :: according to COMPOS_1:def 6 :: thesis: verum