:: The Correspondence Between Monotonic Many Sorted Signatures and Well-Founded Graphs. {P}art {I}
:: by Czes{\l}aw Byli\'nski and Piotr Rudnicki
::
:: Received February 14, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

definition
let G be Graph;
redefine mode Chain of G means :Def1: :: MSSCYC_1:def 1
( it is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of it );
compatibility
 for b1 being set holds
( b1 is Chain of G iff ( b1 is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of b1 ) )
proofend;
end;

:: 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 :: MSSCYC_1:1
canceled;

theorem :: MSSCYC_1:2
for n being Element of NAT
for p, q being FinSequence st n <= len p holds
(1,n) -cut p = (1,n) -cut (p ^ q)
proofend;

notation
let G be Graph;
let IT be Chain of G;
synonym  directed IT for  oriented ;
end;

definition
let G be Graph;
let IT be Chain of G;
attrIT is cyclic  means :Def2: :: MSSCYC_1:def 2
 ex p being FinSequence of the carrier of G st
( p is_vertex_seq_of IT &amp; p . 1 = p . (len p) );
end;

:: 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 &amp; p . 1 = p . (len p) ) );

registration
cluster non empty void V54() for MultiGraphStruct ;
existence
 ex b1 being Graph st b1 is void
proofend;
end;

theorem Th3: :: MSSCYC_1:3
for G being Graph holds (rng the Source of G) \/ (rng the Target of G) c= the carrier of G
proofend;

registration
cluster non empty non void V54() strict simple connected finite for MultiGraphStruct ;
existence
 ex b1 being Graph st
( b1 is finite &amp; b1 is simple &amp; b1 is connected &amp; not b1 is void &amp; b1 is strict )
proofend;
end;

theorem Th4: :: MSSCYC_1:4
for G being Graph
for e being set
for s, t being Element of the carrier of G st s = the Source of G . e &amp; t = the Target of G . e holds
<*s,t*> is_vertex_seq_of <*e*>
proofend;

theorem Th5: :: MSSCYC_1:5
for G being Graph
for e being set st e in the carrier' of G holds
<*e*> is directed Chain of G
proofend;

registration
let G be non void Graph;
cluster Relation-like NAT -defined Function-like V14() non empty finite FinSequence-like FinSubsequence-like directed for Chain of G;
existence
 ex b1 being Chain of G st
( b1 is directed &amp; not b1 is empty &amp; b1 is V14() )
proofend;
end;

Lm1:  for G being Graph
for c being Chain of G
for p being FinSequence of the carrier of G st c is cyclic &amp; p is_vertex_seq_of c holds
p . 1 = p . (len p)
proofend;

theorem Th6: :: MSSCYC_1:6
for G being Graph
for c being Chain of G
for vs being FinSequence of the carrier of G st c is cyclic &amp; vs is_vertex_seq_of c holds
vs . 1 = vs . (len vs) by Lm1;

theorem Th7: :: MSSCYC_1:7
for G being Graph
for e being set st e in the carrier' of G holds
for fe being directed Chain of G st fe = <*e*> holds
vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*>
proofend;

theorem :: MSSCYC_1:8
for m, n being Element of NAT
for f being FinSequence holds len ((m,n) -cut f) <= len f
proofend;

theorem :: MSSCYC_1:9
for m, n being Element of NAT
for G being non void Graph
for c being directed Chain of G st 1 <= m &amp; m <= n &amp; n <= len c holds
(m,n) -cut c is directed Chain of G
proofend;

theorem Th10: :: MSSCYC_1:10
for G being non void Graph
for oc being non empty directed Chain of G holds len (vertex-seq oc) = (len oc) + 1
proofend;

registration
let G be non void Graph;
let oc be non empty directed Chain of G;
cluster vertex-seq oc ->  non empty ;
coherence
 not vertex-seq oc is empty
proofend;
end;

theorem Th11: :: MSSCYC_1:11
for G being non void Graph
for oc being non empty directed Chain of G
for n being Element of NAT st 1 <= n &amp; n <= len oc holds
( (vertex-seq oc) . n = the Source of G . (oc . n) &amp; (vertex-seq oc) . (n + 1) = the Target of G . (oc . n) )
proofend;

theorem Th12: :: MSSCYC_1:12
for m, n being Element of NAT
for f being non empty FinSequence st 1 <= m &amp; m <= n &amp; n <= len f holds
not (m,n) -cut f is empty
proofend;

theorem :: MSSCYC_1:13
for m, n being Element of NAT
for G being non void Graph
for c, c1 being directed Chain of G st 1 <= m &amp; m <= n &amp; n <= len c &amp; c1 = (m,n) -cut c holds
vertex-seq c1 = (m,(n + 1)) -cut (vertex-seq c)
proofend;

theorem Th14: :: MSSCYC_1:14
for G being non void Graph
for oc being non empty directed Chain of G holds (vertex-seq oc) . ((len oc) + 1) = the Target of G . (oc . (len oc))
proofend;

theorem Th15: :: MSSCYC_1:15
for G being non void Graph
for c1, c2 being non empty directed Chain of G holds
( (vertex-seq c1) . ((len c1) + 1) = (vertex-seq c2) . 1 iff c1 ^ c2 is non empty directed Chain of G )
proofend;

theorem Th16: :: MSSCYC_1:16
for G being non void Graph
for c, c1, c2 being non empty directed Chain of G st c = c1 ^ c2 holds
( (vertex-seq c) . 1 = (vertex-seq c1) . 1 &amp; (vertex-seq c) . ((len c) + 1) = (vertex-seq c2) . ((len c2) + 1) )
proofend;

theorem Th17: :: MSSCYC_1:17
for G being non void Graph
for oc being non empty directed Chain of G st oc is cyclic holds
(vertex-seq oc) . 1 = (vertex-seq oc) . ((len oc) + 1)
proofend;

theorem Th18: :: MSSCYC_1:18
for G being non void Graph
for c being non empty directed Chain of G st c is cyclic holds
for n being Element of NAT ex ch being directed Chain of G st
( len ch = n &amp; ch ^ c is non empty directed Chain of G )
proofend;

definition
let IT be Graph;
attrIT is directed_cycle-less  means :Def3: :: MSSCYC_1:def 3
 for dc being directed Chain of IT st not dc is empty holds
not dc is cyclic ;
end;

:: deftheorem Def3 defines directed_cycle-less MSSCYC_1:def_3_:_
 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 );

notation
let IT be Graph;
antonym  with_directed_cycle IT for  directed_cycle-less ;
end;

registration
cluster non empty void  ->  directed_cycle-less for MultiGraphStruct ;
coherence
 for b1 being Graph st b1 is void holds
b1 is directed_cycle-less
proofend;
end;

definition
let IT be Graph;
attrIT is well-founded  means :Def4: :: MSSCYC_1:def 4
 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 &amp; (vertex-seq c) . ((len c) + 1) = v holds
len c <= n;
end;

:: deftheorem Def4 defines well-founded MSSCYC_1:def_4_:_
 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 &amp; (vertex-seq c) . ((len c) + 1) = v holds
len c <= n );

registration
let G be void Graph;
cluster  ->  empty for Chain of G;
coherence
 for b1 being Chain of G holds b1 is empty
proofend;
end;

registration
cluster non empty void  ->  well-founded for MultiGraphStruct ;
coherence
 for b1 being Graph st b1 is void holds
b1 is well-founded
proofend;
end;

registration
cluster non empty non well-founded  ->  non void for MultiGraphStruct ;
coherence
 for b1 being Graph st not b1 is well-founded holds
not b1 is void ;
end;

registration
cluster non empty V54() well-founded for MultiGraphStruct ;
existence
 ex b1 being Graph st b1 is well-founded
proofend;
end;

registration
cluster non empty well-founded  ->  directed_cycle-less for MultiGraphStruct ;
coherence
 for b1 being Graph st b1 is well-founded holds
b1 is directed_cycle-less
proofend;
end;

registration
cluster non empty V54() non well-founded for MultiGraphStruct ;
existence
 not for b1 being Graph holds b1 is well-founded
proofend;
end;

registration
cluster non empty V54() directed_cycle-less for MultiGraphStruct ;
existence
 ex b1 being Graph st b1 is directed_cycle-less
proofend;
end;

theorem :: MSSCYC_1:19
for t being DecoratedTree
for p being Node of t
for k being Element of NAT holds p | k is Node of t
proofend;

begin

theorem :: MSSCYC_1:20
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for t being Term of S,X st not t is root holds
ex o being OperSymbol of S st t . {} = [o, the carrier of S]
proofend;

theorem Th21: :: MSSCYC_1:21
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for G being GeneratorSet of A
for B being MSSubset of A st G c= B holds
B is GeneratorSet of A
proofend;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty finitely-generated MSAlgebra over S;
cluster Relation-like V2() the carrier of S -defined Function-like non empty V25() total for GeneratorSet of A;
existence
 ex b1 being GeneratorSet of A st
( b1 is V2() &amp; b1 is V25() )
proofend;
end;

theorem Th22: :: MSSCYC_1:22
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for X being V2() GeneratorSet of A ex F being ManySortedFunction of (FreeMSA X),A st F is_epimorphism FreeMSA X,A
proofend;

theorem :: MSSCYC_1:23
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for X being V2() GeneratorSet of A st not A is finite-yielding holds
not FreeMSA X is finite-yielding
proofend;

registration
let S be non empty non void ManySortedSign ;
let X be V2() V25() ManySortedSet of the carrier of S;
let v be SortSymbol of S;
cluster FreeGen (v,X) ->  finite ;
coherence
 FreeGen (v,X) is finite
proofend;
end;

theorem Th24: :: MSSCYC_1:24
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for o being OperSymbol of S st the Arity of S . o = {} holds
dom (Den (o,A)) = {{}}
proofend;

definition
let IT be non empty non void ManySortedSign ;
attrIT is finitely_operated  means :Def5: :: MSSCYC_1:def 5
 for s being SortSymbol of IT holds  {  o where o is OperSymbol of IT : the_result_sort_of o = s  }  is finite ;
end;

:: deftheorem Def5 defines finitely_operated MSSCYC_1:def_5_:_
 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 :: MSSCYC_1:25
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for v being SortSymbol of S st S is finitely_operated holds
Constants (A,v) is finite
proofend;

theorem :: MSSCYC_1:26
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for v being SortSymbol of S holds  {  t where t is Element of the Sorts of (FreeMSA X) . v : depth t = 0  }  = (FreeGen (v,X)) \/ (Constants ((FreeMSA X),v))
proofend;

theorem :: MSSCYC_1:27
for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for v, vk being SortSymbol of S
for o being OperSymbol of S
for t being Element of the Sorts of (FreeMSA X) . v
for a being ArgumentSeq of Sym (o,X)
for k being Element of NAT
for ak being Element of the Sorts of (FreeMSA X) . vk st t = [o, the carrier of S] -tree a &amp; k in dom a &amp; ak = a . k holds
depth ak < depth t
proofend;