let XP1, XP2 be strict Colored-PT-net; :: thesis: ( ex P, T, ST, TS, CS, F being ManySortedSet of I ex UF, UQ being Function st
( ( for i being Element of I holds
( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) & F . i = the firing-rule of (CPNT . i) ) ) & UF = union (rng F) & UQ = union (rng q) & the carrier of XP1 = union (rng P) & the carrier' of XP1 = union (rng T) & the S-T_Arcs of XP1 = union (rng ST) & the T-S_Arcs of XP1 = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of XP1 = union (rng CS) & the firing-rule of XP1 = UF +* UQ ) & ex P, T, ST, TS, CS, F being ManySortedSet of I ex UF, UQ being Function st
( ( for i being Element of I holds
( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) & F . i = the firing-rule of (CPNT . i) ) ) & UF = union (rng F) & UQ = union (rng q) & the carrier of XP2 = union (rng P) & the carrier' of XP2 = union (rng T) & the S-T_Arcs of XP2 = union (rng ST) & the T-S_Arcs of XP2 = (union (rng TS)) \/ (union (rng O)) & the ColoredSet of XP2 = union (rng CS) & the firing-rule of XP2 = UF +* UQ ) implies XP1 = XP2 )
assume AS1: ex P1, T1, ST1, TS1, CS1, F1 being ManySortedSet of I ex UF1, UQ1 being Function st
( ( for i being Element of I holds
( P1 . i = the carrier of (CPNT . i) & T1 . i = the carrier' of (CPNT . i) & ST1 . i = the S-T_Arcs of (CPNT . i) & TS1 . i = the T-S_Arcs of (CPNT . i) & CS1 . i = the ColoredSet of (CPNT . i) & F1 . i = the firing-rule of (CPNT . i) ) ) & UF1 = union (rng F1) & UQ1 = union (rng q) & the carrier of XP1 = union (rng P1) & the carrier' of XP1 = union (rng T1) & the S-T_Arcs of XP1 = union (rng ST1) & the T-S_Arcs of XP1 = (union (rng TS1)) \/ (union (rng O)) & the ColoredSet of XP1 = union (rng CS1) & the firing-rule of XP1 = UF1 +* UQ1 ) ; :: thesis: ( for P, T, ST, TS, CS, F being ManySortedSet of I
for UF, UQ being Function holds
( ex i being Element of I st
( P . i = the carrier of (CPNT . i) & T . i = the carrier' of (CPNT . i) & ST . i = the S-T_Arcs of (CPNT . i) & TS . i = the T-S_Arcs of (CPNT . i) & CS . i = the ColoredSet of (CPNT . i) implies not F . i = the firing-rule of (CPNT . i) ) or not UF = union (rng F) or not UQ = union (rng q) or not the carrier of XP2 = union (rng P) or not the carrier' of XP2 = union (rng T) or not the S-T_Arcs of XP2 = union (rng ST) or not the T-S_Arcs of XP2 = (union (rng TS)) \/ (union (rng O)) or not the ColoredSet of XP2 = union (rng CS) or not the firing-rule of XP2 = UF +* UQ ) or XP1 = XP2 )
assume AS2: ex P2, T2, ST2, TS2, CS2, F2 being ManySortedSet of I ex UF2, UQ2 being Function st
( ( for i being Element of I holds
( P2 . i = the carrier of (CPNT . i) & T2 . i = the carrier' of (CPNT . i) & ST2 . i = the S-T_Arcs of (CPNT . i) & TS2 . i = the T-S_Arcs of (CPNT . i) & CS2 . i = the ColoredSet of (CPNT . i) & F2 . i = the firing-rule of (CPNT . i) ) ) & UF2 = union (rng F2) & UQ2 = union (rng q) & the carrier of XP2 = union (rng P2) & the carrier' of XP2 = union (rng T2) & the S-T_Arcs of XP2 = union (rng ST2) & the T-S_Arcs of XP2 = (union (rng TS2)) \/ (union (rng O)) & the ColoredSet of XP2 = union (rng CS2) & the firing-rule of XP2 = UF2 +* UQ2 ) ; :: thesis: XP1 = XP2
consider P1, T1, ST1, TS1, CS1, F1 being ManySortedSet of I, UF1, UQ1 being Function such that
D1: ( ( for i being Element of I holds
( P1 . i = the carrier of (CPNT . i) & T1 . i = the carrier' of (CPNT . i) & ST1 . i = the S-T_Arcs of (CPNT . i) & TS1 . i = the T-S_Arcs of (CPNT . i) & CS1 . i = the ColoredSet of (CPNT . i) & F1 . i = the firing-rule of (CPNT . i) ) ) & UF1 = union (rng F1) & UQ1 = union (rng q) & the carrier of XP1 = union (rng P1) & the carrier' of XP1 = union (rng T1) & the S-T_Arcs of XP1 = union (rng ST1) & the T-S_Arcs of XP1 = (union (rng TS1)) \/ (union (rng O)) & the ColoredSet of XP1 = union (rng CS1) & the firing-rule of XP1 = UF1 +* UQ1 ) by AS1;
consider P2, T2, ST2, TS2, CS2, F2 being ManySortedSet of I, UF2, UQ2 being Function such that
D2: ( ( for i being Element of I holds
( P2 . i = the carrier of (CPNT . i) & T2 . i = the carrier' of (CPNT . i) & ST2 . i = the S-T_Arcs of (CPNT . i) & TS2 . i = the T-S_Arcs of (CPNT . i) & CS2 . i = the ColoredSet of (CPNT . i) & F2 . i = the firing-rule of (CPNT . i) ) ) & UF2 = union (rng F2) & UQ2 = union (rng q) & the carrier of XP2 = union (rng P2) & the carrier' of XP2 = union (rng T2) & the S-T_Arcs of XP2 = union (rng ST2) & the T-S_Arcs of XP2 = (union (rng TS2)) \/ (union (rng O)) & the ColoredSet of XP2 = union (rng CS2) & the firing-rule of XP2 = UF2 +* UQ2 ) by AS2;
X1: dom P1 = I by PARTFUN1:def 2
.= dom P2 by PARTFUN1:def 2 ;
A1: P1 = P2
proof
now :: thesis: for i being object st i in dom P1 holds
P1 . i = P2 . i
let i be object ; :: thesis: ( i in dom P1 implies P1 . i = P2 . i )
assume i in dom P1 ; :: thesis: P1 . i = P2 . i
then reconsider i0 = i as Element of I ;
thus P1 . i = the carrier of (CPNT . i0) by D1
.= P2 . i by D2 ; :: thesis: verum
end;
hence P1 = P2 by FUNCT_1:2, X1; :: thesis: verum
end;
X3: dom T1 = I by PARTFUN1:def 2
.= dom T2 by PARTFUN1:def 2 ;
A2: T1 = T2
proof
now :: thesis: for i being object st i in dom T1 holds
T1 . i = T2 . i
let i be object ; :: thesis: ( i in dom T1 implies T1 . i = T2 . i )
assume i in dom T1 ; :: thesis: T1 . i = T2 . i
then reconsider i0 = i as Element of I ;
thus T1 . i = the carrier' of (CPNT . i0) by D1
.= T2 . i by D2 ; :: thesis: verum
end;
hence T1 = T2 by FUNCT_1:2, X3; :: thesis: verum
end;
X5: dom ST1 = I by PARTFUN1:def 2
.= dom ST2 by PARTFUN1:def 2 ;
A3: ST1 = ST2
proof
now :: thesis: for i being object st i in dom ST1 holds
ST1 . i = ST2 . i
let i be object ; :: thesis: ( i in dom ST1 implies ST1 . i = ST2 . i )
assume i in dom ST1 ; :: thesis: ST1 . i = ST2 . i
then reconsider i0 = i as Element of I ;
thus ST1 . i = the S-T_Arcs of (CPNT . i0) by D1
.= ST2 . i by D2 ; :: thesis: verum
end;
hence ST1 = ST2 by FUNCT_1:2, X5; :: thesis: verum
end;
X7: dom TS1 = I by PARTFUN1:def 2
.= dom TS2 by PARTFUN1:def 2 ;
A4: TS1 = TS2
proof
now :: thesis: for i being object st i in dom TS1 holds
TS1 . i = TS2 . i
let i be object ; :: thesis: ( i in dom TS1 implies TS1 . i = TS2 . i )
assume i in dom TS1 ; :: thesis: TS1 . i = TS2 . i
then reconsider i0 = i as Element of I ;
thus TS1 . i = the T-S_Arcs of (CPNT . i0) by D1
.= TS2 . i by D2 ; :: thesis: verum
end;
hence TS1 = TS2 by FUNCT_1:2, X7; :: thesis: verum
end;
X9: dom CS1 = I by PARTFUN1:def 2
.= dom CS2 by PARTFUN1:def 2 ;
A5: CS1 = CS2
proof
now :: thesis: for i being object st i in dom CS1 holds
CS1 . i = CS2 . i
let i be object ; :: thesis: ( i in dom CS1 implies CS1 . i = CS2 . i )
assume i in dom CS1 ; :: thesis: CS1 . i = CS2 . i
then reconsider i0 = i as Element of I ;
thus CS1 . i = the ColoredSet of (CPNT . i0) by D1
.= CS2 . i by D2 ; :: thesis: verum
end;
hence CS1 = CS2 by FUNCT_1:2, X9; :: thesis: verum
end;
X11: dom F1 = I by PARTFUN1:def 2
.= dom F2 by PARTFUN1:def 2 ;
F1 = F2
proof
now :: thesis: for i being object st i in dom F1 holds
F1 . i = F2 . i
let i be object ; :: thesis: ( i in dom F1 implies F1 . i = F2 . i )
assume i in dom F1 ; :: thesis: F1 . i = F2 . i
then reconsider i0 = i as Element of I ;
thus F1 . i = the firing-rule of (CPNT . i0) by D1
.= F2 . i by D2 ; :: thesis: verum
end;
hence F1 = F2 by FUNCT_1:2, X11; :: thesis: verum
end;
hence XP1 = XP2 by A1, A2, A3, A4, A5, D1, D2; :: thesis: verum