:: On the Instructions of { \bf SCM }
:: by Artur Korni{\l}owicz
::
:: Received May 8, 2001
:: Copyright (c) 2001 Association of Mizar Users

theorem Th1: :: AMI_6:1

for a being Data-Location holds not a in NAT

proof end;

theorem Th2: :: AMI_6:2

SCM-Data-Loc <> NAT by AMI_2:12;

theorem Th3: :: AMI_6:3

for o being Object of SCM holds
( o = IC SCM or o in NAT or o is Data-Location )

proof end;

theorem :: AMI_6:4

canceled;

theorem Th5: :: AMI_6:5

for a being Data-Location
for s1, s2 being State of SCM st s1,s2 equal_outside NAT holds
s1 . a = s2 . a

proof end;

Lm1: for x, y being set st x in dom <*y*> holds
x = 1

proof end;

Lm2: for x, y, z being set holds
( not x in dom <*y,z*> or x = 1 or x = 2 )

proof end;

Lm3: 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 )

proof end;

theorem :: AMI_6:6

canceled;

theorem Th7: :: AMI_6:7

AddressPart (halt SCM ) = {} by AMI_3:71, MCART_1:def 2;

theorem :: AMI_6:8

canceled;

theorem :: AMI_6:9

canceled;

theorem :: AMI_6:10

canceled;

theorem :: AMI_6:11

canceled;

theorem :: AMI_6:12

canceled;

theorem :: AMI_6:13

canceled;

theorem :: AMI_6:14

canceled;

theorem :: AMI_6:15

canceled;

theorem Th16: :: AMI_6:16

for T being InsType of SCM st T = 0 holds
AddressParts T = {0 }

proof end;

registration

let T be InsType of SCM ;
cluster AddressParts T -> non empty ;
coherence
not AddressParts T is empty

proof end;

end;

theorem Th17: :: AMI_6:17

for T being InsType of SCM st T = 1 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th18: :: AMI_6:18

for T being InsType of SCM st T = 2 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th19: :: AMI_6:19

for T being InsType of SCM st T = 3 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th20: :: AMI_6:20

for T being InsType of SCM st T = 4 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th21: :: AMI_6:21

for T being InsType of SCM st T = 5 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th22: :: AMI_6:22

for T being InsType of SCM st T = 6 holds
dom (product" (AddressParts T)) = {1}

proof end;

theorem Th23: :: AMI_6:23

for T being InsType of SCM st T = 7 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th24: :: AMI_6:24

for T being InsType of SCM st T = 8 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th25: :: AMI_6:25

for a, b being Data-Location holds (product" (AddressParts (InsCode (a := b)))) . 1 = SCM-Data-Loc

proof end;

theorem Th26: :: AMI_6:26

for a, b being Data-Location holds (product" (AddressParts (InsCode (a := b)))) . 2 = SCM-Data-Loc

proof end;

theorem Th27: :: AMI_6:27

for a, b being Data-Location holds (product" (AddressParts (InsCode (AddTo a,b)))) . 1 = SCM-Data-Loc

proof end;

theorem Th28: :: AMI_6:28

for a, b being Data-Location holds (product" (AddressParts (InsCode (AddTo a,b)))) . 2 = SCM-Data-Loc

proof end;

theorem Th29: :: AMI_6:29

for a, b being Data-Location holds (product" (AddressParts (InsCode (SubFrom a,b)))) . 1 = SCM-Data-Loc

proof end;

theorem Th30: :: AMI_6:30

for a, b being Data-Location holds (product" (AddressParts (InsCode (SubFrom a,b)))) . 2 = SCM-Data-Loc

proof end;

theorem Th31: :: AMI_6:31

for a, b being Data-Location holds (product" (AddressParts (InsCode (MultBy a,b)))) . 1 = SCM-Data-Loc

proof end;

theorem Th32: :: AMI_6:32

for a, b being Data-Location holds (product" (AddressParts (InsCode (MultBy a,b)))) . 2 = SCM-Data-Loc

proof end;

theorem Th33: :: AMI_6:33

for a, b being Data-Location holds (product" (AddressParts (InsCode (Divide a,b)))) . 1 = SCM-Data-Loc

proof end;

theorem Th34: :: AMI_6:34

for a, b being Data-Location holds (product" (AddressParts (InsCode (Divide a,b)))) . 2 = SCM-Data-Loc

proof end;

theorem Th35: :: AMI_6:35

for i1 being Instruction-Location of SCM holds (product" (AddressParts (InsCode (goto i1)))) . 1 = NAT

proof end;

theorem Th36: :: AMI_6:36

for a being Data-Location
for i1 being Instruction-Location of SCM holds (product" (AddressParts (InsCode (a =0_goto i1)))) . 1 = NAT

proof end;

theorem Th37: :: AMI_6:37

for a being Data-Location
for i1 being Instruction-Location of SCM holds (product" (AddressParts (InsCode (a =0_goto i1)))) . 2 = SCM-Data-Loc

proof end;

theorem Th38: :: AMI_6:38

for a being Data-Location
for i1 being Instruction-Location of SCM holds (product" (AddressParts (InsCode (a >0_goto i1)))) . 1 = NAT

proof end;

theorem Th39: :: AMI_6:39

for a being Data-Location
for i1 being Instruction-Location of SCM holds (product" (AddressParts (InsCode (a >0_goto i1)))) . 2 = SCM-Data-Loc

proof end;

Lm4: for l being Instruction-Location of SCM
for i being Instruction of SCM st ( for s being State of SCM st IC s = l & s . l = i holds
(Exec i,s) . (IC SCM ) = Next ) holds
NIC i,l = {(Next )}

proof end;

Lm5: for i being Instruction of SCM st ( for l being Instruction-Location of SCM holds NIC i,l = {(Next )} ) holds
JUMP i is empty

proof end;

theorem Th40: :: AMI_6:40

for il being Instruction-Location of SCM holds NIC (halt SCM ),il = {il}

proof end;

registration

cluster JUMP (halt SCM ) -> empty ;
coherence
JUMP (halt SCM ) is empty ;

end;

theorem Th41: :: AMI_6:41

for a, b being Data-Location
for il being Instruction-Location of SCM holds NIC (a := b),il = {(Next )}

proof end;

registration

let a, b be Data-Location ;
cluster JUMP (a := b) -> empty ;
coherence
JUMP (a := b) is empty

proof end;

end;

theorem Th42: :: AMI_6:42

for a, b being Data-Location
for il being Instruction-Location of SCM holds NIC (AddTo a,b),il = {(Next )}

proof end;

registration

let a, b be Data-Location ;
cluster JUMP (AddTo a,b) -> empty ;
coherence
JUMP (AddTo a,b) is empty

proof end;

end;

theorem Th43: :: AMI_6:43

for a, b being Data-Location
for il being Instruction-Location of SCM holds NIC (SubFrom a,b),il = {(Next )}

proof end;

registration

let a, b be Data-Location ;
cluster JUMP (SubFrom a,b) -> empty ;
coherence
JUMP (SubFrom a,b) is empty

proof end;

end;

theorem Th44: :: AMI_6:44

for a, b being Data-Location
for il being Instruction-Location of SCM holds NIC (MultBy a,b),il = {(Next )}

proof end;

registration

let a, b be Data-Location ;
cluster JUMP (MultBy a,b) -> empty ;
coherence
JUMP (MultBy a,b) is empty

proof end;

end;

theorem Th45: :: AMI_6:45

for a, b being Data-Location
for il being Instruction-Location of SCM holds NIC (Divide a,b),il = {(Next )}

proof end;

registration

let a, b be Data-Location ;
cluster JUMP (Divide a,b) -> empty ;
coherence
JUMP (Divide a,b) is empty

proof end;

end;

theorem Th46: :: AMI_6:46

for i1, il being Instruction-Location of SCM holds NIC (goto i1),il = {i1}

proof end;

theorem Th47: :: AMI_6:47

for i1 being Instruction-Location of SCM holds JUMP (goto i1) = {i1}

proof end;

registration

let i1 be Instruction-Location of SCM ;
cluster JUMP (goto i1) -> non empty trivial ;
coherence
( not JUMP (goto i1) is empty & JUMP (goto i1) is trivial )

proof end;

end;

theorem Th48: :: AMI_6:48

for a being Data-Location
for i1, il being Instruction-Location of SCM holds NIC (a =0_goto i1),il = {i1,(Next )}

proof end;

theorem Th49: :: AMI_6:49

for a being Data-Location
for i1 being Instruction-Location of SCM holds JUMP (a =0_goto i1) = {i1}

proof end;

registration

let a be Data-Location ;
let i1 be Instruction-Location of SCM ;
cluster JUMP (a =0_goto i1) -> non empty trivial ;
coherence
( not JUMP (a =0_goto i1) is empty & JUMP (a =0_goto i1) is trivial )

proof end;

end;

theorem Th50: :: AMI_6:50

for a being Data-Location
for i1, il being Instruction-Location of SCM holds NIC (a >0_goto i1),il = {i1,(Next )}

proof end;

theorem Th51: :: AMI_6:51

for a being Data-Location
for i1 being Instruction-Location of SCM holds JUMP (a >0_goto i1) = {i1}

proof end;

registration

let a be Data-Location ;
let i1 be Instruction-Location of SCM ;
cluster JUMP (a >0_goto i1) -> non empty trivial ;
coherence
( not JUMP (a >0_goto i1) is empty & JUMP (a >0_goto i1) is trivial )

proof end;

end;

theorem Th52: :: AMI_6:52

for il being Instruction-Location of SCM holds SUCC il = {il,(Next )}

proof end;

theorem Th53: :: AMI_6:53

for f being IL-Function of NAT , SCM st ( for k being Element of NAT holds f . k = il. k ) holds
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) ) ) )

proof end;

registration

cluster SCM -> standard ;
coherence
SCM is standard

proof end;

end;

theorem Th54: :: AMI_6:54

for k being natural number holds il. SCM ,k = il. k

proof end;

theorem Th55: :: AMI_6:55

for k being natural number holds Next = il. SCM ,(k + 1)

proof end;

theorem Th56: :: AMI_6:56

for il being Instruction-Location of SCM holds Next = NextLoc il

proof end;

registration

cluster InsCode (halt SCM ) -> jump-only InsType of SCM ;
coherence
InsCode (halt SCM ) is jump-only InsType of SCM

proof end;

end;

registration

cluster halt SCM -> jump-only ;
coherence
halt SCM is jump-only

proof end;

end;

registration

let i1 be Instruction-Location of SCM ;
cluster InsCode (goto i1) -> jump-only InsType of SCM ;
coherence
InsCode (goto i1) is jump-only InsType of SCM

proof end;

end;

registration

let i1 be Instruction-Location of SCM ;
cluster goto i1 -> jump-only non sequential non ins-loc-free ;
coherence
( goto i1 is jump-only & not goto i1 is sequential & not goto i1 is ins-loc-free )

proof end;

end;

registration

let a be Data-Location ;
let i1 be Instruction-Location of SCM ;
cluster InsCode (a =0_goto i1) -> jump-only InsType of SCM ;
coherence
InsCode (a =0_goto i1) is jump-only InsType of SCM

proof end;

cluster InsCode (a >0_goto i1) -> jump-only InsType of SCM ;
coherence
InsCode (a >0_goto i1) is jump-only InsType of SCM

proof end;

end;

registration

let a be Data-Location ;
let i1 be Instruction-Location of SCM ;
cluster a =0_goto i1 -> jump-only non sequential non ins-loc-free ;
coherence
( a =0_goto i1 is jump-only & not a =0_goto i1 is sequential & not a =0_goto i1 is ins-loc-free )

proof end;

cluster a >0_goto i1 -> jump-only non sequential non ins-loc-free ;
coherence
( a >0_goto i1 is jump-only & not a >0_goto i1 is sequential & not a >0_goto i1 is ins-loc-free )

proof end;

end;

Lm6: dl. 0 <> dl. 1
by AMI_3:52;

registration

let a, b be Data-Location ;
cluster InsCode (a := b) -> non jump-only InsType of SCM ;
coherence
InsCode (a := b) is non jump-only InsType of SCM

proof end;

cluster InsCode (AddTo a,b) -> non jump-only InsType of SCM ;
coherence
InsCode (AddTo a,b) is non jump-only InsType of SCM

proof end;

cluster InsCode (SubFrom a,b) -> non jump-only InsType of SCM ;
coherence
InsCode (SubFrom a,b) is non jump-only InsType of SCM

proof end;

cluster InsCode (MultBy a,b) -> non jump-only InsType of SCM ;
coherence
InsCode (MultBy a,b) is non jump-only InsType of SCM

proof end;

cluster InsCode (Divide a,b) -> non jump-only InsType of SCM ;
coherence
InsCode (Divide a,b) is non jump-only InsType of SCM

proof end;

end;

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 )

proof end;

cluster AddTo a,b -> non jump-only sequential ;
coherence
( not AddTo a,b is jump-only & AddTo a,b is sequential )

proof end;

cluster SubFrom a,b -> non jump-only sequential ;
coherence
( not SubFrom a,b is jump-only & SubFrom a,b is sequential )

proof end;

cluster MultBy a,b -> non jump-only sequential ;
coherence
( not MultBy a,b is jump-only & MultBy a,b is sequential )

proof end;

cluster Divide a,b -> non jump-only sequential ;
coherence
( not Divide a,b is jump-only & Divide a,b is sequential )

proof end;

end;

registration

cluster SCM -> homogeneous with_explicit_jumps without_implicit_jumps ;
coherence
( SCM is homogeneous & SCM is with_explicit_jumps & SCM is without_implicit_jumps )

proof end;

end;

registration

cluster SCM -> regular ;
coherence
SCM is regular

proof end;

end;

theorem Th57: :: AMI_6:57

for i1 being Instruction-Location of SCM
for k being natural number holds IncAddr (goto i1),k = goto (il. SCM ,((locnum i1) + k))

proof end;

theorem Th58: :: AMI_6:58

for a being Data-Location
for i1 being Instruction-Location of SCM
for k being natural number holds IncAddr (a =0_goto i1),k = a =0_goto (il. SCM ,((locnum i1) + k))

proof end;

theorem Th59: :: AMI_6:59

for a being Data-Location
for i1 being Instruction-Location of SCM
for k being natural number holds IncAddr (a >0_goto i1),k = a >0_goto (il. SCM ,((locnum i1) + k))

proof end;

registration

cluster SCM -> IC-good Exec-preserving ;
coherence
( SCM is IC-good & SCM is Exec-preserving )

proof end;

end;