begin
:: deftheorem Def1 defines SCM SCMRING2:def 1 :
:: deftheorem Def2 defines Data-Location SCMRING2:def 2 :
theorem Th1:
theorem Th2:
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 :
:: deftheorem defines AddTo SCMRING2:def 4 :
:: deftheorem defines SubFrom SCMRING2:def 5 :
:: deftheorem defines MultBy SCMRING2:def 6 :
:: deftheorem defines := SCMRING2:def 7 :
:: deftheorem defines goto SCMRING2:def 8 :
:: deftheorem defines =0_goto SCMRING2:def 9 :
theorem Th8:
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