:: by Artur Korni{\l}owicz

::

:: Received November 29, 1998

:: Copyright (c) 1998-2012 Association of Mizar Users

begin

definition

canceled;

canceled;

let S be non empty 1-sorted ;

coherence

<%NAT, the carrier of S%> is ManySortedSet of 2 ;

end;
canceled;

let S be non empty 1-sorted ;

coherence

<%NAT, the carrier of S%> is ManySortedSet of 2 ;

:: deftheorem defines SCM-VAL SCMRING1:def 3 :

for S being non empty 1-sorted holds SCM-VAL S = <%NAT, the carrier of S%>;

for S being non empty 1-sorted holds SCM-VAL S = <%NAT, the carrier of S%>;

Lm1: for S being non empty 1-sorted holds dom ((SCM-VAL S) * SCM-OK) = SCM-Memory

proof end;

theorem Th3: :: SCMRING1:3

for G being non empty 1-sorted

for i being Element of SCM-Memory st i in SCM-Data-Loc holds

((SCM-VAL G) * SCM-OK) . i = the carrier of G

for i being Element of SCM-Memory st i in SCM-Data-Loc holds

((SCM-VAL G) * SCM-OK) . i = the carrier of G

proof end;

registration
end;

definition
end;

theorem :: SCMRING1:4

theorem Th6: :: SCMRING1:6

for G being non empty 1-sorted

for a being Element of SCM-Data-Loc holds pi ((product ((SCM-VAL G) * SCM-OK)),a) = the carrier of G

for a being Element of SCM-Data-Loc holds pi ((product ((SCM-VAL G) * SCM-OK)),a) = the carrier of G

proof end;

definition

let G be non empty 1-sorted ;

let s be SCM-State of G;

coherence

s . NAT is Element of NAT

end;
let s be SCM-State of G;

coherence

s . NAT is Element of NAT

proof end;

:: deftheorem defines IC SCMRING1:def 4 :

for G being non empty 1-sorted

for s being SCM-State of G holds IC s = s . NAT;

for G being non empty 1-sorted

for s being SCM-State of G holds IC s = s . NAT;

definition

let R be non empty 1-sorted ;

let s be SCM-State of R;

let u be Nat;

coherence

s +* (NAT .--> u) is SCM-State of R

end;
let s be SCM-State of R;

let u be Nat;

coherence

s +* (NAT .--> u) is SCM-State of R

proof end;

:: deftheorem defines SCM-Chg SCMRING1:def 5 :

for R being non empty 1-sorted

for s being SCM-State of R

for u being Nat holds SCM-Chg (s,u) = s +* (NAT .--> u);

for R being non empty 1-sorted

for s being SCM-State of R

for u being Nat holds SCM-Chg (s,u) = s +* (NAT .--> u);

theorem :: SCMRING1:7

for G being non empty 1-sorted

for s being SCM-State of G

for u being Nat holds (SCM-Chg (s,u)) . NAT = u

for s being SCM-State of G

for u being Nat holds (SCM-Chg (s,u)) . NAT = u

proof end;

theorem :: SCMRING1:8

for G being non empty 1-sorted

for s being SCM-State of G

for u being Nat

for mk being Element of SCM-Data-Loc holds (SCM-Chg (s,u)) . mk = s . mk

for s being SCM-State of G

for u being Nat

for mk being Element of SCM-Data-Loc holds (SCM-Chg (s,u)) . mk = s . mk

proof end;

theorem :: SCMRING1:9

for G being non empty 1-sorted

for s being SCM-State of G

for u, v being Nat holds (SCM-Chg (s,u)) . v = s . v

for s being SCM-State of G

for u, v being Nat holds (SCM-Chg (s,u)) . v = s . v

proof end;

definition

let R be non empty 1-sorted ;

let s be SCM-State of R;

let t be Element of SCM-Data-Loc ;

let u be Element of R;

coherence

s +* (t .--> u) is SCM-State of R

end;
let s be SCM-State of R;

let t be Element of SCM-Data-Loc ;

let u be Element of R;

coherence

s +* (t .--> u) is SCM-State of R

proof end;

:: deftheorem defines SCM-Chg SCMRING1:def 6 :

for R being non empty 1-sorted

for s being SCM-State of R

for t being Element of SCM-Data-Loc

for u being Element of R holds SCM-Chg (s,t,u) = s +* (t .--> u);

for R being non empty 1-sorted

for s being SCM-State of R

for t being Element of SCM-Data-Loc

for u being Element of R holds SCM-Chg (s,t,u) = s +* (t .--> u);

theorem :: SCMRING1:10

for G being non empty 1-sorted

for s being SCM-State of G

for t being Element of SCM-Data-Loc

for u being Element of G holds (SCM-Chg (s,t,u)) . NAT = s . NAT

for s being SCM-State of G

for t being Element of SCM-Data-Loc

for u being Element of G holds (SCM-Chg (s,t,u)) . NAT = s . NAT

proof end;

theorem :: SCMRING1:11

for G being non empty 1-sorted

for s being SCM-State of G

for t being Element of SCM-Data-Loc

for u being Element of G holds (SCM-Chg (s,t,u)) . t = u

for s being SCM-State of G

for t being Element of SCM-Data-Loc

for u being Element of G holds (SCM-Chg (s,t,u)) . t = u

proof end;

theorem :: SCMRING1:12

for G being non empty 1-sorted

for s being SCM-State of G

for t being Element of SCM-Data-Loc

for u being Element of G

for mk being Element of SCM-Data-Loc st mk <> t holds

(SCM-Chg (s,t,u)) . mk = s . mk

for s being SCM-State of G

for t being Element of SCM-Data-Loc

for u being Element of G

for mk being Element of SCM-Data-Loc st mk <> t holds

(SCM-Chg (s,t,u)) . mk = s . mk

proof end;

definition

let R be non empty 1-sorted ;

let s be SCM-State of R;

let a be Element of SCM-Data-Loc ;

:: original: .

redefine func s . a -> Element of R;

coherence

s . a is Element of R

end;
let s be SCM-State of R;

let a be Element of SCM-Data-Loc ;

:: original: .

redefine func s . a -> Element of R;

coherence

s . a is Element of R

proof end;

definition

let S be non empty 1-sorted ;

let d be Element of SCM-Data-Loc ;

let s be Element of S;

:: original: <*

redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ the carrier of S;

coherence

<*d,s*> is FinSequence of SCM-Data-Loc \/ the carrier of S

end;
let d be Element of SCM-Data-Loc ;

let s be Element of S;

:: original: <*

redefine func <*d,s*> -> FinSequence of SCM-Data-Loc \/ the carrier of S;

coherence

<*d,s*> is FinSequence of SCM-Data-Loc \/ the carrier of S

proof end;

definition

canceled;

canceled;

canceled;

canceled;

canceled;

canceled;

canceled;

let R be Ring;

let x be Element of SCM-Instr R;

let s be SCM-State of R;

( ( 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 of R ) & ( 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 of R ) & ( 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 of R ) & ( 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 of R ) & ( ex mk being Element of NAT st x = [6,<*mk*>,{}] implies SCM-Chg (s,(x jump_address)) is SCM-State of R ) & ( 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. R),(x cjump_address),(succ (IC s))))) is SCM-State of R ) & ( ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,{},<*mk,r*>] implies SCM-Chg ((SCM-Chg (s,(x const_address),(x const_value))),(succ (IC s))) is SCM-State of R ) & ( ( 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 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 SCM-Data-Loc

for r being Element of R holds not x = [5,{},<*mk,r*>] ) implies s is SCM-State of R ) ) ;

consistency

for b_{1} being SCM-State of R 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 ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b_{1} = 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 ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b_{1} = 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 ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b_{1} = 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 being Element of NAT st x = [6,<*mk*>,{}] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b_{1} = 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 ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b_{1} = SCM-Chg (s,(IFEQ ((s . (x cond_address)),(0. R),(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 SCM-Data-Loc ex r being Element of R st x = [5,{},<*mk,r*>] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b_{1} = SCM-Chg ((SCM-Chg (s,(x const_address),(x const_value))),(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 ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b_{1} = 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 ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b_{1} = 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 being Element of NAT st x = [6,<*mk*>,{}] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b_{1} = 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 ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b_{1} = SCM-Chg (s,(IFEQ ((s . (x cond_address)),(0. R),(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 SCM-Data-Loc ex r being Element of R st x = [5,{},<*mk,r*>] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b_{1} = SCM-Chg ((SCM-Chg (s,(x const_address),(x const_value))),(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 ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) iff b_{1} = 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 being Element of NAT st x = [6,<*mk*>,{}] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) iff b_{1} = 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 ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) iff b_{1} = SCM-Chg (s,(IFEQ ((s . (x cond_address)),(0. R),(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 SCM-Data-Loc ex r being Element of R st x = [5,{},<*mk,r*>] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) iff b_{1} = SCM-Chg ((SCM-Chg (s,(x const_address),(x const_value))),(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 ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) iff b_{1} = 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 ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) iff b_{1} = SCM-Chg (s,(IFEQ ((s . (x cond_address)),(0. R),(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 SCM-Data-Loc ex r being Element of R st x = [5,{},<*mk,r*>] implies ( b_{1} = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) iff b_{1} = SCM-Chg ((SCM-Chg (s,(x const_address),(x const_value))),(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 ( b_{1} = SCM-Chg (s,(x jump_address)) iff b_{1} = SCM-Chg (s,(IFEQ ((s . (x cond_address)),(0. R),(x cjump_address),(succ (IC s))))) ) ) & ( ex mk being Element of NAT st x = [6,<*mk*>,{}] & ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,{},<*mk,r*>] implies ( b_{1} = SCM-Chg (s,(x jump_address)) iff b_{1} = SCM-Chg ((SCM-Chg (s,(x const_address),(x const_value))),(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 SCM-Data-Loc ex r being Element of R st x = [5,{},<*mk,r*>] implies ( b_{1} = SCM-Chg (s,(IFEQ ((s . (x cond_address)),(0. R),(x cjump_address),(succ (IC s))))) iff b_{1} = SCM-Chg ((SCM-Chg (s,(x const_address),(x const_value))),(succ (IC s))) ) ) )
by XTUPLE_0:3;

end;
canceled;

canceled;

canceled;

canceled;

canceled;

canceled;

let R be Ring;

let x be Element of SCM-Instr R;

let s be SCM-State of R;

func SCM-Exec-Res (x,s) -> SCM-State of R equals :: SCMRING1: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 (s,(x jump_address)) if ex mk being Element of NAT st x = [6,<*mk*>,{}]

SCM-Chg (s,(IFEQ ((s . (x cond_address)),(0. R),(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 ((SCM-Chg (s,(x const_address),(x const_value))),(succ (IC s))) if ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,{},<*mk,r*>]

otherwise s;

coherence 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 (s,(x jump_address)) if ex mk being Element of NAT st x = [6,<*mk*>,{}]

SCM-Chg (s,(IFEQ ((s . (x cond_address)),(0. R),(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 ((SCM-Chg (s,(x const_address),(x const_value))),(succ (IC s))) if ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,{},<*mk,r*>]

otherwise s;

( ( 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 of R ) & ( 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 of R ) & ( 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 of R ) & ( 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 of R ) & ( ex mk being Element of NAT st x = [6,<*mk*>,{}] implies SCM-Chg (s,(x jump_address)) is SCM-State of R ) & ( 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. R),(x cjump_address),(succ (IC s))))) is SCM-State of R ) & ( ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,{},<*mk,r*>] implies SCM-Chg ((SCM-Chg (s,(x const_address),(x const_value))),(succ (IC s))) is SCM-State of R ) & ( ( 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 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 SCM-Data-Loc

for r being Element of R holds not x = [5,{},<*mk,r*>] ) implies s is SCM-State of R ) ) ;

consistency

for b

( ( 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 ( b

:: deftheorem defines SCM-Exec-Res SCMRING1:def 14 :

for R being Ring

for x being Element of SCM-Instr R

for s being SCM-State of R 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 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. R),(x cjump_address),(succ (IC s))))) ) & ( ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,{},<*mk,r*>] implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(x const_address),(x const_value))),(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 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 SCM-Data-Loc

for r being Element of R holds not x = [5,{},<*mk,r*>] ) implies SCM-Exec-Res (x,s) = s ) );

for R being Ring

for x being Element of SCM-Instr R

for s being SCM-State of R 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 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. R),(x cjump_address),(succ (IC s))))) ) & ( ex mk being Element of SCM-Data-Loc ex r being Element of R st x = [5,{},<*mk,r*>] implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg (s,(x const_address),(x const_value))),(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 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 SCM-Data-Loc

for r being Element of R holds not x = [5,{},<*mk,r*>] ) implies SCM-Exec-Res (x,s) = s ) );

definition

let R be Ring;

ex b_{1} being Action of (SCM-Instr R),(product ((SCM-VAL R) * SCM-OK)) st

for x being Element of SCM-Instr R

for y being SCM-State of R holds (b_{1} . x) . y = SCM-Exec-Res (x,y)

for b_{1}, b_{2} being Action of (SCM-Instr R),(product ((SCM-VAL R) * SCM-OK)) st ( for x being Element of SCM-Instr R

for y being SCM-State of R holds (b_{1} . x) . y = SCM-Exec-Res (x,y) ) & ( for x being Element of SCM-Instr R

for y being SCM-State of R holds (b_{2} . x) . y = SCM-Exec-Res (x,y) ) holds

b_{1} = b_{2}

end;
func SCM-Exec R -> Action of (SCM-Instr R),(product ((SCM-VAL R) * SCM-OK)) means :: SCMRING1:def 15

for x being Element of SCM-Instr R

for y being SCM-State of R holds (it . x) . y = SCM-Exec-Res (x,y);

existence for x being Element of SCM-Instr R

for y being SCM-State of R holds (it . x) . y = SCM-Exec-Res (x,y);

ex b

for x being Element of SCM-Instr R

for y being SCM-State of R holds (b

proof end;

uniqueness for b

for y being SCM-State of R holds (b

for y being SCM-State of R holds (b

b

proof end;

:: deftheorem defines SCM-Exec SCMRING1:def 15 :

for R being Ring

for b_{2} being Action of (SCM-Instr R),(product ((SCM-VAL R) * SCM-OK)) holds

( b_{2} = SCM-Exec R iff for x being Element of SCM-Instr R

for y being SCM-State of R holds (b_{2} . x) . y = SCM-Exec-Res (x,y) );

for R being Ring

for b

( b

for y being SCM-State of R holds (b