let N be with_zero set ; for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for k being Nat
for p being PartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let S be non empty with_non-empty_values IC-Ins-separated Mem-Struct over N; for k being Nat
for p being PartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let k be Nat; for p being PartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let p be PartState of S; for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
p c= s1 +* (DataPart s2)
let s1, s2 be State of S; ( p c= s1 & IncIC (p,k) c= s2 implies p c= s1 +* (DataPart s2) )
assume that
A1:
p c= s1
and
A2:
IncIC (p,k) c= s2
; p c= s1 +* (DataPart s2)
set s3 = DataPart s2;
reconsider s = s1 +* (DataPart s2) as State of S ;
A3:
dom p c= the carrier of S
by RELAT_1:def 18;
then A4:
dom p c= {(IC )} \/ (Data-Locations )
by STRUCT_0:4;
A5:
now for x being object st x in dom p holds
p . x = s . x
Data-Locations = (dom s2) /\ (Data-Locations )
by Th8, XBOOLE_1:28;
then A6:
dom (DataPart s2) = Data-Locations
by RELAT_1:61;
let x be
object ;
( x in dom p implies p . b1 = s . b1 )assume A7:
x in dom p
;
p . b1 = s . b1per cases
( x in {(IC )} or x in Data-Locations )
by A4, A7, XBOOLE_0:def 3;
suppose A9:
x in Data-Locations
;
p . b1 = s . b1set DPp =
DataPart p;
x in (dom p) /\ (Data-Locations )
by A9, A7, XBOOLE_0:def 4;
then A10:
x in dom (DataPart p)
by RELAT_1:61;
A11:
DataPart (IncIC (p,k)) = DataPart p
by Th51;
DataPart p c= IncIC (
p,
k)
by A11, RELAT_1:59;
then A12:
DataPart p c= s2
by A2, XBOOLE_1:1;
then
dom (DataPart p) c= dom s2
by GRFUNC_1:2;
then
x in (dom s2) /\ (Data-Locations )
by A9, A10, XBOOLE_0:def 4;
then A13:
x in dom (DataPart s2)
by RELAT_1:61;
DataPart p c= p
by RELAT_1:59;
then A14:
(DataPart p) . x = p . x
by A10, GRFUNC_1:2;
A15:
s2 . x = (DataPart s2) . x
by A9, FUNCT_1:49;
(DataPart p) . x = s2 . x
by A10, A12, GRFUNC_1:2;
hence
p . x = s . x
by A14, A15, A13, FUNCT_4:13;
verum end; end; end;
dom p c= dom s
by A3, PARTFUN1:def 2;
hence
p c= s1 +* (DataPart s2)
by A5, GRFUNC_1:2; verum