begin
Lm2:
for R being Ring holds the carrier of (SCM R) \ {NAT} = SCM-Data-Loc
definition
let R be
Ring;
let a,
b be
Data-Location of
R;
coherence
[1,{},<*a,b*>] is Instruction of (SCM R)
coherence
[2,{},<*a,b*>] is Instruction of (SCM R)
coherence
[3,{},<*a,b*>] is Instruction of (SCM R)
coherence
[4,{},<*a,b*>] is Instruction of (SCM R)
end;
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
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 ) )
begin
begin
Lm3:
for R being Ring
for a, b being Data-Location of R holds not a := b is halting
Lm4:
for R being Ring
for a, b being Data-Location of R holds not AddTo (a,b) is halting
Lm5:
for R being Ring
for a, b being Data-Location of R holds not SubFrom (a,b) is halting
Lm6:
for R being Ring
for a, b being Data-Location of R holds not MultBy (a,b) is halting
Lm7:
for R being Ring
for i1 being Element of NAT holds not goto (i1,R) is halting
Lm8:
for R being Ring
for a being Data-Location of R
for i1 being Element of NAT holds not a =0_goto i1 is halting
Lm9:
for R being Ring
for r being Element of R
for a being Data-Location of R holds not a := r is halting
Lm10:
for R being Ring
for W being Instruction of (SCM R) st W is halting holds
W = [0,{},{}]