:: 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 b1 being Instruction of SCM+FSA ex I being Instruction of SCM st
( I = i & b1 = IncAddr I,k ) ) & ( not InsCode i in {6,7,8} implies ex b1 being Instruction of SCM+FSA st b1 = i ) )
correctness
consistency
for b1 being Instruction of SCM+FSA holds verum;
uniqueness
for b1, b2 being Instruction of SCM+FSA holds
( ( InsCode i in {6,7,8} & ex I being Instruction of SCM st
( I = i & b1 = IncAddr I,k ) & ex I being Instruction of SCM st
( I = i & b2 = IncAddr I,k ) implies b1 = b2 ) & ( not InsCode i in {6,7,8} & b1 = i & b2 = i implies b1 = b2 ) );
;
end;
:: deftheorem SCMFSA_4:def 1 :
canceled;
:: deftheorem SCMFSA_4:def 2 :
canceled;
:: deftheorem Def3 defines IncAddr SCMFSA_4:def 3 :
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
theorem Th9: :: SCMFSA_4:9
theorem Th10: :: SCMFSA_4:10
theorem Th11: :: SCMFSA_4:11
theorem Th12: :: SCMFSA_4:12
theorem Th13: :: SCMFSA_4:13
theorem Th14: :: SCMFSA_4:14
theorem Th15: :: SCMFSA_4:15
theorem Th16: :: SCMFSA_4:16
theorem Th17: :: SCMFSA_4:17
theorem Th18: :: SCMFSA_4:18
theorem Th19: :: SCMFSA_4:19
theorem Th20: :: SCMFSA_4:20
theorem Th21: :: SCMFSA_4:21
theorem Th22: :: SCMFSA_4:22
theorem Th23: :: SCMFSA_4:23
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 b1 being preProgram of SCM+FSA st
( dom b1 = dom p & ( for m being Element of NAT st insloc m in dom p holds
b1 . (insloc m) = IncAddr (pi p,m),k ) )
uniqueness
for b1, b2 being preProgram of SCM+FSA st dom b1 = dom p & ( for m being Element of NAT st insloc m in dom p holds
b1 . (insloc m) = IncAddr (pi p,m),k ) & dom b2 = dom p & ( for m being Element of NAT st insloc m in dom p holds
b2 . (insloc m) = IncAddr (pi p,m),k ) holds
b1 = b2
end;
:: deftheorem SCMFSA_4:def 4 :
canceled;
:: deftheorem SCMFSA_4:def 5 :
canceled;
:: deftheorem Def6 defines IncAddr SCMFSA_4:def 6 :
theorem Th24: :: SCMFSA_4:24
theorem :: SCMFSA_4:25
theorem :: SCMFSA_4:26
theorem :: SCMFSA_4:27
theorem :: SCMFSA_4:28
theorem :: SCMFSA_4:29
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