:: Oriented Simple Chains Included in Oriented Chains
:: by Yatsuka Nakamura and Piotr Rudnicki
::
:: Received August 19, 1998
:: Copyright (c) 1998 Association of Mizar Users
:: deftheorem Def1 defines orientedly_joins GRAPH_4:def 1 :
theorem Th1: :: GRAPH_4:1
:: deftheorem defines are_orientedly_incident GRAPH_4:def 2 :
theorem Th2: :: GRAPH_4:2
:: deftheorem defines -SVSet GRAPH_4:def 3 :
:: deftheorem defines -TVSet GRAPH_4:def 4 :
theorem :: GRAPH_4:3
canceled;
theorem :: GRAPH_4:4
:: deftheorem Def5 defines is_oriented_vertex_seq_of GRAPH_4:def 5 :
theorem Th5: :: GRAPH_4:5
theorem :: GRAPH_4:6
theorem :: GRAPH_4:7
theorem :: GRAPH_4:8
theorem :: GRAPH_4:9
theorem Th10: :: GRAPH_4:10
theorem Th11: :: GRAPH_4:11
:: deftheorem defines oriented-vertex-seq GRAPH_4:def 6 :
theorem :: GRAPH_4:12
theorem Th13: :: GRAPH_4:13
theorem Th14: :: GRAPH_4:14
theorem Th15: :: GRAPH_4:15
theorem Th16: :: GRAPH_4:16
Lm1:
for G being Graph
for v being Element of the carrier of G holds <*v*> is_oriented_vertex_seq_of {}
:: deftheorem Def7 defines Simple GRAPH_4:def 7 :
theorem :: GRAPH_4:17
canceled;
theorem Th18: :: GRAPH_4:18
theorem :: GRAPH_4:19
theorem Th20: :: GRAPH_4:20
theorem Th21: :: GRAPH_4:21
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 Th22: :: GRAPH_4:22
theorem :: GRAPH_4:23
theorem :: GRAPH_4:24
theorem Th25: :: GRAPH_4:25
theorem :: GRAPH_4:26