begin
theorem
:: deftheorem Def1 defines Chain MSSCYC_1:def 1 :
for G being Graph
for b2 being set holds
( b2 is Chain of G iff ( b2 is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of b2 ) );
theorem
:: deftheorem Def2 defines cyclic MSSCYC_1:def 2 :
for G being Graph
for IT being Chain of G holds
( IT is cyclic iff ex p being FinSequence of the carrier of G st
( p is_vertex_seq_of IT & p . 1 = p . (len p) ) );
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 :
for IT being Graph holds
( IT is directed_cycle-less iff for dc being directed Chain of IT st not dc is empty holds
not dc is cyclic );
:: deftheorem Def5 defines well-founded MSSCYC_1:def 5 :
for IT being Graph holds
( IT is well-founded iff for v being Element of the carrier of IT ex n being Element of NAT st
for c being directed Chain of IT st not c is empty & (vertex-seq c) . ((len c) + 1) = v holds
len c <= n );
theorem
begin
theorem
theorem Th21:
theorem Th22:
theorem
theorem
canceled;
theorem Th25:
:: deftheorem Def6 defines finitely_operated MSSCYC_1:def 6 :
for IT being non empty non void ManySortedSign holds
( IT is finitely_operated iff for s being SortSymbol of IT holds { o where o is OperSymbol of IT : the_result_sort_of o = s } is finite );
theorem
theorem
theorem