let T be _Tree; :: thesis: for a, b, c, d being Vertex of T
for P1, P2 being Path of T st P1 = T .pathBetween a,b & P2 = T .pathBetween a,c & not P1 is_a_prefix_of P2 & not P2 is_a_prefix_of P1 & d = P1 . (len (maxPrefix P1,P2)) holds
((T .pathBetween d,b) .vertices() ) /\ ((T .pathBetween d,c) .vertices() ) = {d}
let a, b, c, d be Vertex of T; :: thesis: for P1, P2 being Path of T st P1 = T .pathBetween a,b & P2 = T .pathBetween a,c & not P1 is_a_prefix_of P2 & not P2 is_a_prefix_of P1 & d = P1 . (len (maxPrefix P1,P2)) holds
((T .pathBetween d,b) .vertices() ) /\ ((T .pathBetween d,c) .vertices() ) = {d}
let P1, P2 be Path of T; :: thesis: ( P1 = T .pathBetween a,b & P2 = T .pathBetween a,c & not P1 is_a_prefix_of P2 & not P2 is_a_prefix_of P1 & d = P1 . (len (maxPrefix P1,P2)) implies ((T .pathBetween d,b) .vertices() ) /\ ((T .pathBetween d,c) .vertices() ) = {d} )
assume that
A1: P1 = T .pathBetween a,b and
A2: P2 = T .pathBetween a,c and
A3: not P1 c= P2 and
A4: not P2 c= P1 and
A5: d = P1 . (len (maxPrefix P1,P2)) ; :: thesis: ((T .pathBetween d,b) .vertices() ) /\ ((T .pathBetween d,c) .vertices() ) = {d}
set Pad = T .pathBetween a,d;
set di = len (maxPrefix P1,P2);
A6: P1 .first() = a by A1, Th28;
A7: P2 .first() = a by A2, Th28;
then reconsider di = len (maxPrefix P1,P2) as odd Element of NAT by A6, Th22;
A8: di <= di + 2 by NAT_1:11;
set Pdb = T .pathBetween d,b;
A9: (T .pathBetween d,b) .first() = d by Th28;
set Pdc = T .pathBetween d,c;
A10: d = P2 . (len (maxPrefix P1,P2)) by A5, Th7;
A11: di <= di + 2 by NAT_1:11;
di + 2 <= len P2 by A4, A6, A7, Th23;
then di <= len P2 by A11, XXREAL_0:2;
then d in P2 .vertices() by A10, GLIB_001:88;
then A12: P2 = (T .pathBetween a,d) .append (T .pathBetween d,c) by A2, Th36;
A13: (T .pathBetween a,d) .last() = d by Th28;
A14: (T .pathBetween d,c) . 1 = (T .pathBetween d,c) .first()
.= d by Th28 ;
A15: (T .pathBetween d,c) .first() = d by Th28;
di + 2 <= len P1 by A3, A6, A7, Th23;
then A16: di <= len P1 by A8, XXREAL_0:2;
then d in P1 .vertices() by A5, GLIB_001:88;
then A17: P1 = (T .pathBetween a,d) .append (T .pathBetween d,b) by A1, Th36;
A18: 1 <= di by ABIAN:12;
then T .pathBetween a,d = P1 .cut ((2 * 0 ) + 1),di by A5, A6, A16, Th35;
then A19: (len (T .pathBetween a,d)) + ((2 * 0 ) + 1) = di + 1 by A16, A18, GLIB_001:37;
A20: (T .pathBetween d,b) . 1 = (T .pathBetween d,b) .first()
.= d by Th28 ;
thus ((T .pathBetween d,b) .vertices() ) /\ ((T .pathBetween d,c) .vertices() ) = {d} :: thesis: verum
proof
hereby :: according to XBOOLE_0:def 10 :: thesis: {d} c= ((T .pathBetween d,b) .vertices() ) /\ ((T .pathBetween d,c) .vertices() )
assume not ((T .pathBetween d,b) .vertices() ) /\ ((T .pathBetween d,c) .vertices() ) c= {d} ; :: thesis: contradiction
then consider e being set such that
A21: e in ((T .pathBetween d,b) .vertices() ) /\ ((T .pathBetween d,c) .vertices() ) and
A22: not e in {d} by TARSKI:def 3;
A23: e in (T .pathBetween d,b) .vertices() by A21, XBOOLE_0:def 4;
A24: e in (T .pathBetween d,c) .vertices() by A21, XBOOLE_0:def 4;
reconsider e = e as Vertex of T by A21;
consider ebi being odd Element of NAT such that
A25: ebi <= len (T .pathBetween d,b) and
A26: e = (T .pathBetween d,b) . ebi by A23, GLIB_001:88;
set Pdeb = (T .pathBetween d,b) .cut 1,ebi;
( 1 <= ebi & (2 * 0 ) + 1 is odd Element of NAT ) by ABIAN:12;
then A27: (T .pathBetween d,b) .cut 1,ebi is_Walk_from d,e by A20, A25, A26, GLIB_001:38;
1 < len ((T .pathBetween d,b) .cut 1,ebi)
proof
assume A28: 1 >= len ((T .pathBetween d,b) .cut 1,ebi) ; :: thesis: contradiction
per cases ( len ((T .pathBetween d,b) .cut 1,ebi) = 2 * 0 or len ((T .pathBetween d,b) .cut 1,ebi) = 1 ) by A28, NAT_1:26;
suppose len ((T .pathBetween d,b) .cut 1,ebi) = 2 * 0 ; :: thesis: contradiction
hence contradiction ; :: thesis: verum
end;
end;
end;
then A31: ((2 * 0 ) + 1) + 2 <= len ((T .pathBetween d,b) .cut 1,ebi) by CHORD:4;
then A32: 2 < len ((T .pathBetween d,b) .cut 1,ebi) by XXREAL_0:2;
consider eci being odd Element of NAT such that
A33: eci <= len (T .pathBetween d,c) and
A34: e = (T .pathBetween d,c) . eci by A24, GLIB_001:88;
set Pdec = (T .pathBetween d,c) .cut 1,eci;
( 1 <= eci & (2 * 0 ) + 1 is odd Element of NAT ) by ABIAN:12;
then A35: (T .pathBetween d,c) .cut 1,eci is_Walk_from d,e by A14, A33, A34, GLIB_001:38;
1 < len ((T .pathBetween d,c) .cut 1,eci)
proof
assume A36: 1 >= len ((T .pathBetween d,c) .cut 1,eci) ; :: thesis: contradiction
per cases ( len ((T .pathBetween d,c) .cut 1,eci) = 2 * 0 or len ((T .pathBetween d,c) .cut 1,eci) = 1 ) by A36, NAT_1:26;
suppose len ((T .pathBetween d,c) .cut 1,eci) = 2 * 0 ; :: thesis: contradiction
hence contradiction ; :: thesis: verum
end;
end;
end;
then A39: ((2 * 0 ) + 1) + 2 <= len ((T .pathBetween d,c) .cut 1,eci) by CHORD:4;
then A40: 2 < len ((T .pathBetween d,c) .cut 1,eci) by XXREAL_0:2;
1 + 2 in dom ((T .pathBetween d,b) .cut 1,ebi) by A31, FINSEQ_3:27;
then A41: ((T .pathBetween d,b) .cut 1,ebi) . (1 + 2) = (T .pathBetween d,b) . (1 + 2) by A25, GLIB_001:47;
len ((T .pathBetween d,b) .cut 1,ebi) <= len (T .pathBetween d,b) by Th10;
then 2 < len (T .pathBetween d,b) by A32, XXREAL_0:2;
then A42: P1 . (di + 2) = (T .pathBetween d,b) . (1 + 2) by A9, A13, A17, A19, GLIB_001:34;
len ((T .pathBetween d,c) .cut 1,eci) <= len (T .pathBetween d,c) by Th10;
then 2 < len (T .pathBetween d,c) by A40, XXREAL_0:2;
then A43: P2 . (di + 2) = (T .pathBetween d,c) . (1 + 2) by A15, A13, A12, A19, GLIB_001:34;
A44: 1 + 2 in dom ((T .pathBetween d,c) .cut 1,eci) by A39, FINSEQ_3:27;
((T .pathBetween d,b) .cut 1,ebi) . (1 + 2) = ((T .pathBetween d,c) .cut 1,eci) . (1 + 2) by A27, A35, Th27;
hence contradiction by A3, A4, A6, A7, A33, A42, A41, A43, A44, Th24, GLIB_001:47; :: thesis: verum
end;
( d in (T .pathBetween d,b) .vertices() & d in (T .pathBetween d,c) .vertices() ) by A9, A15, GLIB_001:89;
then d in ((T .pathBetween d,b) .vertices() ) /\ ((T .pathBetween d,c) .vertices() ) by XBOOLE_0:def 4;
hence {d} c= ((T .pathBetween d,b) .vertices() ) /\ ((T .pathBetween d,c) .vertices() ) by ZFMISC_1:37; :: thesis: verum
end;