begin
:: deftheorem defines SCM-Data-Loc AMI_2:def 1 :
:: deftheorem AMI_2:def 2 :
canceled;
:: deftheorem defines SCM-Memory AMI_2:def 3 :
definition
func SCM-Instr -> non
empty set equals
(({[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } ) \/ { [I,<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ;
coherence
(({[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } ) \/ { [I,<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } is non empty set
;
end;
:: deftheorem defines SCM-Instr AMI_2:def 4 :
SCM-Instr = (({[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } ) \/ { [I,<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ;
theorem
canceled;
theorem
theorem
theorem
theorem
Lm2:
not NAT in SCM-Data-Loc
Lm3:
SCM-Data-Loc misses NAT
:: deftheorem Def5 defines SCM-OK AMI_2:def 5 :
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem
theorem
theorem
Lm4:
NAT in SCM-Memory
theorem Th13:
theorem Th14:
theorem
:: deftheorem defines IC AMI_2:def 6 :
:: deftheorem defines SCM-Chg AMI_2:def 7 :
theorem
theorem
theorem
:: deftheorem defines SCM-Chg AMI_2:def 8 :
theorem
theorem
theorem
theorem
:: deftheorem Def9 defines address_1 AMI_2:def 9 :
:: deftheorem Def10 defines address_2 AMI_2:def 10 :
theorem
:: deftheorem Def11 defines jump_address AMI_2:def 11 :
theorem
definition
let x be
Element of
SCM-Instr ;
given mk being
Element of
NAT ,
ml being
Element of
SCM-Data-Loc ,
I being
Element of
Segm 9
such that A1:
x = [I,<*mk,ml*>]
;
func x cjump_address -> Element of
NAT means :
Def12:
ex
mk being
Element of
NAT ex
ml being
Element of
SCM-Data-Loc st
(
<*mk,ml*> = x `2 &
it = <*mk,ml*> /. 1 );
existence
ex b1, mk being Element of NAT ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b1 = <*mk,ml*> /. 1 )
correctness
uniqueness
for b1, b2 being Element of NAT st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b1 = <*mk,ml*> /. 1 ) & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b2 = <*mk,ml*> /. 1 ) holds
b1 = b2;
;
func x cond_address -> Element of
SCM-Data-Loc means :
Def13:
ex
mk being
Element of
NAT ex
ml being
Element of
SCM-Data-Loc st
(
<*mk,ml*> = x `2 &
it = <*mk,ml*> /. 2 );
existence
ex b1 being Element of SCM-Data-Loc ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b1 = <*mk,ml*> /. 2 )
correctness
uniqueness
for b1, b2 being Element of SCM-Data-Loc st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b1 = <*mk,ml*> /. 2 ) & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st
( <*mk,ml*> = x `2 & b2 = <*mk,ml*> /. 2 ) holds
b1 = b2;
;
end;
:: deftheorem Def12 defines cjump_address AMI_2:def 12 :
:: deftheorem Def13 defines cond_address AMI_2:def 13 :
theorem
definition
canceled;canceled;let x be
Element of
SCM-Instr ;
let s be
SCM-State;
func SCM-Exec-Res x,
s -> SCM-State equals
SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),
(succ (IC s)) if ex
mk,
ml being
Element of
SCM-Data-Loc st
x = [1,<*mk,ml*>] SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),
(succ (IC s)) if ex
mk,
ml being
Element of
SCM-Data-Loc st
x = [2,<*mk,ml*>] SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),
(succ (IC s)) if ex
mk,
ml being
Element of
SCM-Data-Loc st
x = [3,<*mk,ml*>] SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),
(succ (IC s)) if ex
mk,
ml being
Element of
SCM-Data-Loc st
x = [4,<*mk,ml*>] SCM-Chg (SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) div (s . (x address_2 )))),(x address_2 ),((s . (x address_1 )) mod (s . (x address_2 )))),
(succ (IC s)) if ex
mk,
ml being
Element of
SCM-Data-Loc st
x = [5,<*mk,ml*>] SCM-Chg s,
(x jump_address ) if ex
mk being
Element of
NAT st
x = [6,<*mk*>] SCM-Chg s,
(IFEQ (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) if ex
mk being
Element of
NAT ex
ml being
Element of
SCM-Data-Loc st
x = [7,<*mk,ml*>] SCM-Chg s,
(IFGT (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) if ex
mk being
Element of
NAT ex
ml being
Element of
SCM-Data-Loc st
x = [8,<*mk,ml*>] otherwise s;
consistency
for b1 being SCM-State holds
( ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(succ (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(succ (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(succ (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [5,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) div (s . (x address_2 )))),(x address_2 ),((s . (x address_1 )) mod (s . (x address_2 )))),(succ (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] & ex mk being Element of NAT st x = [6,<*mk*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(succ (IC s)) iff b1 = SCM-Chg s,(x jump_address ) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(succ (IC s)) iff b1 = SCM-Chg s,(IFEQ (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(succ (IC s)) iff b1 = SCM-Chg s,(IFGT (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(succ (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(succ (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [5,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) div (s . (x address_2 )))),(x address_2 ),((s . (x address_1 )) mod (s . (x address_2 )))),(succ (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] & ex mk being Element of NAT st x = [6,<*mk*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg s,(x jump_address ) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg s,(IFEQ (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg s,(IFGT (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(succ (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [5,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) div (s . (x address_2 )))),(x address_2 ),((s . (x address_1 )) mod (s . (x address_2 )))),(succ (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] & ex mk being Element of NAT st x = [6,<*mk*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg s,(x jump_address ) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg s,(IFEQ (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg s,(IFGT (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [5,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) div (s . (x address_2 )))),(x address_2 ),((s . (x address_1 )) mod (s . (x address_2 )))),(succ (IC s)) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] & ex mk being Element of NAT st x = [6,<*mk*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg s,(x jump_address ) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg s,(IFEQ (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg s,(IFGT (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,<*mk,ml*>] & ex mk being Element of NAT st x = [6,<*mk*>] implies ( b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) div (s . (x address_2 )))),(x address_2 ),((s . (x address_1 )) mod (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg s,(x jump_address ) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) div (s . (x address_2 )))),(x address_2 ),((s . (x address_1 )) mod (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg s,(IFEQ (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk,ml*>] implies ( b1 = SCM-Chg (SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) div (s . (x address_2 )))),(x address_2 ),((s . (x address_1 )) mod (s . (x address_2 )))),(succ (IC s)) iff b1 = SCM-Chg s,(IFGT (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) ) & ( ex mk being Element of NAT st x = [6,<*mk*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] implies ( b1 = SCM-Chg s,(x jump_address ) iff b1 = SCM-Chg s,(IFEQ (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) ) & ( ex mk being Element of NAT st x = [6,<*mk*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk,ml*>] implies ( b1 = SCM-Chg s,(x jump_address ) iff b1 = SCM-Chg s,(IFGT (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) ) & ( ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk,ml*>] implies ( b1 = SCM-Chg s,(IFEQ (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) iff b1 = SCM-Chg s,(IFGT (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) ) )
by ZFMISC_1:33;
coherence
( ( ex mk, ml being Element of SCM-Data-Loc st x = [1,<*mk,ml*>] implies SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),(succ (IC s)) is SCM-State ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [2,<*mk,ml*>] implies SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),(succ (IC s)) is SCM-State ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [3,<*mk,ml*>] implies SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),(succ (IC s)) is SCM-State ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,<*mk,ml*>] implies SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),(succ (IC s)) is SCM-State ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,<*mk,ml*>] implies SCM-Chg (SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) div (s . (x address_2 )))),(x address_2 ),((s . (x address_1 )) mod (s . (x address_2 )))),(succ (IC s)) is SCM-State ) & ( ex mk being Element of NAT st x = [6,<*mk*>] implies SCM-Chg s,(x jump_address ) is SCM-State ) & ( ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [7,<*mk,ml*>] implies SCM-Chg s,(IFEQ (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) is SCM-State ) & ( ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk,ml*>] implies SCM-Chg s,(IFGT (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) is SCM-State ) & ( ( for mk, ml being Element of SCM-Data-Loc holds not x = [1,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [2,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [3,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [4,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not x = [5,<*mk,ml*>] ) & ( for mk being Element of NAT holds not x = [6,<*mk*>] ) & ( for mk being Element of NAT
for ml being Element of SCM-Data-Loc holds not x = [7,<*mk,ml*>] ) & ( for mk being Element of NAT
for ml being Element of SCM-Data-Loc holds not x = [8,<*mk,ml*>] ) implies s is SCM-State ) )
;
end;
:: deftheorem AMI_2:def 14 :
canceled;
:: deftheorem AMI_2:def 15 :
canceled;
:: deftheorem defines SCM-Exec-Res AMI_2:def 16 :
for
x being
Element of
SCM-Instr for
s being
SCM-State holds
( ( ex
mk,
ml being
Element of
SCM-Data-Loc st
x = [1,<*mk,ml*>] implies
SCM-Exec-Res x,
s = SCM-Chg (SCM-Chg s,(x address_1 ),(s . (x address_2 ))),
(succ (IC s)) ) & ( ex
mk,
ml being
Element of
SCM-Data-Loc st
x = [2,<*mk,ml*>] implies
SCM-Exec-Res x,
s = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) + (s . (x address_2 )))),
(succ (IC s)) ) & ( ex
mk,
ml being
Element of
SCM-Data-Loc st
x = [3,<*mk,ml*>] implies
SCM-Exec-Res x,
s = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) - (s . (x address_2 )))),
(succ (IC s)) ) & ( ex
mk,
ml being
Element of
SCM-Data-Loc st
x = [4,<*mk,ml*>] implies
SCM-Exec-Res x,
s = SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) * (s . (x address_2 )))),
(succ (IC s)) ) & ( ex
mk,
ml being
Element of
SCM-Data-Loc st
x = [5,<*mk,ml*>] implies
SCM-Exec-Res x,
s = SCM-Chg (SCM-Chg (SCM-Chg s,(x address_1 ),((s . (x address_1 )) div (s . (x address_2 )))),(x address_2 ),((s . (x address_1 )) mod (s . (x address_2 )))),
(succ (IC s)) ) & ( ex
mk being
Element of
NAT st
x = [6,<*mk*>] implies
SCM-Exec-Res x,
s = SCM-Chg s,
(x jump_address ) ) & ( ex
mk being
Element of
NAT ex
ml being
Element of
SCM-Data-Loc st
x = [7,<*mk,ml*>] implies
SCM-Exec-Res x,
s = SCM-Chg s,
(IFEQ (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) & ( ex
mk being
Element of
NAT ex
ml being
Element of
SCM-Data-Loc st
x = [8,<*mk,ml*>] implies
SCM-Exec-Res x,
s = SCM-Chg s,
(IFGT (s . (x cond_address )),0 ,(x cjump_address ),(succ (IC s))) ) & ( ( for
mk,
ml being
Element of
SCM-Data-Loc holds not
x = [1,<*mk,ml*>] ) & ( for
mk,
ml being
Element of
SCM-Data-Loc holds not
x = [2,<*mk,ml*>] ) & ( for
mk,
ml being
Element of
SCM-Data-Loc holds not
x = [3,<*mk,ml*>] ) & ( for
mk,
ml being
Element of
SCM-Data-Loc holds not
x = [4,<*mk,ml*>] ) & ( for
mk,
ml being
Element of
SCM-Data-Loc holds not
x = [5,<*mk,ml*>] ) & ( for
mk being
Element of
NAT holds not
x = [6,<*mk*>] ) & ( for
mk being
Element of
NAT for
ml being
Element of
SCM-Data-Loc holds not
x = [7,<*mk,ml*>] ) & ( for
mk being
Element of
NAT for
ml being
Element of
SCM-Data-Loc holds not
x = [8,<*mk,ml*>] ) implies
SCM-Exec-Res x,
s = s ) );
definition
func SCM-Exec -> Function of
SCM-Instr ,
Funcs (product SCM-OK ),
(product SCM-OK ) means
for
x being
Element of
SCM-Instr for
y being
SCM-State holds
(it . x) . y = SCM-Exec-Res x,
y;
existence
ex b1 being Function of SCM-Instr , Funcs (product SCM-OK ),(product SCM-OK ) st
for x being Element of SCM-Instr
for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res x,y
uniqueness
for b1, b2 being Function of SCM-Instr , Funcs (product SCM-OK ),(product SCM-OK ) st ( for x being Element of SCM-Instr
for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res x,y ) & ( for x being Element of SCM-Instr
for y being SCM-State holds (b2 . x) . y = SCM-Exec-Res x,y ) holds
b1 = b2
end;
:: deftheorem defines SCM-Exec AMI_2:def 17 :
begin
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
theorem
theorem