set U1 = (union {INT }) \/ SCM-Memory ;
set UU = [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):];
A1:
SCM-Memory c= (union {INT }) \/ SCM-Memory
by XBOOLE_1:7;
A2:
{ [I1,<*d1,d2,k1,k2*>] where I1 is Element of Segm 14, d1, d2 is Element of SCM-Data-Loc , k1, k2 is Element of INT : I1 in {9,10,11,12,13} } c= [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { [I1,<*d1,d2,k1,k2*>] where I1 is Element of Segm 14, d1, d2 is Element of SCM-Data-Loc , k1, k2 is Element of INT : I1 in {9,10,11,12,13} } or x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):] )
assume
x in { [I1,<*d1,d2,k1,k2*>] where I1 is Element of Segm 14, d1, d2 is Element of SCM-Data-Loc , k1, k2 is Element of INT : I1 in {9,10,11,12,13} }
;
:: thesis: x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
then consider I1 being
Element of
Segm 14,
d1,
d2 being
Element of
SCM-Data-Loc ,
k1,
k2 being
Element of
INT such that A3:
x = [I1,<*d1,d2,k1,k2*>]
and
I1 in {9,10,11,12,13}
;
reconsider d1 =
d1,
d2 =
d2 as
Element of
(union {INT }) \/ SCM-Memory by A1, TARSKI:def 3;
reconsider k1 =
k1,
k2 =
k2 as
Element of
(union {INT }) \/ SCM-Memory by Th9;
<*d1,d2,k1,k2*> in ((union {INT }) \/ SCM-Memory ) *
by FINSEQ_1:def 11;
hence
x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by A3, ZFMISC_1:106;
:: thesis: verum
end;
A4:
{ [I2,<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } c= [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { [I2,<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } or x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):] )
assume
x in { [I2,<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} }
;
:: thesis: x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
then consider I2 being
Element of
Segm 14,
d3 being
Element of
SCM-Data-Loc ,
k3,
k4 being
Element of
INT such that A5:
x = [I2,<*d3,k3,k4*>]
and
I2 in {4,5,6,7,8}
;
reconsider d3 =
d3 as
Element of
(union {INT }) \/ SCM-Memory by A1, TARSKI:def 3;
reconsider k3 =
k3,
k4 =
k4 as
Element of
(union {INT }) \/ SCM-Memory by Th9;
<*d3,k3,k4*> in ((union {INT }) \/ SCM-Memory ) *
by FINSEQ_1:def 11;
hence
x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by A5, ZFMISC_1:106;
:: thesis: verum
end;
A6:
{ [0 ,<*k5*>] where k5 is Element of INT : verum } c= [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
A8:
{ [1,<*d4*>] where d4 is Element of SCM-Data-Loc : verum } c= [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
A10:
{ [I4,<*d5,r*>] where I4 is Element of Segm 14, d5 is Element of SCM-Data-Loc , r is Element of INT : I4 in {2,3} } c= [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { [I4,<*d5,r*>] where I4 is Element of Segm 14, d5 is Element of SCM-Data-Loc , r is Element of INT : I4 in {2,3} } or x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):] )
assume
x in { [I4,<*d5,r*>] where I4 is Element of Segm 14, d5 is Element of SCM-Data-Loc , r is Element of INT : I4 in {2,3} }
;
:: thesis: x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
then consider I4 being
Element of
Segm 14,
d5 being
Element of
SCM-Data-Loc ,
r being
Element of
INT such that A11:
x = [I4,<*d5,r*>]
and
I4 in {2,3}
;
reconsider d5 =
d5,
r =
r as
Element of
(union {INT }) \/ SCM-Memory by Th9, XBOOLE_0:def 3;
<*d5,r*> in ((union {INT }) \/ SCM-Memory ) *
by FINSEQ_1:def 11;
hence
x in [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by A11, ZFMISC_1:106;
:: thesis: verum
end;
set S1 = { [0 ,<*k5*>] where k5 is Element of INT : verum } ;
set S2 = { [1,<*d4*>] where d4 is Element of SCM-Data-Loc : verum } ;
set S3 = { [I4,<*d5,r*>] where I4 is Element of Segm 14, d5 is Element of SCM-Data-Loc , r is Element of INT : I4 in {2,3} } ;
{ [0 ,<*k5*>] where k5 is Element of INT : verum } \/ { [1,<*d4*>] where d4 is Element of SCM-Data-Loc : verum } c= [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by A6, A8, XBOOLE_1:8;
then
({ [0 ,<*k5*>] where k5 is Element of INT : verum } \/ { [1,<*d4*>] where d4 is Element of SCM-Data-Loc : verum } ) \/ { [I4,<*d5,r*>] where I4 is Element of Segm 14, d5 is Element of SCM-Data-Loc , r is Element of INT : I4 in {2,3} } c= [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by A10, XBOOLE_1:8;
then
(({ [0 ,<*k5*>] where k5 is Element of INT : verum } \/ { [1,<*d4*>] where d4 is Element of SCM-Data-Loc : verum } ) \/ { [I4,<*d5,r*>] where I4 is Element of Segm 14, d5 is Element of SCM-Data-Loc , r is Element of INT : I4 in {2,3} } ) \/ { [I2,<*d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I2 in {4,5,6,7,8} } c= [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by A4, XBOOLE_1:8;
hence
((({ [0 ,<*l*>] where l is Element of INT : verum } \/ { [1,<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,<*v,c*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,<*v,c1,c2*>] where I is Element of Segm 14, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) \/ { [I,<*v1,v2,c1,c2*>] where I is Element of Segm 14, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } is Subset of [:NAT ,(((union {INT }) \/ SCM-Memory ) * ):]
by A2, XBOOLE_1:8; :: thesis: verum