set S1 = {(IC )};

set S2 = SCM-Data-Loc ;

set S3 = NAT ;

defpred S_{1}[ object , object ] means ex m being Nat st

( ( $1 = IC & $2 = F_{2}() ) or ( $1 = DataLoc (m,0) & $2 = F_{1}(m) ) );

A1: for e being object st e in the carrier of SCMPDS holds

ex u being object st S_{1}[e,u]

A6: dom f = the carrier of SCMPDS and

A7: for e being object st e in the carrier of SCMPDS holds

S_{1}[e,f . e]
from CLASSES1:sch 1(A1);

A8: dom the Object-Kind of SCMPDS = the carrier of SCMPDS by FUNCT_2:def 1;

consider m being Nat such that

A13: ( ( IC = IC & f . (IC ) = F_{2}() ) or ( IC = DataLoc (m,0) & f . (IC ) = F_{1}(m) ) )
by A7;

take f ; :: thesis: ( IC f = F_{2}() & ( for i being Nat holds f . (DataLoc (i,0)) = F_{1}(i) ) )

thus IC f = F_{2}()
by A13, SCMPDS_2:43; :: thesis: for i being Nat holds f . (DataLoc (i,0)) = F_{1}(i)

let i be Nat; :: thesis: f . (DataLoc (i,0)) = F_{1}(i)

ex m being Nat st

( ( DataLoc (i,0) = IC & f . (DataLoc (i,0)) = F_{2}() ) or ( DataLoc (i,0) = DataLoc (m,0) & f . (DataLoc (i,0)) = F_{1}(m) ) )
by A7;

hence f . (DataLoc (i,0)) = F_{1}(i)
by Th3, SCMPDS_2:43; :: thesis: verum

set S2 = SCM-Data-Loc ;

set S3 = NAT ;

defpred S

( ( $1 = IC & $2 = F

A1: for e being object st e in the carrier of SCMPDS holds

ex u being object st S

proof

consider f being Function such that
let e be object ; :: thesis: ( e in the carrier of SCMPDS implies ex u being object st S_{1}[e,u] )

assume e in the carrier of SCMPDS ; :: thesis: ex u being object st S_{1}[e,u]

then A2: e in {(IC )} \/ SCM-Data-Loc by SCMPDS_2:84, STRUCT_0:4;

A3: ( e = IC or e = DataLoc (m,0) ) ;

end;assume e in the carrier of SCMPDS ; :: thesis: ex u being object st S

then A2: e in {(IC )} \/ SCM-Data-Loc by SCMPDS_2:84, STRUCT_0:4;

now :: thesis: ( ( e in {(IC )} & e = IC ) or ( e in SCM-Data-Loc & ex m being Nat st e = DataLoc (m,0) ) )end;

then consider m being Nat such that per cases
( e in {(IC )} or e in SCM-Data-Loc )
by A2, XBOOLE_0:def 3;

end;

case
e in SCM-Data-Loc
; :: thesis: ex m being Nat st e = DataLoc (m,0)

then
e is Int_position
by AMI_2:def 16;

hence ex m being Nat st e = DataLoc (m,0) by Th4; :: thesis: verum

end;hence ex m being Nat st e = DataLoc (m,0) by Th4; :: thesis: verum

A3: ( e = IC or e = DataLoc (m,0) ) ;

A6: dom f = the carrier of SCMPDS and

A7: for e being object st e in the carrier of SCMPDS holds

S

A8: dom the Object-Kind of SCMPDS = the carrier of SCMPDS by FUNCT_2:def 1;

now :: thesis: for x being object st x in dom the Object-Kind of SCMPDS holds

f . x in (the_Values_of SCMPDS) . x

then reconsider f = f as State of SCMPDS by A6, A8, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;f . x in (the_Values_of SCMPDS) . x

let x be object ; :: thesis: ( x in dom the Object-Kind of SCMPDS implies f . b_{1} in (the_Values_of SCMPDS) . b_{1} )

assume A9: x in dom the Object-Kind of SCMPDS ; :: thesis: f . b_{1} in (the_Values_of SCMPDS) . b_{1}

then A10: x in {(IC )} \/ SCM-Data-Loc by A8, SCMPDS_2:84, STRUCT_0:4;

consider m being Nat such that

A11: ( ( x = IC & f . x = F_{2}() ) or ( x = DataLoc (m,0) & f . x = F_{1}(m) ) )
by A7, A8, A9;

end;assume A9: x in dom the Object-Kind of SCMPDS ; :: thesis: f . b

then A10: x in {(IC )} \/ SCM-Data-Loc by A8, SCMPDS_2:84, STRUCT_0:4;

consider m being Nat such that

A11: ( ( x = IC & f . x = F

per cases
( x in SCM-Data-Loc or x in {(IC )} )
by A10, XBOOLE_0:def 3;

end;

suppose
x in SCM-Data-Loc
; :: thesis: f . b_{1} in (the_Values_of SCMPDS) . b_{1}

then
x is Int_position
by AMI_2:def 16;

then (the_Values_of SCMPDS) . x = Values (DataLoc (m,0)) by A11, SCMPDS_2:43

.= INT by SCMPDS_2:5 ;

hence f . x in (the_Values_of SCMPDS) . x by A11, INT_1:def 2; :: thesis: verum

end;then (the_Values_of SCMPDS) . x = Values (DataLoc (m,0)) by A11, SCMPDS_2:43

.= INT by SCMPDS_2:5 ;

hence f . x in (the_Values_of SCMPDS) . x by A11, INT_1:def 2; :: thesis: verum

suppose A12:
x in {(IC )}
; :: thesis: f . b_{1} in (the_Values_of SCMPDS) . b_{1}

(the_Values_of SCMPDS) . x =
Values (IC )
by TARSKI:def 1, A12

.= NAT by MEMSTR_0:def 6 ;

hence f . x in (the_Values_of SCMPDS) . x by A11, A12, SCMPDS_2:2, TARSKI:def 1; :: thesis: verum

end;.= NAT by MEMSTR_0:def 6 ;

hence f . x in (the_Values_of SCMPDS) . x by A11, A12, SCMPDS_2:2, TARSKI:def 1; :: thesis: verum

consider m being Nat such that

A13: ( ( IC = IC & f . (IC ) = F

take f ; :: thesis: ( IC f = F

thus IC f = F

let i be Nat; :: thesis: f . (DataLoc (i,0)) = F

ex m being Nat st

( ( DataLoc (i,0) = IC & f . (DataLoc (i,0)) = F

hence f . (DataLoc (i,0)) = F