thus SCM R is halting :: thesis: ( SCM R is definite & SCM R is realistic )

proof

the haltF of (SCM R) = [0,{},{}] by Def1;
hence the haltF of (SCM R) is halting by Th21; :: according to EXTPRO_1:def 4 :: thesis: verum

end;

thus SCM R is definite :: thesis: SCM R is realistic

proof

let l be Element of NAT ; :: according to COMPOS_1:def 8 :: thesis: the Object-Kind of (SCM R) . l = the Instructions of (SCM R)
reconsider L = l as Element of NAT ;
thus the Object-Kind of (SCM R) . l = (SCM-OK R) . L by Def1
.= SCM-Instr R by SCMRING1:6
.= the Instructions of (SCM R) by Def1 ; :: thesis: verum

end;

assume A11: the ZeroF of (SCM R) in NAT ; :: according to COMPOS_1:def 12 :: thesis: contradiction
the ZeroF of (SCM R) = NAT by Def1;
hence contradiction by A11; :: thesis: verum