:: 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;
clustera := b ->  ins-loc-free ;
coherence
 a := b is ins-loc-free
proofend;
cluster AddTo (a,b) ->  ins-loc-free ;
coherence
 AddTo (a,b) is ins-loc-free
proofend;
cluster SubFrom (a,b) ->  ins-loc-free ;
coherence
 SubFrom (a,b) is ins-loc-free
proofend;
cluster MultBy (a,b) ->  ins-loc-free ;
coherence
 MultBy (a,b) is ins-loc-free
proofend;
cluster Divide (a,b) ->  ins-loc-free ;
coherence
 Divide (a,b) is ins-loc-free
proofend;
end;

theorem Th1: :: SCMFSA_4:1
for k, loc being Element of NAT holds IncAddr ((goto loc),k) = goto (loc + k)
proofend;

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)
proofend;

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)
proofend;

registration
let a, b be Int-Location;
let f be FinSeq-Location ;
clusterb := (f,a) ->  ins-loc-free ;
coherence
 b := (f,a) is ins-loc-free
proofend;
cluster(f,a) := b ->  ins-loc-free ;
coherence
 (f,a) := b is ins-loc-free
proofend;
end;

registration
let a be Int-Location;
let f be FinSeq-Location ;
clustera :=len f ->  ins-loc-free ;
coherence
 a :=len f is ins-loc-free
proofend;
clusterf :=<0,...,0> a ->  ins-loc-free ;
coherence
 f :=<0,...,0> a is ins-loc-free
proofend;
end;

begin

registration
cluster SCM+FSA  ->  relocable ;
coherence
 SCM+FSA is relocable
proofend;
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
proofend;