:: Chordal Graphs
:: by Broderick Arneson and Piotr Rudnicki
::
:: Received August 18, 2006
:: Copyright (c) 2006 Association of Mizar Users
theorem Th1: :: CHORD:1
theorem Th2: :: CHORD:2
Lm1:
for a, b, c being Integer st a + 2 < b holds
((c - b) + 1) + 2 < (c - a) + 1
theorem Th3: :: CHORD:3
theorem Th4: :: CHORD:4
theorem Th5: :: CHORD:5
theorem Th6: :: CHORD:6
theorem Th7: :: CHORD:7
theorem Th8: :: CHORD:8
theorem :: CHORD:9
theorem Th10: :: CHORD:10
theorem Th11: :: CHORD:11
theorem Th12: :: CHORD:12
theorem Th13: :: CHORD:13
Lm2:
for i, j being natural odd number st i <= j holds
ex k being natural number st i + (2 * k) = j
theorem :: CHORD:14
theorem Th15: :: CHORD:15
:: deftheorem defines .followSet CHORD:def 1 :
theorem Th16: :: CHORD:16
theorem Th17: :: CHORD:17
theorem Th18: :: CHORD:18
theorem Th19: :: CHORD:19
theorem :: CHORD:20
theorem Th21: :: CHORD:21
theorem Th22: :: CHORD:22
theorem Th23: :: CHORD:23
theorem Th24: :: CHORD:24
theorem Th25: :: CHORD:25
theorem :: CHORD:26
theorem Th27: :: CHORD:27
theorem Th28: :: CHORD:28
theorem Th29: :: CHORD:29
theorem Th30: :: CHORD:30
theorem Th31: :: CHORD:31
theorem Th32: :: CHORD:32
theorem Th33: :: CHORD:33
:: deftheorem Def2 defines minlength CHORD:def 2 :
theorem Th34: :: CHORD:34
theorem Th35: :: CHORD:35
theorem :: CHORD:36
theorem :: CHORD:37
theorem Th38: :: CHORD:38
theorem Th39: :: CHORD:39
theorem Th40: :: CHORD:40
theorem Th41: :: CHORD:41
theorem Th42: :: CHORD:42
theorem :: CHORD:43
:: deftheorem Def3 defines are_adjacent CHORD:def 3 :
theorem Th44: :: CHORD:44
theorem Th45: :: CHORD:45
theorem Th46: :: CHORD:46
theorem Th47: :: CHORD:47
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: :: CHORD:48
:: deftheorem defines .AdjacentSet CHORD:def 4 :
theorem :: CHORD:49
theorem Th50: :: CHORD:50
theorem Th51: :: CHORD:51
theorem Th52: :: CHORD:52
theorem :: CHORD:53
theorem :: CHORD:54
theorem Th55: :: CHORD:55
theorem :: CHORD:56
theorem Th57: :: CHORD:57
theorem Th58: :: CHORD:58
:: deftheorem Def5 defines AdjGraph CHORD:def 5 :
theorem Th59: :: CHORD:59
theorem Th60: :: CHORD:60
:: deftheorem Def6 defines complete CHORD:def 6 :
theorem Th61: :: CHORD:61
theorem Th62: :: CHORD:62
theorem Th63: :: CHORD:63
:: deftheorem Def7 defines simplicial CHORD:def 7 :
theorem Th64: :: CHORD:64
theorem Th65: :: CHORD:65
theorem Th66: :: CHORD:66
theorem Th67: :: CHORD:67
theorem Th68: :: CHORD:68
theorem Th69: :: CHORD:69
:: deftheorem Def8 defines VertexSeparator CHORD:def 8 :
theorem Th70: :: CHORD:70
theorem Th71: :: CHORD:71
theorem Th72: :: CHORD:72
theorem Th73: :: CHORD:73
theorem :: CHORD:74
theorem Th75: :: CHORD:75
theorem Th76: :: CHORD:76
theorem Th77: :: CHORD:77
:: deftheorem Def9 defines minimal CHORD:def 9 :
theorem :: CHORD:78
theorem Th79: :: CHORD:79
theorem Th80: :: CHORD:80
theorem :: CHORD:81
theorem Th82: :: CHORD:82
theorem Th83: :: CHORD:83
:: deftheorem Def10 defines chordal CHORD:def 10 :
theorem Th84: :: CHORD:84
theorem Th85: :: CHORD:85
theorem Th86: :: CHORD:86
theorem Th87: :: CHORD:87
theorem :: CHORD:88
theorem Th89: :: CHORD:89
theorem :: CHORD:90
Lm3:
for G being _Graph
for W being Walk of G st W is chordal holds
W .reverse() is chordal
theorem :: CHORD:91
theorem Th92: :: CHORD:92
theorem :: CHORD:93
theorem :: CHORD:94
:: deftheorem Def11 defines chordal CHORD:def 11 :
theorem Th95: :: CHORD:95
theorem Th96: :: CHORD:96
theorem :: CHORD:97
theorem Th98: :: CHORD:98
theorem :: CHORD:99
theorem Th100: :: CHORD:100
theorem :: CHORD:101
theorem Th102: :: CHORD:102
theorem Th103: :: CHORD:103
:: deftheorem Def12 defines VertexScheme CHORD:def 12 :
theorem :: CHORD:104
theorem :: CHORD:105
theorem Th106: :: CHORD:106
theorem Th107: :: CHORD:107
:: deftheorem Def13 defines perfect CHORD:def 13 :
theorem Th108: :: CHORD:108
theorem :: CHORD:109
theorem :: CHORD:110
theorem :: CHORD:111