halt SCM+FSA = [0,{},{}] by FUNCT_7:def 1, SCMFSA_1:4;
then JumpPart (halt SCM+FSA) is empty by RECDEF_2:def 2;
then halt SCM+FSA is ins-loc-free by COMPOS_1:def 16;
hence SCM+FSA is proper-halt by COMPOS_1:def 18; :: thesis: SCM+FSA is IC-Ins-separated
ObjectKind (IC ) = NAT by FUNCT_7:def 1, SCMFSA_1:5, SCMFSA_1:9;
hence SCM+FSA is IC-Ins-separated by MEMSTR_0:def 3; :: thesis: verum