let I be set ; :: thesis: ( I is Instruction of SCM+FSA iff ( 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 ) )
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 ) :: thesis: ( ( 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 ) implies I is Instruction of SCM+FSA )

proof

assume I is Instruction of SCM+FSA ; :: thesis: ( 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 )
then reconsider J = I as Instruction of SCM+FSA ;
set n = InsCode J;
A1: ( not InsCode J <= 10 or 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 )

proof

assume InsCode J <= 10 ; :: thesis: ( 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 )
then InsCode J <= 9 + 1 ;
hence ( 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 ) by NAT_1:8, NAT_1:34; :: thesis: verum

end;

InsCode J <= 11 + 1 by Th35;
then A2: ( InsCode J <= 11 or InsCode J = 12 ) by NAT_1:8;
( not InsCode J <= 10 + 1 or InsCode J <= 10 or InsCode J = 11 ) by NAT_1:8;
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 ) by A1, A2, Th54, Th55, Th56, Th57, Th58, Th59, Th60, Th61, Th62, Th63, Th64, Th65, Th119; :: thesis: verum

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 ) implies I is Instruction of SCM+FSA ) by SCMFSA_1:4; :: thesis: verum