:: 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;