let I be set ; :: thesis:
thus ( not I is Instruction of SCM+FSA or I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex la being Element of NAT st I = goto la or ex lb being Element of NAT ex da being Int-Location st I = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st I = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st I = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st I = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a or ex a being Int-Location st I = a :==1 ) :: thesis:

assume I is Instruction of SCM+FSA ; :: thesis:
then reconsider J = I as Instruction of SCM+FSA ;
set n = InsCode J;
InsCode J <= 13 by Th35;
then ( InsCode J = 0 or InsCode J = 1 or InsCode J = 2 or InsCode J = 3 or InsCode J = 4 or InsCode J = 5 or InsCode J = 6 or InsCode J = 7 or InsCode J = 8 or InsCode J = 9 or InsCode J = 10 or InsCode J = 11 or InsCode J = 12 or InsCode J = 13 ) by NAT_1:38;
hence ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex la being Element of NAT st I = goto la or ex lb being Element of NAT ex da being Int-Location st I = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st I = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st I = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st I = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a or ex a being Int-Location st I = a :==1 ) by Th54, Th55, Th56, Th57, Th58, Th59, Th60, Th61, Th62, Th63, Th64, Th65, Th119, LmX; :: thesis:

end;

thus ( ( I = [0,{},{}] or ex a, b being Int-Location st I = a := b or ex a, b being Int-Location st I = AddTo (a,b) or ex a, b being Int-Location st I = SubFrom (a,b) or ex a, b being Int-Location st I = MultBy (a,b) or ex a, b being Int-Location st I = Divide (a,b) or ex la being Element of NAT st I = goto la or ex lb being Element of NAT ex da being Int-Location st I = da =0_goto lb or ex lb being Element of NAT ex da being Int-Location st I = da >0_goto lb or ex b, a being Int-Location ex fa being FinSeq-Location st I = a := (fa,b) or ex a, b being Int-Location ex fa being FinSeq-Location st I = (fa,a) := b or ex a being Int-Location ex f being FinSeq-Location st I = a :=len f or ex a being Int-Location ex f being FinSeq-Location st I = f :=<0,...,0> a or ex a being Int-Location st I = a :==1 ) implies I is Instruction of SCM+FSA ) by SCMFSA_1:4; :: thesis: