begin
theorem Th1:
theorem
theorem Th3:
theorem
canceled;
theorem Th5:
theorem
canceled;
theorem Th7:
for
T being
InsType of
SCM holds
(
T = 0 or
T = 1 or
T = 2 or
T = 3 or
T = 4 or
T = 5 or
T = 6 or
T = 7 or
T = 8 )
theorem
canceled;
theorem Th9:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th37:
theorem Th38:
theorem
canceled;
theorem Th40:
Lm1:
for l being Element of NAT
for i being Instruction of SCM st ( for s being State of SCM st IC s = l holds
(Exec (i,s)) . (IC ) = succ (IC s) ) holds
NIC (i,l) = {(succ l)}
Lm2:
for i being Instruction of SCM st ( for l being Element of NAT holds NIC (i,l) = {(succ l)} ) holds
JUMP i is empty
theorem
canceled;
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
Lm3:
dl. 0 <> dl. 1
by AMI_3:52;
registration
let a,
b be
Data-Location ;
cluster a := b -> non
jump-only sequential ;
coherence
( not a := b is jump-only & a := b is sequential )
cluster AddTo (
a,
b)
-> non
jump-only sequential ;
coherence
( not AddTo (a,b) is jump-only & AddTo (a,b) is sequential )
cluster SubFrom (
a,
b)
-> non
jump-only sequential ;
coherence
( not SubFrom (a,b) is jump-only & SubFrom (a,b) is sequential )
cluster MultBy (
a,
b)
-> non
jump-only sequential ;
coherence
( not MultBy (a,b) is jump-only & MultBy (a,b) is sequential )
cluster Divide (
a,
b)
-> non
jump-only sequential ;
coherence
( not Divide (a,b) is jump-only & Divide (a,b) is sequential )
end;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th59:
theorem Th60:
theorem Th61: