let R be good Ring; for I being set holds
( I is Instruction of (SCM R) iff ( I = [0 ,{} ] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo a,b or ex a, b being Data-Location of R st I = SubFrom a,b or ex a, b being Data-Location of R st I = MultBy a,b or ex i1 being Element of NAT st I = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) )
let J be set ; ( J is Instruction of (SCM R) iff ( J = [0 ,{} ] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) )
A1:
the Instructions of (SCM R) = SCM-Instr R
by Def1;
thus
( not J is Instruction of (SCM R) or J = [0 ,{} ] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r )
( ( J = [0 ,{} ] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) implies J is Instruction of (SCM R) )proof
assume
J is
Instruction of
(SCM R)
;
( J = [0 ,{} ] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r )
then
(
J in (({[0 ,{} ]} \/ { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>] where i is Element of NAT : verum } ) \/ { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or
J in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of R : verum } )
by A1, XBOOLE_0:def 3;
then
(
J in ({[0 ,{} ]} \/ { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>] where i is Element of NAT : verum } or
J in { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or
J in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of R : verum } )
by XBOOLE_0:def 3;
then A2:
(
J in {[0 ,{} ]} \/ { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } or
J in { [6,<*i*>] where i is Element of NAT : verum } or
J in { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or
J in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of R : verum } )
by XBOOLE_0:def 3;
per cases
( J in {[0 ,{} ]} or J in { [6,<*i*>] where i is Element of NAT : verum } or J in { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } or J in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of R : verum } or J in { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } )
by A2, XBOOLE_0:def 3;
suppose
J in {[0 ,{} ]}
;
( J = [0 ,{} ] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r )end; suppose
J in { [6,<*i*>] where i is Element of NAT : verum }
;
( J = [0 ,{} ] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r )then consider i being
Element of
NAT such that A3:
J = [6,<*i*>]
and
verum
;
reconsider i =
i as
Element of
NAT ;
J = goto i,
R
by A3;
hence
(
J = [0 ,{} ] or ex
a,
b being
Data-Location of
R st
J = a := b or ex
a,
b being
Data-Location of
R st
J = AddTo a,
b or ex
a,
b being
Data-Location of
R st
J = SubFrom a,
b or ex
a,
b being
Data-Location of
R st
J = MultBy a,
b or ex
i1 being
Element of
NAT st
J = goto i1,
R or ex
a being
Data-Location of
R ex
i1 being
Element of
NAT st
J = a =0_goto i1 or ex
a being
Data-Location of
R ex
r being
Element of
R st
J = a := r )
;
verum end; suppose
J in { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum }
;
( J = [0 ,{} ] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r )then consider i being
Element of
NAT ,
a being
Element of
SCM-Data-Loc such that A4:
J = [7,<*i,a*>]
and
verum
;
reconsider A =
a as
Data-Location of
R by Th1;
reconsider I =
i as
Element of
NAT ;
J = A =0_goto I
by A4;
hence
(
J = [0 ,{} ] or ex
a,
b being
Data-Location of
R st
J = a := b or ex
a,
b being
Data-Location of
R st
J = AddTo a,
b or ex
a,
b being
Data-Location of
R st
J = SubFrom a,
b or ex
a,
b being
Data-Location of
R st
J = MultBy a,
b or ex
i1 being
Element of
NAT st
J = goto i1,
R or ex
a being
Data-Location of
R ex
i1 being
Element of
NAT st
J = a =0_goto i1 or ex
a being
Data-Location of
R ex
r being
Element of
R st
J = a := r )
;
verum end; suppose
J in { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of R : verum }
;
( J = [0 ,{} ] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r )then consider a being
Element of
SCM-Data-Loc ,
r being
Element of
R such that A5:
J = [5,<*a,r*>]
and
verum
;
reconsider A =
a as
Data-Location of
R by Th1;
J = A := r
by A5;
hence
(
J = [0 ,{} ] or ex
a,
b being
Data-Location of
R st
J = a := b or ex
a,
b being
Data-Location of
R st
J = AddTo a,
b or ex
a,
b being
Data-Location of
R st
J = SubFrom a,
b or ex
a,
b being
Data-Location of
R st
J = MultBy a,
b or ex
i1 being
Element of
NAT st
J = goto i1,
R or ex
a being
Data-Location of
R ex
i1 being
Element of
NAT st
J = a =0_goto i1 or ex
a being
Data-Location of
R ex
r being
Element of
R st
J = a := r )
;
verum end; suppose
J in { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} }
;
( J = [0 ,{} ] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r )then consider I being
Element of
Segm 8,
a,
b being
Element of
SCM-Data-Loc such that A6:
(
J = [I,<*a,b*>] &
I in {1,2,3,4} )
;
reconsider A =
a,
B =
b as
Data-Location of
R by Th1;
(
J = A := B or
J = AddTo A,
B or
J = SubFrom A,
B or
J = MultBy A,
B )
by A6, ENUMSET1:def 2;
hence
(
J = [0 ,{} ] or ex
a,
b being
Data-Location of
R st
J = a := b or ex
a,
b being
Data-Location of
R st
J = AddTo a,
b or ex
a,
b being
Data-Location of
R st
J = SubFrom a,
b or ex
a,
b being
Data-Location of
R st
J = MultBy a,
b or ex
i1 being
Element of
NAT st
J = goto i1,
R or ex
a being
Data-Location of
R ex
i1 being
Element of
NAT st
J = a =0_goto i1 or ex
a being
Data-Location of
R ex
r being
Element of
R st
J = a := r )
;
verum end;
end;
thus
( ( J = [0 ,{} ] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) implies J is Instruction of (SCM R) )
by A1, Th2; verum