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

theorem :: AMI_6:1

for T being InsType of the InstructionsF of SCM holds
not not T = 0 & ... & not T = 8

proof end;

theorem Th2: :: AMI_6:2

JumpPart (halt SCM) = {} ;

theorem :: AMI_6:3

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

proof end;

theorem :: AMI_6:4

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

proof end;

theorem :: AMI_6:5

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

proof end;

theorem :: AMI_6:6

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

proof end;

theorem :: AMI_6:7

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

proof end;

theorem :: AMI_6:8

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

proof end;

theorem Th9: :: AMI_6:9

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

proof end;

theorem Th10: :: AMI_6:10

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

proof end;

theorem Th11: :: AMI_6:11

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

proof end;

theorem :: AMI_6:12

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

proof end;

theorem :: AMI_6:13

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

proof end;

theorem :: AMI_6:14

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

proof end;

Lm1: for i being Instruction of SCM st ( for l being Element of NAT holds NIC (i,l) = {(l + 1)} ) 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 by AMI_3:2;

cluster AddTo (a,b) -> sequential ;

coherence
AddTo (a,b) is sequential by AMI_3:3;

cluster SubFrom (a,b) -> sequential ;

coherence
SubFrom (a,b) is sequential by AMI_3:4;

cluster MultBy (a,b) -> sequential ;

coherence
MultBy (a,b) is sequential by AMI_3:5;

cluster Divide (a,b) -> sequential ;

coherence
Divide (a,b) is sequential by AMI_3:6;

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 Th15: :: AMI_6:15

for il, k being Nat holds NIC ((SCM-goto k),il) = {k}

proof end;

theorem Th16: :: AMI_6:16

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

proof end;

registration

let i1 be Nat;

cluster JUMP (SCM-goto i1) -> 1 -element ;

coherence
JUMP (SCM-goto i1) is 1 -element

proof end;

end;

theorem Th17: :: AMI_6:17

for a being Data-Location
for il, k being Nat holds NIC ((a =0_goto k),il) = {k,(il + 1)}

proof end;

theorem Th18: :: AMI_6:18

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

proof end;

registration

let a be Data-Location;
let i1 be Nat;

cluster JUMP (a =0_goto i1) -> 1 -element ;

coherence
JUMP (a =0_goto i1) is 1 -element

proof end;

end;

theorem Th19: :: AMI_6:19

for a being Data-Location
for il, k being Nat holds NIC ((a >0_goto k),il) = {k,(il + 1)}

proof end;

theorem Th20: :: AMI_6:20

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

proof end;

registration

let a be Data-Location;
let i1 be Nat;

cluster JUMP (a >0_goto i1) -> 1 -element ;

coherence
JUMP (a >0_goto i1) is 1 -element

proof end;

end;

theorem Th21: :: AMI_6:21

for il being Nat holds SUCC (il,SCM) = {il,(il + 1)}

proof end;

theorem Th22: :: AMI_6:22

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

proof end;

registration

cluster SCM -> standard ;

coherence
SCM is standard by Th22, AMISTD_1:3;

end;

registration

cluster InsCode (halt SCM) -> jump-only for InsType of the InstructionsF of SCM;

coherence
for b₁ being InsType of the InstructionsF 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 ;

end;

registration

let i1 be Nat;

cluster InsCode (SCM-goto i1) -> jump-only for InsType of the InstructionsF of SCM;

coherence
for b₁ being InsType of the InstructionsF of SCM st b₁ = InsCode (SCM-goto i1) holds
b₁ is jump-only

proof end;

end;

registration

let i1 be 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 Nat;

cluster InsCode (a =0_goto i1) -> jump-only for InsType of the InstructionsF of SCM;

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

proof end;

cluster InsCode (a >0_goto i1) -> jump-only for InsType of the InstructionsF of SCM;

coherence
for b₁ being InsType of the InstructionsF 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 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;

Lm2: dl. 0 <> dl. 1
by AMI_3:10;

registration

let a, b be Data-Location;

cluster InsCode (a := b) -> non jump-only for InsType of the InstructionsF of SCM;

coherence
for b₁ being InsType of the InstructionsF of SCM st b₁ = InsCode (a := b) holds
not b₁ is jump-only

proof end;

cluster InsCode (AddTo (a,b)) -> non jump-only for InsType of the InstructionsF of SCM;

coherence
for b₁ being InsType of the InstructionsF of SCM st b₁ = InsCode (AddTo (a,b)) holds
not b₁ is jump-only

proof end;

cluster InsCode (SubFrom (a,b)) -> non jump-only for InsType of the InstructionsF of SCM;

coherence
for b₁ being InsType of the InstructionsF of SCM st b₁ = InsCode (SubFrom (a,b)) holds
not b₁ is jump-only

proof end;

cluster InsCode (MultBy (a,b)) -> non jump-only for InsType of the InstructionsF of SCM;

coherence
for b₁ being InsType of the InstructionsF of SCM st b₁ = InsCode (MultBy (a,b)) holds
not b₁ is jump-only

proof end;

cluster InsCode (Divide (a,b)) -> non jump-only for InsType of the InstructionsF of SCM;

coherence
for b₁ being InsType of the InstructionsF 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 ;

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

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

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

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

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

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

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

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

end;

registration

cluster SCM -> with_explicit_jumps ;

coherence
SCM is with_explicit_jumps

proof end;

end;

theorem Th23: :: AMI_6:23

for i1, k being Nat holds IncAddr ((SCM-goto i1),k) = SCM-goto (i1 + k)

proof end;

theorem Th24: :: AMI_6:24

for a being Data-Location
for i1, k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)

proof end;

theorem Th25: :: AMI_6:25

for a being Data-Location
for i1, k being Nat holds IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k)

proof end;

registration

cluster SCM -> IC-relocable ;

coherence
SCM is IC-relocable

proof end;

end;