:: On a Mathematical Model of Programs
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received December 29, 1992
:: Copyright (c) 1992 Association of Mizar Users
:: 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 -> Subset of
[:NAT ,(((union {INT }) \/ SCM-Memory ) * ):] equals :: AMI_2:def 4
(({[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 Subset of [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
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 :: AMI_2:1
canceled;
theorem :: AMI_2:2
theorem :: AMI_2:3
theorem :: AMI_2:4
theorem :: AMI_2:5
Lm2:
not NAT in SCM-Data-Loc
Lm3:
SCM-Data-Loc misses NAT
:: deftheorem Def5 defines SCM-OK AMI_2:def 5 :
theorem Th6: :: AMI_2:6
theorem Th7: :: AMI_2:7
theorem Th8: :: AMI_2:8
theorem Th9: :: AMI_2:9
theorem :: AMI_2:10
theorem :: AMI_2:11
theorem :: AMI_2:12
Lm4:
NAT in SCM-Memory
theorem Th13: :: AMI_2:13
theorem Th14: :: AMI_2:14
theorem :: AMI_2:15
:: deftheorem defines IC AMI_2:def 6 :
:: deftheorem defines SCM-Chg AMI_2:def 7 :
theorem :: AMI_2:16
theorem :: AMI_2:17
theorem :: AMI_2:18
:: deftheorem defines SCM-Chg AMI_2:def 8 :
theorem :: AMI_2:19
theorem :: AMI_2:20
theorem :: AMI_2:21
theorem :: AMI_2:22
:: deftheorem Def9 defines address_1 AMI_2:def 9 :
:: deftheorem Def10 defines address_2 AMI_2:def 10 :
theorem :: AMI_2:23
:: deftheorem Def11 defines jump_address AMI_2:def 11 :
theorem :: AMI_2:24
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:
:: AMI_2:def 12
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:
:: AMI_2:def 13
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 :: AMI_2:25
definition
canceled;canceled;let x be
Element of
SCM-Instr ;
let s be
SCM-State;
func SCM-Exec-Res x,
s -> SCM-State equals :: AMI_2:def 16
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 :: AMI_2:def 17
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 :
theorem :: AMI_2:26
canceled;
theorem :: AMI_2:27
theorem :: AMI_2:28
canceled;
theorem :: AMI_2:29
theorem :: AMI_2:30
theorem :: AMI_2:31
canceled;
theorem :: AMI_2:32
theorem :: AMI_2:33