theorem Th7:
for
R being
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 ) )