:: On the Instructions of { \bf SCM }
:: by Artur Korni{\l}owicz
::
:: Received May 8, 2001
:: Copyright (c) 2001-2018 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

theorem :: AMI_6:3
for T being InsType of the InstructionsF of SCM st T = 0 holds
JumpParts T =
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 () = {1}
proof end;

theorem Th10: :: AMI_6:10
for T being InsType of the InstructionsF of SCM st T = 7 holds
dom () = {1}
proof end;

theorem Th11: :: AMI_6:11
for T being InsType of the InstructionsF of SCM st T = 8 holds
dom () = {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 () -> empty ;
coherence
JUMP () 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 ((),il) = {k}
proof end;

theorem Th16: :: AMI_6:16
for k being Nat holds JUMP () = {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
coherence by ;
end;

registration
cluster K81(()) -> jump-only for InsType of the InstructionsF of SCM;
coherence
for b1 being InsType of the InstructionsF of SCM st b1 = InsCode () holds
b1 is jump-only
proof end;
end;

registration
coherence ;
end;

registration
let i1 be Nat;
cluster K81((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;
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 K81((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 K81((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:
by AMI_3:10;

registration
let a, b be Data-Location;
cluster K81((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 K81((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 K81((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 K81((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 K81((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
coherence
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
coherence
proof end;
end;