:: The Construction of { \bf SCM } over Ring
:: by Artur Korni{\l}owicz
::
:: Copyright (c) 1998-2021 Association of Mizar Users

definition
let S be non empty 1-sorted ;
func SCM-VAL S -> ManySortedSet of Segm 2 equals :: SCMRING1:def 3
<%NAT, the carrier of S%>;
coherence
<%NAT, the carrier of S%> is ManySortedSet of Segm 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-OK) = SCM-Memory
proof end;

theorem :: SCMRING1:1
canceled;

::$CT theorem Th1: :: SCMRING1:2 for G being non empty 1-sorted holds (() * SCM-OK) . NAT = NAT proof end; theorem Th2: :: SCMRING1:3 for G being non empty 1-sorted for i being Element of SCM-Memory st i in SCM-Data-Loc holds (() * SCM-OK) . i = the carrier of G proof end; registration let G be non empty 1-sorted ; coherence () * 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-OK); end; theorem :: SCMRING1:4 for d1 being Element of SCM-Data-Loc for G being non empty 1-sorted holds (() * SCM-OK) . d1 = the carrier of G by Th2; theorem Th4: :: SCMRING1:5 for G being non empty 1-sorted holds pi ((product (() * SCM-OK)),NAT) = NAT proof end; theorem Th5: :: SCMRING1:6 for G being non empty 1-sorted for a being Element of SCM-Data-Loc holds pi ((product (() * 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 natural Number ; func SCM-Chg (s,u) -> SCM-State of R equals :: SCMRING1:def 5 s +* (); coherence s +* () 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 natural Number holds SCM-Chg (s,u) = s +* (); theorem :: SCMRING1:7 for G being non empty 1-sorted for s being SCM-State of G for u being natural Number 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 natural Number 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 natural Number 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 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,(),(s . ()))),((IC s) + 1)) if ex mk, ml being Element of SCM-Data-Loc st x = [1,{},<*mk,ml*>] SCM-Chg ((SCM-Chg (s,(),((s . ()) + (s . ())))),((IC s) + 1)) if ex mk, ml being Element of SCM-Data-Loc st x = [2,{},<*mk,ml*>] SCM-Chg ((SCM-Chg (s,(),((s . ()) - (s . ())))),((IC s) + 1)) if ex mk, ml being Element of SCM-Data-Loc st x = [3,{},<*mk,ml*>] SCM-Chg ((SCM-Chg (s,(),((s . ()) * (s . ())))),((IC s) + 1)) if ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>] SCM-Chg (s,()) if ex mk being Element of NAT st x = [6,<*mk*>,{}] SCM-Chg (s,(IFEQ ((s . ()),(0. R),(),((IC s) + 1)))) 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,(),())),((IC s) + 1)) 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,(),(s . ()))),((IC s) + 1)) 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,(),((s . ()) + (s . ())))),((IC s) + 1)) 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,(),((s . ()) - (s . ())))),((IC s) + 1)) 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,(),((s . ()) * (s . ())))),((IC s) + 1)) is SCM-State of R ) & ( ex mk being Element of NAT st x = [6,<*mk*>,{}] implies SCM-Chg (s,()) 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 . ()),(0. R),(),((IC s) + 1)))) 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,(),())),((IC s) + 1)) 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,(),(s . ()))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) + (s . ())))),((IC s) + 1)) ) ) & ( 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,(),(s . ()))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) - (s . ())))),((IC s) + 1)) ) ) & ( 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,(),(s . ()))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) * (s . ())))),((IC s) + 1)) ) ) & ( 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,(),(s . ()))),((IC s) + 1)) iff b1 = SCM-Chg (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 = [7,<*mk*>,<*ml*>] implies ( b1 = SCM-Chg ((SCM-Chg (s,(),(s . ()))),((IC s) + 1)) iff b1 = SCM-Chg (s,(IFEQ ((s . ()),(0. R),(),((IC s) + 1)))) ) ) & ( 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,(),(s . ()))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),())),((IC s) + 1)) ) ) & ( 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,(),((s . ()) + (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) - (s . ())))),((IC s) + 1)) ) ) & ( 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,(),((s . ()) + (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) * (s . ())))),((IC s) + 1)) ) ) & ( 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,(),((s . ()) + (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (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 = [7,<*mk*>,<*ml*>] implies ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) + (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,(IFEQ ((s . ()),(0. R),(),((IC s) + 1)))) ) ) & ( 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,(),((s . ()) + (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),())),((IC s) + 1)) ) ) & ( 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,(),((s . ()) - (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) * (s . ())))),((IC s) + 1)) ) ) & ( 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,(),((s . ()) - (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (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 = [7,<*mk*>,<*ml*>] implies ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) - (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,(IFEQ ((s . ()),(0. R),(),((IC s) + 1)))) ) ) & ( 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,(),((s . ()) - (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),())),((IC s) + 1)) ) ) & ( 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,(),((s . ()) * (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (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 = [7,<*mk*>,<*ml*>] implies ( b1 = SCM-Chg ((SCM-Chg (s,(),((s . ()) * (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg (s,(IFEQ ((s . ()),(0. R),(),((IC s) + 1)))) ) ) & ( 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,(),((s . ()) * (s . ())))),((IC s) + 1)) iff b1 = SCM-Chg ((SCM-Chg (s,(),())),((IC s) + 1)) ) ) & ( 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,()) iff b1 = SCM-Chg (s,(IFEQ ((s . ()),(0. R),(),((IC s) + 1)))) ) ) & ( 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,()) iff b1 = SCM-Chg ((SCM-Chg (s,(),())),((IC s) + 1)) ) ) & ( 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 . ()),(0. R),(),((IC s) + 1)))) iff b1 = SCM-Chg ((SCM-Chg (s,(),())),((IC s) + 1)) ) ) ) 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,(),(s . ()))),((IC s) + 1)) ) & ( 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,(),((s . ()) + (s . ())))),((IC s) + 1)) ) & ( 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,(),((s . ()) - (s . ())))),((IC s) + 1)) ) & ( 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,(),((s . ()) * (s . ())))),((IC s) + 1)) ) & ( ex mk being Element of NAT st x = [6,<*mk*>,{}] implies SCM-Exec-Res (x,s) = SCM-Chg (s,()) ) & ( 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 . ()),(0. R),(),((IC s) + 1)))) ) & ( 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,(),())),((IC s) + 1)) ) & ( ( 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 (),(product (() * 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 (),(product (() * 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 (),(product (() * 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 (),(product (() * 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; ::$CT 6
theorem :: SCMRING1:19
for S being non empty 1-sorted
for s being SCM-State of S holds dom s = SCM-Memory
proof end;