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

definition

let la, lb be Int-Location;
let a, b be Integer;
:: original: -->
redefine func (la,lb) --> (a,b) -> PartState of SCM+FSA;
coherence
(la,lb) --> (a,b) is PartState of SCM+FSA

proof end;

end;

theorem Th1: :: SCMFSA10:1

for o being Object of SCM+FSA holds
( not o in Data-Locations or o is Int-Location or o is FinSeq-Location )

proof end;

theorem Th2: :: SCMFSA10:2

for a, b being Int-Location holds a := b = [1,{},<*a,b*>]

proof end;

theorem Th3: :: SCMFSA10:3

for a, b being Int-Location holds AddTo (a,b) = [2,{},<*a,b*>]

proof end;

theorem Th4: :: SCMFSA10:4

for a, b being Int-Location holds SubFrom (a,b) = [3,{},<*a,b*>]

proof end;

theorem Th5: :: SCMFSA10:5

for a, b being Int-Location holds MultBy (a,b) = [4,{},<*a,b*>]

proof end;

theorem Th6: :: SCMFSA10:6

for a, b being Int-Location holds Divide (a,b) = [5,{},<*a,b*>]

proof end;

theorem Th7: :: SCMFSA10:7

for a being Int-Location
for il being Nat holds a =0_goto il = [7,<*il*>,<*a*>]

proof end;

theorem Th8: :: SCMFSA10:8

for a being Int-Location
for il being Nat holds a >0_goto il = [8,<*il*>,<*a*>]

proof end;

theorem Th9: :: SCMFSA10:9

JumpPart (halt SCM+FSA) = {} ;

theorem Th10: :: SCMFSA10:10

for a, b being Int-Location holds JumpPart (a := b) = {}

proof end;

theorem Th11: :: SCMFSA10:11

for a, b being Int-Location holds JumpPart (AddTo (a,b)) = {}

proof end;

theorem Th12: :: SCMFSA10:12

for a, b being Int-Location holds JumpPart (SubFrom (a,b)) = {}

proof end;

theorem Th13: :: SCMFSA10:13

for a, b being Int-Location holds JumpPart (MultBy (a,b)) = {}

proof end;

theorem Th14: :: SCMFSA10:14

for a, b being Int-Location holds JumpPart (Divide (a,b)) = {}

proof end;

theorem Th15: :: SCMFSA10:15

for i1 being Nat
for a being Int-Location holds JumpPart (a =0_goto i1) = <*i1*>

proof end;

theorem Th16: :: SCMFSA10:16

for i1 being Nat
for a being Int-Location holds JumpPart (a >0_goto i1) = <*i1*>

proof end;

theorem :: SCMFSA10:17

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

proof end;

theorem :: SCMFSA10:18

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

proof end;

theorem :: SCMFSA10:19

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

proof end;

theorem :: SCMFSA10:20

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

proof end;

theorem :: SCMFSA10:21

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

proof end;

theorem :: SCMFSA10:22

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

proof end;

theorem Th23: :: SCMFSA10:23

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

proof end;

theorem Th24: :: SCMFSA10:24

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

proof end;

theorem Th25: :: SCMFSA10:25

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

proof end;

theorem :: SCMFSA10:26

for T being InsType of the InstructionsF of SCM+FSA st T = 9 holds
JumpParts T = {{}}

proof end;

theorem :: SCMFSA10:27

for T being InsType of the InstructionsF of SCM+FSA st T = 10 holds
JumpParts T = {{}}

proof end;

theorem :: SCMFSA10:28

for T being InsType of the InstructionsF of SCM+FSA st T = 11 holds
JumpParts T = {{}}

proof end;

theorem :: SCMFSA10:29

for T being InsType of the InstructionsF of SCM+FSA st T = 12 holds
JumpParts T = {{}}

proof end;

theorem :: SCMFSA10:30

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

proof end;

theorem :: SCMFSA10:31

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

proof end;

theorem :: SCMFSA10:32

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

proof end;

Lm1: for i being Instruction of SCM+FSA st ( for l being Nat holds NIC (i,l) = {(l + 1)} ) holds
JUMP i is empty

proof end;

registration

cluster JUMP (halt SCM+FSA) -> empty ;

coherence
JUMP (halt SCM+FSA) is empty ;

end;

registration

let a, b be Int-Location;

cluster a := b -> sequential ;

coherence
a := b is sequential by SCMFSA_2:63;

cluster AddTo (a,b) -> sequential ;

coherence
AddTo (a,b) is sequential by SCMFSA_2:64;

cluster SubFrom (a,b) -> sequential ;

coherence
SubFrom (a,b) is sequential by SCMFSA_2:65;

cluster MultBy (a,b) -> sequential ;

coherence
MultBy (a,b) is sequential by SCMFSA_2:66;

cluster Divide (a,b) -> sequential ;

coherence
Divide (a,b) is sequential by SCMFSA_2:67;

end;

registration

let a, b be Int-Location;

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

coherence
JUMP (a := b) is empty

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

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

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

proof end;

end;

theorem Th33: :: SCMFSA10:33

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

proof end;

theorem Th34: :: SCMFSA10:34

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

proof end;

registration

let i1 be Nat;

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

coherence
JUMP (goto i1) is 1 -element

proof end;

end;

theorem Th35: :: SCMFSA10:35

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

proof end;

theorem Th36: :: SCMFSA10:36

for i1 being Nat
for a being Int-Location holds JUMP (a =0_goto i1) = {i1}

proof end;

registration

let a be Int-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 Th37: :: SCMFSA10:37

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

proof end;

theorem Th38: :: SCMFSA10:38

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

proof end;

registration

let a be Int-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;

registration

let a, b be Int-Location;
let f be FinSeq-Location ;

cluster a := (f,b) -> sequential ;

coherence
a := (f,b) is sequential by SCMFSA_2:72;

end;

registration

let a, b be Int-Location;
let f be FinSeq-Location ;

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

coherence
JUMP (a := (f,b)) is empty

proof end;

end;

registration

let a, b be Int-Location;
let f be FinSeq-Location ;

cluster (f,b) := a -> sequential ;

coherence
(f,b) := a is sequential by SCMFSA_2:73;

end;

registration

let a, b be Int-Location;
let f be FinSeq-Location ;

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

coherence
JUMP ((f,b) := a) is empty

proof end;

end;

registration

let a be Int-Location;
let f be FinSeq-Location ;

cluster a :=len f -> sequential ;

coherence
a :=len f is sequential by SCMFSA_2:74;

end;

registration

let a be Int-Location;
let f be FinSeq-Location ;

cluster JUMP (a :=len f) -> empty ;

coherence
JUMP (a :=len f) is empty

proof end;

end;

registration

let a be Int-Location;
let f be FinSeq-Location ;

cluster f :=<0,...,0> a -> sequential ;

coherence
f :=<0,...,0> a is sequential by SCMFSA_2:75;

end;

registration

let a be Int-Location;
let f be FinSeq-Location ;

cluster JUMP (f :=<0,...,0> a) -> empty ;

coherence
JUMP (f :=<0,...,0> a) is empty

proof end;

end;

theorem Th39: :: SCMFSA10:39

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

proof end;

theorem Th40: :: SCMFSA10:40

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

proof end;

registration

cluster SCM+FSA -> standard ;

coherence
SCM+FSA is standard by Th40, AMISTD_1:3;

end;

registration

cluster (halt SCM+FSA) `1_3 -> jump-only for InsType of the InstructionsF of SCM+FSA;

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

proof end;

end;

registration

cluster halt SCM+FSA -> jump-only ;

coherence
halt SCM+FSA is jump-only ;

end;

registration

let i1 be Nat;

cluster (goto i1) `1_3 -> jump-only for InsType of the InstructionsF of SCM+FSA;

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

proof end;

end;

registration

let i1 be Nat;

cluster goto i1 -> non ins-loc-free jump-only non sequential ;

coherence
( goto i1 is jump-only & not goto i1 is sequential & not goto i1 is ins-loc-free )

proof end;

end;

registration

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

cluster (a =0_goto i1) `1_3 -> jump-only for InsType of the InstructionsF of SCM+FSA;

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

proof end;

cluster (a >0_goto i1) `1_3 -> jump-only for InsType of the InstructionsF of SCM+FSA;

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

proof end;

end;

registration

let a be Int-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: intloc 0 <> intloc 1
by AMI_3:10;

registration

let a, b be Int-Location;

cluster (a := b) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;

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

proof end;

cluster (AddTo (a,b)) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;

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

proof end;

cluster (SubFrom (a,b)) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;

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

proof end;

cluster (MultBy (a,b)) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;

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

proof end;

cluster (Divide (a,b)) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;

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

proof end;

end;

Lm3: fsloc 0 <> intloc 0
by SCMFSA_2:99;

Lm4: fsloc 0 <> intloc 1
by SCMFSA_2:99;

registration

let a, b be Int-Location;
let f be FinSeq-Location ;

cluster (b := (f,a)) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;

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

proof end;

cluster ((f,a) := b) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;

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

proof end;

end;

registration

let a, b be Int-Location;
let f be FinSeq-Location ;

cluster b := (f,a) -> non jump-only ;

coherence
not b := (f,a) is jump-only ;

cluster (f,a) := b -> non jump-only ;

coherence
not (f,a) := b is jump-only ;

end;

registration

let a be Int-Location;
let f be FinSeq-Location ;

cluster (a :=len f) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;

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

proof end;

cluster (f :=<0,...,0> a) `1_3 -> non jump-only for InsType of the InstructionsF of SCM+FSA;

coherence
for b₁ being InsType of the InstructionsF of SCM+FSA st b₁ = InsCode (f :=<0,...,0> a) holds
not b₁ is jump-only

proof end;

end;

registration

let a be Int-Location;
let f be FinSeq-Location ;

cluster a :=len f -> non jump-only ;

coherence
not a :=len f is jump-only ;

cluster f :=<0,...,0> a -> non jump-only ;

coherence
not f :=<0,...,0> a is jump-only ;

end;

registration

cluster SCM+FSA -> with_explicit_jumps ;

coherence
SCM+FSA is with_explicit_jumps

proof end;

end;

theorem Th41: :: SCMFSA10:41

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

proof end;

theorem Th42: :: SCMFSA10:42

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

proof end;

theorem Th43: :: SCMFSA10:43

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

proof end;

registration

cluster SCM+FSA -> IC-relocable ;

coherence
SCM+FSA is IC-relocable

proof end;

end;