:: 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-2019 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, FINSEQ_6;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, GRAPH_1, GRAPH_2, MSAFREE, PBOOLE, FINSET_1, MSUALG_3,
      STRUCT_0;
 equalities MSAFREE;
 expansions TARSKI, GRAPH_1, GRAPH_2, MSAFREE, PBOOLE, FINSET_1, MSUALG_3;
 theorems TARSKI, NAT_1, ZFMISC_1, GRAPH_1, GRAPH_2, FUNCOP_1, FUNCT_1,
      FUNCT_2, FUNCT_6, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_5,
      CARD_1, CARD_3, TREES_1, TREES_3, TREES_4, PBOOLE, MSUALG_1, MSUALG_2,
      MSUALG_3, MSAFREE, MSAFREE2, MSATERM, EXTENS_1, INT_1, XBOOLE_0,
      XBOOLE_1, XREAL_1, XXREAL_0, PARTFUN1, RELAT_1, RELSET_1, XTUPLE_0,
      FINSEQ_6;
 schemes NAT_1, FRAENKEL, PBOOLE, DOMAIN_1;

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
    :Def1:
    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
  proof
    let c be FinSequence;
    hereby
      assume
A1:   c is Chain of G;
      then consider p being FinSequence such that
A2:   len p = len c + 1 and
A3:   for n st 1 <= n & n <= len p holds p.n in the carrier of G and
A4:   for n st 1 <= n & n <= len c ex x9, y9 being Element of the
carrier of G st x9 = p.n & y9 = p.(n+1) & c.n joins x9, y9 by GRAPH_1:def 14;
      thus c is FinSequence of the carrier' of G by A1;
      now
        let i be Nat;
        assume i in dom p;
        then
A5:     1<=i & i<=len p by FINSEQ_3:25;
        thus p.i in the carrier of G by A3,A5;
      end;
      then reconsider p as FinSequence of the carrier of G by FINSEQ_2:12;
      take p;
      thus p is_vertex_seq_of c
      proof
        thus len p = len c + 1 by A2;
        let n;
        assume that
A6:     1<=n and
A7:     n<=len c;
        n+1<=len p by A2,A7,XREAL_1:6;
        then
A8:     p/.(n+1)=p.(n+1) by FINSEQ_4:15,NAT_1:12;
        n<=len p & ex x9, y9 being Element of the carrier of G st x9 = p.
        n & y9 = p. (n+1) & c.n joins x9, y9 by A2,A4,A6,A7,NAT_1:12;
        hence thesis by A6,A8,FINSEQ_4:15;
      end;
    end;
    assume
A9: c is FinSequence of the carrier' of G;
    given p being FinSequence of the carrier of G such that
A10: p is_vertex_seq_of c;
    hereby
      let n;
      assume 1 <= n & n <= len c;
      then n in dom c by FINSEQ_3:25;
      then
A11:  c.n in rng c by FUNCT_1:def 3;
      rng c c= the carrier' of G by A9,FINSEQ_1:def 4;
      hence c.n in the carrier' of G by A11;
    end;
    take p;
    thus
A12: len p = len c + 1 by A10;
    hereby
      let n;
      assume 1 <= n & n <= len p;
      then n in dom p by FINSEQ_3:25;
      then
A13:  p.n in rng p by FUNCT_1:def 3;
      rng p c= the carrier of G by FINSEQ_1:def 4;
      hence p.n in the carrier of G by A13;
    end;
    let n;
    assume that
A14: 1 <= n and
A15: n <= len c;
    take x9=p/.n, y9=p/.(n+1);
    n<=len p & n+1<=len p by A12,A15,NAT_1:12,XREAL_1:6;
    hence x9 = p.n & y9 = p.(n+1) by A14,FINSEQ_4:15,NAT_1:12;
    thus thesis by A10,A14,A15;
  end;
end;

::$CT

theorem
  for p,q being FinSequence st n<=len p holds (1,n)-cut p = (1,n)-cut (p ^q)
proof
  let p,q be FinSequence;
  assume
A1: n<=len p;
  per cases;
  suppose
A2: n < 1;
    then (1,n)-cut p = {} by FINSEQ_6:def 4;
    hence thesis by A2,FINSEQ_6:def 4;
  end;
  suppose
A3: 1<=n;
    set cp = (1,n)-cut p, cpq = (1,n)-cut (p^q);
    now
A4:   len cp +1 = n+1 by A1,A3,FINSEQ_6:def 4;
      len (p^q) = len p + len q by FINSEQ_1:22;
      then
A5:   n<=len (p^q) by A1,NAT_1:12;
      then
A6:   len cpq +1 = n +1 by A3,FINSEQ_6:def 4;
      hence len cp = len cpq by A4;
      let k be Nat;
      assume that
A7:   1 <=k and
A8:   k <= len cp;
      k<=len p by A1,A4,A8,XXREAL_0:2;
      then
A9:   k in dom p by A7,FINSEQ_3:25;
      0+1 = 1;
      then
A10:  ex i being Nat st 0<=i & i<len cp & k=i+1 by A7,A8,FINSEQ_6:127;
      hence cp.k = p.k by A1,A3,FINSEQ_6:def 4
        .= (p^q).k by A9,FINSEQ_1:def 7
        .= cpq.k by A3,A5,A4,A6,A10,FINSEQ_6:def 4;
    end;
    hence thesis by FINSEQ_1:14;
  end;
end;

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

  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;
  existence
  proof
    set V = {1}, E = {};
    set S = the Function of E, V;
    reconsider G = MultiGraphStruct (# V, E, S, S #) as Graph;
    take G;
    thus the carrier' of G is empty;
  end;
end;

theorem Th2:
  for G being Graph holds rng (the Source of G) \/ rng (the Target
  of G) c= the carrier of G
proof
  let G be Graph;
  rng (the Source of G) c= the carrier of G & rng (the Target of G) c= the
  carrier of G by RELAT_1:def 19;
  hence thesis by XBOOLE_1:8;
end;

registration
  cluster finite simple connected non void strict for Graph;
  existence
  proof
    set V = {1,2}, E = {1};
    1 in V & 2 in V by TARSKI:def 2;
    then reconsider S = E --> 1, T = E --> 2 as Function of E, V by FUNCOP_1:45
;
    reconsider G = MultiGraphStruct(# V, E, S, T #) as Graph;
    take G;
    thus G is finite;
A1: 1 in E by TARSKI:def 1;
    then
A2: S.1 = 1 by FUNCOP_1:7;
    thus G is simple
    proof
      given x be set such that
A3:   x in the carrier' of G and
A4:   (the Source of G).x = (the Target of G).x;
      x = 1 by A3,TARSKI:def 1;
      hence contradiction by A1,A2,A4,FUNCOP_1:7;
    end;
A5: T.1 = 2 by A1,FUNCOP_1:7;
    thus G is connected
    proof
      set MSG = the MultiGraphStruct of G;
      given G1, G2 being Graph such that
A6:   (the carrier of G1) misses (the carrier of G2) and
A7:   G is_sum_of G1, G2;
A8:   the MultiGraphStruct of G = G1 \/ G2 by A7;
      set V1 = the carrier of G1, V2 = the carrier of G2;
      set T1 = the Target of G1, T2 = the Target of G2;
      set S1 = the Source of G1, S2 = the Source of G2;
      set E1 = the carrier' of G1, E2 = the carrier' of G2;
A9:   rng S1 \/ rng T1 c= V1 by Th2;
A10:  rng S2 \/ rng T2 c= V2 by Th2;
A11:  (the Target of G1) tolerates (the Target of G2) & (the Source of G1
      ) tolerates (the Source of G2) by A7;
      then
A12:  the carrier of MSG = (the carrier of G1) \/ (the carrier of G2) by A8,
GRAPH_1:def 5;
A13:  the carrier' of MSG = (the carrier' of G1) \/ (the carrier' of G2)
      by A11,A8,GRAPH_1:def 5;
      per cases by A13,ZFMISC_1:37;
      suppose
A14:    E1 = E & E2 = E;
        then S2.1 = S.1 by A1,A11,A8,GRAPH_1:def 5;
        then 1 in rng S2 by A1,A2,A14,FUNCT_2:4;
        then
A15:    1 in rng S2 \/ rng T2 by XBOOLE_0:def 3;
        S1.1 = S.1 by A1,A11,A8,A14,GRAPH_1:def 5;
        then 1 in rng S1 by A1,A2,A14,FUNCT_2:4;
        then 1 in rng S1 \/ rng T1 by XBOOLE_0:def 3;
        hence contradiction by A6,A9,A10,A15,XBOOLE_0:3;
      end;
      suppose
A16:    E1 = E & E2 = {};
        then T1.1 = T.1 by A1,A11,A8,GRAPH_1:def 5;
        then 2 in rng T1 by A1,A5,A16,FUNCT_2:4;
        then
A17:    2 in rng S1 \/ rng T1 by XBOOLE_0:def 3;
A18:    V1 c=V by A12,XBOOLE_1:7;
        S1.1 = S.1 by A1,A11,A8,A16,GRAPH_1:def 5;
        then 1 in rng S1 by A1,A2,A16,FUNCT_2:4;
        then 1 in rng S1 \/ rng T1 by XBOOLE_0:def 3;
        then V c=V1 by A9,A17,ZFMISC_1:32;
        then V = V1 by A18,XBOOLE_0:def 10;
        then V2 c=V1 by A12,XBOOLE_1:7;
        hence contradiction by A6,XBOOLE_1:67;
      end;
      suppose
A19:    E1 = {} & E2 = E;
        then T2.1 = T.1 by A1,A11,A8,GRAPH_1:def 5;
        then 2 in rng T2 by A1,A5,A19,FUNCT_2:4;
        then
A20:    2 in rng S2 \/ rng T2 by XBOOLE_0:def 3;
A21:    V2 c=V by A12,XBOOLE_1:7;
        S2.1 = S.1 by A1,A11,A8,A19,GRAPH_1:def 5;
        then 1 in rng S2 by A1,A2,A19,FUNCT_2:4;
        then 1 in rng S2 \/ rng T2 by XBOOLE_0:def 3;
        then V c=V2 by A10,A20,ZFMISC_1:32;
        then V = V2 by A21,XBOOLE_0:def 10;
        then V1 c=V2 by A12,XBOOLE_1:7;
        hence contradiction by A6,XBOOLE_1:67;
      end;
    end;
    thus G is non void;
    thus thesis;
  end;
end;

theorem Th3:
  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
  let e be set;
  let s, t be Element of the carrier of G;
  assume
A1: s = (the Source of G).e & t = (the Target of G).e;
  set c = <*e*>;
  set vs = <*s, t*>;
A2: vs/.(1+1) = t by FINSEQ_4:17;
A3: len c = 1 by FINSEQ_1:39;
  hence len vs = len c + 1 by FINSEQ_1:44;
  let n be Nat;
  assume 1<=n & n<=len c;
  then
A4: n = 1 by A3,XXREAL_0:1;
  c.1 = e & vs/.1 = s by FINSEQ_1:40,FINSEQ_4:17;
  hence thesis by A1,A4,A2;
end;

theorem Th4:
  for e being set st e in the carrier' of G holds <*e*> is directed Chain of G
proof
  let e be set;
  assume
A1: e in the carrier' of G;
  then reconsider
  s = (the Source of G).e, t = (the Target of G).e as Element of
  the carrier of G by FUNCT_2:5;
  reconsider E = the carrier' of G as non empty set by A1;
  reconsider e as Element of E by A1;
  <*s,t*> is_vertex_seq_of <*e*> by Th3;
  then reconsider c = <*e*> as Chain of G by Def1;
  c is directed
  by FINSEQ_1:39;
  hence thesis;
end;

reserve G for non void Graph;

registration
  let G;
  cluster directed non empty one-to-one for Chain of G;
  existence
  proof
    set e = the Element of the carrier' of G;
    reconsider c = <*e*> as directed Chain of G by Th4;
    take c;
    thus c is directed;
    thus c is non empty;
    let n, m be Nat;
    assume that
A1: 1 <= n & n < m and
A2: m <= len c;
    1 < m by A1,XXREAL_0:2;
    hence thesis by A2,FINSEQ_1:39;
  end;
end;

Lm1: for G being non empty Graph, c being Chain of G, 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
  let G be non empty Graph;
  let c be Chain of G, p be FinSequence of the carrier of G;
  assume that
A1: c is cyclic and
A2: p is_vertex_seq_of c;
  consider P being FinSequence of the carrier of G such that
A3: P is_vertex_seq_of c and
A4: P.1 = P.(len P) by A1;
  per cases;
  suppose
    card the carrier of G = 1 or c <>{} & not c alternates_vertices_in G;
    then P = vertex-seq c & p = vertex-seq c by A2,A3,GRAPH_2:def 8;
    hence thesis by A4;
  end;
  suppose
A5: not(card the carrier of G =1 or c <>{}&not c alternates_vertices_in G);
A6: len p = len c+1 by A2;
A7: len P = len c +1 by A3;
    now
      per cases by A5;
      suppose
        card the carrier of G <>1& c ={};
        then len c =0;
        hence thesis by A6;
      end;
      suppose
A8:     card the carrier of G <>1 & c alternates_vertices_in G;
        then
A9:     p is TwoValued Alternating & P is TwoValued Alternating by A2,A3,
GRAPH_2:37;
        now
          set S=the Source of G, T=the Target of G;
          assume p<>P;
A10:      rng p ={S.(c.1),T.(c.1)} by A2,A8,GRAPH_2:36;
A11:      1<=len p by A6,NAT_1:11;
          then len p in dom p by FINSEQ_3:25;
          then p.(len p) in rng p by FUNCT_1:def 3;
          then
A12:      p.(len p) = S.(c.1) or p.(len p) = T.(c.1) by A10,TARSKI:def 2;
A13:      rng P ={S.(c.1),T.(c.1)} by A3,A8,GRAPH_2:36;
          1 in dom P by A6,A7,A11,FINSEQ_3:25;
          then P.1 in rng p by A10,A13,FUNCT_1:def 3;
          then
A14:      P.1 = S.(c.1) or P.1 = T.(c.1) by A10,TARSKI:def 2;
          1 in dom p by A11,FINSEQ_3:25;
          then p.1 in rng p by FUNCT_1:def 3;
          then p.1 = S.(c.1) or p.1 = T.(c.1) by A10,TARSKI:def 2;
          hence thesis by A4,A6,A7,A9,A10,A13,A11,A12,A14,FINSEQ_6:147;
        end;
        hence thesis by A4;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th5:
  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) by Lm1;

theorem Th6:
  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*>
proof
  let G be Graph;
  let e be set;
  assume e in the carrier' of G;
  then reconsider
  so = (the Source of G).e, ta = (the Target of G).e as Element of
  the carrier of G by FUNCT_2:5;
  reconsider sota = <*so, ta*> as FinSequence of the carrier of G;
  let fe be directed Chain of G;
  assume
A1: fe = <*e*>;
  then
A2: len fe = 1 by FINSEQ_1:39;
A3: sota is_vertex_seq_of fe
  proof
    thus len sota = len fe + 1 by A2,FINSEQ_1:44;
    let n;
A4: sota/.2=ta by FINSEQ_4:17;
    assume 1<=n & n<=len fe;
    then
A5: n=1 by A2,XXREAL_0:1;
    e joins so, ta & sota/.1 = so by FINSEQ_4:17;
    hence thesis by A1,A5,A4,FINSEQ_1:40;
  end;
  e = fe.1 by A1,FINSEQ_1:40;
  then sota.1 = (the Source of G).(fe.1) by FINSEQ_1:44;
  hence thesis by A1,A3,GRAPH_2:def 10;
end;

theorem
  for f being FinSequence holds len (m,n)-cut f <= len f
proof
  let f be FinSequence;
  set lmnf = len (m,n)-cut f;
  set lf = len f;
  per cases;
  suppose
A1: 1<=m & m<=n & n<=len f;
    then lmnf +m = n+1 by FINSEQ_6:def 4;
    then n+(lmnf +m) <= n+1+lf by A1,XREAL_1:6;
    then n+(lmnf +m) <= n+(1+lf);
    then lmnf +m <= 1+lf by XREAL_1:6;
    then (lmnf +m)+1 <= m+(1+lf) by A1,XREAL_1:7;
    then lmnf +(m+1) <= m+1+lf;
    hence thesis by XREAL_1:6;
  end;
  suppose
    not (1<=m & m<=n & n<=len f);
    then (m,n)-cut f is empty by FINSEQ_6:def 4;
    hence thesis;
  end;
end;

theorem
  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
  let c be directed Chain of G;
  assume that
A1: 1<=m and
A2: m<=n and
A3: n<=len c;
  reconsider mnc = (m,n)-cut c as Chain of G by A1,A2,A3,GRAPH_2:41;
A4: len mnc +m = n+1 by A1,A2,A3,FINSEQ_6:def 4;
  now
A5: len mnc +m<=len c +1 by A3,A4,XREAL_1:6;
    let k;
    assume that
A6: 1 <= k and
A7: k < len mnc;
    0+1<=k by A6;
    then consider i being Nat such that
    0<=i and
A8: i<len mnc and
A9: k=i+1 by A7,FINSEQ_6:127;
A10: 1<=m+i by A1,NAT_1:12;
    m+(i+1)<len mnc +m by A7,A9,XREAL_1:6;
    then m+i+1 < len c + 1 by A5,XXREAL_0:2;
    then
A11: m+i<len c by XREAL_1:6;
A12: mnc.(k+1) = c.(m+k) by A1,A2,A3,A7,FINSEQ_6:def 4;
    mnc.(i+1) = c.(m+i) & m+k = (m+i)+1 by A1,A2,A3,A8,A9,FINSEQ_6:def 4;
    hence (the Source of G).(mnc.(k+1)) = (the Target of G).(mnc.k) by A12,A10
,A11,GRAPH_1:def 15;
  end;
  hence thesis by GRAPH_1:def 15;
end;

theorem Th9:
  for oc being non empty directed Chain of G holds len vertex-seq
  oc = len oc +1
proof
  let oc be non empty directed Chain of G;
  vertex-seq oc is_vertex_seq_of oc by GRAPH_2:def 10;
  hence thesis;
end;

registration
  let G;
  let oc be directed non empty Chain of G;
  cluster vertex-seq oc -> non empty;
  coherence
  proof
    len vertex-seq oc = len oc +1 by Th9;
    hence thesis;
  end;
end;

theorem Th10:
  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)
proof
  let oc be directed non empty Chain of G;
  set vsoc = vertex-seq oc, S = the Source of G, T = the Target of G;
  defpred P[Nat] means 1<=$1 & $1<=len oc implies vsoc.$1 = S.(oc.
  $1) & vsoc.($1+1) = T.(oc.$1);
A1: for k be Nat st P[k] holds P[k+1]
  proof
    let n;
    assume
A2: 1<=n & n<=len oc implies vsoc.n = S.(oc.n) & vsoc.(n+1) = T.(oc.n);
A3: vsoc is_vertex_seq_of oc by GRAPH_2:def 10;
    assume that
A4: 1<=n+1 and
A5: n+1<=len oc;
    per cases;
    suppose
A6:   n=0;
      hence
A7:   vsoc.(n+1) = S.(oc.(n+1)) by GRAPH_2:def 10;
      1 in dom vsoc by FINSEQ_5:6;
      then
A8:   vsoc/.1=vsoc.1 by PARTFUN1:def 6;
A9:  1<=len oc by A4,A5,XXREAL_0:2;
      len vsoc = len oc +1 by Th9;
      then 1+1<=len vsoc by A9,XREAL_1:6;
      then 1+1 in dom vsoc by FINSEQ_3:25;
      then
A10:  vsoc/.(1+1)=vsoc.(1+1) by PARTFUN1:def 6;
      oc.1 joins vsoc/.1,vsoc/.(1+1) by A3,A9;
      hence thesis by A6,A7,A8,A10;
    end;
    suppose
A11:  n<>0;
A12:  n<len oc by A5,NAT_1:13;
      1<=n by A11,NAT_1:14;
      hence
A13:  vsoc.(n+1) = S.(oc.(n+1)) by A2,A12,GRAPH_1:def 15;
A14:  len vsoc = len oc +1 by Th9;
      then 1<=n+1+1 & n+1+1<=len vsoc by A5,NAT_1:11,XREAL_1:6;
      then n+1+1 in dom vsoc by FINSEQ_3:25;
      then
A15:  vsoc/.(n+1+1)=vsoc.(n+1+1) by PARTFUN1:def 6;
      n<=n+1 by NAT_1:11;
      then n<=len oc by A5,XXREAL_0:2;
      then n+1<=len vsoc by A14,XREAL_1:6;
      then n+1 in dom vsoc by A4,FINSEQ_3:25;
      then
A16:  vsoc/.(n+1)=vsoc.(n+1) by PARTFUN1:def 6;
      oc.(n+1) joins vsoc/.(n+1),vsoc/.(n+1+1) by A4,A5,A3;
      hence thesis by A13,A16,A15;
    end;
  end;
A17: P[ 0 ];
  thus for n holds P[n] from NAT_1:sch 2 (A17, A1);
end;

theorem Th11:
  for f being non empty FinSequence st 1<=m & m<=n & n<=len f
  holds (m,n)-cut f is non empty
proof
  let f be non empty FinSequence;
  set lmn = len (m,n)-cut f;
  assume 1<=m & m<=n & n<=len f;
  then m<n+1 & lmn+m = n+1 by FINSEQ_6:def 4,NAT_1:13;
  then m-(lmn+m)<(n+1)-(n+1) by XREAL_1:9;
  then --lmn>0;
  hence thesis;
end;

theorem
  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
  let c, c1 be directed Chain of G;
  assume that
A1: 1<=m and
A2: m<=n and
A3: n<=len c and
A4: c1 = (m,n)-cut c;
  set mn1c=(m,n+1)-cut vertex-seq c;
A5: c is non empty by A1,A2,A3;
  then
A6: vertex-seq c is_vertex_seq_of c by GRAPH_2:def 10;
  then
A7: mn1c is_vertex_seq_of c1 by A1,A2,A3,A4,GRAPH_2:42;
  set vsc = vertex-seq c;
A8: m<=n+1 by A2,NAT_1:12;
A9: len vsc = len c +1 by A6;
  then
A10: n+1<=len vsc by A3,XREAL_1:6;
A11: c1 is non empty by A1,A2,A3,A4,A5,Th11;
  then 0<len c1;
  then
A12: c1.(0+1) = c.(m+0) by A1,A2,A3,A4,FINSEQ_6:def 4;
A13: m<=n+1 by A2,NAT_1:12;
  vsc is non empty by A9;
  then mn1c is non empty by A1,A8,A10,Th11;
  then 0<len mn1c;
  then
A14: vsc.(m+0) = mn1c.(0+1) by A1,A10,A13,FINSEQ_6:def 4;
  m<=len c by A2,A3,XXREAL_0:2;
  then mn1c.1 = (the Source of G).(c1.1) by A1,A5,A12,A14,Th10;
  hence thesis by A7,A11,GRAPH_2:def 10;
end;

theorem Th13:
  for oc being directed non empty Chain of G holds (vertex-seq oc)
  .(len oc +1) = (the Target of G).(oc.len oc)
proof
  let oc be directed non empty Chain of G;
  1 in dom oc by FINSEQ_5:6;
  then 1<=len oc by FINSEQ_3:25;
  hence thesis by Th10;
end;

theorem Th14:
  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
proof
  let c1, c2 be directed non empty Chain of G;
  set vsc1 = vertex-seq c1, vsc2 = vertex-seq c2;
A1: len (c1^c2) = len c1 + len c2 by FINSEQ_1:22;
A2: vsc1 is_vertex_seq_of c1 by GRAPH_2:def 10;
  then
A3: vsc2 is_vertex_seq_of c2 & len vsc1 = len c1 +1 by GRAPH_2:def 10;
  hereby
    assume
A4: (vertex-seq c1).(len c1 + 1) = (vertex-seq c2).1;
    then reconsider c1c2 = c1^c2 as Chain of G by A2,A3,GRAPH_2:43;
    c1c2 is directed
    proof
      let n;
      assume that
A5:   1 <= n and
A6:   n < len c1c2;
      per cases by XXREAL_0:1;
      suppose
A7:     n<len c1;
        then 1<=n+1 & n+1<=len c1 by NAT_1:11,13;
        then n+1 in dom c1 by FINSEQ_3:25;
        then
A8:     c1c2.(n+1) = c1.(n+1) by FINSEQ_1:def 7;
        n in dom c1 by A5,A7,FINSEQ_3:25;
        then c1c2.n = c1.n by FINSEQ_1:def 7;
        hence thesis by A5,A7,A8,GRAPH_1:def 15;
      end;
      suppose
A9:     n=len c1;
        then n in dom c1 by FINSEQ_5:6;
        then
A10:    c1c2.n = c1.n by FINSEQ_1:def 7;
        1 in dom c2 by FINSEQ_5:6;
        then
A11:    c1c2.(n+1) = c2.1 by A9,FINSEQ_1:def 7;
        vsc1.(len c1 +1) =(the Target of G).(c1.(len c1)) by Th13;
        hence thesis by A4,A9,A11,A10,GRAPH_2:def 10;
      end;
      suppose
A12:    n>len c1;
        then reconsider k = n-len c1 as Element of NAT by INT_1:5;
A13:    n = len c1 + k;
A14:    n+1 = len c1 +(k+1);
A15:    k<len c2 by A1,A6,XREAL_1:19;
        then 1<=k+1 & k+1<=len c2 by NAT_1:11,13;
        then k+1 in dom c2 by FINSEQ_3:25;
        then
A16:    c1c2.(n+1) = c2.(k+1) by A14,FINSEQ_1:def 7;
        n>=len c1 +1 by A12,NAT_1:13;
        then
A17:    1<=k by XREAL_1:19;
        then k in dom c2 by A15,FINSEQ_3:25;
        then c1c2.n = c2.k by A13,FINSEQ_1:def 7;
        hence thesis by A17,A15,A16,GRAPH_1:def 15;
      end;
    end;
    hence c1^c2 is directed non empty Chain of G;
  end;
  set n = len c1;
  assume c1^c2 is directed non empty Chain of G;
  then reconsider c1c2 = c1^c2 as directed non empty Chain of G;
A18: n<len c1c2 by A1,XREAL_1:29;
A19: n in dom c1 by FINSEQ_5:6;
  then
A20: c1c2.n = c1.n by FINSEQ_1:def 7;
  1<=n by A19,FINSEQ_3:25;
  then
A21: (the Source of G).(c1c2.(n+1)) = (the Target of G).(c1c2.n) by A18,
GRAPH_1:def 15;
  1 in dom c2 by FINSEQ_5:6;
  then
A22: c1c2.(n+1) = c2.1 by FINSEQ_1:def 7;
  vsc1.(len c1 +1) =(the Target of G).(c1.(len c1)) by Th13;
  hence thesis by A21,A22,A20,GRAPH_2:def 10;
end;

theorem Th15:
  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)
proof
  let c, c1, c2 be directed non empty Chain of G;
  1 in dom c by FINSEQ_5:6;
  then 1<=len c by FINSEQ_3:25;
  then
A1: (vertex-seq c).1 = (the Source of G).(c.1) & (vertex-seq c).(len c +1)
  = ( the Target of G).(c.len c) by Th10;
A2: 1 in dom c1 by FINSEQ_5:6;
  then 1<=len c1 by FINSEQ_3:25;
  then
A3: (vertex-seq c1).1 = (the Source of G).(c1.1) by Th10;
  1 in dom c2 by FINSEQ_5:6;
  then 1<=len c2 by FINSEQ_3:25;
  then
A4: (vertex-seq c2).(len c2 +1) = (the Target of G).(c2.len c2) by Th10;
  assume
A5: c =c1^c2;
  then len c2 in dom c2 & len c = len c1 + len c2 by FINSEQ_1:22,FINSEQ_5:6;
  hence thesis by A5,A2,A3,A1,A4,FINSEQ_1:def 7;
end;

theorem Th16:
  for oc being directed non empty Chain of G st oc is cyclic holds
  (vertex-seq oc).1 = (vertex-seq oc).(len oc +1)
proof
  let oc be directed non empty Chain of G;
  assume
A1: oc is cyclic;
  set vsoc = vertex-seq oc;
A2: vsoc is_vertex_seq_of oc by GRAPH_2:def 10;
  thus thesis by A1,A2,Th5;
end;

theorem Th17:
  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
proof
  let c be directed non empty Chain of G;
  defpred Z[Nat] means ex ch being directed Chain of G st rng ch c=
  rng c & len ch = $1 & ch^c is directed non empty Chain of G;
  c is FinSequence of the carrier' of G by Def1;
  then
A1: rng c c= the carrier' of G by FINSEQ_1:def 4;
  assume
A2: c is cyclic;
A3: for i be Nat st Z[i] holds Z[i+1]
  proof
    len c in dom c by FINSEQ_5:6;
    then
A4: c.len c in rng c by FUNCT_1:def 3;
    then reconsider clc = c.len c as Element of the carrier' of G by A1;
    reconsider ch9= <*clc*> as directed Chain of G by Th4;
A5: rng ch9 = {c.len c} by FINSEQ_1:38;
    then
A6: rng ch9 c= rng c by A4,ZFMISC_1:31;
A7: len ch9 = 1 by FINSEQ_1:39;
    let n be Nat;
    given ch being directed Chain of G such that
A8: rng ch c= rng c and
A9: len ch = n and
A10: ch^c is directed non empty Chain of G;
    per cases;
    suppose
A11:  n = 0;
      take ch9;
      thus rng ch9 c= rng c by A4,A5,ZFMISC_1:31;
      thus len ch9 = n+1 by A11,FINSEQ_1:39;
      set vsch9 = vertex-seq ch9;
      vsch9 = <*(the Source of G).clc, (the Target of G).clc*> by Th6;
      then vsch9.(len ch9 +1) = (the Target of G).clc by A7,FINSEQ_1:44
        .= (vertex-seq c).(len c +1) by Th13
        .= (vertex-seq c).1 by A2,Th16;
      hence thesis by Th14;
    end;
    suppose
      n<>0;
      then
A12:  ch is non empty by A9;
      then 1 in dom ch by FINSEQ_5:6;
      then ch.1 in rng ch by FUNCT_1:def 3;
      then consider i being Nat such that
A13:  i in dom c and
A14:  c.i = ch.1 by A8,FINSEQ_2:10;
A15:  i<=len c by A13,FINSEQ_3:25;
A16:  1<=i by A13,FINSEQ_3:25;
      now
        per cases;
        suppose
A17:      i = 1;
          set vsch9 = vertex-seq ch9;
          vsch9 = <*(the Source of G).clc, (the Target of G).clc*> by Th6;
          then vsch9.(len ch9 +1) = (the Target of G).clc by A7,FINSEQ_1:44
            .= (vertex-seq c).(len c +1) by Th13
            .= (vertex-seq c).1 by A2,Th16
            .= (the Source of G).(ch.1) by A14,A17,GRAPH_2:def 10
            .= (vertex-seq ch).1 by A12,GRAPH_2:def 10;
          then reconsider ch1 = ch9^ch as directed Chain of G by A12,Th14;
          take ch1;
          rng ch1 = rng ch9 \/ rng ch by FINSEQ_1:31;
          hence rng ch1 c= rng c by A8,A6,XBOOLE_1:8;
          thus len ch1 = n+1 by A9,A7,FINSEQ_1:22;
          (vertex-seq ch1).(len ch1 +1) = (vertex-seq ch).(len ch +1) by A12
,Th15
            .= (vertex-seq c).1 by A10,A12,Th14;
          hence ch1^c is directed non empty Chain of G by Th14;
        end;
        suppose
          i <> 1;
          then 1<i by A16,XXREAL_0:1;
          then 1+1<=i by NAT_1:13;
          then consider k being Nat such that
A18:      1<=k & k<len c and
A19:      i=k+1 by A15,FINSEQ_6:127;
          k in dom c by A18,FINSEQ_3:25;
          then
A20:      c.k in rng c by FUNCT_1:def 3;
          then reconsider ck = c.k as Element of the carrier' of G by A1;
          reconsider ch9= <*ck*> as directed Chain of G by Th4;
          set vsch9 = vertex-seq ch9;
A21:      len ch9 = 1 by FINSEQ_1:39;
          vsch9 = <*(the Source of G).ck, (the Target of G).ck*> by Th6;
          then vsch9.(len ch9 +1) = (the Target of G).ck by A21,FINSEQ_1:44
            .= (the Source of G).(ch.1) by A14,A18,A19,GRAPH_1:def 15
            .= (vertex-seq ch).1 by A12,GRAPH_2:def 10;
          then reconsider ch1 = ch9^ch as directed Chain of G by A12,Th14;
          take ch1;
          rng ch9 = {c.k} by FINSEQ_1:38;
          then
A22:      rng ch9 c= rng c by A20,ZFMISC_1:31;
          rng ch1 = rng ch9 \/ rng ch by FINSEQ_1:31;
          hence rng ch1 c= rng c by A8,A22,XBOOLE_1:8;
          thus len ch1 = n+1 by A9,A21,FINSEQ_1:22;
          (vertex-seq ch1).(len ch1 +1) = (vertex-seq ch).(len ch +1) by A12
,Th15
            .= (vertex-seq c).1 by A10,A12,Th14;
          hence ch1^c is directed non empty Chain of G by Th14;
        end;
      end;
      hence thesis;
    end;
  end;
  let n be Nat;
A23: Z[ 0 ]
  proof
    reconsider ch = {} as empty Chain of G by GRAPH_1:14;
    reconsider ch as directed Chain of G;
    take ch;
    thus rng ch c= rng c;
    thus len ch = 0;
    thus thesis by FINSEQ_1:34;
  end;
  for n being Nat holds Z[n] from NAT_1:sch 2 (A23, A3);
  then ex ch being directed Chain of G st rng ch c= rng c & len ch = n & ch^c
  is directed non empty Chain of G;
  hence thesis;
end;

definition

  let IT be Graph;
  attr IT is directed_cycle-less means

  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;
  coherence
  proof
    let G be Graph;
    assume
A1: G is void;
    let c be directed Chain of G;
    assume
A2: c is non empty;
    c is FinSequence of the carrier' of G by Def1;
    hence thesis by A1,A2;
  end;
end;

definition
  let IT be Graph;
  attr IT is well-founded means

  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;
  coherence
  proof
    let c be Chain of G;
    assume
A1: c is non empty;
    c is FinSequence of the carrier' of G by Def1;
    hence thesis by A1;
  end;
end;

registration
  cluster void -> well-founded for Graph;
  coherence
  proof
    let G be Graph;
    assume G is void;
    then reconsider G9 = G as void Graph;
    let v be Element of the carrier of G;
    take 0;
    let c be directed Chain of G;
    reconsider c as Chain of G9;
    c is empty;
    hence thesis;
  end;
end;

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

registration
  cluster well-founded for Graph;
  existence
  proof
    set G = the void Graph;
    G is well-founded;
    hence thesis;
  end;
end;

registration
  cluster well-founded -> directed_cycle-less for Graph;
  coherence
  proof
    let G be Graph;
    per cases;
    suppose
      G is void;
      then reconsider G as void Graph;
      G is directed_cycle-less;
      hence thesis;
    end;
    suppose
      G is non void;
      then reconsider G9=G as non void Graph;
      assume that
A1:   G is well-founded and
A2:   G is non directed_cycle-less;
      consider dc being directed Chain of G9 such that
A3:   dc is non empty and
A4:   dc is cyclic by A2;
      set p = vertex-seq dc;
      len p = len dc +1 by A3,Th9;
      then 1<=len p by NAT_1:11;
      then 1 in dom p by FINSEQ_3:25;
      then reconsider v = p.1 as Element of the carrier of G by FINSEQ_2:11;
      consider n such that
A5:   for c being directed Chain of G9 st c is non empty & (
      vertex-seq c).(len c +1) = v holds len c <= n by A1;
      consider ch being directed Chain of G9 such that
A6:   len ch = n+1 and
A7:   ch^dc is directed non empty Chain of G9 by A3,A4,Th17;
      reconsider ch as directed non empty Chain of G9 by A6;
      reconsider cc = ch^dc as directed non empty Chain of G9 by A7;
      (vertex-seq dc).1 = (vertex-seq dc).(len dc +1) by A3,A4,Th16;
      then (vertex-seq cc).(len cc +1) = v by A3,Th15;
      then
A8:   len cc <=n by A5;
      len cc = n+1 + len dc by A6,FINSEQ_1:22;
      then n+1<=len cc by NAT_1:11;
      hence contradiction by A8,NAT_1:13;
    end;
  end;
end;

registration
  cluster non well-founded for Graph;
  existence
  proof
    set V = {1}, E = {1};
    reconsider j = 1 as Element of V by TARSKI:def 1;
    reconsider S = E --> j, T = E --> j as Function of E, V;
    reconsider G = MultiGraphStruct(# V, E, S, T #) as Graph;
    reconsider v = 1 as Element of the carrier of G;
    take G;
A1: S.1 = 1 by FUNCOP_1:7;
A2: G is with_directed_cycle
    proof
      reconsider dc = <*1*> as directed Chain of G by Th4;
      take dc;
      thus dc is non empty;
A3:   <*v,v*>.2 = v & len <*v,v*> = 2 by FINSEQ_1:44;
      <*v,v*> is_vertex_seq_of dc & <*v,v*>.1 = v by A1,Th3,FINSEQ_1:44;
      hence thesis by A3;
    end;
    assume G is well-founded;
    then reconsider G as well-founded Graph;
    G is directed_cycle-less;
    hence contradiction by A2;
  end;
end;

registration
  cluster directed_cycle-less for Graph;
  existence
  proof
    set G = the well-founded Graph;
    G is directed_cycle-less;
    hence thesis;
  end;
end;

theorem
  for t being DecoratedTree, p being Node of t, k being Element of NAT
  holds p|k is Node of t
proof
  let t be DecoratedTree, p be Node of t, k be Element of NAT;
  p|k = p|Seg k by FINSEQ_1:def 15;
  then p|k is_a_prefix_of p by TREES_1:def 1;
  hence thesis by TREES_1:20;
end;

begin :: Some properties of many sorted algebras

theorem
  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]
proof
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet
  of the carrier of S, t be Term of S,X;
  assume
A1: t is not root;
  per cases by MSATERM:2;
  suppose
    ex s being SortSymbol of S,v being Element of X.s st t.{} = [v,s];
    then consider s being SortSymbol of S, v being Element of X.s such that
A2: t.{} = [v,s];
    t = root-tree [v,s] by A2,MSATERM:5;
    hence thesis by A1;
  end;
  suppose
    t.{} in [:the carrier' of S,{the carrier of S}:];
    then consider o, c being object such that
A3: o in the carrier' of S and
A4: c in {the carrier of S} & t.{} = [o,c] by ZFMISC_1:def 2;
    reconsider o as OperSymbol of S by A3;
    take o;
    thus thesis by A4,TARSKI:def 1;
  end;
end;

theorem Th20:
  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
proof
  let S be non void non empty ManySortedSign, A be MSAlgebra over S, G be
  GeneratorSet of A, B be MSSubset of A;
  B is MSSubset of GenMSAlg B by MSUALG_2:def 17;
  then
A1: B c= the Sorts of GenMSAlg B by PBOOLE:def 18;
  assume G c= B;
  then G c= the Sorts of GenMSAlg B by A1,PBOOLE:13;
  then G is MSSubset of GenMSAlg B by PBOOLE:def 18;
  then GenMSAlg G is MSSubAlgebra of GenMSAlg B by MSUALG_2:def 17;
  then the Sorts of GenMSAlg G is MSSubset of GenMSAlg B by MSUALG_2:def 9;
  then
A2: the Sorts of GenMSAlg G c= the Sorts of GenMSAlg B by PBOOLE:def 18;
A3: the Sorts of GenMSAlg(G) = the Sorts of A by MSAFREE:def 4;
  then the Sorts of GenMSAlg B is MSSubset of GenMSAlg G by MSUALG_2:def 9;
  then the Sorts of GenMSAlg B c= the Sorts of GenMSAlg G by PBOOLE:def 18;
  hence the Sorts of GenMSAlg(B) = the Sorts of A by A3,A2,PBOOLE:146;
end;

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;
  existence
  proof
    consider G being GeneratorSet of A such that
A1: G is finite-yielding by MSAFREE2:def 10;
    consider B being ManySortedSet of the carrier of S such that
A2: B in the Sorts of A by PBOOLE:134;
    deffunc F(object) = {B.$1};
    consider C being ManySortedSet of the carrier of S such that
A3: for i being object st i in the carrier of S holds C.i = F(i) from
    PBOOLE:sch 4;
    set H = G (\/) C;
    now
      let i be object;
      assume
A4:   i in the carrier of S;
      then B.i in (the Sorts of A).i by A2;
      then {B.i} c= (the Sorts of A).i by ZFMISC_1:31;
      hence C.i c= (the Sorts of A).i by A3,A4;
    end;
    then G c= the Sorts of A & C c= the Sorts of A by PBOOLE:def 18;
    then
A5: C c= H & G (\/) C c= the Sorts of A by PBOOLE:14,16;
    now
      let i be object;
      assume i in the carrier of S;
      then C.i = {B.i} by A3;
      hence C.i is non empty;
    end;
    then C is non-empty;
    then reconsider H as non-empty MSSubset of A by A5,PBOOLE:131,def 18;
    G c= H by PBOOLE:14;
    then reconsider H as GeneratorSet of A by Th20;
    take H;
    thus H is non-empty;
    let i be object;
    assume
A6: i in the carrier of S;
    then
A7: C.i = {B.i} by A3;
A8: H.i = G.i \/ C.i by A6,PBOOLE:def 4;
    G.i is finite by A1;
    hence thesis by A7,A8;
  end;
end;

theorem Th21:
  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
proof
  let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S,
  X be non-empty GeneratorSet of A;
  reconsider X9 = X as MSSubset of A;
  now
    let i be object such that
A1: i in the carrier of S;
A2: (Reverse X).i is Function of (FreeGen X).i, X.i by A1,PBOOLE:def 15;
    X c= the Sorts of A by PBOOLE:def 18;
    then X.i c= (the Sorts of A).i by A1;
    hence
    (Reverse X).i is Function of (FreeGen X).i, (the Sorts of A).i by A1,A2,
FUNCT_2:7;
  end;
  then reconsider
  ff = Reverse X as ManySortedFunction of FreeGen X,the Sorts of A
  by PBOOLE:def 15;
  FreeGen X is free by MSAFREE:16;
  then consider h being ManySortedFunction of FreeMSA X, A such that
A3: h is_homomorphism FreeMSA X, A and
A4: h || FreeGen X = ff;
  take h;
  thus h is_homomorphism FreeMSA X, A by A3;
  let i be set;
  assume i in the carrier of S;
  then reconsider s = i as SortSymbol of S;
  set f = h.s;
  consider g being ManySortedFunction of FreeMSA X, Image h such that
A5: h = g and
A6: g is_epimorphism FreeMSA X, Image h by A3,MSUALG_3:21;
A7: g is_homomorphism FreeMSA X, Image h by A6;
A8: Image g = Image h by A6,MSUALG_3:19;
  X is MSSubset of Image h
  proof
    let i be object;
    assume
A9: i in the carrier of S;
    then reconsider s = i as SortSymbol of S;
    s in dom Reverse X by A9,PARTFUN1:def 2;
    then
A10: rngs Reverse X = X & (rngs Reverse X).s = rng ((Reverse X).s) by
EXTENS_1:10,FUNCT_6:22;
    reconsider hs = h.s as Function of (the Sorts of FreeMSA X).s, (the Sorts
    of A).s;
    let x be object;
    FreeGen X c= the Sorts of FreeMSA X by PBOOLE:def 18;
    then
A11: (FreeGen X).s c= (the Sorts of FreeMSA X).s;
    the Sorts of Image h = h.:.:(the Sorts of FreeMSA X) by A3,MSUALG_3:def 12;
    then
A12: (the Sorts of Image h).s = hs.:((the Sorts of FreeMSA X).s) by
PBOOLE:def 20;
    assume x in X.i;
    then consider c being object such that
A13: c in dom (ff.s) and
A14: x = ff.s.c by A10,FUNCT_1:def 3;
A15: ff.s = hs | ((FreeGen X).s) by A4,MSAFREE:def 1;
    then dom (ff.s) = dom hs /\ (FreeGen X).s by RELAT_1:61;
    then
A16: c in (FreeGen X).s & c in dom hs by A13,XBOOLE_0:def 4;
    x = hs.c by A15,A13,A14,FUNCT_1:47;
    hence thesis by A12,A11,A16,FUNCT_1:def 6;
  end;
  then GenMSAlg X9 is MSSubAlgebra of Image h by MSUALG_2:def 17;
  then the Sorts of GenMSAlg X9 is MSSubset of Image h by MSUALG_2:def 9;
  then
A17: the Sorts of GenMSAlg X9 c= the Sorts of Image h by PBOOLE:def 18;
  the Sorts of Image g = h.:.:(the Sorts of FreeMSA X) by A5,A7,MSUALG_3:def 12
;
  then
A18: (the Sorts of Image g).i = f.:((the Sorts of FreeMSA X).i) by
PBOOLE:def 20;
  the Sorts of Image h is MSSubset of A by MSUALG_2:def 9;
  then
  the Sorts of GenMSAlg X9 = the Sorts of A & the Sorts of Image h c= the
  Sorts of A by MSAFREE:def 4,PBOOLE:def 18;
  then the Sorts of Image h = the Sorts of A by A17,PBOOLE:146;
  hence thesis by A18,A8,RELSET_1:22;
end;

theorem
  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
proof
  let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S,
  X be non-empty GeneratorSet of A such that
A1: A is non finite-yielding and
A2: FreeMSA X is finite-yielding;
  the Sorts of A is non finite-yielding by A1,MSAFREE2:def 11;
  then consider i being object such that
A3: i in the carrier of S and
A4: (the Sorts of A).i is infinite;
  the Sorts of FreeMSA X is finite-yielding by A2,MSAFREE2:def 11;
  then
A5: (the Sorts of FreeMSA X).i is finite;
  reconsider FXi = (the Sorts of FreeMSA X).i as non empty set by A3;
  reconsider SAi = (the Sorts of A).i as non empty set by A3;
  consider F being ManySortedFunction of FreeMSA X, A such that
A6: F is_epimorphism FreeMSA X, A by Th21;
  reconsider i as Element of S by A3;
  reconsider Fi = F.i as Function of FXi, SAi;
  F is "onto" by A6;
  then rng Fi = SAi;
  hence contradiction by A4,A5;
end;

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;
  coherence
  proof
A1: X.v,FreeGen(v, X) are_equipotent
    proof
      set Z = the set of all [a, root-tree[a,v]] where a is Element of X.v;
      take Z;
      hereby
        let x be object such that
A2:     x in X.v;
        reconsider y = root-tree [x, v] as object;
        take y;
        thus y in FreeGen(v,X) by A2,MSAFREE:def 15;
        thus [x,y] in Z by A2;
      end;
      hereby
        let y be object;
        assume y in FreeGen(v, X);
        then consider x being set such that
A3:     x in X.v and
A4:     y = root-tree [x,v] by MSAFREE:def 15;
        reconsider x as object;
        take x;
        thus x in X.v by A3;
        thus [x,y] in Z by A3,A4;
      end;
      let x,y,z,u be object;
      assume that
A5:   [x,y] in Z and
A6:   [z,u] in Z;
      consider a being Element of X.v such that
A7:   [x,y] = [a, root-tree[a,v]] by A5;
      consider b being Element of X.v such that
A8:   [z,u] = [b, root-tree[b,v]] by A6;
A9:   z = b by A8,XTUPLE_0:1;
A10:  x = a by A7,XTUPLE_0:1;
      hence x = z implies y = u by A7,A8,A9,XTUPLE_0:1;
A11:  y = root-tree[a,v] by A7,XTUPLE_0:1;
A12:  u = root-tree[b,v] by A8,XTUPLE_0:1;
      assume y = u;
      then [a,v] = [b,v] by A11,A12,TREES_4:4;
      hence thesis by A10,A9,XTUPLE_0:1;
    end;
    thus thesis by A1,CARD_1:38;
  end;
end;

theorem Th23:
  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) = {{}}
proof
  dom {} = {} & rng {} = {};
  then reconsider b = {} as Function of {},{} by FUNCT_2:1;
  let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S,
  o be OperSymbol of S such that
A1: (the Arity of S).o = {};
A2: dom (the Arity of S) = the carrier' of S by FUNCT_2:def 1;
  then dom ((the Sorts of A)# qua ManySortedSet of(the carrier of S)*) = (the
  carrier of S)* & (the Arity of S).o in rng (the Arity of S) by FUNCT_1:def 3
,PARTFUN1:def 2;
  then
A3: o in dom ((the Sorts of A)# * the Arity of S) by A2,FUNCT_1:11;
  thus dom Den(o,A) = Args(o,A) by FUNCT_2:def 1
    .= ((the Sorts of A)# * the Arity of S).o by MSUALG_1:def 4
    .= (the Sorts of A)# . ((the Arity of S).o) by A3,FUNCT_1:12
    .= (the Sorts of A)# . (the_arity_of o) by MSUALG_1:def 1
    .= product ((the Sorts of A) * (the_arity_of o) qua Function) by
FINSEQ_2:def 5
    .= product ((the Sorts of A) * b) by A1,MSUALG_1:def 1
    .= {{}} by CARD_3:10;
end;

definition
  let IT be non void non empty ManySortedSign;
  attr IT is finitely_operated means

  for s being SortSymbol of IT holds
  {o where o is OperSymbol of IT: the_result_sort_of o = s} is finite;
end;

theorem
  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
proof
  let S be non void non empty ManySortedSign, A be non-empty MSAlgebra over S,
  v be SortSymbol of S such that
A1: S is finitely_operated;
  set Ov = {o where o is OperSymbol of S: the_result_sort_of o = v};
  consider Av being non empty set such that
  Av =(the Sorts of A).v and
A2: Constants(A,v) = { a where a is Element of Av : ex o be OperSymbol
of S st (the Arity of S).o = {} & (the ResultSort of S).o = v & a in rng Den(o,
  A)} by MSUALG_2:def 3;
A3: Ov is finite by A1;
A4: now
    assume Ov is non empty;
    then reconsider Ov as non empty set;
    deffunc G(Element of the carrier' of S)=Den($1,A).{};
    defpred P[Element of Ov] means (the Arity of S).$1 = {};
    set COv = {o where o is Element of Ov: P[o]};
    set aCOv = {G(o) where o is Element of the carrier' of S : o in COv };
A5: Constants(A,v) c= aCOv
    proof
      let c be object;
      assume c in Constants(A,v);
      then consider a being Element of Av such that
A6:   a = c and
A7:   ex o be OperSymbol of S st (the Arity of S).o = {} & (the
      ResultSort of S).o = v & a in rng Den(o,A) by A2;
      consider o being OperSymbol of S such that
A8:   (the Arity of S).o = {} and
A9:   (the ResultSort of S).o = v and
A10:  a in rng Den(o,A) by A7;
      the_result_sort_of o = (the ResultSort of S).o by MSUALG_1:def 2;
      then o in Ov by A9;
      then reconsider o9 = o as Element of Ov;
A11:  o9 in COv by A8;
      set f = Den(o,A);
      consider x being object such that
A12:  x in dom f and
A13:  a = f.x by A10,FUNCT_1:def 3;
      dom f = {{}} by A8,Th23;
      then x = {} by A12,TARSKI:def 1;
      hence thesis by A6,A11,A13;
    end;
    COv is Subset of Ov from DOMAIN_1:sch 7;
    then
A14: COv is finite by A3;
    aCOv is finite from FRAENKEL:sch 21(A14);
    hence thesis by A5;
  end;
  now
    assume
A15: Ov is empty;
    now
      assume Constants(A, v) is non empty;
      then consider c being object such that
A16:  c in Constants(A,v) by XBOOLE_0:def 1;
      consider a being Element of Av such that
      a = c and
A17:  ex o be OperSymbol of S st (the Arity of S).o = {} & (the
      ResultSort of S).o = v & a in rng Den(o,A) by A2,A16;
      consider o being OperSymbol of S such that
      (the Arity of S).o = {} and
A18:  (the ResultSort of S).o = v and
      a in rng Den(o,A) by A17;
      the_result_sort_of o = (the ResultSort of S).o by MSUALG_1:def 2;
      then o in Ov by A18;
      hence contradiction by A15;
    end;
    hence thesis;
  end;
  hence thesis by A4;
end;

theorem
  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)
proof
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, v be SortSymbol of S;
  set SF = the Sorts of FreeMSA X;
  set d0 = {t where t is Element of SF.v: depth t = 0};
A1: d0 c= FreeGen(v, X) \/ Constants(FreeMSA X, v)
  proof
    let x be object;
    assume x in d0;
    then consider t being Element of SF.v such that
A2: x = t and
A3: depth t = 0;
    t in SF.v;
    then t in FreeSort(X, v) by MSAFREE:def 11;
    then consider a being Element of TS(DTConMSA(X)) such that
A4: t = a and
A5: (ex x be set st x in X.v & a = root-tree [x,v]) or ex o be
    OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = v;
    consider dt being finite DecoratedTree, ft being finite Tree such that
A6: dt = t and
A7: ft = dom dt & depth t = height ft by MSAFREE2:def 14;
    per cases by A5;
    suppose
      ex x be set st x in X.v & a = root-tree [x,v];
      then t in FreeGen(v,X) by A4,MSAFREE:def 15;
      hence thesis by A2,XBOOLE_0:def 3;
    end;
    suppose
      ex o be OperSymbol of S st [o,the carrier of S] = a.{} &
      the_result_sort_of o = v;
      then consider o be OperSymbol of S such that
A8:   [o,the carrier of S] = a.{} and
A9:   the_result_sort_of o = v;
A10:  (the ResultSort of S).o = v by A9,MSUALG_1:def 2;
      set ars9 = <*>TS DTConMSA X;
      reconsider t9= t as Term of S, X by A4,MSATERM:def 1;
A11:  ex Av being non empty set st Av = SF.v & Constants( FreeMSA X,v) = {
a1 where a1 is Element of Av : ex o be OperSymbol of S st (the Arity of S).o =
{} & (the ResultSort of S).o = v & a1 in rng Den(o, FreeMSA X)} by
MSUALG_2:def 3;
      consider ars being ArgumentSeq of Sym(o,X) such that
A12:  t9 = [o,the carrier of S]-tree ars by A4,A8,MSATERM:10;
      dt = root-tree (dt.{}) by A3,A7,TREES_1:43,TREES_4:5;
      then
A13:  ars = {} by A6,A12,TREES_4:17;
      then 0 = len ars .= len the_arity_of o by MSATERM:22;
      then the_arity_of o = {};
      then
A14:  (the Arity of S).o = {} by MSUALG_1:def 1;
      then dom Den(o, FreeMSA X) = {{}} by Th23;
      then
A15:  {} in dom Den(o, FreeMSA X) by TARSKI:def 1;
      Sym(o, X) ==> roots ars by MSATERM:21;
      then
A16:  DenOp(o, X).ars9 = t by A12,A13,MSAFREE:def 12;
      Den(o, FreeMSA X) = (FreeOper X).o by MSUALG_1:def 6
        .= DenOp(o, X) by MSAFREE:def 13;
      then t in rng Den(o, FreeMSA X) by A16,A15,FUNCT_1:def 3;
      then t in Constants(FreeMSA X, v) by A14,A10,A11;
      hence thesis by A2,XBOOLE_0:def 3;
    end;
  end;
A17: Constants(FreeMSA X, v) c= d0
  proof
    set p = <*>TS(DTConMSA(X));
    let x be object;
    consider Av being non empty set such that
A18: Av =(the Sorts of FreeMSA X).v and
A19: Constants(FreeMSA X,v) = { a where a is Element of Av : ex o be
OperSymbol of S st (the Arity of S).o = {} & (the ResultSort of S).o = v & a in
    rng Den(o,FreeMSA X)} by MSUALG_2:def 3;
    assume x in Constants(FreeMSA X, v);
    then consider a being Element of Av such that
A20: x = a and
A21: ex o be OperSymbol of S st (the Arity of S).o = {} & (the
    ResultSort of S).o = v & a in rng Den(o,FreeMSA X) by A19;
    consider o being OperSymbol of S such that
A22: (the Arity of S).o = {} and
    (the ResultSort of S).o = v and
A23: a in rng Den(o,FreeMSA X) by A21;
A24: dom Den(o, FreeMSA X) = {{}} by A22,Th23;
    ((FreeSort X)# * (the Arity of S)).o = Args(o,FreeMSA X) by MSUALG_1:def 4
      .= dom Den(o,FreeMSA X) by FUNCT_2:def 1;
    then p in ((FreeSort X)# * (the Arity of S)).o by A24,TARSKI:def 1;
    then Sym(o,X) ==> roots p by MSAFREE:10;
    then
A25: DenOp(o,X).p = (Sym(o,X))-tree p by MSAFREE:def 12;
    reconsider a as Element of (the Sorts of FreeMSA X).v by A18;
    consider d being object such that
A26: d in dom Den(o,FreeMSA X) and
A27: a = Den(o,FreeMSA X).d by A23,FUNCT_1:def 3;
    consider dt being finite DecoratedTree, t being finite Tree such that
A28: dt = a & t = dom dt and
A29: depth a = height t by MSAFREE2:def 14;
A30: Den(o, FreeMSA X) = (FreeOper X).o by MSUALG_1:def 6
      .= DenOp(o, X) by MSAFREE:def 13;
    d = {} by A24,A26,TARSKI:def 1;
    then a = root-tree (Sym(o,X)) by A27,A30,A25,TREES_4:20;
    then height t = 0 by A28,TREES_1:42,TREES_4:3;
    hence thesis by A20,A29;
  end;
  FreeGen(v, X) c= d0
  proof
    let x be object;
    assume
A31: x in FreeGen(v, X);
    then reconsider x9 = x as Element of SF.v;
    consider dt being finite DecoratedTree, t being finite Tree such that
A32: dt = x9 & t = dom dt and
A33: depth x9 = height t by MSAFREE2:def 14;
    ex a being set st a in X.v & x = root-tree [a,v] by A31,MSAFREE:def 15;
    then height t = 0 by A32,TREES_1:42,TREES_4:3;
    hence thesis by A33;
  end;
  then FreeGen(v, X) \/ Constants(FreeMSA X, v) c= d0 by A17,XBOOLE_1:8;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem
  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
proof
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
the carrier of S, v, vk be SortSymbol of S, o be OperSymbol of S, t be Element
of (the Sorts of FreeMSA X).v, a be (ArgumentSeq of Sym(o,X)), k be Element of
  NAT, ak be Element of (the Sorts of FreeMSA X).vk;
  assume that
A1: t = [o,the carrier of S]-tree a and
A2: k in dom a and
A3: ak = a.k;
  reconsider a9 = a as DTree-yielding FinSequence;
A4: (ex dt being finite DecoratedTree, tt being finite Tree st dt = t & tt =
dom dt & depth t = height tt )& ex q being DTree-yielding FinSequence st a9 = q
  & dom t = tree doms q by A1,MSAFREE2:def 14,TREES_4:def 4;
  reconsider da = doms a as FinTree-yielding FinSequence;
  consider dtk being finite DecoratedTree, ttk being finite Tree such that
A5: dtk = ak & ttk = dom dtk and
A6: depth ak = height ttk by MSAFREE2:def 14;
  dom doms a9 = dom a9 & ttk = da.k by A2,A3,A5,FUNCT_6:22,TREES_3:37;
  then ttk in rng da by A2,FUNCT_1:def 3;
  hence thesis by A6,A4,TREES_3:78;
end;