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