begin
:: deftheorem Def1 defines SCM SCMRING2:def 1 :
for R being good Ring
for b2 being strict AMI-Struct of {the carrier of R} holds
( b2 = SCM R iff ( the carrier of b2 = SCM-Memory & the Instruction-Counter of b2 = NAT & the Instructions of b2 = SCM-Instr R & the haltF of b2 = [0 ,{} ,{} ] & the Object-Kind of b2 = SCM-OK R & the Execution of b2 = SCM-Exec R ) );
:: deftheorem Def2 defines Data-Location SCMRING2:def 2 :
for R being good Ring
for b2 being Object of (SCM R) holds
( b2 is Data-Location of R iff b2 in the carrier of (SCM R) \ (NAT \/ {NAT }) );
theorem Th1:
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
definition
let R be
good Ring;
let a,
b be
Data-Location of
R;
func a := b -> Instruction of
(SCM R) equals
[1,{} ,<*a,b*>];
coherence
[1,{} ,<*a,b*>] is Instruction of (SCM R)
func AddTo a,
b -> Instruction of
(SCM R) equals
[2,{} ,<*a,b*>];
coherence
[2,{} ,<*a,b*>] is Instruction of (SCM R)
func SubFrom a,
b -> Instruction of
(SCM R) equals
[3,{} ,<*a,b*>];
coherence
[3,{} ,<*a,b*>] is Instruction of (SCM R)
func MultBy a,
b -> Instruction of
(SCM R) equals
[4,{} ,<*a,b*>];
coherence
[4,{} ,<*a,b*>] is Instruction of (SCM R)
end;
:: deftheorem defines := SCMRING2:def 3 :
for R being good Ring
for a, b being Data-Location of R holds a := b = [1,{} ,<*a,b*>];
:: deftheorem defines AddTo SCMRING2:def 4 :
for R being good Ring
for a, b being Data-Location of R holds AddTo a,b = [2,{} ,<*a,b*>];
:: deftheorem defines SubFrom SCMRING2:def 5 :
for R being good Ring
for a, b being Data-Location of R holds SubFrom a,b = [3,{} ,<*a,b*>];
:: deftheorem defines MultBy SCMRING2:def 6 :
for R being good Ring
for a, b being Data-Location of R holds MultBy a,b = [4,{} ,<*a,b*>];
:: deftheorem defines := SCMRING2:def 7 :
for R being good Ring
for a being Data-Location of R
for r being Element of R holds a := r = [5,{} ,<*a,r*>];
:: deftheorem defines goto SCMRING2:def 8 :
for R being good Ring
for l being Element of NAT holds goto l,R = [6,<*l*>,{} ];
:: deftheorem defines =0_goto SCMRING2:def 9 :
for R being good Ring
for l being Element of NAT
for a being Data-Location of R holds a =0_goto l = [7,<*l*>,<*a*>];
theorem Th8:
for
R being
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 ) )
theorem
theorem
theorem
canceled;
theorem Th12:
begin
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem Th19:
begin
theorem Th20:
theorem Th21:
Lm1:
for R being good Ring
for a, b being Data-Location of R holds not a := b is halting
Lm2:
for R being good Ring
for a, b being Data-Location of R holds not AddTo a,b is halting
Lm3:
for R being good Ring
for a, b being Data-Location of R holds not SubFrom a,b is halting
Lm4:
for R being good Ring
for a, b being Data-Location of R holds not MultBy a,b is halting
Lm5:
for R being good Ring
for i1 being Element of NAT holds not goto i1,R is halting
Lm6:
for R being good Ring
for a being Data-Location of R
for i1 being Element of NAT holds not a =0_goto i1 is halting
Lm7:
for R being good Ring
for r being Element of R
for a being Data-Location of R holds not a := r is halting
Lm8:
for R being good Ring
for W being Instruction of (SCM R) st W is halting holds
W = [0 ,{} ,{} ]
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th29:
theorem
theorem