let G1 be _Graph; :: thesis: for G2 being removeParallelEdges of G1 holds

( G1 is chordal iff G2 is chordal )

let G2 be removeParallelEdges of G1; :: thesis: ( G1 is chordal iff G2 is chordal )

consider E being RepEdgeSelection of G1 such that

A1: G2 is inducedSubgraph of G1, the_Vertices_of G1,E by Def7;

( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) ) by GLIB_000:34;

then A2: the_Edges_of G2 = E by A1, GLIB_000:def 37;

( G1 is chordal iff G2 is chordal )

let G2 be removeParallelEdges of G1; :: thesis: ( G1 is chordal iff G2 is chordal )

consider E being RepEdgeSelection of G1 such that

A1: G2 is inducedSubgraph of G1, the_Vertices_of G1,E by Def7;

( the_Vertices_of G1 c= the_Vertices_of G1 & the_Edges_of G1 = G1 .edgesBetween (the_Vertices_of G1) ) by GLIB_000:34;

then A2: the_Edges_of G2 = E by A1, GLIB_000:def 37;

hereby :: thesis: ( G2 is chordal implies G1 is chordal )

assume A10:
G2 is chordal
; :: thesis: G1 is chordal assume A3:
G1 is chordal
; :: thesis: G2 is chordal

end;now :: thesis: for P2 being Walk of G2 st P2 .length() > 3 & P2 is Cycle-like holds

P2 is chordal

hence
G2 is chordal
by CHORD:def 11; :: thesis: verumP2 is chordal

let P2 be Walk of G2; :: thesis: ( P2 .length() > 3 & P2 is Cycle-like implies P2 is chordal )

assume A4: ( P2 .length() > 3 & P2 is Cycle-like ) ; :: thesis: P2 is chordal

end;assume A4: ( P2 .length() > 3 & P2 is Cycle-like ) ; :: thesis: P2 is chordal

now :: thesis: ex m, n being odd Nat st

( m + 2 < n & n <= len P2 & P2 . m <> P2 . n & ex e being object st e Joins P2 . m,P2 . n,G2 & ( for f being object st f in P2 .edges() holds

not f Joins P2 . m,P2 . n,G2 ) )

hence
P2 is chordal
by CHORD:def 10; :: thesis: verum( m + 2 < n & n <= len P2 & P2 . m <> P2 . n & ex e being object st e Joins P2 . m,P2 . n,G2 & ( for f being object st f in P2 .edges() holds

not f Joins P2 . m,P2 . n,G2 ) )

reconsider P1 = P2 as Walk of G1 by GLIB_001:167;

( P1 .length() > 3 & P1 is Cycle-like ) by A4, GLIB_001:114, GLIB_006:24;

then consider m, n being odd Nat such that

A5: ( m + 2 < n & n <= len P1 & P1 . m <> P1 . n ) and

A6: ex e being object st e Joins P1 . m,P1 . n,G1 and

A7: for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1 by A3, CHORD:def 11, CHORD:def 10;

take m = m; :: thesis: ex n being odd Nat st

( m + 2 < n & n <= len P2 & P2 . m <> P2 . n & ex e being object st e Joins P2 . m,P2 . n,G2 & ( for f being object st f in P2 .edges() holds

not f Joins P2 . m,P2 . n,G2 ) )

take n = n; :: thesis: ( m + 2 < n & n <= len P2 & P2 . m <> P2 . n & ex e being object st e Joins P2 . m,P2 . n,G2 & ( for f being object st f in P2 .edges() holds

not f Joins P2 . m,P2 . n,G2 ) )

thus ( m + 2 < n & n <= len P2 & P2 . m <> P2 . n ) by A5; :: thesis: ( ex e being object st e Joins P2 . m,P2 . n,G2 & ( for f being object st f in P2 .edges() holds

not f Joins P2 . m,P2 . n,G2 ) )

assume f in P2 .edges() ; :: thesis: not f Joins P2 . m,P2 . n,G2

then f in P1 .edges() by GLIB_001:110;

hence not f Joins P2 . m,P2 . n,G2 by A7, GLIB_000:72; :: thesis: verum

end;( P1 .length() > 3 & P1 is Cycle-like ) by A4, GLIB_001:114, GLIB_006:24;

then consider m, n being odd Nat such that

A5: ( m + 2 < n & n <= len P1 & P1 . m <> P1 . n ) and

A6: ex e being object st e Joins P1 . m,P1 . n,G1 and

A7: for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1 by A3, CHORD:def 11, CHORD:def 10;

take m = m; :: thesis: ex n being odd Nat st

( m + 2 < n & n <= len P2 & P2 . m <> P2 . n & ex e being object st e Joins P2 . m,P2 . n,G2 & ( for f being object st f in P2 .edges() holds

not f Joins P2 . m,P2 . n,G2 ) )

take n = n; :: thesis: ( m + 2 < n & n <= len P2 & P2 . m <> P2 . n & ex e being object st e Joins P2 . m,P2 . n,G2 & ( for f being object st f in P2 .edges() holds

not f Joins P2 . m,P2 . n,G2 ) )

thus ( m + 2 < n & n <= len P2 & P2 . m <> P2 . n ) by A5; :: thesis: ( ex e being object st e Joins P2 . m,P2 . n,G2 & ( for f being object st f in P2 .edges() holds

not f Joins P2 . m,P2 . n,G2 ) )

hereby :: thesis: for f being object st f in P2 .edges() holds

not f Joins P2 . m,P2 . n,G2

let f be object ; :: thesis: ( f in P2 .edges() implies not f Joins P2 . m,P2 . n,G2 )not f Joins P2 . m,P2 . n,G2

consider e0 being object such that

A8: e0 Joins P1 . m,P1 . n,G1 by A6;

consider e being object such that

A9: ( e Joins P1 . m,P1 . n,G1 & e in E ) and

for e9 being object st e9 Joins P1 . m,P1 . n,G1 & e9 in E holds

e9 = e by A8, Def5;

take e = e; :: thesis: e Joins P2 . m,P2 . n,G2

thus e Joins P2 . m,P2 . n,G2 by A2, A9, GLIB_000:73; :: thesis: verum

end;A8: e0 Joins P1 . m,P1 . n,G1 by A6;

consider e being object such that

A9: ( e Joins P1 . m,P1 . n,G1 & e in E ) and

for e9 being object st e9 Joins P1 . m,P1 . n,G1 & e9 in E holds

e9 = e by A8, Def5;

take e = e; :: thesis: e Joins P2 . m,P2 . n,G2

thus e Joins P2 . m,P2 . n,G2 by A2, A9, GLIB_000:73; :: thesis: verum

assume f in P2 .edges() ; :: thesis: not f Joins P2 . m,P2 . n,G2

then f in P1 .edges() by GLIB_001:110;

hence not f Joins P2 . m,P2 . n,G2 by A7, GLIB_000:72; :: thesis: verum

now :: thesis: for P1 being Walk of G1 st P1 .length() > 3 & P1 is Cycle-like holds

P1 is chordal

hence
G1 is chordal
by CHORD:def 11; :: thesis: verumP1 is chordal

let P1 be Walk of G1; :: thesis: ( P1 .length() > 3 & P1 is Cycle-like implies P1 is chordal )

assume A11: ( P1 .length() > 3 & P1 is Cycle-like ) ; :: thesis: P1 is chordal

A12: len P1 <> 5

end;assume A11: ( P1 .length() > 3 & P1 is Cycle-like ) ; :: thesis: P1 is chordal

A12: len P1 <> 5

proof

assume
len P1 = 5
; :: thesis: contradiction

then (2 * (P1 .length())) + 1 = (2 * 2) + 1 by GLIB_001:112;

hence contradiction by A11; :: thesis: verum

end;then (2 * (P1 .length())) + 1 = (2 * 2) + 1 by GLIB_001:112;

hence contradiction by A11; :: thesis: verum

now :: thesis: ex m, n being odd Nat st

( m + 2 < n & n <= len P1 & P1 . m <> P1 . n & ex e being object st e Joins P1 . m,P1 . n,G1 & ( for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1 ) )

hence
P1 is chordal
by CHORD:def 10; :: thesis: verum( m + 2 < n & n <= len P1 & P1 . m <> P1 . n & ex e being object st e Joins P1 . m,P1 . n,G1 & ( for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1 ) )

consider P2 being Walk of G2 such that

A13: P1 .vertexSeq() = P2 .vertexSeq() by Th98;

A14: ( P1 .length() = P2 .length() & P2 is Cycle-like ) by A11, A12, A13, Th30, Th32;

then consider m, n being odd Nat such that

A15: ( m + 2 < n & n <= len P2 & P2 . m <> P2 . n ) and

A16: ex e being object st e Joins P2 . m,P2 . n,G2 and

A17: for f being object st f in P2 .edges() holds

not f Joins P2 . m,P2 . n,G2 by A10, A11, CHORD:def 11, CHORD:def 10;

take m = m; :: thesis: ex n being odd Nat st

( m + 2 < n & n <= len P1 & P1 . m <> P1 . n & ex e being object st e Joins P1 . m,P1 . n,G1 & ( for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1 ) )

take n = n; :: thesis: ( m + 2 < n & n <= len P1 & P1 . m <> P1 . n & ex e being object st e Joins P1 . m,P1 . n,G1 & ( for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1 ) )

A18: len P1 = (2 * (P1 .length())) + 1 by GLIB_001:112

.= len P2 by A14, GLIB_001:112 ;

hence ( m + 2 < n & n <= len P1 ) by A15; :: thesis: ( P1 . m <> P1 . n & ex e being object st e Joins P1 . m,P1 . n,G1 & ( for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1 ) )

A19: ( P1 . n = P2 . n & P1 . m = P2 . m ) by A13, Th29;

hence P1 . m <> P1 . n by A15; :: thesis: ( ex e being object st e Joins P1 . m,P1 . n,G1 & ( for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1 ) )

thus ex e being object st e Joins P1 . m,P1 . n,G1 by A16, A19, GLIB_000:72; :: thesis: for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1

let f be object ; :: thesis: ( f in P1 .edges() implies not f Joins P1 . m,P1 . n,G1 )

assume f in P1 .edges() ; :: thesis: not f Joins P1 . m,P1 . n,G1

then consider k being odd Element of NAT such that

A20: ( k < len P1 & P1 . (k + 1) = f ) by GLIB_001:100;

A21: f Joins P1 . k,P1 . (k + 2),G1 by A20, GLIB_001:def 3;

assume A22: f Joins P1 . m,P1 . n,G1 ; :: thesis: contradiction

then consider f2 being object such that

A23: ( f2 Joins P1 . m,P1 . n,G1 & f2 in E ) and

A24: for f9 being object st f9 Joins P1 . m,P1 . n,G1 & f9 in E holds

f9 = f2 by Def5;

A25: f2 Joins P2 . m,P2 . n,G2 by A2, A19, A23, GLIB_000:73;

A26: k < len P2 by A18, A20;

then A27: P2 . (k + 1) Joins P2 . k,P2 . (k + 2),G2 by GLIB_001:def 3;

( P1 . k = P2 . k & P1 . (k + 2) = P2 . (k + 2) ) by A13, Th29;

then A28: P2 . (k + 1) Joins P1 . k,P1 . (k + 2),G1 by A27, GLIB_000:72;

A29: P2 . (k + 1) in E by A2, A27, GLIB_000:def 13;

( ( P1 . m = P1 . k & P1 . n = P1 . (k + 2) ) or ( P1 . m = P1 . (k + 2) & P1 . n = P1 . k ) ) by A21, A22, GLIB_000:15;

then P2 . (k + 1) = f2 by A24, A28, A29, GLIB_000:14;

hence contradiction by A17, A25, A26, GLIB_001:100; :: thesis: verum

end;A13: P1 .vertexSeq() = P2 .vertexSeq() by Th98;

A14: ( P1 .length() = P2 .length() & P2 is Cycle-like ) by A11, A12, A13, Th30, Th32;

then consider m, n being odd Nat such that

A15: ( m + 2 < n & n <= len P2 & P2 . m <> P2 . n ) and

A16: ex e being object st e Joins P2 . m,P2 . n,G2 and

A17: for f being object st f in P2 .edges() holds

not f Joins P2 . m,P2 . n,G2 by A10, A11, CHORD:def 11, CHORD:def 10;

take m = m; :: thesis: ex n being odd Nat st

( m + 2 < n & n <= len P1 & P1 . m <> P1 . n & ex e being object st e Joins P1 . m,P1 . n,G1 & ( for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1 ) )

take n = n; :: thesis: ( m + 2 < n & n <= len P1 & P1 . m <> P1 . n & ex e being object st e Joins P1 . m,P1 . n,G1 & ( for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1 ) )

A18: len P1 = (2 * (P1 .length())) + 1 by GLIB_001:112

.= len P2 by A14, GLIB_001:112 ;

hence ( m + 2 < n & n <= len P1 ) by A15; :: thesis: ( P1 . m <> P1 . n & ex e being object st e Joins P1 . m,P1 . n,G1 & ( for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1 ) )

A19: ( P1 . n = P2 . n & P1 . m = P2 . m ) by A13, Th29;

hence P1 . m <> P1 . n by A15; :: thesis: ( ex e being object st e Joins P1 . m,P1 . n,G1 & ( for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1 ) )

thus ex e being object st e Joins P1 . m,P1 . n,G1 by A16, A19, GLIB_000:72; :: thesis: for f being object st f in P1 .edges() holds

not f Joins P1 . m,P1 . n,G1

let f be object ; :: thesis: ( f in P1 .edges() implies not f Joins P1 . m,P1 . n,G1 )

assume f in P1 .edges() ; :: thesis: not f Joins P1 . m,P1 . n,G1

then consider k being odd Element of NAT such that

A20: ( k < len P1 & P1 . (k + 1) = f ) by GLIB_001:100;

A21: f Joins P1 . k,P1 . (k + 2),G1 by A20, GLIB_001:def 3;

assume A22: f Joins P1 . m,P1 . n,G1 ; :: thesis: contradiction

then consider f2 being object such that

A23: ( f2 Joins P1 . m,P1 . n,G1 & f2 in E ) and

A24: for f9 being object st f9 Joins P1 . m,P1 . n,G1 & f9 in E holds

f9 = f2 by Def5;

A25: f2 Joins P2 . m,P2 . n,G2 by A2, A19, A23, GLIB_000:73;

A26: k < len P2 by A18, A20;

then A27: P2 . (k + 1) Joins P2 . k,P2 . (k + 2),G2 by GLIB_001:def 3;

( P1 . k = P2 . k & P1 . (k + 2) = P2 . (k + 2) ) by A13, Th29;

then A28: P2 . (k + 1) Joins P1 . k,P1 . (k + 2),G1 by A27, GLIB_000:72;

A29: P2 . (k + 1) in E by A2, A27, GLIB_000:def 13;

( ( P1 . m = P1 . k & P1 . n = P1 . (k + 2) ) or ( P1 . m = P1 . (k + 2) & P1 . n = P1 . k ) ) by A21, A22, GLIB_000:15;

then P2 . (k + 1) = f2 by A24, A28, A29, GLIB_000:14;

hence contradiction by A17, A25, A26, GLIB_001:100; :: thesis: verum