:: On a Mathematical Model of Programs :: by Yatsuka Nakamura and Andrzej Trybulec :: :: Received December 29, 1992 :: Copyright (c) 1992-2012 Association of Mizar Users begin :: Na razie potrzebny w SCM_INST ::definition :: func SCM-Data-Loc equals :: [:{1},NAT:]; :: coherence; ::end; definition func SCM-Memory -> set equals :: AMI_2:def 1 {NAT} \/ SCM-Data-Loc; coherence {NAT} \/ SCM-Data-Loc is set ; end; :: deftheorem defines SCM-Memory AMI_2:def_1_:_ SCM-Memory = {NAT} \/ SCM-Data-Loc; registration cluster SCM-Memory -> non empty ; coherence not SCM-Memory is empty ; end; definition :: original:SCM-Data-Loc redefine func SCM-Data-Loc -> Subset of SCM-Memory; coherence SCM-Data-Loc is Subset of SCM-Memory by XBOOLE_1:7; end; Lm1: now__::_thesis:_for_k_being_Element_of_SCM-Memory_holds_ (_k_=_NAT_or_k_in_SCM-Data-Loc_) let k be Element of SCM-Memory ; ::_thesis: ( k = NAT or k in SCM-Data-Loc ) ( k in {NAT} or k in SCM-Data-Loc ) by XBOOLE_0:def_3; hence ( k = NAT or k in SCM-Data-Loc ) by TARSKI:def_1; ::_thesis: verum end; Lm2: not NAT in SCM-Data-Loc proofend; definition canceled; canceled; func SCM-OK -> Function of SCM-Memory,2 means :Def4: :: AMI_2:def 4 for k being Element of SCM-Memory holds ( ( k = NAT implies it . k = 0 ) & ( k in SCM-Data-Loc implies it . k = 1 ) ); existence ex b1 being Function of SCM-Memory,2 st for k being Element of SCM-Memory holds ( ( k = NAT implies b1 . k = 0 ) & ( k in SCM-Data-Loc implies b1 . k = 1 ) ) proofend; uniqueness for b1, b2 being Function of SCM-Memory,2 st ( for k being Element of SCM-Memory holds ( ( k = NAT implies b1 . k = 0 ) & ( k in SCM-Data-Loc implies b1 . k = 1 ) ) ) & ( for k being Element of SCM-Memory holds ( ( k = NAT implies b2 . k = 0 ) & ( k in SCM-Data-Loc implies b2 . k = 1 ) ) ) holds b1 = b2 proofend; end; :: deftheorem AMI_2:def_2_:_ canceled; :: deftheorem AMI_2:def_3_:_ canceled; :: deftheorem Def4 defines SCM-OK AMI_2:def_4_:_ for b1 being Function of SCM-Memory,2 holds ( b1 = SCM-OK iff for k being Element of SCM-Memory holds ( ( k = NAT implies b1 . k = 0 ) & ( k in SCM-Data-Loc implies b1 . k = 1 ) ) ); theorem :: AMI_2:1 canceled; definition func SCM-VAL -> ManySortedSet of 2 equals :: AMI_2:def 5 <%NAT,INT%>; coherence <%NAT,INT%> is ManySortedSet of 2 ; end; :: deftheorem defines SCM-VAL AMI_2:def_5_:_ SCM-VAL = <%NAT,INT%>; Lm3: NAT in SCM-Memory proofend; theorem :: AMI_2:2 canceled; theorem :: AMI_2:3 canceled; theorem :: AMI_2:4 canceled; theorem :: AMI_2:5 canceled; theorem Th6: :: AMI_2:6 (SCM-VAL * SCM-OK) . NAT = NAT proofend; theorem Th7: :: AMI_2:7 for i being Element of SCM-Memory st i in SCM-Data-Loc holds (SCM-VAL * SCM-OK) . i = INT proofend; Lm4: dom SCM-OK = SCM-Memory by PARTFUN1:def_2; len <%NAT,INT%> = 2 by AFINSQ_1:38; then rng SCM-OK c= dom SCM-VAL by RELAT_1:def_19; then Lm5: dom (SCM-VAL * SCM-OK) = SCM-Memory by Lm4, RELAT_1:27; registration clusterSCM-OK * SCM-VAL -> non-empty ; coherence SCM-VAL * SCM-OK is non-empty proofend; end; definition mode SCM-State is Element of product (SCM-VAL * SCM-OK); end; theorem :: AMI_2:8 for a being Element of SCM-Data-Loc holds (SCM-VAL * SCM-OK) . a = INT by Th7; theorem Th9: :: AMI_2:9 pi ((product (SCM-VAL * SCM-OK)),NAT) = NAT by Th6, Lm5, Lm3, CARD_3:12; theorem Th10: :: AMI_2:10 for a being Element of SCM-Data-Loc holds pi ((product (SCM-VAL * SCM-OK)),a) = INT proofend; definition let s be SCM-State; func IC s -> Element of NAT equals :: AMI_2:def 6 s . NAT; coherence s . NAT is Element of NAT by Th9, CARD_3:def_6; end; :: deftheorem defines IC AMI_2:def_6_:_ for s being SCM-State holds IC s = s . NAT; definition let s be SCM-State; let u be Nat; func SCM-Chg (s,u) -> SCM-State equals :: AMI_2:def 7 s +* (NAT .--> u); coherence s +* (NAT .--> u) is SCM-State proofend; end; :: 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 :: AMI_2:11 for s being SCM-State for u being Nat holds (SCM-Chg (s,u)) . NAT = u proofend; theorem :: AMI_2:12 for s being SCM-State for u being Nat for mk being Element of SCM-Data-Loc holds (SCM-Chg (s,u)) . mk = s . mk proofend; theorem :: AMI_2:13 for s being SCM-State for u, v being Nat holds (SCM-Chg (s,u)) . v = s . v proofend; definition let s be SCM-State; let t be Element of SCM-Data-Loc ; let u be Integer; func SCM-Chg (s,t,u) -> SCM-State equals :: AMI_2:def 8 s +* (t .--> u); coherence s +* (t .--> u) is SCM-State proofend; end; :: 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 :: AMI_2:14 for s being SCM-State for t being Element of SCM-Data-Loc for u being Integer holds (SCM-Chg (s,t,u)) . NAT = s . NAT proofend; theorem :: AMI_2:15 for s being SCM-State for t being Element of SCM-Data-Loc for u being Integer holds (SCM-Chg (s,t,u)) . t = u proofend; theorem :: AMI_2:16 for s being SCM-State for t being Element of SCM-Data-Loc for u being Integer for mk being Element of SCM-Data-Loc st mk <> t holds (SCM-Chg (s,t,u)) . mk = s . mk proofend; registration let s be SCM-State; let a be Element of SCM-Data-Loc ; clusters . a -> integer ; coherence s . a is integer proofend; end; definition canceled; canceled; canceled; 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 14 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 XTUPLE_0:3; 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_9_:_ canceled; :: deftheorem AMI_2:def_10_:_ canceled; :: deftheorem AMI_2:def_11_:_ canceled; :: deftheorem AMI_2:def_12_:_ canceled; :: deftheorem AMI_2:def_13_:_ canceled; :: deftheorem defines SCM-Exec-Res AMI_2:def_14_:_ 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 -> Action of SCM-Instr,(product (SCM-VAL * SCM-OK)) means :: AMI_2:def 15 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 Action of SCM-Instr,(product (SCM-VAL * SCM-OK)) st for x being Element of SCM-Instr for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res (x,y) proofend; uniqueness for b1, b2 being Action of SCM-Instr,(product (SCM-VAL * 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 proofend; end; :: deftheorem defines SCM-Exec AMI_2:def_15_:_ for b1 being Action of SCM-Instr,(product (SCM-VAL * 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 :: AMI_2:17 canceled; theorem :: AMI_2:18 canceled; theorem :: AMI_2:19 canceled; theorem :: AMI_2:20 not NAT in SCM-Data-Loc by Lm2; theorem :: AMI_2:21 canceled; theorem :: AMI_2:22 NAT in SCM-Memory by Lm3; theorem :: AMI_2:23 for x being set st x in SCM-Data-Loc holds ex k being Element of NAT st x = [1,k] proofend; theorem :: AMI_2:24 for k being Nat holds [1,k] in SCM-Data-Loc proofend; theorem :: AMI_2:25 canceled; theorem :: AMI_2:26 for k being Element of SCM-Memory holds ( k = NAT or k in SCM-Data-Loc ) by Lm1; theorem :: AMI_2:27 dom (SCM-VAL * SCM-OK) = SCM-Memory by Lm5; theorem :: AMI_2:28 for s being SCM-State holds dom s = SCM-Memory by Lm5, CARD_3:9; definition let x be set ; attrx is Int-like means :: AMI_2:def 16 x in SCM-Data-Loc ; end; :: deftheorem defines Int-like AMI_2:def_16_:_ for x being set holds ( x is Int-like iff x in SCM-Data-Loc );