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

coherence

a := b is ins-loc-free

AddTo (a,b) is ins-loc-free

SubFrom (a,b) is ins-loc-free

MultBy (a,b) is ins-loc-free

Divide (a,b) is ins-loc-free

end;
coherence

a := b is ins-loc-free

proof end;

coherence AddTo (a,b) is ins-loc-free

proof end;

coherence SubFrom (a,b) is ins-loc-free

proof end;

coherence MultBy (a,b) is ins-loc-free

proof end;

coherence Divide (a,b) is ins-loc-free

proof end;

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)

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)

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 ;

coherence

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

coherence

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

end;
let f be FinSeq-Location ;

coherence

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

coherence

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

registration

let a be Int-Location;

let f be FinSeq-Location ;

coherence

a :=len f is ins-loc-free ;

coherence

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

end;
let f be FinSeq-Location ;

coherence

a :=len f is ins-loc-free ;

coherence

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

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

for i being Instruction of SCM+FSA st not InsCode i in {6,7,8} holds

IncAddr (i,k) = i

proof end;