begin
theorem Th1:
theorem Th2:
Lm1:
for a, b, c being Integer st a + 2 < b holds
((c - b) + 1) + 2 < (c - a) + 1
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
Lm2:
for i, j being natural odd number st i <= j holds
ex k being natural number st i + (2 * k) = j
theorem
theorem Th15:
:: deftheorem defines .followSet CHORD:def 1 :
theorem Th16:
theorem Th17:
theorem Th18:
begin
theorem Th19:
theorem
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
scheme
FinGraphOrderCompInd{
P1[
set ] } :
provided
theorem Th32:
theorem Th33:
begin
:: deftheorem Def2 defines minlength CHORD:def 2 :
theorem Th34:
theorem Th35:
theorem
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem
begin
:: deftheorem Def3 defines are_adjacent CHORD:def 3 :
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
for
G being
_Graph for
v1,
v2,
v3 being
Vertex of
G st
v1 <> v2 &
v1 <> v3 &
v2 <> v3 &
v1,
v2 are_adjacent &
v2,
v3 are_adjacent holds
ex
P being
Path of
G ex
e1,
e2 being
set st
( not
P is
closed &
len P = 5 &
P .length() = 2 &
e1 Joins v1,
v2,
G &
e2 Joins v2,
v3,
G &
P .edges() = {e1,e2} &
P .vertices() = {v1,v2,v3} &
P . 1
= v1 &
P . 3
= v2 &
P . 5
= v3 )
theorem Th48:
:: deftheorem defines .AdjacentSet CHORD:def 4 :
theorem
theorem Th50:
theorem Th51:
theorem Th52:
theorem
theorem
theorem Th55:
theorem
theorem Th57:
theorem Th58:
:: deftheorem Def5 defines AdjGraph CHORD:def 5 :
theorem Th59:
theorem Th60:
:: deftheorem Def6 defines complete CHORD:def 6 :
theorem Th61:
theorem Th62:
theorem Th63:
begin
:: deftheorem Def7 defines simplicial CHORD:def 7 :
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
begin
:: deftheorem Def8 defines VertexSeparator CHORD:def 8 :
theorem Th70:
theorem Th71:
theorem Th72:
theorem Th73:
theorem
theorem Th75:
theorem Th76:
theorem Th77:
:: deftheorem Def9 defines minimal CHORD:def 9 :
theorem
theorem Th79:
theorem Th80:
theorem
theorem Th82:
theorem Th83:
begin
:: deftheorem Def10 defines chordal CHORD:def 10 :
theorem Th84:
theorem Th85:
theorem Th86:
theorem Th87:
theorem
theorem Th89:
theorem
Lm3:
for G being _Graph
for W being Walk of G st W is chordal holds
W .reverse() is chordal
theorem
theorem Th92:
theorem
theorem
:: deftheorem Def11 defines chordal CHORD:def 11 :
theorem Th95:
theorem Th96:
theorem
theorem Th98:
theorem
theorem Th100:
theorem
theorem Th102:
theorem Th103:
begin
:: deftheorem Def12 defines VertexScheme CHORD:def 12 :
theorem
theorem
theorem Th106:
theorem Th107:
:: deftheorem Def13 defines perfect CHORD:def 13 :
theorem Th108:
theorem
theorem
theorem