consider a, b being Data-Location of R, i1 being Instruction-Location of SCM R, r being Element of R;
A1: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 ) by Lm3;
( InsCode (halt (SCM R)) = 0 & InsCode (a := b) = 1 & InsCode (AddTo a,b) = 2 & InsCode (SubFrom a,b) = 3 & InsCode (MultBy a,b) = 4 & InsCode (a := r) = 5 & InsCode (goto i1) = 6 & InsCode (a =0_goto i1) = 7 ) by Th8, MCART_1:def 1;
then ( AddressPart (halt (SCM R)) in AddressParts T or AddressPart (a := b) in AddressParts T or AddressPart (AddTo a,b) in AddressParts T or AddressPart (SubFrom a,b) in AddressParts T or AddressPart (MultBy a,b) in AddressParts T or AddressPart (a := r) in AddressParts T or AddressPart (goto i1) in AddressParts T or AddressPart (a =0_goto i1) in AddressParts T ) by A1;
hence not AddressParts T is empty ; :: thesis: verum