:: 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-2021 Association of Mizar Users


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 ) )
proof end;
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;

::$CT
theorem :: MSSCYC_1:2
for n being Nat
for p, q being FinSequence st n <= len p holds
(1,n) -cut p = (1,n) -cut (p ^ q)
proof end;

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;
attr IT is cyclic means :: MSSCYC_1:def 2
 ex p being FinSequence of the carrier of G st
( p is_vertex_seq_of IT & p . 1 = p . (len p) );
end;

:: deftheorem 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) ) );

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

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

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

theorem Th3: :: 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 & t = the Target of G . e holds
<*s,t*> is_vertex_seq_of <*e*>
proof end;

theorem Th4: :: 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
proof end;

registration
let G be non void Graph;
cluster Relation-like NAT -defined Function-like V18() non empty finite FinSequence-like FinSubsequence-like directed for Chain of G;
existence
ex b1 being Chain of G st
( b1 is directed & not b1 is empty & b1 is V18() )
proof end;
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 & p is_vertex_seq_of c holds
p . 1 = p . (len p)
proof end;

theorem Th5: :: 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 & vs is_vertex_seq_of c holds
vs . 1 = vs . (len vs) by Lm1;

theorem Th6: :: 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)*>
proof end;

theorem :: MSSCYC_1:8
for m, n being Nat
for f being FinSequence holds len ((m,n) -cut f) <= len f
proof end;

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

theorem Th9: :: 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
proof end;

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
proof end;
end;

theorem Th10: :: MSSCYC_1:11
for G being non void Graph
for oc being non empty directed Chain of G
for n being Nat st 1 <= n & n <= len oc holds
( (vertex-seq oc) . n = the Source of G . (oc . n) & (vertex-seq oc) . (n + 1) = the Target of G . (oc . n) )
proof end;

theorem Th11: :: MSSCYC_1:12
for m, n being Nat
for f being non empty FinSequence st 1 <= m & m <= n & n <= len f holds
not (m,n) -cut f is empty
proof end;

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

theorem Th13: :: 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))
proof end;

theorem Th14: :: 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 )
proof end;

theorem Th15: :: 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 & (vertex-seq c) . ((len c) + 1) = (vertex-seq c2) . ((len c2) + 1) )
proof end;

theorem Th16: :: 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)
proof end;

theorem Th17: :: 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 Nat ex ch being directed Chain of G st
( len ch = n & ch ^ c is non empty directed Chain of G )
proof end;

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

:: deftheorem 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
proof end;
end;

definition
let IT be Graph;
attr IT is well-founded means :: MSSCYC_1:def 4
 for v being Element of the carrier of IT ex n being 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;
end;

:: deftheorem 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 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 );

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

registration
cluster non empty void -> well-founded for MultiGraphStruct ;
coherence
for b1 being Graph st b1 is void holds
b1 is well-founded
proof end;
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 V57() well-founded for MultiGraphStruct ;
existence
ex b1 being Graph st b1 is well-founded
proof end;
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
proof end;
end;

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

registration
cluster non empty V57() directed_cycle-less for MultiGraphStruct ;
existence
ex b1 being Graph st b1 is directed_cycle-less
proof end;
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
proof end;

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]
proof end;

theorem Th20: :: 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
proof end;

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 V28() total for GeneratorSet of A;
existence
ex b1 being GeneratorSet of A st
( b1 is V2() & b1 is V28() )
proof end;
end;

theorem Th21: :: 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
proof end;

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
proof end;

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

theorem Th23: :: 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)) = {{}}
proof end;

definition
let IT be non empty non void ManySortedSign ;
attr IT is finitely_operated means :: 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 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
proof end;

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))
proof end;

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 & k in dom a & ak = a . k holds
depth ak < depth t
proof end;