begin
:: deftheorem defines SCM-Data-Loc AMI_2:def 1 :
SCM-Data-Loc = [:{1},NAT :];
:: deftheorem AMI_2:def 2 :
canceled;
:: deftheorem defines SCM-Memory AMI_2:def 3 :
SCM-Memory = ({NAT } \/ SCM-Data-Loc ) \/ NAT ;
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 :
for b1 being Function of SCM-Memory ,({INT } \/ {SCM-Instr ,NAT }) holds
( b1 = SCM-OK iff for k being Element of SCM-Memory holds
( ( k = NAT implies b1 . k = NAT ) & ( k in SCM-Data-Loc implies b1 . k = INT ) & ( k in NAT implies b1 . k = SCM-Instr ) ) );
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 :
for s being SCM-State holds IC s = s . NAT ;
:: deftheorem defines SCM-Chg AMI_2:def 7 :
for s being SCM-State
for u being Nat holds SCM-Chg s,u = s +* (NAT .--> u);
theorem
theorem
theorem
:: deftheorem defines SCM-Chg AMI_2:def 8 :
for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer holds SCM-Chg s,t,u = s +* (t .--> u);
theorem
theorem
theorem
theorem
:: deftheorem Def9 defines address_1 AMI_2:def 9 :
for x being Element of SCM-Instr st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,{} ,<*mk,ml*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x address_1 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b2 = f /. 1 ) );
:: deftheorem Def10 defines address_2 AMI_2:def 10 :
for x being Element of SCM-Instr st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,{} ,<*mk,ml*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x address_2 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b2 = f /. 2 ) );
theorem
:: deftheorem Def11 defines jump_address AMI_2:def 11 :
for x being Element of SCM-Instr st ex mk being Element of NAT ex I being Element of Segm 9 st x = [I,<*mk*>,{} ] holds
for b2 being Element of NAT holds
( b2 = x jump_address iff ex f being FinSequence of NAT st
( f = x `2_3 & b2 = f /. 1 ) );
theorem
:: deftheorem Def12 defines cjump_address AMI_2:def 12 :
for x being Element of SCM-Instr st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
for b2 being Element of NAT holds
( b2 = x cjump_address iff ex mk being Element of NAT st
( <*mk*> = x `2_3 & b2 = <*mk*> /. 1 ) );
:: deftheorem Def13 defines cond_address AMI_2:def 13 :
for x being Element of SCM-Instr st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 9 st x = [I,<*mk*>,<*ml*>] holds
for b2 being Element of SCM-Data-Loc holds
( b2 = x cond_address iff ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b2 = <*ml*> /. 1 ) );
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 MCART_1:28;
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 ) );
:: deftheorem defines SCM-Exec AMI_2:def 17 :
for b1 being Action of SCM-Instr ,(product SCM-OK ) holds
( b1 = SCM-Exec iff for x being Element of SCM-Instr
for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res x,y );
begin
theorem
canceled;
theorem
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
theorem
theorem