:: The Correspondence Between Monotonic Many Sorted Signaturesand Well-Founded Graphs. {P}art {I}
:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki
::
:: Received February 14, 1996
:: Copyright (c) 1996 Association of Mizar Users
theorem :: MSSCYC_1:1
:: deftheorem Def1 defines Chain MSSCYC_1:def 1 :
theorem :: MSSCYC_1:2
:: deftheorem Def2 defines cyclic MSSCYC_1:def 2 :
theorem Th3: :: MSSCYC_1:3
theorem Th4: :: MSSCYC_1:4
theorem Th5: :: MSSCYC_1:5
Lm1:
for G being non empty Graph
for c being Chain of G
for p being FinSequence of the carrier of G st c is cyclic & p is_vertex_seq_of c holds
p . 1 = p . (len p)
theorem Th6: :: MSSCYC_1:6
theorem Th7: :: MSSCYC_1:7
theorem :: MSSCYC_1:8
theorem :: MSSCYC_1:9
theorem Th10: :: MSSCYC_1:10
theorem Th11: :: MSSCYC_1:11
theorem Th12: :: MSSCYC_1:12
theorem :: MSSCYC_1:13
theorem Th14: :: MSSCYC_1:14
theorem Th15: :: MSSCYC_1:15
theorem Th16: :: MSSCYC_1:16
theorem Th17: :: MSSCYC_1:17
theorem Th18: :: MSSCYC_1:18
:: deftheorem MSSCYC_1:def 3 :
canceled;
:: deftheorem Def4 defines directed_cycle-less MSSCYC_1:def 4 :
:: deftheorem Def5 defines well-founded MSSCYC_1:def 5 :
theorem :: MSSCYC_1:19
theorem :: MSSCYC_1:20
theorem Th21: :: MSSCYC_1:21
theorem Th22: :: MSSCYC_1:22
theorem :: MSSCYC_1:23
theorem :: MSSCYC_1:24
canceled;
theorem Th25: :: MSSCYC_1:25
:: deftheorem Def6 defines finitely_operated MSSCYC_1:def 6 :
theorem :: MSSCYC_1:26
theorem :: MSSCYC_1:27
theorem :: MSSCYC_1:28