consider a, b being Int-Location , i1 being Element of NAT , f being FinSeq-Location ;
A1: InsCode (a := b) = 1 by SCMFSA_2:42;
A2: InsCode (AddTo a,b) = 2 by SCMFSA_2:43;
A3: InsCode (MultBy a,b) = 4 by SCMFSA_2:45;
A4: InsCode (SubFrom a,b) = 3 by SCMFSA_2:44;
A5: InsCode (a >0_goto i1) = 8 by SCMFSA_2:49;
A6: InsCode (a =0_goto i1) = 7 by SCMFSA_2:48;
A7: InsCode (goto i1) = 6 by SCMFSA_2:47;
A8: InsCode (Divide a,b) = 5 by SCMFSA_2:46;
A9: InsCode (f :=<0,...,0> a) = 12 by SCMFSA_2:53;
A10: InsCode (a :=len f) = 11 by SCMFSA_2:52;
A11: InsCode (f,a := b) = 10 by SCMFSA_2:51;
A12: InsCode (b := f,a) = 9 by SCMFSA_2:50;
( 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 or T = 9 or T = 10 or T = 11 or T = 12 ) by Lm4;
then ( AddressPart (halt SCM+FSA ) 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 or AddressPart (b := f,a) in AddressParts T or AddressPart (f,a := b) in AddressParts T or AddressPart (a :=len f) in AddressParts T or AddressPart (f :=<0,...,0> a) in AddressParts T ) by A1, A2, A4, A3, A8, A7, A6, A5, A12, A11, A10, A9, SCMFSA_2:124;
hence not AddressParts T is empty ; :: thesis: verum