begin
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:
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
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
begin
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:
(
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:
theorem
theorem
theorem
theorem
theorem
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem