environ
vocabularies HIDDEN, NUMBERS, XCMPLX_0, ORDINAL1, ARYTM_1, XXREAL_0, NAT_1, CARD_1, ARYTM_3, ABIAN, SUBSET_1, RELAT_1, INT_1, FINSEQ_1, FUNCT_1, FINSEQ_4, XBOOLE_0, FINSET_1, GRAPH_2, ORDINAL4, GLIB_000, GLIB_001, TARSKI, ZFMISC_1, RCOMP_1, GRAPH_1, RELAT_2, REWRITE1, FUNCOP_1, GLIB_002, PARTFUN1, MEMBERED, TOPGEN_1, CHORD;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, XXREAL_2, ORDINAL1, INT_1, XCMPLX_0, XXREAL_0, DOMAIN_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, CARD_1, FINSET_1, NAT_1, ZFMISC_1, GLIB_000, GLIB_001, GLIB_002, FUNCOP_1, ABIAN, ENUMSET1, FINSEQ_4, NUMBERS, GRAPH_2, MEMBERED;
definitions TARSKI, XBOOLE_0, GLIB_000, GLIB_002;
theorems FINSEQ_1, FUNCT_1, GLIB_000, GLIB_001, GLIB_002, GRAPH_2, GRAPH_3, TREES_1, INT_1, JORDAN12, NAT_1, ORDINAL1, RELAT_1, TARSKI, XBOOLE_0, XBOOLE_1, FUNCOP_1, FUNCT_2, FINSEQ_3, FINSEQ_4, ZFMISC_1, ABIAN, CARD_2, ENUMSET1, FINSEQ_2, XREAL_1, MEMBERED, FINSEQ_5, XXREAL_0, NAT_D, PARTFUN1, XXREAL_2, NUMBERS;
schemes NAT_1, PRE_CIRC, FUNCT_2, FRAENKEL;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, GLIB_000, ABIAN, GRAPH_2, GLIB_001, GLIB_002, FUNCT_2, XXREAL_2, CARD_1, RELSET_1;
constructors HIDDEN, DOMAIN_1, REAL_1, NAT_D, FINSEQ_4, GRAPH_2, GLIB_001, GLIB_002, VALUED_1, XXREAL_2, RELSET_1, NUMBERS;
requirements HIDDEN, ARITHM, BOOLE, NUMERALS, REAL, SUBSET;
equalities GLIB_000, GLIB_001, FUNCOP_1;
expansions TARSKI, XBOOLE_0, GLIB_000, GLIB_001, GLIB_002;
Lm1:
for a, b, c being Integer st a + 2 < b holds
((c - b) + 1) + 2 < (c - a) + 1
theorem Th7:
for
n being
odd Nat holds
( not
n <= 4 or
n = 1 or
n = 3 )
theorem Th8:
for
n being
odd Nat holds
( not
n <= 6 or
n = 1 or
n = 3 or
n = 5 )
theorem
for
n being
odd Nat holds
( not
n <= 8 or
n = 1 or
n = 3 or
n = 5 or
n = 7 )
theorem Th12:
for
n being
even Nat holds
( not
n <= 5 or
n = 0 or
n = 2 or
n = 4 )
theorem Th13:
for
n being
even Nat holds
( not
n <= 7 or
n = 0 or
n = 2 or
n = 4 or
n = 6 )
Lm2:
for i, j being odd Nat st i <= j holds
ex k being Nat st i + (2 * k) = j
scheme
FinGraphOrderCompInd{
P1[
set ] } :
provided
theorem Th46:
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
object st
(
P is
open &
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 )
Lm3:
for G being _Graph
for W being Walk of G st W is chordal holds
W .reverse() is chordal