begin
theorem
:: deftheorem Def1 defines Chain MSSCYC_1:def 1 :
theorem
:: deftheorem Def2 defines cyclic MSSCYC_1:def 2 :
theorem Th3:
theorem Th4:
theorem Th5:
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:
theorem Th7:
theorem
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
:: 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
begin
theorem
theorem Th21:
theorem Th22:
theorem
theorem
canceled;
theorem Th25:
:: deftheorem Def6 defines finitely_operated MSSCYC_1:def 6 :
theorem
theorem
theorem