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

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

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

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

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

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

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

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

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

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

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 AMISTD_2:def 14;

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

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 AMISTD_2:def 15;

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

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;