:: SCMRING2 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
:: deftheorem Def1 defines SCM SCMRING2:def 1 :
:: deftheorem Def2 defines Data-Location SCMRING2:def 2 :
theorem Th1: :: SCMRING2:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th2: :: SCMRING2:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th3: :: SCMRING2:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th4: :: SCMRING2:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th5: :: SCMRING2:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th6: :: SCMRING2:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th7: :: SCMRING2:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
definition
let R be
good Ring;
let a,
b be
Data-Location of
R;
func a := b -> Instruction of
(SCM R) equals :: SCMRING2:def 3
[1,<*a,b*>];
coherence
[1,<*a,b*>] is Instruction of (SCM R)
func AddTo a,
b -> Instruction of
(SCM R) equals :: SCMRING2:def 4
[2,<*a,b*>];
coherence
[2,<*a,b*>] is Instruction of (SCM R)
func SubFrom a,
b -> Instruction of
(SCM R) equals :: SCMRING2:def 5
[3,<*a,b*>];
coherence
[3,<*a,b*>] is Instruction of (SCM R)
func MultBy a,
b -> Instruction of
(SCM R) equals :: SCMRING2:def 6
[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: :: SCMRING2:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th9: :: SCMRING2:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th10: :: SCMRING2:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def10 defines Next SCMRING2:def 10 :
theorem Th11: :: SCMRING2:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th12: :: SCMRING2:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th13: :: SCMRING2:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th14: :: SCMRING2:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th15: :: SCMRING2:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th16: :: SCMRING2:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: SCMRING2:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th18: :: SCMRING2:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th19: :: SCMRING2:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th20: :: SCMRING2:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th21: :: SCMRING2:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
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 Instruction-Location of (SCM R) holds not goto i1 is halting
Lm6:
for R being good Ring
for a being Data-Location of R
for i1 being Instruction-Location of (SCM R) 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
theorem :: SCMRING2:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: SCMRING2:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: SCMRING2:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: SCMRING2:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: SCMRING2:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: SCMRING2:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: SCMRING2:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th29: :: SCMRING2:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: SCMRING2:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) 