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

for k being Element of NAT holds IncAddr ((halt SCM+FSA),k) = halt SCM+FSA by COMPOS_1:93;

theorem Th9: :: SCMFSA_4:9

for k being Element of NAT
for a, b being Int-Location holds IncAddr ((a := b),k) = a := b by COMPOS_1:92;

theorem Th10: :: SCMFSA_4:10

for k being Element of NAT
for a, b being Int-Location holds IncAddr ((AddTo (a,b)),k) = AddTo (a,b) by COMPOS_1:92;

theorem Th11: :: SCMFSA_4:11

for k being Element of NAT
for a, b being Int-Location holds IncAddr ((SubFrom (a,b)),k) = SubFrom (a,b) by COMPOS_1:92;

theorem Th12: :: SCMFSA_4:12

for k being Element of NAT
for a, b being Int-Location holds IncAddr ((MultBy (a,b)),k) = MultBy (a,b) by COMPOS_1:92;

theorem Th13: :: SCMFSA_4:13

for k being Element of NAT
for a, b being Int-Location holds IncAddr ((Divide (a,b)),k) = Divide (a,b) by COMPOS_1:92;

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;

theorem Th17: :: SCMFSA_4:17

for k being Element of NAT
for a, b being Int-Location
for f being FinSeq-Location holds IncAddr ((b := (f,a)),k) = b := (f,a) by COMPOS_1:92;

theorem Th18: :: SCMFSA_4:18

for k being Element of NAT
for a, b being Int-Location
for f being FinSeq-Location holds IncAddr (((f,a) := b),k) = (f,a) := b by COMPOS_1:92;

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;

theorem Th19: :: SCMFSA_4:19

for k being Element of NAT
for a being Int-Location
for f being FinSeq-Location holds IncAddr ((a :=len f),k) = a :=len f by COMPOS_1:92;

theorem Th20: :: SCMFSA_4:20

for k being Element of NAT
for a being Int-Location
for f being FinSeq-Location holds IncAddr ((f :=<0,...,0> a),k) = f :=<0,...,0> a by COMPOS_1:92;

theorem :: SCMFSA_4:21

canceled;

theorem Th22: :: SCMFSA_4:22

for I being Instruction of SCM+FSA
for k being Element of NAT holds InsCode (IncAddr (I,k)) = InsCode I by COMPOS_1:def 38;

theorem Th23: :: SCMFSA_4:23

for m, n being Element of NAT
for i being Instruction of SCM+FSA holds IncAddr ((IncAddr (i,m)),n) = IncAddr (i,(m + n)) by COMPOS_1:97;

begin

theorem Th24: :: SCMFSA_4:24

for p being NAT -defined the Instructions of SCM+FSA -valued finite Function
for k, l being Element of NAT st l in dom p holds
(IncAddr (p,k)) . l = IncAddr ((p /. l),k) by COMPOS_1:def 40;

theorem :: SCMFSA_4:25

for n being Element of NAT
for I, J being NAT -defined the Instructions of SCM+FSA -valued finite Function holds IncAddr ((I +* J),n) = (IncAddr (I,n)) +* (IncAddr (J,n))

proof end;

theorem :: SCMFSA_4:26

for n being Element of NAT
for i being Instruction of SCM+FSA
for f being Function of the Instructions of SCM+FSA, the Instructions of SCM+FSA st f = (id the Instructions of SCM+FSA) +* ((halt SCM+FSA) .--> i) holds
for s being NAT -defined the Instructions of SCM+FSA -valued finite Function holds IncAddr ((f * s),n) = ((id the Instructions of SCM+FSA) +* ((halt SCM+FSA) .--> (IncAddr (i,n)))) * (IncAddr (s,n))

proof end;

theorem :: SCMFSA_4:27

for m, n being Element of NAT
for I being NAT -defined the Instructions of SCM+FSA -valued finite Function holds IncAddr ((IncAddr (I,m)),n) = IncAddr (I,(m + n)) by COMPOS_1:99;

theorem :: SCMFSA_4:28

for k being Element of NAT
for p being the Instructions of SCM+FSA -valued Function
for s being State of SCM+FSA holds Exec ((IncAddr ((CurInstr (p,s)),k)),(s +* (Start-At (((IC s) + k),SCM+FSA)))) = (Following (p,s)) +* (Start-At (((IC (Following (p,s))) + k),SCM+FSA))

proof end;

theorem :: SCMFSA_4:29

for INS being Instruction of SCM+FSA
for s being State of SCM+FSA
for p being FinPartState of SCM+FSA
for i, j, k being Element of NAT st IC s = j + k holds
Exec (INS,(s +* (Start-At (((IC s) -' k),SCM+FSA)))) = (Exec ((IncAddr (INS,k)),s)) +* (Start-At (((IC (Exec ((IncAddr (INS,k)),s))) -' k),SCM+FSA))

proof end;

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;