:: Modifying addresses of instructions of { \bf SCM_FSA }
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received February 14, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users
begin
registration
let
a
,
b
be
Int-Location
;
cluster
a
:=
b
->
ins-loc-free
;
coherence
a
:=
b
is
ins-loc-free
proof
end;
cluster
AddTo
(
a
,
b
)
->
ins-loc-free
;
coherence
AddTo
(
a
,
b
) is
ins-loc-free
proof
end;
cluster
SubFrom
(
a
,
b
)
->
ins-loc-free
;
coherence
SubFrom
(
a
,
b
) is
ins-loc-free
proof
end;
cluster
MultBy
(
a
,
b
)
->
ins-loc-free
;
coherence
MultBy
(
a
,
b
) is
ins-loc-free
proof
end;
cluster
Divide
(
a
,
b
)
->
ins-loc-free
;
coherence
Divide
(
a
,
b
) is
ins-loc-free
proof
end;
end;
theorem
Th1
:
:: SCMFSA_4:1
for
k
,
loc
being
Element
of
NAT
holds
IncAddr
(
(
goto
loc
)
,
k
)
=
goto
(
loc
+
k
)
proof
end;
theorem
Th2
:
:: SCMFSA_4:2
for
k
,
loc
being
Element
of
NAT
for
a
being
Int-Location
holds
IncAddr
(
(
a
=0_goto
loc
)
,
k
)
=
a
=0_goto
(
loc
+
k
)
proof
end;
theorem
Th3
:
:: SCMFSA_4:3
for
k
,
loc
being
Element
of
NAT
for
a
being
Int-Location
holds
IncAddr
(
(
a
>0_goto
loc
)
,
k
)
=
a
>0_goto
(
loc
+
k
)
proof
end;
registration
let
a
,
b
be
Int-Location
;
let
f
be
FinSeq-Location
;
cluster
b
:=
(
f
,
a
)
->
ins-loc-free
;
coherence
b
:=
(
f
,
a
) is
ins-loc-free
proof
end;
cluster
(
f
,
a
)
:=
b
->
ins-loc-free
;
coherence
(
f
,
a
)
:=
b
is
ins-loc-free
proof
end;
end;
registration
let
a
be
Int-Location
;
let
f
be
FinSeq-Location
;
cluster
a
:=len
f
->
ins-loc-free
;
coherence
a
:=len
f
is
ins-loc-free
proof
end;
cluster
f
:=<0,...,0>
a
->
ins-loc-free
;
coherence
f
:=<0,...,0>
a
is
ins-loc-free
proof
end;
end;
begin
registration
cluster
SCM+FSA
->
relocable
;
coherence
SCM+FSA
is
relocable
proof
end;
end;
theorem
:: SCMFSA_4:4
for
k
being
Element
of
NAT
for
i
being
Instruction
of
SCM+FSA
st not
InsCode
i
in
{
6,7,8
}
holds
IncAddr
(
i
,
k
)
=
i
proof
end;