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

begin

theorem Th1: :: AMI_6:1

for a being Data-Location holds not a in NAT

proof end;

theorem :: 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 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 NPP s1 = NPP s2 holds
s1 . a = s2 . a

proof end;

registration

cluster InsCodes SCM -> non empty ;
coherence
not InsCodes SCM is empty ;

end;

theorem :: AMI_6:6

canceled;

theorem Th7: :: AMI_6:7

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:8

canceled;

theorem Th9: :: AMI_6:9

JumpPart (halt SCM) = {} ;

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 :: AMI_6:16

canceled;

theorem :: AMI_6:17

canceled;

theorem Th18: :: AMI_6:18

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

proof end;

theorem Th19: :: AMI_6:19

for T being InsType of SCM st T = 1 holds
JumpParts T = {{}}

proof end;

theorem Th20: :: AMI_6:20

for T being InsType of SCM st T = 2 holds
JumpParts T = {{}}

proof end;

theorem Th21: :: AMI_6:21

for T being InsType of SCM st T = 3 holds
JumpParts T = {{}}

proof end;

theorem Th22: :: AMI_6:22

for T being InsType of SCM st T = 4 holds
JumpParts T = {{}}

proof end;

theorem Th23: :: AMI_6:23

for T being InsType of SCM st T = 5 holds
JumpParts T = {{}}

proof end;

theorem Th24: :: AMI_6:24

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

proof end;

theorem Th25: :: AMI_6:25

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

proof end;

theorem Th26: :: AMI_6:26

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

proof end;

theorem :: AMI_6:27

canceled;

theorem :: AMI_6:28

canceled;

theorem :: AMI_6:29

canceled;

theorem :: AMI_6:30

canceled;

theorem :: AMI_6:31

canceled;

theorem :: AMI_6:32

canceled;

theorem :: AMI_6:33

canceled;

theorem :: AMI_6:34

canceled;

theorem :: AMI_6:35

canceled;

theorem :: AMI_6:36

canceled;

theorem Th37: :: AMI_6:37

for k1 being natural number holds (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 = NAT

proof end;

theorem Th38: :: AMI_6:38

for a being Data-Location
for k1 being natural number holds (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 = NAT

proof end;

theorem :: AMI_6:39

canceled;

theorem Th40: :: AMI_6:40

for a being Data-Location
for k1 being natural number holds (product" (JumpParts (InsCode (a >0_goto k1)))) . 1 = NAT

proof end;

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

proof end;

registration

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

end;

registration

let a, b be Data-Location ;
cluster a := b -> sequential ;
coherence
a := b is sequential

proof end;

cluster AddTo (a,b) -> sequential ;
coherence
AddTo (a,b) is sequential

proof end;

cluster SubFrom (a,b) -> sequential ;
coherence
SubFrom (a,b) is sequential

proof end;

cluster MultBy (a,b) -> sequential ;
coherence
MultBy (a,b) is sequential

proof end;

cluster Divide (a,b) -> sequential ;
coherence
Divide (a,b) is sequential

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

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 :: AMI_6:41

canceled;

theorem :: AMI_6:42

canceled;

theorem :: AMI_6:43

canceled;

theorem :: AMI_6:44

canceled;

theorem :: AMI_6:45

canceled;

theorem :: AMI_6:46

canceled;

theorem :: AMI_6:47

canceled;

theorem Th48: :: AMI_6:48

for il being Element of NAT
for k being natural number holds NIC ((SCM-goto k),il) = {k}

proof end;

theorem Th49: :: AMI_6:49

for k being natural number holds JUMP (SCM-goto k) = {k}

proof end;

registration

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

proof end;

end;

theorem Th50: :: AMI_6:50

for a being Data-Location
for il being Element of NAT
for k being natural number holds NIC ((a =0_goto k),il) = {k,(succ il)}

proof end;

theorem Th51: :: AMI_6:51

for a being Data-Location
for k being natural number holds JUMP (a =0_goto k) = {k}

proof end;

registration

let a be Data-Location ;
let i1 be Element of NAT ;
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 a being Data-Location
for il being Element of NAT
for k being natural number holds NIC ((a >0_goto k),il) = {k,(succ il)}

proof end;

theorem Th53: :: AMI_6:53

for a being Data-Location
for k being natural number holds JUMP (a >0_goto k) = {k}

proof end;

registration

let a be Data-Location ;
let i1 be Element of NAT ;
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 Th54: :: AMI_6:54

for il being Element of NAT holds SUCC (il,SCM) = {il,(succ il)}

proof end;

theorem Th55: :: AMI_6:55

for k being Element of NAT holds
( k + 1 in SUCC (k,SCM) & ( for j being Element of NAT st j in SUCC (k,SCM) holds
k <= j ) )

proof end;

registration

cluster SCM -> standard ;
coherence
SCM is standard by Th55, AMISTD_1:19;

end;

registration

cluster InsCode (halt SCM) -> jump-only InsType of SCM;
coherence
for b₁ being InsType of SCM st b₁ = InsCode (halt SCM) holds
b₁ is jump-only

proof end;

end;

registration

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

proof end;

end;

registration

let i1 be Element of NAT ;
cluster InsCode (SCM-goto i1) -> jump-only InsType of SCM;
coherence
for b₁ being InsType of SCM st b₁ = InsCode (SCM-goto i1) holds
b₁ is jump-only

proof end;

end;

registration

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

proof end;

end;

registration

let a be Data-Location ;
let i1 be Element of NAT ;
cluster InsCode (a =0_goto i1) -> jump-only InsType of SCM;
coherence
for b₁ being InsType of SCM st b₁ = InsCode (a =0_goto i1) holds
b₁ is jump-only

proof end;

cluster InsCode (a >0_goto i1) -> jump-only InsType of SCM;
coherence
for b₁ being InsType of SCM st b₁ = InsCode (a >0_goto i1) holds
b₁ is jump-only

proof end;

end;

registration

let a be Data-Location ;
let i1 be Element of NAT ;
cluster a =0_goto i1 -> non ins-loc-free jump-only non sequential ;
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 -> non ins-loc-free jump-only non sequential ;
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;

Lm3: 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
for b₁ being InsType of SCM st b₁ = InsCode (a := b) holds
not b₁ is jump-only

proof end;

cluster InsCode (AddTo (a,b)) -> non jump-only InsType of SCM;
coherence
for b₁ being InsType of SCM st b₁ = InsCode (AddTo (a,b)) holds
not b₁ is jump-only

proof end;

cluster InsCode (SubFrom (a,b)) -> non jump-only InsType of SCM;
coherence
for b₁ being InsType of SCM st b₁ = InsCode (SubFrom (a,b)) holds
not b₁ is jump-only

proof end;

cluster InsCode (MultBy (a,b)) -> non jump-only InsType of SCM;
coherence
for b₁ being InsType of SCM st b₁ = InsCode (MultBy (a,b)) holds
not b₁ is jump-only

proof end;

cluster InsCode (Divide (a,b)) -> non jump-only InsType of SCM;
coherence
for b₁ being InsType of SCM st b₁ = InsCode (Divide (a,b)) holds
not b₁ is jump-only

proof end;

end;

registration

let a, b be Data-Location ;
cluster a := b -> non jump-only ;
coherence
not a := b is jump-only

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

end;

registration

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

proof end;

end;

registration

cluster SCM -> regular J/A-independent ;
coherence
( SCM is regular & SCM is J/A-independent )

proof end;

end;

theorem :: AMI_6:56

canceled;

theorem :: AMI_6:57

canceled;

theorem :: AMI_6:58

canceled;

theorem Th59: :: AMI_6:59

for i1 being Element of NAT
for k being natural number holds IncAddr ((SCM-goto i1),k) = SCM-goto (i1 + k)

proof end;

theorem Th60: :: AMI_6:60

for a being Data-Location
for i1 being Element of NAT
for k being natural number holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)

proof end;

theorem Th61: :: AMI_6:61

for a being Data-Location
for i1 being Element of NAT
for k being natural number holds IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k)

proof end;

registration

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

proof end;

end;