consider a, b being Int-Location , i1 being Instruction-Location of SCM+FSA , f being FinSeq-Location ;
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 or T = 9 or T = 10 or T = 11 or T = 12 ) by Lm4;
( InsCode (halt SCM+FSA ) = 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 & InsCode (b := f,a) = 9 & InsCode (f,a := b) = 10 & InsCode (a :=len f) = 11 & InsCode (f :=<0,...,0> a) = 12 ) by SCMFSA_2:42, SCMFSA_2:43, SCMFSA_2:44, SCMFSA_2:45, SCMFSA_2:46, SCMFSA_2:47, SCMFSA_2:48, SCMFSA_2:49, SCMFSA_2:50, SCMFSA_2:51, SCMFSA_2:52, SCMFSA_2:53, SCMFSA_2:124;
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;
hence not AddressParts T is empty ; :: thesis: verum