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

begin

registration

cluster SCM-Instr -> non trivial ;
coherence
not SCM-Instr is trivial

proof end;

end;

definition

let S be non empty 1-sorted ;
func SCM-Instr S -> non empty set equals :: SCMRING1:def 1
((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ;
coherence
((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } is non empty set ;

end;

:: deftheorem defines SCM-Instr SCMRING1:def 1 :
for S being non empty 1-sorted holds SCM-Instr S = ((({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Element of NAT : verum } ) \/ { [7,<*i*>,<*a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ) \/ { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ;

registration

let S be non empty 1-sorted ;
cluster SCM-Instr S -> non empty non trivial ;
coherence
not SCM-Instr S is trivial

proof end;

end;

definition

let S be non empty 1-sorted ;
attr S is good means :Def2: :: SCMRING1:def 2
( the carrier of S <> NAT & the carrier of S <> SCM-Instr S );

end;

:: deftheorem Def2 defines good SCMRING1:def 2 :
for S being non empty 1-sorted holds
( S is good iff ( the carrier of S <> NAT & the carrier of S <> SCM-Instr S ) );

registration

cluster non empty trivial -> non empty good 1-sorted ;
coherence
for b₁ being non empty 1-sorted st b₁ is trivial holds
b₁ is good

proof end;

end;

Lm1: now

let k be Element of SCM-Memory ; :: thesis: ( k = NAT or k in SCM-Data-Loc or k in NAT )
( k in {NAT} \/ SCM-Data-Loc or k in NAT ) by XBOOLE_0:def 3;
then ( k in {NAT} or k in SCM-Data-Loc or k in NAT ) by XBOOLE_0:def 3;
hence ( k = NAT or k in SCM-Data-Loc or k in NAT ) by TARSKI:def 1; :: thesis: verum

end;

definition

let S be non empty 1-sorted ;
func SCM-OK S -> Function of SCM-Memory,({ the carrier of S} \/ {(SCM-Instr S),NAT}) means :Def3: :: SCMRING1:def 3
for k being Element of SCM-Memory holds
( ( k = NAT implies it . k = NAT ) & ( k in SCM-Data-Loc implies it . k = the carrier of S ) & ( k in NAT implies it . k = SCM-Instr S ) );
existence
ex b₁ being Function of SCM-Memory,({ the carrier of S} \/ {(SCM-Instr S),NAT}) st
for k being Element of SCM-Memory holds
( ( k = NAT implies b₁ . k = NAT ) & ( k in SCM-Data-Loc implies b₁ . k = the carrier of S ) & ( k in NAT implies b₁ . k = SCM-Instr S ) )

proof end;

uniqueness
for b₁, b₂ being Function of SCM-Memory,({ the carrier of S} \/ {(SCM-Instr S),NAT}) st ( for k being Element of SCM-Memory holds
( ( k = NAT implies b₁ . k = NAT ) & ( k in SCM-Data-Loc implies b₁ . k = the carrier of S ) & ( k in NAT implies b₁ . k = SCM-Instr S ) ) ) & ( for k being Element of SCM-Memory holds
( ( k = NAT implies b₂ . k = NAT ) & ( k in SCM-Data-Loc implies b₂ . k = the carrier of S ) & ( k in NAT implies b₂ . k = SCM-Instr S ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines SCM-OK SCMRING1:def 3 :
for S being non empty 1-sorted
for b₂ being Function of SCM-Memory,({ the carrier of S} \/ {(SCM-Instr S),NAT}) holds
( b₂ = SCM-OK S iff for k being Element of SCM-Memory holds
( ( k = NAT implies b₂ . k = NAT ) & ( k in SCM-Data-Loc implies b₂ . k = the carrier of S ) & ( k in NAT implies b₂ . k = SCM-Instr S ) ) );

definition

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

end;

theorem Th1: :: SCMRING1:1

for S being non empty 1-sorted holds NAT <> SCM-Instr S

proof end;

theorem Th2: :: SCMRING1:2

for G being non empty good 1-sorted
for i being Element of SCM-Memory holds
( (SCM-OK G) . i = NAT iff i = NAT )

proof end;

theorem Th3: :: SCMRING1:3

for G being non empty good 1-sorted
for i being Element of SCM-Memory holds
( (SCM-OK G) . i = the carrier of G iff i in SCM-Data-Loc )

proof end;

theorem Th4: :: SCMRING1:4

for G being non empty good 1-sorted
for i being Element of SCM-Memory holds
( (SCM-OK G) . i = SCM-Instr G iff i in NAT )

proof end;

theorem :: SCMRING1:5

for d1 being Element of SCM-Data-Loc
for G being non empty good 1-sorted holds (SCM-OK G) . d1 = the carrier of G by Th3;

Lm2: NAT c= SCM-Memory
by XBOOLE_1:7;

theorem :: SCMRING1:6

for i1 being Element of NAT
for G being non empty good 1-sorted holds (SCM-OK G) . i1 = SCM-Instr G

proof end;

theorem Th7: :: SCMRING1:7

for S being non empty 1-sorted holds pi ((product (SCM-OK S)),NAT) = NAT

proof end;

theorem Th8: :: SCMRING1:8

for d1 being Element of SCM-Data-Loc
for G being non empty good 1-sorted holds pi ((product (SCM-OK G)),d1) = the carrier of G

proof end;

definition

let S be non empty 1-sorted ;
let s be SCM-State of S;
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 S being non empty 1-sorted
for s being SCM-State of S holds IC s = s . NAT;

definition

let R be non empty good 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 good 1-sorted
for s being SCM-State of R
for u being Nat holds SCM-Chg (s,u) = s +* (NAT .--> u);

theorem :: SCMRING1:9

canceled;

theorem :: SCMRING1:10

for G being non empty good 1-sorted
for s being SCM-State of G
for u being Nat holds (SCM-Chg (s,u)) . NAT = u

proof end;

theorem :: SCMRING1:11

for G being non empty good 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:12

for G being non empty good 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 good 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 good 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:13

for G being non empty good 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:14

for G being non empty good 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:15

for G being non empty good 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;

theorem :: SCMRING1:16

for G being non empty good 1-sorted
for s being SCM-State of G
for t being Element of SCM-Data-Loc
for u being Element of G
for v being Element of NAT holds (SCM-Chg (s,t,u)) . v = s . v

proof end;

definition

let R be non empty good 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 x be Element of SCM-Instr S;
given mk, ml being Element of SCM-Data-Loc , I being Element of Segm 8 such that A1: x = [I,{},<*mk,ml*>] ;
func x address_1 -> Element of SCM-Data-Loc means :Def7: :: SCMRING1:def 7
ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & it = f /. 1 );
existence
ex b<sub>1</sub> being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b₁ = f /. 1 )

proof end;

uniqueness
for b₁, b₂ being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b<sub>1</sub> = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b₂ = f /. 1 ) holds
b₁ = b₂ ;
func x address_2 -> Element of SCM-Data-Loc means :Def8: :: SCMRING1:def 8
ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & it = f /. 2 );
existence
ex b<sub>1</sub> being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b₁ = f /. 2 )

proof end;

uniqueness
for b₁, b₂ being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b<sub>1</sub> = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b₂ = f /. 2 ) holds
b₁ = b₂ ;

end;

:: deftheorem Def7 defines address_1 SCMRING1:def 7 :
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,{},<*mk,ml*>] holds
for b₃ being Element of SCM-Data-Loc holds
( b₃ = x address_1 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b₃ = f /. 1 ) );

:: deftheorem Def8 defines address_2 SCMRING1:def 8 :
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk, ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,{},<*mk,ml*>] holds
for b₃ being Element of SCM-Data-Loc holds
( b₃ = x address_2 iff ex f being FinSequence of SCM-Data-Loc st
( f = x `3_3 & b₃ = f /. 2 ) );

theorem :: SCMRING1:17

for I being Element of Segm 8
for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk, ml being Element of SCM-Data-Loc st x = [I,{},<*mk,ml*>] holds
( x address_1 = mk & x address_2 = ml )

proof end;

definition

let R be non empty 1-sorted ;
let x be Element of SCM-Instr R;
given mk being Element of NAT , I being Element of Segm 8 such that A1: x = [I,<*mk*>,{}] ;
func x jump_address -> Element of NAT means :Def9: :: SCMRING1:def 9
ex f being FinSequence of NAT st
( f = x `2_3 & it = f /. 1 );
existence
ex b<sub>1</sub> being Element of NAT ex f being FinSequence of NAT st
( f = x `2_3 & b₁ = f /. 1 )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ex f being FinSequence of NAT st
( f = x `2_3 & b<sub>1</sub> = f /. 1 ) & ex f being FinSequence of NAT st
( f = x `2_3 & b₂ = f /. 1 ) holds
b₁ = b₂ ;

end;

:: deftheorem Def9 defines jump_address SCMRING1:def 9 :
for R being non empty 1-sorted
for x being Element of SCM-Instr R st ex mk being Element of NAT ex I being Element of Segm 8 st x = [I,<*mk*>,{}] holds
for b₃ being Element of NAT holds
( b₃ = x jump_address iff ex f being FinSequence of NAT st
( f = x `2_3 & b₃ = f /. 1 ) );

theorem :: SCMRING1:18

for I being Element of Segm 8
for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk being Element of NAT st x = [I,<*mk*>,{}] holds
x jump_address = mk

proof end;

definition

let S be non empty 1-sorted ;
let x be Element of SCM-Instr S;
given mk being Element of NAT , ml being Element of SCM-Data-Loc , I being Element of Segm 8 such that A1: x = [I,<*mk*>,<*ml*>] ;
func x cjump_address -> Element of NAT means :Def10: :: SCMRING1:def 10
ex mk being Element of NAT st
( <*mk*> = x `2_3 & it = <*mk*> /. 1 );
existence
ex b<sub>1</sub>, mk being Element of NAT st
( <*mk*> = x `2_3 & b₁ = <*mk*> /. 1 )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ex mk being Element of NAT st
( <*mk*> = x `2_3 & b<sub>1</sub> = <*mk*> /. 1 ) & ex mk being Element of NAT st
( <*mk*> = x `2_3 & b₂ = <*mk*> /. 1 ) holds
b₁ = b₂ ;
func x cond_address -> Element of SCM-Data-Loc means :Def11: :: SCMRING1:def 11
ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & it = <*ml*> /. 1 );
existence
ex b<sub>1</sub>, ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b₁ = <*ml*> /. 1 )

proof end;

uniqueness
for b₁, b₂ being Element of SCM-Data-Loc st ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b<sub>1</sub> = <*ml*> /. 1 ) & ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b₂ = <*ml*> /. 1 ) holds
b₁ = b₂ ;

end;

:: deftheorem Def10 defines cjump_address SCMRING1:def 10 :
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,<*mk*>,<*ml*>] holds
for b₃ being Element of NAT holds
( b₃ = x cjump_address iff ex mk being Element of NAT st
( <*mk*> = x `2_3 & b₃ = <*mk*> /. 1 ) );

:: deftheorem Def11 defines cond_address SCMRING1:def 11 :
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of NAT ex ml being Element of SCM-Data-Loc ex I being Element of Segm 8 st x = [I,<*mk*>,<*ml*>] holds
for b₃ being Element of SCM-Data-Loc holds
( b₃ = x cond_address iff ex ml being Element of SCM-Data-Loc st
( <*ml*> = x `3_3 & b₃ = <*ml*> /. 1 ) );

theorem :: SCMRING1:19

for I being Element of Segm 8
for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk being Element of NAT
for ml being Element of SCM-Data-Loc st x = [I,<*mk*>,<*ml*>] holds
( x cjump_address = mk & x cond_address = ml )

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

proof end;

end;

definition

let S be non empty 1-sorted ;
let x be Element of SCM-Instr S;
given mk being Element of SCM-Data-Loc , r being Element of S, I being Element of Segm 8 such that A1: x = [I,{},<*mk,r*>] ;
func x const_address -> Element of SCM-Data-Loc means :Def12: :: SCMRING1:def 12
ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & it = f /. 1 );
existence
ex b<sub>1</sub> being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b₁ = f /. 1 )

proof end;

uniqueness
for b₁, b₂ being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b<sub>1</sub> = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b₂ = f /. 1 ) holds
b₁ = b₂ ;
func x const_value -> Element of S means :Def13: :: SCMRING1:def 13
ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & it = f /. 2 );
existence
ex b<sub>1</sub> being Element of S ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b₁ = f /. 2 )

proof end;

uniqueness
for b₁, b₂ being Element of S st ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b<sub>1</sub> = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b₂ = f /. 2 ) holds
b₁ = b₂ ;

end;

:: deftheorem Def12 defines const_address SCMRING1:def 12 :
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of SCM-Data-Loc ex r being Element of S ex I being Element of Segm 8 st x = [I,{},<*mk,r*>] holds
for b₃ being Element of SCM-Data-Loc holds
( b₃ = x const_address iff ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b₃ = f /. 1 ) );

:: deftheorem Def13 defines const_value SCMRING1:def 13 :
for S being non empty 1-sorted
for x being Element of SCM-Instr S st ex mk being Element of SCM-Data-Loc ex r being Element of S ex I being Element of Segm 8 st x = [I,{},<*mk,r*>] holds
for b₃ being Element of S holds
( b₃ = x const_value iff ex f being FinSequence of SCM-Data-Loc \/ the carrier of S st
( f = x `3_3 & b₃ = f /. 2 ) );

theorem :: SCMRING1:20

for I being Element of Segm 8
for S being non empty 1-sorted
for x being Element of SCM-Instr S
for mk being Element of SCM-Data-Loc
for r being Element of S st x = [I,{},<*mk,r*>] holds
( x const_address = mk & x const_value = r )

proof end;

definition

let R be good 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 b₁ 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) + (s . (x address_2))))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) - (s . (x address_2))))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) * (s . (x address_2))))),(succ (IC s))) iff b₁ = 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₁ = SCM-Chg (s,(x jump_address)) iff b₁ = 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₁ = SCM-Chg (s,(x jump_address)) iff b₁ = 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₁ = SCM-Chg (s,(IFEQ ((s . (x cond_address)),(0. R),(x cjump_address),(succ (IC s))))) iff b₁ = SCM-Chg ((SCM-Chg (s,(x const_address),(x const_value))),(succ (IC s))) ) ) ) by MCART_1:28;

end;

:: deftheorem defines SCM-Exec-Res SCMRING1:def 14 :
for R being good 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 ) );

registration

let S be non empty 1-sorted ;
let f be Action of (SCM-Instr S),(product (SCM-OK S));
let x be Element of SCM-Instr S;
cluster f . x -> Relation-like Function-like ;
coherence
( f . x is Function-like & f . x is Relation-like ) ;

end;

definition

let R be good Ring;
func SCM-Exec R -> Action of (SCM-Instr R),(product (SCM-OK R)) 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 b₁ being Action of (SCM-Instr R),(product (SCM-OK R)) st
for x being Element of SCM-Instr R
for y being SCM-State of R holds (b₁ . x) . y = SCM-Exec-Res (x,y)

proof end;

uniqueness
for b₁, b₂ being Action of (SCM-Instr R),(product (SCM-OK R)) st ( for x being Element of SCM-Instr R
for y being SCM-State of R holds (b₁ . x) . y = SCM-Exec-Res (x,y) ) & ( for x being Element of SCM-Instr R
for y being SCM-State of R holds (b₂ . x) . y = SCM-Exec-Res (x,y) ) holds
b₁ = b₂

proof end;

end;

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

theorem :: SCMRING1:21

for S being non empty 1-sorted holds SCM-Instr S c= [:NAT,(NAT *),(proj2 (SCM-Instr S)):]

proof end;

registration

let S be non empty 1-sorted ;
cluster proj2 (SCM-Instr S) -> FinSequence-membered ;
coherence
proj2 (SCM-Instr S) is FinSequence-membered

proof end;

end;

theorem :: SCMRING1:22

for S being non empty 1-sorted holds [0,{},{}] in SCM-Instr S

proof end;