consider a, b being Data-Location of R, i1 being Element of NAT , r being Element of R;
A1: ( InsCode (AddTo a,b) = 2 & InsCode (SubFrom a,b) = 3 ) by MCART_1:def 1;
A2: ( InsCode (MultBy a,b) = 4 & InsCode (a := r) = 5 ) by MCART_1:def 1;
A3: ( InsCode (halt (SCM R)) = 0 & InsCode (a := b) = 1 ) by Th8, MCART_1:def 1;
A4: ( InsCode (goto i1,R) = 6 & InsCode (a =0_goto i1) = 7 ) by MCART_1:def 1;
( 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;
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,R) in AddressParts T or AddressPart (a =0_goto i1) in AddressParts T ) by A3, A1, A2, A4;
hence not AddressParts T is empty ; :: thesis: verum