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