:: 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
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, FINSET_1, FUNCT_1, RELAT_1, CARD_3, GRAPH_1, SUBSET_1,
      TREES_2, FINSEQ_1, STRUCT_0, GRAPH_2, ARYTM_3, XXREAL_0, NAT_1, PARTFUN1,
      TARSKI, ORDINAL4, XBOOLE_0, CARD_1, WAYBEL_0, GLIB_000, RELAT_2,
      FUNCOP_1, ARYTM_1, TREES_4, TREES_1, MSUALG_1, PBOOLE, MSATERM, TREES_9,
      ZFMISC_1, MSAFREE, MSUALG_2, MSAFREE2, MSUALG_3, PRELAMB, REALSET1,
      GROUP_6, FUNCT_6, MARGREL1, UNIALG_2, DTCONSTR, TDGROUP, TREES_3,
      TREES_A, MSSCYC_1, SETLIM_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, XCMPLX_0, CARD_1,
      ORDINAL1, NUMBERS, NAT_1, FINSEQ_2, STRUCT_0, CARD_3, RELAT_1, FUNCT_1,
      PARTFUN1, FUNCT_2, FINSET_1, FUNCOP_1, FINSEQ_1, GRAPH_1, FINSEQ_6,
      GRAPH_2, TREES_1, TREES_2, TREES_3, FUNCT_6, TREES_4, LANG1, DTCONSTR,
      PBOOLE, MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE, MSAFREE2, TREES_9,
      MSATERM, XXREAL_0, PRE_POLY;
 constructors WELLORD2, FINSEQ_4, MSUALG_3, MSATERM, MSAFREE2, GRAPH_2,
      RELSET_1, PRE_POLY, XTUPLE_0, FINSEQ_6;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1,
      INT_1, FINSEQ_1, PBOOLE, TREES_2, TREES_3, PRE_CIRC, TREES_9, STRUCT_0,
      MSUALG_1, MSAFREE, MSAFREE2, EXTENS_1, ORDINAL1, CARD_1, GRAPH_1,
      RELSET_1, TREES_1, MSATERM;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;


begin :: Some properties of graphs and trees

reserve G for Graph,
  k, m, n for Nat;

definition
  let G be Graph;
  redefine mode Chain of G means
:: 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;
end;

::$CT

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

notation
  let G be Graph;
  let IT be Chain of G;
  synonym IT is directed for IT is 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;

registration
  cluster void for Graph;
end;

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

registration
  cluster finite simple connected non void strict for Graph;
end;

theorem :: MSSCYC_1:4
  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*>;

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

reserve G for non void Graph;

registration
  let G;
  cluster directed non empty one-to-one for Chain of G;
end;

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

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

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

theorem :: MSSCYC_1:9
  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;

theorem :: MSSCYC_1:10
  for oc being non empty directed Chain of G holds len vertex-seq
  oc = len oc +1;

registration
  let G;
  let oc be directed non empty Chain of G;
  cluster vertex-seq oc -> non empty;
end;

theorem :: MSSCYC_1:11
  for oc being directed non empty Chain of G, n 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);

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

theorem :: MSSCYC_1:13
  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;

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

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

theorem :: MSSCYC_1:16
  for c, c1, c2 being directed non empty 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);

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

theorem :: MSSCYC_1:18
  for c being directed non empty Chain of G st c is cyclic for n
  ex ch being directed Chain of G st len ch = n & ch^c is directed non empty
  Chain of G;

definition

  let IT be Graph;
  attr IT is directed_cycle-less means
:: MSSCYC_1:def 3

  for dc being directed Chain of IT st dc is non empty holds dc is non cyclic;
end;

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

registration
  cluster void -> directed_cycle-less for Graph;
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 st for c being directed Chain of IT st c is non empty & (vertex-seq c).
  (len c +1) = v holds len c <= n;
end;

registration
  let G be void Graph;
  cluster -> empty for Chain of G;
end;

registration
  cluster void -> well-founded for Graph;
end;

registration
  cluster non well-founded -> non void for Graph;
end;

registration
  cluster well-founded for Graph;
end;

registration
  cluster well-founded -> directed_cycle-less for Graph;
end;

registration
  cluster non well-founded for Graph;
end;

registration
  cluster directed_cycle-less for Graph;
end;

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

begin :: Some properties of many sorted algebras

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

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

registration
  let S be non void non empty ManySortedSign, A be finitely-generated
  non-empty MSAlgebra over S;
  cluster non-empty finite-yielding for GeneratorSet of A;
end;

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

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

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

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

definition
  let IT be non void non empty 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;

theorem :: MSSCYC_1:25
  for S being non void non empty ManySortedSign, A being non-empty
  MSAlgebra over S, v be SortSymbol of S st S is finitely_operated holds
  Constants(A, v) is finite;

theorem :: MSSCYC_1:26
  for S being non void non empty ManySortedSign, X being non-empty
ManySortedSet of the carrier of S, 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);

theorem :: MSSCYC_1:27
  for S being non void non empty ManySortedSign, X being non-empty
  ManySortedSet of the carrier of S, v, vk being SortSymbol of S, o being
  OperSymbol of S, t being Element of (the Sorts of FreeMSA X).v, a being (
  ArgumentSeq of Sym(o,X)), k being Element of NAT, 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;