begin
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
canceled;
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
Lm1:
for x, y being set st x in dom <*y*> holds
x = 1
Lm2:
for x, y, z being set holds
( not x in dom <*y,z*> or x = 1 or x = 2 )
Lm3:
for x, y, z, t being set holds
( not x in dom <*y,z,t*> or x = 1 or x = 2 or x = 3 )
Lm4:
for T being InsType of 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 or T = 9 or T = 10 or T = 11 or T = 12 )
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem
theorem
theorem
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
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:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
Lm5:
for l being Instruction-Location of SCM+FSA
for i being Instruction of st ( for s being State of st IC s = l & s . l = i holds
(Exec i,s) . (IC SCM+FSA ) = Next (IC s) ) holds
NIC i,l = {(Next l)}
Lm6:
for i being Instruction of st ( for l being Instruction-Location of SCM+FSA holds NIC i,l = {(Next l)} ) holds
JUMP i is empty
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem Th80:
theorem Th81:
theorem Th82:
theorem Th83:
theorem Th84:
theorem Th85:
theorem Th86:
theorem Th87:
theorem Th88:
Lm7:
intloc 0 <> intloc 1
by AMI_3:52;
registration
let a,
b be
Int-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;
Lm8:
fsloc 0 <> intloc 0
by SCMFSA_2:126;
Lm9:
fsloc 0 <> intloc 1
by SCMFSA_2:126;
theorem Th89:
theorem Th90:
theorem Th91: