:: Modifying addresses of instructions of { \bf SCM_FSA }
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received February 14, 1996
:: Copyright (c) 1996-2011 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 :: SCMFSA_4:1

canceled;

theorem :: SCMFSA_4:2

canceled;

theorem :: SCMFSA_4:3

canceled;

theorem :: SCMFSA_4:4

canceled;

theorem :: SCMFSA_4:5

canceled;

theorem :: SCMFSA_4:6

canceled;

theorem :: SCMFSA_4:7

canceled;

theorem :: SCMFSA_4:8

canceled;

theorem :: SCMFSA_4:9

canceled;

theorem :: SCMFSA_4:10

canceled;

theorem :: SCMFSA_4:11

canceled;

theorem :: SCMFSA_4:12

canceled;

theorem :: SCMFSA_4:13

canceled;

theorem Th14: :: SCMFSA_4:14

for k, loc being Element of NAT holds IncAddr ((goto loc),k) = goto (loc + k)

proof end;

theorem Th15: :: SCMFSA_4:15

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 Th16: :: SCMFSA_4:16

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;

registration

let a be Int-Location ;
cluster a :==1 -> ins-loc-free ;
coherence
a :==1 is ins-loc-free

proof end;

end;

begin

registration

cluster SCM+FSA -> relocable ;
coherence
SCM+FSA is relocable

proof end;

end;

theorem :: SCMFSA_4:17

canceled;

theorem :: SCMFSA_4:18

canceled;

theorem :: SCMFSA_4:19

canceled;

theorem :: SCMFSA_4:20

canceled;

theorem :: SCMFSA_4:21

canceled;

theorem :: SCMFSA_4:22

canceled;

theorem :: SCMFSA_4:23

canceled;

theorem :: SCMFSA_4:24

canceled;

theorem :: SCMFSA_4:25

canceled;

theorem :: SCMFSA_4:26

canceled;

theorem :: SCMFSA_4:27

canceled;

theorem :: SCMFSA_4:28

canceled;

theorem :: SCMFSA_4:29

canceled;

theorem :: SCMFSA_4:30

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;