:: SCMRING1 semantic presentation

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
let S be non empty 1-sorted ; ::_thesis: dom ((SCM-VAL S) * SCM-OK) = SCM-Memory
A1: dom SCM-OK = SCM-Memory by PARTFUN1:def_2;
 len <%NAT, the carrier of S%> = 2 by AFINSQ_1:38;
then  rng SCM-OK c= dom (SCM-VAL S) by RELAT_1:def_19;
hence  dom ((SCM-VAL S) * SCM-OK) = SCM-Memory by A1, RELAT_1:27; ::_thesis: verum
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
let G be non empty 1-sorted ; ::_thesis: ((SCM-VAL G) * SCM-OK) . NAT = NAT
A1: NAT in SCM-Memory by AMI_2:22;
then  NAT in dom SCM-OK by PARTFUN1:def_2;
then A2: ((SCM-VAL G) * SCM-OK) . NAT = (SCM-VAL G) . (SCM-OK . NAT) by FUNCT_1:13;
 ((SCM-VAL G) * SCM-OK) . NAT = (SCM-VAL G) . 0 by A2, A1, AMI_2:def_4;
hence  ((SCM-VAL G) * SCM-OK) . NAT = NAT by AFINSQ_1:38; ::_thesis: verum
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
let G be non empty 1-sorted ; ::_thesis: for i being Element of SCM-Memory st i in SCM-Data-Loc holds
((SCM-VAL G) * SCM-OK) . i = the carrier of G
let i be Element of SCM-Memory ; ::_thesis: ( i in SCM-Data-Loc implies ((SCM-VAL G) * SCM-OK) . i = the carrier of G )
 i in SCM-Memory ;
then  i in dom SCM-OK by PARTFUN1:def_2;
then A1: ((SCM-VAL G) * SCM-OK) . i = (SCM-VAL G) . (SCM-OK . i) by FUNCT_1:13;
assume  i in SCM-Data-Loc ; ::_thesis: ((SCM-VAL G) * SCM-OK) . i = the carrier of G
then  ((SCM-VAL G) * SCM-OK) . i = (SCM-VAL G) . 1 by A1, AMI_2:def_4;
hence  ((SCM-VAL G) * SCM-OK) . i = the carrier of G by AFINSQ_1:38; ::_thesis: verum
end;

registration
let G be non empty 1-sorted ;
clusterSCM-OK * (SCM-VAL G) ->  non-empty ;
coherence
 (SCM-VAL G) * SCM-OK is non-empty
proof
set F = (SCM-VAL G) * SCM-OK;
let n be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not n in proj1 ((SCM-VAL G) * SCM-OK) or not ((SCM-VAL G) * SCM-OK) . n is empty )
assume A1: n in dom ((SCM-VAL G) * SCM-OK) ; ::_thesis: not ((SCM-VAL G) * SCM-OK) . n is empty
 dom ((SCM-VAL G) * SCM-OK) = SCM-Memory by Lm1;
percasesthen  ( n = NAT or n in SCM-Data-Loc ) by A1, AMI_2:26;
supposeA2: n = NAT ; ::_thesis: not ((SCM-VAL G) * SCM-OK) . n is empty
 ((SCM-VAL G) * SCM-OK) . n = NAT by A2, Th2;
hence  not ((SCM-VAL G) * SCM-OK) . n is empty ; ::_thesis: verum
end;
suppose n in SCM-Data-Loc ; ::_thesis: not ((SCM-VAL G) * SCM-OK) . n is empty
then  ((SCM-VAL G) * SCM-OK) . n = the carrier of G by Th3;
hence  not ((SCM-VAL G) * SCM-OK) . n is empty ; ::_thesis: verum
end;
end;
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
let G be non empty 1-sorted ; ::_thesis: pi ((product ((SCM-VAL G) * SCM-OK)),NAT) = NAT
 NAT in dom ((SCM-VAL G) * SCM-OK) by Lm1, AMI_2:22;
hence  pi ((product ((SCM-VAL G) * SCM-OK)),NAT) = ((SCM-VAL G) * SCM-OK) . NAT by CARD_3:12
.= NAT by Th2 ;
::_thesis: verum
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
let G be non empty 1-sorted ; ::_thesis: for a being Element of SCM-Data-Loc holds pi ((product ((SCM-VAL G) * SCM-OK)),a) = the carrier of G
let a be Element of SCM-Data-Loc ; ::_thesis: pi ((product ((SCM-VAL G) * SCM-OK)),a) = the carrier of G
 a in SCM-Memory ;
then  a in dom ((SCM-VAL G) * SCM-OK) by Lm1;
hence  pi ((product ((SCM-VAL G) * SCM-OK)),a) = ((SCM-VAL G) * SCM-OK) . a by CARD_3:12
.= the carrier of G by Th3 ;
::_thesis: verum
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
 s . NAT in pi ((product ((SCM-VAL G) * SCM-OK)),NAT) by CARD_3:def_6;
hence  s . NAT is Element of NAT by Th5; ::_thesis: verum
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
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_((SCM-VAL_R)_*_SCM-OK)_holds_
(s_+*_(NAT_.-->_u))_._x_in_((SCM-VAL_R)_*_SCM-OK)_._x
let x be set ; ::_thesis: ( x in dom ((SCM-VAL R) * SCM-OK) implies (s +* (NAT .--> u)) . b1 in ((SCM-VAL R) * SCM-OK) . b1 )
assume A2: x in dom ((SCM-VAL R) * SCM-OK) ; ::_thesis: (s +* (NAT .--> u)) . b1 in ((SCM-VAL R) * SCM-OK) . b1
percases ( x = NAT or x <> NAT ) ;
supposeA3: x = NAT ; ::_thesis: (s +* (NAT .--> u)) . b1 in ((SCM-VAL R) * SCM-OK) . b1
 {NAT} = dom (NAT .--> u) by FUNCOP_1:13;
then  NAT in dom (NAT .--> u) by TARSKI:def_1;
then (s +* (NAT .--> u)) . NAT = (NAT .--> u) . NAT by FUNCT_4:13
.= u by FUNCOP_1:72 ;
then  (s +* (NAT .--> u)) . NAT in NAT by ORDINAL1:def_12;
hence  (s +* (NAT .--> u)) . x in ((SCM-VAL R) * SCM-OK) . x by A3, Th2; ::_thesis: verum
end;
supposeA4: x <> NAT ; ::_thesis: (s +* (NAT .--> u)) . b1 in ((SCM-VAL R) * SCM-OK) . b1
 {NAT} = dom (NAT .--> u) by FUNCOP_1:13;
then  not x in dom (NAT .--> u) by A4, TARSKI:def_1;
then  (s +* (NAT .--> u)) . x = s . x by FUNCT_4:11;
hence  (s +* (NAT .--> u)) . x in ((SCM-VAL R) * SCM-OK) . x by A2, CARD_3:9; ::_thesis: verum
end;
end;
end;
A5: dom ((SCM-VAL R) * SCM-OK) = SCM-Memory by Lm1;
then  dom s = SCM-Memory by CARD_3:9;
then  dom (s +* (NAT .--> u)) = SCM-Memory \/ (dom (NAT .--> u)) by FUNCT_4:def_1
.= SCM-Memory \/ {NAT} by FUNCOP_1:13
.= dom ((SCM-VAL R) * SCM-OK) by A5, AMI_2:22, ZFMISC_1:40 ;
hence  s +* (NAT .--> u) is SCM-State of R by A1, CARD_3:9; ::_thesis: verum
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
let G be non empty 1-sorted ; ::_thesis: for s being SCM-State of G
for u being Nat holds (SCM-Chg (s,u)) . NAT = u
let s be SCM-State of G; ::_thesis: for u being Nat holds (SCM-Chg (s,u)) . NAT = u
let u be Nat; ::_thesis: (SCM-Chg (s,u)) . NAT = u
 {NAT} = dom (NAT .--> u) by FUNCOP_1:13;
then  NAT in dom (NAT .--> u) by TARSKI:def_1;
hence (SCM-Chg (s,u)) . NAT = (NAT .--> u) . NAT by FUNCT_4:13
.= u by FUNCOP_1:72 ;
::_thesis: verum
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
let G be non empty 1-sorted ; ::_thesis: 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
let s be SCM-State of G; ::_thesis: for u being Nat
for mk being Element of SCM-Data-Loc holds (SCM-Chg (s,u)) . mk = s . mk
let u be Nat; ::_thesis: for mk being Element of SCM-Data-Loc holds (SCM-Chg (s,u)) . mk = s . mk
let mk be Element of SCM-Data-Loc ; ::_thesis: (SCM-Chg (s,u)) . mk = s . mk
A1: {NAT} = dom (NAT .--> u) by FUNCOP_1:13;
 NAT in SCM-Memory by AMI_2:22;
then  ( SCM-OK . NAT = 0 & SCM-OK . mk = 1 ) by AMI_2:def_4;
then  not mk in dom (NAT .--> u) by A1, TARSKI:def_1;
hence  (SCM-Chg (s,u)) . mk = s . mk by FUNCT_4:11; ::_thesis: verum
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
let G be non empty 1-sorted ; ::_thesis: for s being SCM-State of G
for u, v being Nat holds (SCM-Chg (s,u)) . v = s . v
let s be SCM-State of G; ::_thesis: for u, v being Nat holds (SCM-Chg (s,u)) . v = s . v
let u, v be Nat; ::_thesis: (SCM-Chg (s,u)) . v = s . v
 {NAT} = dom (NAT .--> u) by FUNCOP_1:13;
then  not v in dom (NAT .--> u) by TARSKI:def_1;
hence  (SCM-Chg (s,u)) . v = s . v by FUNCT_4:11; ::_thesis: verum
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
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_((SCM-VAL_R)_*_SCM-OK)_holds_
(s_+*_(t_.-->_u))_._x_in_((SCM-VAL_R)_*_SCM-OK)_._x
let x be set ; ::_thesis: ( x in dom ((SCM-VAL R) * SCM-OK) implies (s +* (t .--> u)) . b1 in ((SCM-VAL R) * SCM-OK) . b1 )
assume A2: x in dom ((SCM-VAL R) * SCM-OK) ; ::_thesis: (s +* (t .--> u)) . b1 in ((SCM-VAL R) * SCM-OK) . b1
percases ( x = t or x <> t ) ;
supposeA3: x = t ; ::_thesis: (s +* (t .--> u)) . b1 in ((SCM-VAL R) * SCM-OK) . b1
 {t} = dom (t .--> u) by FUNCOP_1:13;
then  t in dom (t .--> u) by TARSKI:def_1;
then (s +* (t .--> u)) . t = (t .--> u) . t by FUNCT_4:13
.= u by FUNCOP_1:72 ;
then  (s +* (t .--> u)) . t in the carrier of R ;
hence  (s +* (t .--> u)) . x in ((SCM-VAL R) * SCM-OK) . x by A3, Th3; ::_thesis: verum
end;
supposeA4: x <> t ; ::_thesis: (s +* (t .--> u)) . b1 in ((SCM-VAL R) * SCM-OK) . b1
 {t} = dom (t .--> u) by FUNCOP_1:13;
then  not x in dom (t .--> u) by A4, TARSKI:def_1;
then  (s +* (t .--> u)) . x = s . x by FUNCT_4:11;
hence  (s +* (t .--> u)) . x in ((SCM-VAL R) * SCM-OK) . x by A2, CARD_3:9; ::_thesis: verum
end;
end;
end;
A5: dom ((SCM-VAL R) * SCM-OK) = SCM-Memory by Lm1;
then  dom s = SCM-Memory by CARD_3:9;
then  dom (s +* (t .--> u)) = SCM-Memory \/ (dom (t .--> u)) by FUNCT_4:def_1
.= SCM-Memory \/ {t} by FUNCOP_1:13
.= dom ((SCM-VAL R) * SCM-OK) by A5, ZFMISC_1:40 ;
hence  s +* (t .--> u) is SCM-State of R by A1, CARD_3:9; ::_thesis: verum
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
let G be non empty 1-sorted ; ::_thesis: 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
let s be SCM-State of G; ::_thesis: for t being Element of SCM-Data-Loc
for u being Element of G holds (SCM-Chg (s,t,u)) . NAT = s . NAT
let t be Element of SCM-Data-Loc ; ::_thesis: for u being Element of G holds (SCM-Chg (s,t,u)) . NAT = s . NAT
let u be Element of G; ::_thesis: (SCM-Chg (s,t,u)) . NAT = s . NAT
A1: {t} = dom (t .--> u) by FUNCOP_1:13;
 NAT in SCM-Memory by AMI_2:22;
then  ( SCM-OK . NAT = 0 & SCM-OK . t = 1 ) by AMI_2:def_4;
then  not NAT in dom (t .--> u) by A1, TARSKI:def_1;
hence  (SCM-Chg (s,t,u)) . NAT = s . NAT by FUNCT_4:11; ::_thesis: verum
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
let G be non empty 1-sorted ; ::_thesis: 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
let s be SCM-State of G; ::_thesis: for t being Element of SCM-Data-Loc
for u being Element of G holds (SCM-Chg (s,t,u)) . t = u
let t be Element of SCM-Data-Loc ; ::_thesis: for u being Element of G holds (SCM-Chg (s,t,u)) . t = u
let u be Element of G; ::_thesis: (SCM-Chg (s,t,u)) . t = u
 {t} = dom (t .--> u) by FUNCOP_1:13;
then  t in dom (t .--> u) by TARSKI:def_1;
hence (SCM-Chg (s,t,u)) . t = (t .--> u) . t by FUNCT_4:13
.= u by FUNCOP_1:72 ;
::_thesis: verum
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
let G be non empty 1-sorted ; ::_thesis: 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
let s be SCM-State of G; ::_thesis: 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
let t be Element of SCM-Data-Loc ; ::_thesis: 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
let u be Element of G; ::_thesis: for mk being Element of SCM-Data-Loc st mk <> t holds
(SCM-Chg (s,t,u)) . mk = s . mk
let mk be Element of SCM-Data-Loc ; ::_thesis: ( mk <> t implies (SCM-Chg (s,t,u)) . mk = s . mk )
assume A1: mk <> t ; ::_thesis: (SCM-Chg (s,t,u)) . mk = s . mk
 {t} = dom (t .--> u) by FUNCOP_1:13;
then  not mk in dom (t .--> u) by A1, TARSKI:def_1;
hence  (SCM-Chg (s,t,u)) . mk = s . mk by FUNCT_4:11; ::_thesis: verum
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 funcs . a ->  Element of R;
coherence
 s . a is Element of R
proof
 s . a in pi ((product ((SCM-VAL R) * SCM-OK)),a) by CARD_3:def_6;
hence  s . a is Element of R by Th6; ::_thesis: verum
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
let y be set ; :: according to TARSKI:def_3,FINSEQ_1:def_4 ::_thesis: ( not y in proj2 <*d,s*> or y in SCM-Data-Loc \/ the carrier of S )
A1: dom <*d,s*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
assume  y in rng <*d,s*> ; ::_thesis: y in SCM-Data-Loc \/ the carrier of S
then consider x being set  such that
A2: x in dom <*d,s*> and
A3: <*d,s*> . x = y by FUNCT_1:def_3;
percases ( x = 1 or x = 2 ) by A2, A1, TARSKI:def_2;
suppose x = 1 ; ::_thesis: y in SCM-Data-Loc \/ the carrier of S
then  y = d by A3, FINSEQ_1:44;
hence  y in SCM-Data-Loc \/ the carrier of S by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose x = 2 ; ::_thesis: y in SCM-Data-Loc \/ the carrier of S
then  y = s by A3, FINSEQ_1:44;
hence  y in SCM-Data-Loc \/ the carrier of S by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
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
deffunc H1( Element of SCM-Instr R, SCM-State of R) ->  SCM-State of R = SCM-Exec-Res ($1,$2);
consider f being Function of [:(SCM-Instr R),(product ((SCM-VAL R) * SCM-OK)):],(product ((SCM-VAL R) * SCM-OK)) such that
A1: for x being Element of SCM-Instr R
for y being SCM-State of R holds f . (x,y) = H1(x,y) from BINOP_1:sch_4();
take  curry f ; ::_thesis: for x being Element of SCM-Instr R
for y being SCM-State of R holds ((curry f) . x) . y = SCM-Exec-Res (x,y)
let x be Element of SCM-Instr R; ::_thesis: for y being SCM-State of R holds ((curry f) . x) . y = SCM-Exec-Res (x,y)
let y be SCM-State of R; ::_thesis: ((curry f) . x) . y = SCM-Exec-Res (x,y)
thus ((curry f) . x) . y = f . (x,y) by FUNCT_5:69
.= SCM-Exec-Res (x,y) by A1 ; ::_thesis: verum
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
let f, g be Action of (SCM-Instr R),(product ((SCM-VAL R) * SCM-OK)); ::_thesis: ( ( for x being Element of SCM-Instr R
for y being SCM-State of R holds (f . x) . y = SCM-Exec-Res (x,y) ) & ( for x being Element of SCM-Instr R
for y being SCM-State of R holds (g . x) . y = SCM-Exec-Res (x,y) ) implies f = g )
assume that
A2: for x being Element of SCM-Instr R
for y being SCM-State of R holds (f . x) . y = SCM-Exec-Res (x,y) and
A3: for x being Element of SCM-Instr R
for y being SCM-State of R holds (g . x) . y = SCM-Exec-Res (x,y) ; ::_thesis: f = g
now__::_thesis:_for_x_being_Element_of_SCM-Instr_R_holds_f_._x_=_g_._x
let x be Element of SCM-Instr R; ::_thesis: f . x = g . x
reconsider gx = g . x, fx = f . x as Function of (product ((SCM-VAL R) * SCM-OK)),(product ((SCM-VAL R) * SCM-OK)) by FUNCT_2:66;
now__::_thesis:_for_y_being_SCM-State_of_R_holds_fx_._y_=_gx_._y
let y be SCM-State of R; ::_thesis: fx . y = gx . y
thus fx . y = SCM-Exec-Res (x,y) by A2
.= gx . y by A3 ; ::_thesis: verum
end;
hence  f . x = g . x by FUNCT_2:63; ::_thesis: verum
end;
hence  f = g by FUNCT_2:63; ::_thesis: verum
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
let S be non empty 1-sorted ; ::_thesis: for s being SCM-State of S holds dom s = SCM-Memory
let s be SCM-State of S; ::_thesis: dom s = SCM-Memory
 dom s = dom ((SCM-VAL S) * SCM-OK) by CARD_3:9;
hence  dom s = SCM-Memory by Lm1; ::_thesis: verum
end;