:: Vertex sequences induced by chains
:: by Yatsuka Nakamura and Piotr Rudnicki
::
:: Received May 13, 1995
:: Copyright (c) 1995 Association of Mizar Users
theorem Th1: :: GRAPH_2:1
for
m,
k,
n being
Nat holds
( (
m + 1
<= k &
k <= n ) iff ex
i being
Element of
NAT st
(
m <= i &
i < n &
k = i + 1 ) )
theorem Th2: :: GRAPH_2:2
theorem Th3: :: GRAPH_2:3
Lm1:
for m, n being Element of NAT
for F being finite set st F = { k where k is Element of NAT : ( m <= k & k <= m + n ) } holds
card F = n + 1
theorem Th4: :: GRAPH_2:4
theorem Th5: :: GRAPH_2:5
:: deftheorem Def1 defines -cut GRAPH_2:def 1 :
Lm2:
for p being FinSequence
for m, n being Element of NAT st 1 <= m & m <= n + 1 & n <= len p holds
( (len (m,n -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len (m,n -cut p) holds
(m,n -cut p) . (i + 1) = p . (m + i) ) )
theorem Th6: :: GRAPH_2:6
theorem Th7: :: GRAPH_2:7
theorem Th8: :: GRAPH_2:8
theorem :: GRAPH_2:9
theorem :: GRAPH_2:10
theorem Th11: :: GRAPH_2:11
theorem Th12: :: GRAPH_2:12
:: deftheorem defines ^' GRAPH_2:def 2 :
theorem Th13: :: GRAPH_2:13
theorem Th14: :: GRAPH_2:14
theorem Th15: :: GRAPH_2:15
theorem Th16: :: GRAPH_2:16
theorem Th17: :: GRAPH_2:17
theorem :: GRAPH_2:18
:: deftheorem Def3 defines TwoValued GRAPH_2:def 3 :
theorem Th19: :: GRAPH_2:19
then Lm4:
<*1,2*> is TwoValued
by Lm3;
Lm5:
now
set p =
<*1,2*>;
let i be
Nat;
:: thesis: ( 1 <= i & i + 1 <= len <*1,2*> implies <*1,2*> . i <> <*1,2*> . (i + 1) )assume that A1:
1
<= i
and A2:
i + 1
<= len <*1,2*>
;
:: thesis: <*1,2*> . i <> <*1,2*> . (i + 1)
i + 1
<= 1
+ 1
by A2, FINSEQ_1:61;
then
i <= 1
by XREAL_1:8;
then
i = 1
by A1, XXREAL_0:1;
then
(
<*1,2*> . i = 1 &
<*1,2*> . (i + 1) = 2 )
by FINSEQ_1:61;
hence
<*1,2*> . i <> <*1,2*> . (i + 1)
;
:: thesis: verum
end;
:: deftheorem Def4 defines Alternating GRAPH_2:def 4 :
Lm6:
<*1,2*> is Alternating
by Def4, Lm5;
theorem Th20: :: GRAPH_2:20
theorem Th21: :: GRAPH_2:21
theorem Th22: :: GRAPH_2:22
theorem Th23: :: GRAPH_2:23
theorem :: GRAPH_2:24
canceled;
theorem :: GRAPH_2:25
canceled;
theorem Th26: :: GRAPH_2:26
theorem :: GRAPH_2:27
theorem Th28: :: GRAPH_2:28
theorem Th29: :: GRAPH_2:29
theorem Th30: :: GRAPH_2:30
theorem Th31: :: GRAPH_2:31
theorem Th32: :: GRAPH_2:32
:: deftheorem GRAPH_2:def 5 :
canceled;
:: deftheorem defines -VSet GRAPH_2:def 6 :
:: deftheorem Def7 defines is_vertex_seq_of GRAPH_2:def 7 :
theorem :: GRAPH_2:33
canceled;
theorem Th34: :: GRAPH_2:34
theorem Th35: :: GRAPH_2:35
theorem Th36: :: GRAPH_2:36
theorem Th37: :: GRAPH_2:37
:: deftheorem Def8 defines alternates_vertices_in GRAPH_2:def 8 :
theorem Th38: :: GRAPH_2:38
theorem Th39: :: GRAPH_2:39
theorem Th40: :: GRAPH_2:40
theorem Th41: :: GRAPH_2:41
Lm7:
for D being non empty set st ( for x, y being set st x in D & y in D holds
x = y ) holds
card D = 1
theorem Th42: :: GRAPH_2:42
:: deftheorem defines vertex-seq GRAPH_2:def 9 :
theorem Th43: :: GRAPH_2:43
theorem Th44: :: GRAPH_2:44
theorem Th45: :: GRAPH_2:45
theorem Th46: :: GRAPH_2:46
theorem Th47: :: GRAPH_2:47
Lm8:
for G being Graph
for v being Element of the carrier of G holds <*v*> is_vertex_seq_of {}
:: deftheorem Def10 defines simple GRAPH_2:def 10 :
theorem :: GRAPH_2:48
canceled;
theorem :: GRAPH_2:49
theorem Th50: :: GRAPH_2:50
theorem :: GRAPH_2:51
theorem Th52: :: GRAPH_2:52
theorem :: GRAPH_2:53
theorem :: GRAPH_2:54
theorem :: GRAPH_2:55
theorem :: GRAPH_2:56
:: deftheorem defines vertex-seq GRAPH_2:def 11 :
theorem :: GRAPH_2:57
theorem :: GRAPH_2:58
theorem Th59: :: GRAPH_2:59
theorem :: GRAPH_2:60
theorem :: GRAPH_2:61
theorem :: GRAPH_2:62
definition
let F be
FinSequence of
INT ;
let m,
n be
Element of
NAT ;
assume A1:
( 1
<= m &
m <= n &
n <= len F )
;
func min_at F,
m,
n -> Element of
NAT means :
Def12:
:: GRAPH_2:def 12
ex
X being non
empty finite Subset of
INT st
(
X = rng (m,n -cut F) &
it + 1
= ((min X) .. (m,n -cut F)) + m );
existence
ex b1 being Element of NAT ex X being non empty finite Subset of INT st
( X = rng (m,n -cut F) & b1 + 1 = ((min X) .. (m,n -cut F)) + m )
uniqueness
for b1, b2 being Element of NAT st ex X being non empty finite Subset of INT st
( X = rng (m,n -cut F) & b1 + 1 = ((min X) .. (m,n -cut F)) + m ) & ex X being non empty finite Subset of INT st
( X = rng (m,n -cut F) & b2 + 1 = ((min X) .. (m,n -cut F)) + m ) holds
b1 = b2
;
end;
:: deftheorem Def12 defines min_at GRAPH_2:def 12 :
theorem Th63: :: GRAPH_2:63
theorem :: GRAPH_2:64
:: deftheorem Def13 defines is_non_decreasing_on GRAPH_2:def 13 :
:: deftheorem Def14 defines is_split_at GRAPH_2:def 14 :
theorem :: GRAPH_2:65
theorem :: GRAPH_2:66