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

begin

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 Th7: :: 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 Th9: :: SCMFSA10:2

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

proof end;

theorem Th10: :: SCMFSA10:3

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

proof end;

theorem Th11: :: SCMFSA10:4

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

proof end;

theorem Th12: :: SCMFSA10:5

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

proof end;

theorem Th13: :: SCMFSA10:6

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

proof end;

theorem Th15: :: SCMFSA10:7

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

proof end;

theorem Th16: :: SCMFSA10:8

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

proof end;

Lm1: for T being InsType of SCM+FSA holds
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 or T = 9 or T = 10 or T = 11 or T = 12 )

proof end;

theorem Th17: :: SCMFSA10:9

JumpPart (halt SCM+FSA) = {} ;

theorem Th18: :: SCMFSA10:10

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

proof end;

theorem Th19: :: SCMFSA10:11

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

proof end;

theorem Th20: :: SCMFSA10:12

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

proof end;

theorem Th21: :: SCMFSA10:13

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

proof end;

theorem Th22: :: SCMFSA10:14

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

proof end;

theorem Th24: :: SCMFSA10:15

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

proof end;

theorem Th25: :: SCMFSA10:16

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

proof end;

theorem Th30: :: SCMFSA10:17

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

proof end;

theorem Th31: :: SCMFSA10:18

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

proof end;

theorem Th32: :: SCMFSA10:19

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

proof end;

theorem Th33: :: SCMFSA10:20

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

proof end;

theorem Th34: :: SCMFSA10:21

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

proof end;

theorem Th35: :: SCMFSA10:22

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

proof end;

theorem Th36: :: SCMFSA10:23

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

proof end;

theorem Th37: :: SCMFSA10:24

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

proof end;

theorem Th38: :: SCMFSA10:25

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

proof end;

theorem Th39: :: SCMFSA10:26

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

proof end;

theorem Th40: :: SCMFSA10:27

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

proof end;

theorem Th41: :: SCMFSA10:28

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

proof end;

theorem Th42: :: SCMFSA10:29

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

proof end;

theorem Th53: :: SCMFSA10:30

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

proof end;

theorem Th54: :: SCMFSA10:31

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

proof end;

theorem Th56: :: SCMFSA10:32

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

proof end;

Lm3: for i being Instruction of SCM+FSA st ( for l being Element of NAT holds NIC (i,l) = {(succ l)} ) 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

proof end;

cluster AddTo (a,b) -> sequential ;
coherence
AddTo (a,b) is sequential

proof end;

cluster SubFrom (a,b) -> sequential ;
coherence
SubFrom (a,b) is sequential

proof end;

cluster MultBy (a,b) -> sequential ;
coherence
MultBy (a,b) is sequential

proof end;

cluster Divide (a,b) -> sequential ;
coherence
Divide (a,b) is sequential

proof end;

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 Th74: :: SCMFSA10:33

for i1, il being Element of NAT holds NIC ((goto i1),il) = {i1}

proof end;

theorem Th75: :: SCMFSA10:34

for i1 being Element of NAT holds JUMP (goto i1) = {i1}

proof end;

registration

let i1 be Element of NAT ;
cluster JUMP (goto i1) -> 1 -element ;
coherence
JUMP (goto i1) is 1 -element

proof end;

end;

theorem Th76: :: SCMFSA10:35

for i1, il being Element of NAT
for a being Int-Location holds NIC ((a =0_goto i1),il) = {i1,(succ il)}

proof end;

theorem Th77: :: SCMFSA10:36

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

proof end;

registration

let a be Int-Location ;
let i1 be Element of NAT ;
cluster JUMP (a =0_goto i1) -> 1 -element ;
coherence
JUMP (a =0_goto i1) is 1 -element

proof end;

end;

theorem Th78: :: SCMFSA10:37

for i1, il being Element of NAT
for a being Int-Location holds NIC ((a >0_goto i1),il) = {i1,(succ il)}

proof end;

theorem Th79: :: SCMFSA10:38

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

proof end;

registration

let a be Int-Location ;
let i1 be Element of 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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 Th84: :: SCMFSA10:39

for il being Element of NAT holds SUCC (il,SCM+FSA) = {il,(succ il)}

proof end;

theorem Th85: :: SCMFSA10:40

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

proof end;

registration

cluster SCM+FSA -> standard ;
coherence
SCM+FSA is standard by Th85, AMISTD_1:3;

end;

registration

cluster (halt SCM+FSA) `1_3 -> jump-only for InsType of SCM+FSA;
coherence
for b₁ being InsType 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

proof end;

end;

registration

let i1 be Element of NAT ;
cluster (goto i1) `1_3 -> jump-only for InsType of SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (goto i1) holds
b₁ is jump-only

proof end;

end;

registration

let i1 be Element of 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 Element of NAT ;
cluster (a =0_goto i1) `1_3 -> jump-only for InsType of SCM+FSA;
coherence
for b₁ being InsType 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 SCM+FSA;
coherence
for b₁ being InsType 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 Element of 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;

Lm4: 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 SCM+FSA;
coherence
for b₁ being InsType 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 SCM+FSA;
coherence
for b₁ being InsType 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 SCM+FSA;
coherence
for b₁ being InsType 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 SCM+FSA;
coherence
for b₁ being InsType 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 SCM+FSA;
coherence
for b₁ being InsType of SCM+FSA st b₁ = InsCode (Divide (a,b)) holds
not b₁ is jump-only

proof end;

end;

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

Lm6: 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 SCM+FSA;
coherence
for b₁ being InsType 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 SCM+FSA;
coherence
for b₁ being InsType 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

proof end;

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

proof end;

end;

registration

let a be Int-Location ;
let f be FinSeq-Location ;
cluster (a :=len f) `1_3 -> non jump-only for InsType of SCM+FSA;
coherence
for b₁ being InsType 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 SCM+FSA;
coherence
for b₁ being InsType 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

proof end;

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

proof end;

end;

registration

cluster SCM+FSA -> homogeneous with_explicit_jumps ;
coherence
( SCM+FSA is homogeneous & SCM+FSA is with_explicit_jumps )

proof end;

end;

registration

cluster SCM+FSA -> regular J/A-independent ;
coherence
( SCM+FSA is regular & SCM+FSA is J/A-independent )

proof end;

end;

theorem Th88: :: SCMFSA10:41

for i1 being Element of NAT
for k being natural number holds IncAddr ((goto i1),k) = goto (i1 + k)

proof end;

theorem Th89: :: SCMFSA10:42

for i1 being Element of NAT
for k being natural number
for a being Int-Location holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)

proof end;

theorem Th90: :: SCMFSA10:43

for i1 being Element of NAT
for k being natural number
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;