:: 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 b1 being InsType of the InstructionsF of SCM st b1 = InsCode (halt SCM) holds
b1 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 b1 being InsType of the InstructionsF of SCM st b1 = InsCode (SCM-goto i1) holds
b1 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 b1 being InsType of the InstructionsF of SCM st b1 = InsCode (a =0_goto i1) holds
b1 is jump-only
proof end;
cluster InsCode (a >0_goto i1) -> jump-only for InsType of the InstructionsF of SCM;
coherence
for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (a >0_goto i1) holds
b1 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 b1 being InsType of the InstructionsF of SCM st b1 = InsCode (a := b) holds
not b1 is jump-only
proof end;
cluster InsCode (AddTo (a,b)) -> non jump-only for InsType of the InstructionsF of SCM;
coherence
for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (AddTo (a,b)) holds
not b1 is jump-only
proof end;
cluster InsCode (SubFrom (a,b)) -> non jump-only for InsType of the InstructionsF of SCM;
coherence
for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (SubFrom (a,b)) holds
not b1 is jump-only
proof end;
cluster InsCode (MultBy (a,b)) -> non jump-only for InsType of the InstructionsF of SCM;
coherence
for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (MultBy (a,b)) holds
not b1 is jump-only
proof end;
cluster InsCode (Divide (a,b)) -> non jump-only for InsType of the InstructionsF of SCM;
coherence
for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (Divide (a,b)) holds
not b1 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;