consider a, b being Data-Location , i1 being Instruction-Location of SCM ;
A1: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 ) by Lm3;
( InsCode (halt SCM ) = 0 & InsCode (a := b) = 1 & InsCode (AddTo a,b) = 2 & InsCode (SubFrom a,b) = 3 & InsCode (MultBy a,b) = 4 & InsCode (Divide a,b) = 5 & InsCode (goto i1) = 6 & InsCode (a =0_goto i1) = 7 & InsCode (a >0_goto i1) = 8 ) by AMI_5:37, MCART_1:7;
then ( AddressPart (halt SCM ) 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 (Divide a,b) in AddressParts T or AddressPart (goto i1) in AddressParts T or AddressPart (a =0_goto i1) in AddressParts T or AddressPart (a >0_goto i1) in AddressParts T ) by A1;
hence not AddressParts T is empty ; :: thesis: verum