:: Modifying addresses of instructions of { \bf SCM_FSA }
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received February 14, 1996
:: Copyright (c) 1996-2021 Association of Mizar Users

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 Nat holds IncAddr ((goto loc),k) = goto (loc + k) by SCMFSA10:41;

theorem Th2: :: SCMFSA_4:2

for k, loc being 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 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 ;

cluster (f,a) := b -> ins-loc-free ;

coherence
(f,a) := b is ins-loc-free ;

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 ;

cluster f :=<0,...,0> a -> ins-loc-free ;

coherence
f :=<0,...,0> a is ins-loc-free ;

end;

registration

cluster SCM+FSA -> relocable ;

coherence
SCM+FSA is relocable

proof end;

end;

theorem :: SCMFSA_4:4

for k being Nat
for i being Instruction of SCM+FSA st not InsCode i in {6,7,8} holds
IncAddr (i,k) = i

proof end;