let I be set ; ( 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 )
( ( 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
;
( 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;
(
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 )
by Th35, NAT_1:36;
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 Th54, Th55, Th56, Th57, Th58, Th59, Th60, Th61, Th62, Th63, Th64, Th65, Th119;
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; verum