:: The Construction of { \bf SCM } over Ring
:: 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 ;
func SCM-VAL S -> ManySortedSet of 2 equals :: SCMRING1:def 3
<%NAT, the carrier of S%>;
coherence
<%NAT, the carrier of S%> is ManySortedSet of 2
;
end;

:: deftheorem SCMRING1:def 1 :
canceled;

:: deftheorem SCMRING1:def 2 :
canceled;

:: deftheorem defines SCM-VAL SCMRING1:def 3 :
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 :: SCMRING1:1
canceled;

theorem Th2: :: SCMRING1:2
for G being non empty 1-sorted holds ((SCM-VAL G) * SCM-OK) . NAT = NAT
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
proof end;

registration
let G be non empty 1-sorted ;
cluster SCM-OK * (SCM-VAL G) -> non-empty ;
coherence
(SCM-VAL G) * SCM-OK is non-empty
proof end;
end;

definition
let S be non empty 1-sorted ;
mode SCM-State of S is Element of product ((SCM-VAL S) * SCM-OK);
end;

theorem :: SCMRING1:4
for d1 being Element of SCM-Data-Loc
for G being non empty 1-sorted holds ((SCM-VAL G) * SCM-OK) . d1 = the carrier of G by Th3;

theorem Th5: :: SCMRING1:5
for G being non empty 1-sorted holds pi ((product ((SCM-VAL G) * SCM-OK)),NAT) = NAT
proof end;

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
proof end;

definition
let G be non empty 1-sorted ;
let s be SCM-State of G;
func IC s -> Element of NAT equals :: SCMRING1:def 4
s . NAT;
coherence
s . NAT is Element of NAT
proof end;
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;

definition
let R be non empty 1-sorted ;
let s be SCM-State of R;
let u be Nat;
func SCM-Chg (s,u) -> SCM-State of R equals :: SCMRING1:def 5
s +* (NAT .--> u);
coherence
s +* (NAT .--> u) is SCM-State of R
proof end;
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);

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
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
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
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;
func SCM-Chg (s,t,u) -> SCM-State of R equals :: SCMRING1:def 6
s +* (t .--> u);
coherence
s +* (t .--> u) is SCM-State of R
proof end;
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);

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
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
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
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
proof end;
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
proof end;
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;
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
( ( 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 b1 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 ( 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 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. 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 ( b1 = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b1 = 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 ( 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 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. 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 ( 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 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 ( 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 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. 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 ( 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 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 ( 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. 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 ( 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 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 ( b1 = SCM-Chg (s,(x jump_address)) iff b1 = 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 ( b1 = SCM-Chg (s,(x jump_address)) iff b1 = 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 ( b1 = SCM-Chg (s,(IFEQ ((s . (x cond_address)),(0. R),(x cjump_address),(succ (IC s))))) iff b1 = SCM-Chg ((SCM-Chg (s,(x const_address),(x const_value))),(succ (IC s))) ) ) )
by XTUPLE_0:3;
end;

:: deftheorem SCMRING1:def 7 :
canceled;

:: deftheorem SCMRING1:def 8 :
canceled;

:: deftheorem SCMRING1:def 9 :
canceled;

:: deftheorem SCMRING1:def 10 :
canceled;

:: deftheorem SCMRING1:def 11 :
canceled;

:: deftheorem SCMRING1:def 12 :
canceled;

:: deftheorem SCMRING1:def 13 :
canceled;

:: 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 ) );

definition
let R be Ring;
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
ex b1 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 (b1 . x) . y = SCM-Exec-Res (x,y)
proof end;
uniqueness
for b1, b2 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 (b1 . x) . y = SCM-Exec-Res (x,y) ) & ( for x being Element of SCM-Instr R
for y being SCM-State of R holds (b2 . x) . y = SCM-Exec-Res (x,y) ) holds
b1 = b2
proof end;
end;

:: deftheorem defines SCM-Exec SCMRING1:def 15 :
for R being Ring
for b2 being Action of (SCM-Instr R),(product ((SCM-VAL R) * SCM-OK)) holds
( b2 = SCM-Exec R iff for x being Element of SCM-Instr R
for y being SCM-State of R holds (b2 . x) . y = SCM-Exec-Res (x,y) );

theorem :: SCMRING1:13
canceled;

theorem :: SCMRING1:14
canceled;

theorem :: SCMRING1:15
canceled;

theorem :: SCMRING1:16
canceled;

theorem :: SCMRING1:17
canceled;

theorem :: SCMRING1:18
canceled;

theorem :: SCMRING1:19
for S being non empty 1-sorted
for s being SCM-State of S holds dom s = SCM-Memory
proof end;