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

definition

canceled;
canceled;
let i be Instruction of SCM+FSA ;
let k be Element of NAT ;
func IncAddr i,k -> Instruction of SCM+FSA means :Def3: :: SCMFSA_4:def 3
ex I being Instruction of SCM st
( I = i & it = IncAddr I,k ) if InsCode i in {6,7,8}
otherwise it = i;
existence
( ( InsCode i in {6,7,8} implies ex b₁ being Instruction of SCM+FSA ex I being Instruction of SCM st
( I = i & b₁ = IncAddr I,k ) ) & ( not InsCode i in {6,7,8} implies ex b₁ being Instruction of SCM+FSA st b₁ = i ) )

proof end;

correctness
consistency
for b₁ being Instruction of SCM+FSA holds verum;
uniqueness
for b₁, b₂ being Instruction of SCM+FSA holds
( ( InsCode i in {6,7,8} & ex I being Instruction of SCM st
( I = i & b₁ = IncAddr I,k ) & ex I being Instruction of SCM st
( I = i & b₂ = IncAddr I,k ) implies b₁ = b₂ ) & ( not InsCode i in {6,7,8} & b₁ = i & b₂ = i implies b₁ = b₂ ) );
;

end;

:: deftheorem SCMFSA_4:def 1 :

canceled;

:: deftheorem SCMFSA_4:def 2 :

canceled;

:: deftheorem Def3 defines IncAddr SCMFSA_4:def 3 :

for i being Instruction of SCM+FSA
for k being Element of NAT
for b₃ being Instruction of SCM+FSA holds
( ( InsCode i in {6,7,8} implies ( b₃ = IncAddr i,k iff ex I being Instruction of SCM st
( I = i & b₃ = IncAddr I,k ) ) ) & ( not InsCode i in {6,7,8} implies ( b₃ = IncAddr i,k iff b₃ = i ) ) );

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

proof end;

theorem Th9: :: SCMFSA_4:9

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

theorem Th14: :: SCMFSA_4:14

for k being Element of NAT
for loc being Instruction-Location of SCM+FSA holds IncAddr (goto loc),k = goto (loc + k)

proof end;

theorem Th15: :: SCMFSA_4:15

for k being Element of NAT
for loc being Instruction-Location of SCM+FSA
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 being Element of NAT
for loc being Instruction-Location of SCM+FSA
for a being Int-Location holds IncAddr (a >0_goto loc),k = a >0_goto (loc + k)

proof 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

proof end;

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

proof 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

proof end;

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

proof end;

theorem Th21: :: SCMFSA_4:21

for k being Element of NAT
for i being Instruction of SCM+FSA
for I being Instruction of SCM st i = I holds
IncAddr i,k = IncAddr I,k

proof end;

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

proof end;

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)

proof end;

definition

canceled;
canceled;
let p be preProgram of SCM+FSA ;
let k be Element of NAT ;
func IncAddr p,k -> preProgram of SCM+FSA means :Def6: :: SCMFSA_4:def 6
( dom it = dom p & ( for m being Element of NAT st insloc m in dom p holds
it . (insloc m) = IncAddr (pi p,m),k ) );
existence
ex b₁ being preProgram of SCM+FSA st
( dom b₁ = dom p & ( for m being Element of NAT st insloc m in dom p holds
b₁ . (insloc m) = IncAddr (pi p,m),k ) )

proof end;

uniqueness
for b₁, b₂ being preProgram of SCM+FSA st dom b₁ = dom p & ( for m being Element of NAT st insloc m in dom p holds
b₁ . (insloc m) = IncAddr (pi p,m),k ) & dom b₂ = dom p & ( for m being Element of NAT st insloc m in dom p holds
b₂ . (insloc m) = IncAddr (pi p,m),k ) holds
b₁ = b₂

proof end;

end;

:: deftheorem SCMFSA_4:def 4 :

canceled;

:: deftheorem SCMFSA_4:def 5 :

canceled;

:: deftheorem Def6 defines IncAddr SCMFSA_4:def 6 :

for p being preProgram of SCM+FSA
for k being Element of NAT
for b₃ being preProgram of SCM+FSA holds
( b₃ = IncAddr p,k iff ( dom b₃ = dom p & ( for m being Element of NAT st insloc m in dom p holds
b₃ . (insloc m) = IncAddr (pi p,m),k ) ) );

theorem Th24: :: SCMFSA_4:24

for p being preProgram of SCM+FSA
for k, l being Element of NAT st l in dom p holds
(IncAddr p,k) . l = IncAddr (pi p,l),k

proof end;

theorem :: SCMFSA_4:25

for n being Element of NAT
for I, J being preProgram of SCM+FSA 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 preProgram of SCM+FSA 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 preProgram of SCM+FSA holds IncAddr (IncAddr I,m),n = IncAddr I,(m + n)

proof end;

theorem :: SCMFSA_4:28

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

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))) = (Exec (IncAddr INS,k),s) +* (Start-At ((IC (Exec (IncAddr INS,k),s)) -' k))

proof end;

theorem :: SCMFSA_4:30

canceled;

theorem :: SCMFSA_4:31

canceled;

theorem :: SCMFSA_4:32

canceled;

theorem :: SCMFSA_4:33

canceled;

theorem :: SCMFSA_4:34

canceled;

theorem :: SCMFSA_4:35

for i, j being Element of NAT
for p being preProgram of SCM+FSA holds Shift (IncAddr p,i),j = IncAddr (Shift p,j),i

proof end;