let R be 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 Nat st I = goto (i1,R) or ex a being Data-Location of R ex i1 being 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 Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being 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 InstructionsF 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 Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being 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 Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being 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 Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being 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 Data-Locations : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of Data-Locations : verum } or
J in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } )
by A1, AMI_3:27, XBOOLE_0:def 3;
then
(
J in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } or
J in { [7,<*i*>,<*a*>] where i is Nat, a is Element of Data-Locations : verum } or
J in { [5,{},<*a,r*>] where a is Element of Data-Locations , 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 Data-Locations : I in {1,2,3,4} } or
J in { [6,<*i*>,{}] where i is Nat : verum } or
J in { [7,<*i*>,<*a*>] where i is Nat, a is Element of Data-Locations : verum } or
J in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } )
by XBOOLE_0:def 3;
per cases
( J in {[0,{},{}]} or J in { [6,<*i*>,{}] where i is Nat : verum } or J in { [7,<*i*>,<*a*>] where i is Nat, a is Element of Data-Locations : verum } or J in { [5,{},<*a,r*>] where a is Element of Data-Locations , r is Element of R : verum } or J in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of Data-Locations : 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 Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being 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 )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
Nat st
J = goto (
i1,
R) or ex
a being
Data-Location of
R ex
i1 being
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 )
by TARSKI:def 1;
verum end; suppose
J in { [6,<*i*>,{}] where i is 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 Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being 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
Nat such that A3:
J = [6,<*i*>,{}]
and
verum
;
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
Nat st
J = goto (
i1,
R) or ex
a being
Data-Location of
R ex
i1 being
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 Nat, a is Element of Data-Locations : 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 Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being 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
Nat,
a being
Element of
Data-Locations such that A4:
J = [7,<*i*>,<*a*>]
and
verum
;
reconsider A =
a as
Data-Location of
R by Th1, AMI_3:27;
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
Nat st
J = goto (
i1,
R) or ex
a being
Data-Location of
R ex
i1 being
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 Data-Locations , 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 Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being 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
Data-Locations ,
r being
Element of
R such that A5:
J = [5,{},<*a,r*>]
and
verum
;
reconsider A =
a as
Data-Location of
R by Th1, AMI_3:27;
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
Nat st
J = goto (
i1,
R) or ex
a being
Data-Location of
R ex
i1 being
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 Data-Locations : 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 Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being 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
Data-Locations 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, AMI_3:27;
(
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
Nat st
J = goto (
i1,
R) or ex
a being
Data-Location of
R ex
i1 being
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 Nat st J = goto (i1,R) or ex a being Data-Location of R ex i1 being 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, SCMRINGI:6; verum