:: The Properties of Instructions of { \bf SCM } over Ring
:: by Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users

theorem Th1: :: SCMRING3:1

for R being Ring
for a being Data-Location of R holds Values a = the carrier of R

proof end;

definition

let R be Ring;
let la, lb be Data-Location of R;
let a, b be Element of R;
:: original: -->
redefine func (la,lb) --> (a,b) -> FinPartState of (SCM R);
coherence
(la,lb) --> (a,b) is FinPartState of (SCM R)

proof end;

end;

theorem Th2: :: SCMRING3:2

for R being Ring
for a being Data-Location of R holds a <> IC

proof end;

theorem :: SCMRING3:3

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

proof end;

theorem :: SCMRING3:4

canceled;

::$CT

theorem :: SCMRING3:5

for R being Ring
for a, b being Data-Location of R holds InsCode (a := b) = 1 ;

theorem :: SCMRING3:6

for R being Ring
for a, b being Data-Location of R holds InsCode (AddTo (a,b)) = 2 ;

theorem :: SCMRING3:7

for R being Ring
for a, b being Data-Location of R holds InsCode (SubFrom (a,b)) = 3 ;

theorem :: SCMRING3:8

for R being Ring
for a, b being Data-Location of R holds InsCode (MultBy (a,b)) = 4 ;

theorem :: SCMRING3:9

for R being Ring
for r being Element of R
for a being Data-Location of R holds InsCode (a := r) = 5 ;

theorem :: SCMRING3:10

for R being Ring
for i1 being Nat holds InsCode (goto (i1,R)) = 6 ;

theorem :: SCMRING3:11

for R being Ring
for a being Data-Location of R
for i1 being Nat holds InsCode (a =0_goto i1) = 7 ;

theorem Th11: :: SCMRING3:12

for R being Ring
for I being Instruction of (SCM R) st InsCode I = 0 holds
I = halt (SCM R)

proof end;

theorem Th12: :: SCMRING3:13

for R being Ring
for I being Instruction of (SCM R) st InsCode I = 1 holds
ex a, b being Data-Location of R st I = a := b

proof end;

theorem Th13: :: SCMRING3:14

for R being Ring
for I being Instruction of (SCM R) st InsCode I = 2 holds
ex a, b being Data-Location of R st I = AddTo (a,b)

proof end;

theorem Th14: :: SCMRING3:15

for R being Ring
for I being Instruction of (SCM R) st InsCode I = 3 holds
ex a, b being Data-Location of R st I = SubFrom (a,b)

proof end;

theorem Th15: :: SCMRING3:16

for R being Ring
for I being Instruction of (SCM R) st InsCode I = 4 holds
ex a, b being Data-Location of R st I = MultBy (a,b)

proof end;

theorem Th16: :: SCMRING3:17

for R being Ring
for I being Instruction of (SCM R) st InsCode I = 5 holds
ex a being Data-Location of R ex r being Element of R st I = a := r

proof end;

theorem Th17: :: SCMRING3:18

for R being Ring
for I being Instruction of (SCM R) st InsCode I = 6 holds
ex i2 being Nat st I = goto (i2,R)

proof end;

theorem Th18: :: SCMRING3:19

for R being Ring
for I being Instruction of (SCM R) st InsCode I = 7 holds
ex a being Data-Location of R ex i1 being Nat st I = a =0_goto i1

proof end;

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

proof end;

Lm2: for R being Ring
for T being InsType of the InstructionsF of (SCM R) holds
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )

proof end;

theorem :: SCMRING3:20

for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 0 holds
JumpParts T = {0}

proof end;

theorem :: SCMRING3:21

for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 1 holds
JumpParts T = {{}}

proof end;

theorem :: SCMRING3:22

for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 2 holds
JumpParts T = {{}}

proof end;

theorem :: SCMRING3:23

for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 3 holds
JumpParts T = {{}}

proof end;

theorem :: SCMRING3:24

for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 4 holds
JumpParts T = {{}}

proof end;

theorem :: SCMRING3:25

for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 5 holds
JumpParts T = {{}}

proof end;

theorem Th25: :: SCMRING3:26

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

proof end;

theorem Th26: :: SCMRING3:27

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

proof end;

theorem :: SCMRING3:28

for R being Ring
for i1 being Nat holds (product" (JumpParts (InsCode (goto (i1,R))))) . 1 = NAT

proof end;

theorem :: SCMRING3:29

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

proof end;

Lm3: for R being Ring
for i being Instruction of (SCM R) st ( for l being Element of NAT holds NIC (i,l) = {(l + 1)} ) holds
JUMP i is empty

proof end;

registration

let R be Ring;

cluster JUMP (halt (SCM R)) -> empty ;

coherence
JUMP (halt (SCM R)) is empty ;

end;

registration

let R be Ring;
let a, b be Data-Location of R;

cluster a := b -> sequential ;

coherence
a := b is sequential by SCMRING2:11;

cluster AddTo (a,b) -> sequential ;

coherence
AddTo (a,b) is sequential by SCMRING2:12;

cluster SubFrom (a,b) -> sequential ;

coherence
SubFrom (a,b) is sequential by SCMRING2:13;

cluster MultBy (a,b) -> sequential ;

coherence
MultBy (a,b) is sequential by SCMRING2:14;

end;

registration

let R be Ring;
let a be Data-Location of R;
let r be Element of R;

cluster a := r -> sequential ;

coherence
a := r is sequential by SCMRING2:17;

end;

registration

let R be Ring;
let a, b be Data-Location of R;

cluster JUMP (a := b) -> empty ;

coherence
JUMP (a := b) is empty

proof end;

end;

registration

let R be Ring;
let a, b be Data-Location of R;

cluster JUMP (AddTo (a,b)) -> empty ;

coherence
JUMP (AddTo (a,b)) is empty

proof end;

end;

registration

let R be Ring;
let a, b be Data-Location of R;

cluster JUMP (SubFrom (a,b)) -> empty ;

coherence
JUMP (SubFrom (a,b)) is empty

proof end;

end;

registration

let R be Ring;
let a, b be Data-Location of R;

cluster JUMP (MultBy (a,b)) -> empty ;

coherence
JUMP (MultBy (a,b)) is empty

proof end;

end;

registration

let R be Ring;
let a be Data-Location of R;
let r be Element of R;

cluster JUMP (a := r) -> empty ;

coherence
JUMP (a := r) is empty

proof end;

end;

theorem Th29: :: SCMRING3:30

for R being Ring
for il, i1 being Nat holds NIC ((goto (i1,R)),il) = {i1}

proof end;

theorem Th30: :: SCMRING3:31

for R being Ring
for i1 being Nat holds JUMP (goto (i1,R)) = {i1}

proof end;

registration

let R be Ring;
let i1 be Nat;

cluster JUMP (goto (i1,R)) -> 1 -element ;

coherence
JUMP (goto (i1,R)) is 1 -element

proof end;

end;

theorem Th31: :: SCMRING3:32

for R being Ring
for a being Data-Location of R
for il, i1 being Nat holds
( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(il + 1)} )

proof end;

theorem :: SCMRING3:33

for R being non trivial Ring
for a being Data-Location of R
for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(il + 1)}

proof end;

theorem Th33: :: SCMRING3:34

for R being Ring
for a being Data-Location of R
for i1 being Nat holds JUMP (a =0_goto i1) = {i1}

proof end;

registration

let R be Ring;
let a be Data-Location of R;
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 Th34: :: SCMRING3:35

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

proof end;

theorem Th35: :: SCMRING3:36

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

proof end;

registration

let R be Ring;

cluster SCM R -> standard ;

coherence
SCM R is standard

proof end;

end;

definition

let R be Ring;
let k be Nat;

func dl. (R,k) -> Data-Location of R equals :: SCMRING3:def 1
dl. k;

coherence
dl. k is Data-Location of R by AMI_2:def 16, AMI_3:27, SCMRING2:1;

end;

:: deftheorem defines dl. SCMRING3:def 1 :
for R being Ring
for k being Nat holds dl. (R,k) = dl. k;

registration

let R be Ring;

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

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

proof end;

end;

registration

let R be Ring;

cluster halt (SCM R) -> jump-only ;

coherence
halt (SCM R) is jump-only ;

end;

registration

let R be Ring;
let i1 be Nat;

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

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

proof end;

end;

registration

let R be Ring;
let i1 be Nat;

cluster goto (i1,R) -> jump-only ;

coherence
goto (i1,R) is jump-only ;

end;

registration

let R be Ring;
let a be Data-Location of R;
let i1 be Nat;

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

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

proof end;

end;

registration

let R be Ring;
let a be Data-Location of R;
let i1 be Nat;

cluster a =0_goto i1 -> jump-only ;

coherence
a =0_goto i1 is jump-only ;

end;

registration

let S be non trivial Ring;
let p, q be Data-Location of S;

cluster InsCode (p := q) -> non jump-only for InsType of the InstructionsF of (SCM S);

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

proof end;

end;

registration

let S be non trivial Ring;
let p, q be Data-Location of S;

cluster p := q -> non jump-only ;

coherence
not p := q is jump-only ;

end;

registration

let S be non trivial Ring;
let p, q be Data-Location of S;

cluster InsCode (AddTo (p,q)) -> non jump-only for InsType of the InstructionsF of (SCM S);

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

proof end;

end;

registration

let S be non trivial Ring;
let p, q be Data-Location of S;

cluster AddTo (p,q) -> non jump-only ;

coherence
not AddTo (p,q) is jump-only ;

end;

registration

let S be non trivial Ring;
let p, q be Data-Location of S;

cluster InsCode (SubFrom (p,q)) -> non jump-only for InsType of the InstructionsF of (SCM S);

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

proof end;

end;

registration

let S be non trivial Ring;
let p, q be Data-Location of S;

cluster SubFrom (p,q) -> non jump-only ;

coherence
not SubFrom (p,q) is jump-only ;

end;

registration

let S be non trivial Ring;
let p, q be Data-Location of S;

cluster InsCode (MultBy (p,q)) -> non jump-only for InsType of the InstructionsF of (SCM S);

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

proof end;

end;

registration

let S be non trivial Ring;
let p, q be Data-Location of S;

cluster MultBy (p,q) -> non jump-only ;

coherence
not MultBy (p,q) is jump-only ;

end;

registration

let S be non trivial Ring;
let p be Data-Location of S;
let w be Element of S;

cluster InsCode (p := w) -> non jump-only for InsType of the InstructionsF of (SCM S);

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

proof end;

end;

registration

let S be non trivial Ring;
let p be Data-Location of S;
let w be Element of S;

cluster p := w -> non jump-only ;

coherence
not p := w is jump-only ;

end;

registration

let R be Ring;
let i1 be Nat;

cluster goto (i1,R) -> non sequential ;

coherence
not goto (i1,R) is sequential

proof end;

end;

registration

let R be Ring;
let a be Data-Location of R;
let i1 be Nat;

cluster a =0_goto i1 -> non sequential ;

coherence
not a =0_goto i1 is sequential

proof end;

end;

registration

let R be Ring;
let i1 be Nat;

cluster goto (i1,R) -> non ins-loc-free ;

coherence
not goto (i1,R) is ins-loc-free ;

end;

registration

let R be Ring;
let a be Data-Location of R;
let i1 be Nat;

cluster a =0_goto i1 -> non ins-loc-free ;

coherence
not a =0_goto i1 is ins-loc-free ;

end;

registration

let R be Ring;

cluster SCM R -> with_explicit_jumps ;

coherence
SCM R is with_explicit_jumps

proof end;

end;

theorem Th36: :: SCMRING3:37

for R being Ring
for i1, k being Nat holds IncAddr ((goto (i1,R)),k) = goto ((i1 + k),R)

proof end;

theorem Th37: :: SCMRING3:38

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

proof end;

registration

let R be Ring;

cluster SCM R -> IC-relocable ;

coherence
SCM R is IC-relocable

proof end;

end;

theorem :: SCMRING3:39

for R being Ring
for I being Instruction of (SCM R) holds InsCode I <= 7

proof end;