:: AMI_2 semantic presentation

begin


definition
func SCM-Memory  ->  set  equals :: AMI_2:def 1
{NAT} \/ SCM-Data-Loc;
coherence
 {NAT} \/ SCM-Data-Loc is set ;
end;

:: deftheorem  defines SCM-Memory AMI_2:def_1_:_
 SCM-Memory = {NAT} \/ SCM-Data-Loc;

registration
cluster SCM-Memory  ->  non empty ;
coherence
 not SCM-Memory is empty ;
end;

definition
:: original: SCM-Data-Loc
redefine func SCM-Data-Loc  ->  Subset of SCM-Memory;
coherence
 SCM-Data-Loc is Subset of SCM-Memory by XBOOLE_1:7;
end;


Lm1: now__::_thesis:_for_k_being_Element_of_SCM-Memory_holds_
(_k_=_NAT_or_k_in_SCM-Data-Loc_)
let k be Element of SCM-Memory ; ::_thesis: ( k = NAT or k in SCM-Data-Loc )
 ( k in {NAT} or k in SCM-Data-Loc ) by XBOOLE_0:def_3;
hence  ( k = NAT or k in SCM-Data-Loc ) by TARSKI:def_1; ::_thesis: verum
end;

Lm2:  not NAT in SCM-Data-Loc
proof
assume  NAT in SCM-Data-Loc ; ::_thesis: contradiction
then  ex x, y being set st NAT = [x,y] by RELAT_1:def_1;
hence  contradiction ; ::_thesis: verum
end;

definition
canceled;
canceled;
func SCM-OK  ->  Function of SCM-Memory,2 means :Def4: :: AMI_2:def 4
 for k being Element of SCM-Memory holds
( ( k = NAT implies it . k = 0 ) & ( k in SCM-Data-Loc implies it . k = 1 ) );
existence
 ex b1 being Function of SCM-Memory,2 st
for k being Element of SCM-Memory holds
( ( k = NAT implies b1 . k = 0 ) & ( k in SCM-Data-Loc implies b1 . k = 1 ) )
proof
defpred S1[ set , set ] means ( ( $1 = NAT & $2 = 0 ) or ( $1 in SCM-Data-Loc & $2 = 1 ) );
A1: now__::_thesis:_for_k_being_Element_of_SCM-Memory_ex_b_being_Element_of_2_st_S1[k,b]
let k be Element of SCM-Memory ; ::_thesis: ex b being Element of 2 st S1[k,b]
A2: {0} \/ {1} = {0,1} by ENUMSET1:1;
then A3: 0 in {1} \/ {0} by TARSKI:def_2;
A4: ( S1[k, 0 ] or S1[k,1] ) by Lm1;
 1 in {1} \/ {0} by A2, TARSKI:def_2;
hence  ex b being Element of 2 st S1[k,b] by A2, A3, A4, CARD_1:50; ::_thesis: verum
end;
consider h being Function of SCM-Memory,2 such that
A5: for a being Element of SCM-Memory holds S1[a,h . a] from FUNCT_2:sch_3(A1);
take  h ; ::_thesis: for k being Element of SCM-Memory holds
( ( k = NAT implies h . k = 0 ) & ( k in SCM-Data-Loc implies h . k = 1 ) )
let k be Element of SCM-Memory ; ::_thesis: ( ( k = NAT implies h . k = 0 ) & ( k in SCM-Data-Loc implies h . k = 1 ) )
thus  ( k = NAT implies h . k = 0 ) by A5, Lm2; ::_thesis: ( k in SCM-Data-Loc implies h . k = 1 )
thus  ( k in SCM-Data-Loc implies h . k = 1 ) by A5, Lm2; ::_thesis: verum
thus  verum ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of SCM-Memory,2 st ( for k being Element of SCM-Memory holds
( ( k = NAT implies b1 . k = 0 ) & ( k in SCM-Data-Loc implies b1 . k = 1 ) ) ) & ( for k being Element of SCM-Memory holds
( ( k = NAT implies b2 . k = 0 ) & ( k in SCM-Data-Loc implies b2 . k = 1 ) ) ) holds
b1 = b2
proof
let f, g be Function of SCM-Memory,2; ::_thesis: ( ( for k being Element of SCM-Memory holds
( ( k = NAT implies f . k = 0 ) & ( k in SCM-Data-Loc implies f . k = 1 ) ) ) & ( for k being Element of SCM-Memory holds
( ( k = NAT implies g . k = 0 ) & ( k in SCM-Data-Loc implies g . k = 1 ) ) ) implies f = g )
assume that
A6: for k being Element of SCM-Memory holds
( ( k = NAT implies f . k = 0 ) & ( k in SCM-Data-Loc implies f . k = 1 ) ) and
A7: for k being Element of SCM-Memory holds
( ( k = NAT implies g . k = 0 ) & ( k in SCM-Data-Loc implies g . k = 1 ) ) ; ::_thesis: f = g
now__::_thesis:_for_k_being_Element_of_SCM-Memory_holds_f_._k_=_g_._k
let k be Element of SCM-Memory ; ::_thesis: f . k = g . k
now__::_thesis:_f_._k_=_g_._k
percases ( k = NAT or k in SCM-Data-Loc ) by Lm1;
supposeA8: k = NAT ; ::_thesis: f . k = g . k
hence f . k = 0 by A6
.= g . k by A7, A8 ;
::_thesis: verum
end;
supposeA9: k in SCM-Data-Loc ; ::_thesis: f . k = g . k
hence f . k = 1 by A6
.= g . k by A7, A9 ;
::_thesis: verum
end;
end;
end;
hence  f . k = g . k ; ::_thesis: verum
end;
hence  f = g by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem  AMI_2:def_2_:_
canceled;

:: deftheorem  AMI_2:def_3_:_
canceled;

:: deftheorem Def4 defines SCM-OK AMI_2:def_4_:_
 for b1 being Function of SCM-Memory,2 holds
( b1 = SCM-OK iff for k being Element of SCM-Memory holds
( ( k = NAT implies b1 . k = 0 ) & ( k in SCM-Data-Loc implies b1 . k = 1 ) ) );

theorem :: AMI_2:1
canceled;

definition
func SCM-VAL  ->  ManySortedSet of 2 equals :: AMI_2:def 5
<%NAT,INT%>;
coherence
 <%NAT,INT%> is ManySortedSet of 2 ;
end;

:: deftheorem  defines SCM-VAL AMI_2:def_5_:_
 SCM-VAL = <%NAT,INT%>;

Lm3:  NAT in SCM-Memory
proof
 NAT in {NAT} by TARSKI:def_1;
hence  NAT in SCM-Memory by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: AMI_2:2
canceled;

theorem :: AMI_2:3
canceled;

theorem :: AMI_2:4
canceled;

theorem :: AMI_2:5
canceled;

theorem Th6: :: AMI_2:6
(SCM-VAL * SCM-OK) . NAT = NAT
proof
 NAT in dom SCM-OK by Lm3, PARTFUN1:def_2;
then A1: (SCM-VAL * SCM-OK) . NAT = SCM-VAL . (SCM-OK . NAT) by FUNCT_1:13;
 (SCM-VAL * SCM-OK) . NAT = SCM-VAL . 0 by A1, Def4, Lm3;
hence  (SCM-VAL * SCM-OK) . NAT = NAT by AFINSQ_1:38; ::_thesis: verum
end;

theorem Th7: :: AMI_2:7
for i being Element of SCM-Memory st i in SCM-Data-Loc holds
(SCM-VAL * SCM-OK) . i = INT
proof
let i be Element of SCM-Memory ; ::_thesis: ( i in SCM-Data-Loc implies (SCM-VAL * SCM-OK) . i = INT )
 i in SCM-Memory ;
then  i in dom SCM-OK by PARTFUN1:def_2;
then A1: (SCM-VAL * SCM-OK) . i = SCM-VAL . (SCM-OK . i) by FUNCT_1:13;
assume  i in SCM-Data-Loc ; ::_thesis: (SCM-VAL * SCM-OK) . i = INT
then  (SCM-VAL * SCM-OK) . i = SCM-VAL . 1 by A1, Def4;
hence  (SCM-VAL * SCM-OK) . i = INT by AFINSQ_1:38; ::_thesis: verum
end;

Lm4:  dom SCM-OK = SCM-Memory
by PARTFUN1:def_2;

 len <%NAT,INT%> = 2
by AFINSQ_1:38;

then  rng SCM-OK c= dom SCM-VAL
by RELAT_1:def_19;

then Lm5:  dom (SCM-VAL * SCM-OK) = SCM-Memory
by Lm4, RELAT_1:27;

registration
clusterSCM-OK * SCM-VAL ->  non-empty ;
coherence
 SCM-VAL * SCM-OK is non-empty
proof
set F = SCM-VAL * SCM-OK;
let n be set ; :: according to FUNCT_1:def_9 ::_thesis: ( not n in proj1 (SCM-VAL * SCM-OK) or not (SCM-VAL * SCM-OK) . n is empty )
assume A1: n in dom (SCM-VAL * SCM-OK) ; ::_thesis: not (SCM-VAL * SCM-OK) . n is empty
percases ( n = NAT or n in SCM-Data-Loc ) by A1, Lm1, Lm5;
suppose n = NAT ; ::_thesis: not (SCM-VAL * SCM-OK) . n is empty
hence  not (SCM-VAL * SCM-OK) . n is empty by Th6; ::_thesis: verum
end;
suppose n in SCM-Data-Loc ; ::_thesis: not (SCM-VAL * SCM-OK) . n is empty
hence  not (SCM-VAL * SCM-OK) . n is empty by Th7; ::_thesis: verum
end;
end;
end;
end;

definition
mode SCM-State is Element of product (SCM-VAL * SCM-OK);
end;

theorem :: AMI_2:8
for a being Element of SCM-Data-Loc holds (SCM-VAL * SCM-OK) . a = INT by Th7;

theorem Th9: :: AMI_2:9
pi ((product (SCM-VAL * SCM-OK)),NAT) = NAT by Th6, Lm5, Lm3, CARD_3:12;

theorem Th10: :: AMI_2:10
for a being Element of SCM-Data-Loc holds pi ((product (SCM-VAL * SCM-OK)),a) = INT
proof
let a be Element of SCM-Data-Loc ; ::_thesis: pi ((product (SCM-VAL * SCM-OK)),a) = INT
thus  pi ((product (SCM-VAL * SCM-OK)),a) = (SCM-VAL * SCM-OK) . a by Lm5, CARD_3:12
.= INT by Th7 ; ::_thesis: verum
end;

definition
let s be SCM-State;
func IC s ->  Element of NAT  equals :: AMI_2:def 6
s . NAT;
coherence
 s . NAT is Element of NAT by Th9, CARD_3:def_6;
end;

:: deftheorem  defines IC AMI_2:def_6_:_
 for s being SCM-State holds IC s = s . NAT;

definition
let s be SCM-State;
let u be Nat;
func SCM-Chg (s,u) ->  SCM-State equals :: AMI_2:def 7
s +* (NAT .--> u);
coherence
 s +* (NAT .--> u) is SCM-State
proof
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_(SCM-VAL_*_SCM-OK)_holds_
(s_+*_(NAT_.-->_u))_._x_in_(SCM-VAL_*_SCM-OK)_._x
let x be set ; ::_thesis: ( x in dom (SCM-VAL * SCM-OK) implies (s +* (NAT .--> u)) . b1 in (SCM-VAL * SCM-OK) . b1 )
assume A2: x in dom (SCM-VAL * SCM-OK) ; ::_thesis: (s +* (NAT .--> u)) . b1 in (SCM-VAL * SCM-OK) . b1
percases ( x = NAT or x <> NAT ) ;
supposeA3: x = NAT ; ::_thesis: (s +* (NAT .--> u)) . b1 in (SCM-VAL * 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 ;
hence  (s +* (NAT .--> u)) . x in (SCM-VAL * SCM-OK) . x by A3, Th6, ORDINAL1:def_12; ::_thesis: verum
end;
supposeA4: x <> NAT ; ::_thesis: (s +* (NAT .--> u)) . b1 in (SCM-VAL * 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 * SCM-OK) . x by A2, CARD_3:9; ::_thesis: verum
end;
end;
end;
 dom s = SCM-Memory by Lm5, 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 * SCM-OK) by Lm5, Lm3, ZFMISC_1:40 ;
hence  s +* (NAT .--> u) is SCM-State by A1, CARD_3:9; ::_thesis: verum
end;
end;

:: deftheorem  defines SCM-Chg AMI_2:def_7_:_
 for s being SCM-State
for u being Nat holds SCM-Chg (s,u) = s +* (NAT .--> u);

theorem :: AMI_2:11
for s being SCM-State
for u being Nat holds (SCM-Chg (s,u)) . NAT = u
proof
let s be SCM-State; ::_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 :: AMI_2:12
for s being SCM-State
for u being Nat
for mk being Element of SCM-Data-Loc holds (SCM-Chg (s,u)) . mk = s . mk
proof
let s be SCM-State; ::_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;
 ( (SCM-VAL * SCM-OK) . NAT = NAT & (SCM-VAL * SCM-OK) . mk = INT ) by Th6, Th7;
then  not mk in dom (NAT .--> u) by A1, NUMBERS:27, TARSKI:def_1;
hence  (SCM-Chg (s,u)) . mk = s . mk by FUNCT_4:11; ::_thesis: verum
end;

theorem :: AMI_2:13
for s being SCM-State
for u, v being Nat holds (SCM-Chg (s,u)) . v = s . v
proof
let s be SCM-State; ::_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 s be SCM-State;
let t be Element of SCM-Data-Loc ;
let u be Integer;
func SCM-Chg (s,t,u) ->  SCM-State equals :: AMI_2:def 8
s +* (t .--> u);
coherence
 s +* (t .--> u) is SCM-State
proof
A1: now__::_thesis:_for_x_being_set_st_x_in_dom_(SCM-VAL_*_SCM-OK)_holds_
(s_+*_(t_.-->_u))_._x_in_(SCM-VAL_*_SCM-OK)_._x
let x be set ; ::_thesis: ( x in dom (SCM-VAL * SCM-OK) implies (s +* (t .--> u)) . b1 in (SCM-VAL * SCM-OK) . b1 )
assume A2: x in dom (SCM-VAL * SCM-OK) ; ::_thesis: (s +* (t .--> u)) . b1 in (SCM-VAL * SCM-OK) . b1
percases ( x = t or x <> t ) ;
supposeA3: x = t ; ::_thesis: (s +* (t .--> u)) . b1 in (SCM-VAL * 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 INT by INT_1:def_2;
hence  (s +* (t .--> u)) . x in (SCM-VAL * SCM-OK) . x by A3, Th7; ::_thesis: verum
end;
supposeA4: x <> t ; ::_thesis: (s +* (t .--> u)) . b1 in (SCM-VAL * 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 * SCM-OK) . x by A2, CARD_3:9; ::_thesis: verum
end;
end;
end;
 dom s = SCM-Memory by Lm5, 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 * SCM-OK) by Lm5, ZFMISC_1:40 ;
hence  s +* (t .--> u) is SCM-State by A1, CARD_3:9; ::_thesis: verum
end;
end;

:: deftheorem  defines SCM-Chg AMI_2:def_8_:_
 for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer holds SCM-Chg (s,t,u) = s +* (t .--> u);

theorem :: AMI_2:14
for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer holds (SCM-Chg (s,t,u)) . NAT = s . NAT
proof
let s be SCM-State; ::_thesis: for t being Element of SCM-Data-Loc
for u being Integer holds (SCM-Chg (s,t,u)) . NAT = s . NAT
let t be Element of SCM-Data-Loc ; ::_thesis: for u being Integer holds (SCM-Chg (s,t,u)) . NAT = s . NAT
let u be Integer; ::_thesis: (SCM-Chg (s,t,u)) . NAT = s . NAT
A1: {t} = dom (t .--> u) by FUNCOP_1:13;
 ( (SCM-VAL * SCM-OK) . NAT = NAT & (SCM-VAL * SCM-OK) . t = INT ) by Th6, Th7;
then  not NAT in dom (t .--> u) by A1, NUMBERS:27, TARSKI:def_1;
hence  (SCM-Chg (s,t,u)) . NAT = s . NAT by FUNCT_4:11; ::_thesis: verum
end;

theorem :: AMI_2:15
for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer holds (SCM-Chg (s,t,u)) . t = u
proof
let s be SCM-State; ::_thesis: for t being Element of SCM-Data-Loc
for u being Integer holds (SCM-Chg (s,t,u)) . t = u
let t be Element of SCM-Data-Loc ; ::_thesis: for u being Integer holds (SCM-Chg (s,t,u)) . t = u
let u be Integer; ::_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 :: AMI_2:16
for s being SCM-State
for t being Element of SCM-Data-Loc
for u being Integer
for mk being Element of SCM-Data-Loc st mk <> t holds
(SCM-Chg (s,t,u)) . mk = s . mk
proof
let s be SCM-State; ::_thesis: for t being Element of SCM-Data-Loc
for u being Integer
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 Integer
for mk being Element of SCM-Data-Loc st mk <> t holds
(SCM-Chg (s,t,u)) . mk = s . mk
let u be Integer; ::_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;

registration
let s be SCM-State;
let a be Element of SCM-Data-Loc ;
clusters . a ->  integer ;
coherence
 s . a is integer
proof
 s . a in pi ((product (SCM-VAL * SCM-OK)),a) by CARD_3:def_6;
then  s . a in INT by Th10;
hence  s . a is integer ; ::_thesis: verum
end;
end;

definition
canceled;
canceled;
canceled;
canceled;
canceled;
let x be Element of SCM-Instr ;
let s be SCM-State;
func SCM-Exec-Res (x,s) ->  SCM-State equals :: AMI_2: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 ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(succ (IC s))) if  ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*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,(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 (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) if  ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>]
otherwise s;
consistency
 for b1 being SCM-State 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, ml being Element of SCM-Data-Loc st x = [5,{},<*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 ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (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,(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 NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b1 = SCM-Chg ((SCM-Chg (s,(x address_1),(s . (x address_2)))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(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, ml being Element of SCM-Data-Loc st x = [5,{},<*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 ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (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,(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 NAT ex ml being Element of SCM-Data-Loc st x = [8,<*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,(IFGT ((s . (x cond_address)),0,(x cjump_address),(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, ml being Element of SCM-Data-Loc st x = [5,{},<*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 ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (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,(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 NAT ex ml being Element of SCM-Data-Loc st x = [8,<*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,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [4,{},<*mk,ml*>] & ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*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 ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(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,(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 NAT ex ml being Element of SCM-Data-Loc st x = [8,<*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,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] & ex mk being Element of NAT st x = [6,<*mk*>,{}] implies ( b1 = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (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 = [5,{},<*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 ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] & ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b1 = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(succ (IC s))) iff b1 = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(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,(x cjump_address),(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 = [8,<*mk*>,<*ml*>] implies ( b1 = SCM-Chg (s,(x jump_address)) iff b1 = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(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 NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies ( b1 = SCM-Chg (s,(IFEQ ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) iff b1 = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) ) ) ) by XTUPLE_0:3;
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 ) & ( 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 ) & ( 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 ) & ( 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 ) & ( ex mk, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] implies SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (s . (x address_2))))),(succ (IC s))) is SCM-State ) & ( ex mk being Element of NAT st x = [6,<*mk*>,{}] implies SCM-Chg (s,(x jump_address)) is SCM-State ) & ( 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,(x cjump_address),(succ (IC s))))) is SCM-State ) & ( ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(succ (IC s))))) is SCM-State ) & ( ( 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, ml being Element of SCM-Data-Loc holds not x = [5,{},<*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 NAT
for ml being Element of SCM-Data-Loc holds not x = [8,<*mk*>,<*ml*>] ) implies s is SCM-State ) ) ;
end;

:: deftheorem  AMI_2:def_9_:_
canceled;

:: deftheorem  AMI_2:def_10_:_
canceled;

:: deftheorem  AMI_2:def_11_:_
canceled;

:: deftheorem  AMI_2:def_12_:_
canceled;

:: deftheorem  AMI_2:def_13_:_
canceled;

:: deftheorem  defines SCM-Exec-Res AMI_2:def_14_:_
 for x being Element of SCM-Instr
for s being SCM-State 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, ml being Element of SCM-Data-Loc st x = [5,{},<*mk,ml*>] implies SCM-Exec-Res (x,s) = SCM-Chg ((SCM-Chg ((SCM-Chg (s,(x address_1),((s . (x address_1)) div (s . (x address_2))))),(x address_2),((s . (x address_1)) mod (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,(x cjump_address),(succ (IC s))))) ) & ( ex mk being Element of NAT ex ml being Element of SCM-Data-Loc st x = [8,<*mk*>,<*ml*>] implies SCM-Exec-Res (x,s) = SCM-Chg (s,(IFGT ((s . (x cond_address)),0,(x cjump_address),(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, ml being Element of SCM-Data-Loc holds not x = [5,{},<*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 NAT
for ml being Element of SCM-Data-Loc holds not x = [8,<*mk*>,<*ml*>] ) implies SCM-Exec-Res (x,s) = s ) );

definition
func SCM-Exec  ->  Action of SCM-Instr,(product (SCM-VAL * SCM-OK)) means :: AMI_2:def 15
 for x being Element of SCM-Instr
for y being SCM-State holds (it . x) . y = SCM-Exec-Res (x,y);
existence
 ex b1 being Action of SCM-Instr,(product (SCM-VAL * SCM-OK)) st
for x being Element of SCM-Instr
for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res (x,y)
proof
consider f being Function of [:SCM-Instr,(product (SCM-VAL * SCM-OK)):],(product (SCM-VAL * SCM-OK)) such that
A1: for x being Element of SCM-Instr
for y being SCM-State holds f . (x,y) = SCM-Exec-Res (x,y) from BINOP_1:sch_4();
take  curry f ; ::_thesis: for x being Element of SCM-Instr
for y being SCM-State holds ((curry f) . x) . y = SCM-Exec-Res (x,y)
let x be Element of SCM-Instr ; ::_thesis: for y being SCM-State holds ((curry f) . x) . y = SCM-Exec-Res (x,y)
let y be SCM-State; ::_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,(product (SCM-VAL * SCM-OK)) st ( for x being Element of SCM-Instr
for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res (x,y) ) & ( for x being Element of SCM-Instr
for y being SCM-State holds (b2 . x) . y = SCM-Exec-Res (x,y) ) holds
b1 = b2
proof
let f, g be Action of SCM-Instr,(product (SCM-VAL * SCM-OK)); ::_thesis: ( ( for x being Element of SCM-Instr
for y being SCM-State holds (f . x) . y = SCM-Exec-Res (x,y) ) & ( for x being Element of SCM-Instr
for y being SCM-State holds (g . x) . y = SCM-Exec-Res (x,y) ) implies f = g )
assume that
A2: for x being Element of SCM-Instr
for y being SCM-State holds (f . x) . y = SCM-Exec-Res (x,y) and
A3: for x being Element of SCM-Instr
for y being SCM-State holds (g . x) . y = SCM-Exec-Res (x,y) ; ::_thesis: f = g
now__::_thesis:_for_x_being_Element_of_SCM-Instr_holds_f_._x_=_g_._x
let x be Element of SCM-Instr ; ::_thesis: f . x = g . x
reconsider gx = g . x, fx = f . x as Function of (product (SCM-VAL * SCM-OK)),(product (SCM-VAL * SCM-OK)) by FUNCT_2:66;
now__::_thesis:_for_y_being_SCM-State_holds_fx_._y_=_gx_._y
let y be SCM-State; ::_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 AMI_2:def_15_:_
 for b1 being Action of SCM-Instr,(product (SCM-VAL * SCM-OK)) holds
( b1 = SCM-Exec iff for x being Element of SCM-Instr
for y being SCM-State holds (b1 . x) . y = SCM-Exec-Res (x,y) );

begin

theorem :: AMI_2:17
canceled;

theorem :: AMI_2:18
canceled;

theorem :: AMI_2:19
canceled;

theorem :: AMI_2:20
not NAT in SCM-Data-Loc by Lm2;

theorem :: AMI_2:21
canceled;

theorem :: AMI_2:22
NAT in SCM-Memory by Lm3;

theorem :: AMI_2:23
for x being set st x in SCM-Data-Loc holds
ex k being Element of NAT st x = [1,k]
proof
let x be set ; ::_thesis: ( x in SCM-Data-Loc implies ex k being Element of NAT st x = [1,k] )
assume  x in SCM-Data-Loc ; ::_thesis: ex k being Element of NAT st x = [1,k]
then consider y, z being set  such that
A1: y in {1} and
A2: z in NAT and
A3: x = [y,z] by ZFMISC_1:84;
reconsider k = z as Element of NAT by A2;
take  k ; ::_thesis: x = [1,k]
thus  x = [1,k] by A1, A3, TARSKI:def_1; ::_thesis: verum
end;

theorem :: AMI_2:24
for k being Nat holds [1,k] in SCM-Data-Loc
proof
let k be Nat; ::_thesis: [1,k] in SCM-Data-Loc
 ( 1 in {1} & k in NAT ) by ORDINAL1:def_12, TARSKI:def_1;
hence  [1,k] in SCM-Data-Loc by ZFMISC_1:87; ::_thesis: verum
end;

theorem :: AMI_2:25
canceled;

theorem :: AMI_2:26
for k being Element of SCM-Memory holds
( k = NAT or k in SCM-Data-Loc ) by Lm1;

theorem :: AMI_2:27
dom (SCM-VAL * SCM-OK) = SCM-Memory by Lm5;

theorem :: AMI_2:28
for s being SCM-State holds dom s = SCM-Memory by Lm5, CARD_3:9;

definition
let x be set ;
attrx is Int-like  means :: AMI_2:def 16
x in SCM-Data-Loc ;
end;

:: deftheorem  defines Int-like AMI_2:def_16_:_
 for x being set holds
( x is Int-like iff x in SCM-Data-Loc );