text:
:: Free Many Sorted Universal Algebra
::  by Beata Perkowska

environ

 vocabularies XBOOLE_0, FUNCT_1, RELAT_1, PBOOLE, SUBSET_1, CARD_3, REALSET1,
      TARSKI, ZFMISC_1, PARTFUN1, STRUCT_0, MSUALG_1, MSUALG_2, PRELAMB,
      MSUALG_3, FINSEQ_1, MARGREL1, LANG1, TDGROUP, DTCONSTR, TREES_3, TREES_4,
      NAT_1, TREES_2, MCART_1, UNIALG_2, QC_LANG1, GROUP_6, MSAFREE;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NAT_1,
      RELAT_1, RELSET_1, STRUCT_0, FUNCT_1, PARTFUN1, MCART_1, FUNCT_2,
      FINSEQ_1, PBOOLE, TREES_2, FINSEQ_2, CARD_3, LANG1, TREES_4, DTCONSTR,
      MSUALG_1, MSUALG_2, MSUALG_3;
 constructors XXREAL_0, NAT_1, NAT_D, CARD_3, FINSEQOP, DTCONSTR, MSUALG_3,
      RELSET_1, PBOOLE, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
      FINSEQ_1, PBOOLE, TREES_2, TREES_3, STRUCT_0, DTCONSTR, MSUALG_1,
      MSUALG_3, FUNCT_2, RELSET_1, XTUPLE_0;
 requirements BOOLE, SUBSET;
 definitions TARSKI, XBOOLE_0, PBOOLE, MSUALG_3;
 equalities TARSKI;
 expansions TARSKI, XBOOLE_0, PBOOLE, MSUALG_3;
 theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, PBOOLE, CARD_3, MSUALG_1,
      MSUALG_2, MSUALG_3, RELAT_1, LANG1, DTCONSTR, FINSEQ_1, TREES_4, TREES_1,
      DOMAIN_1, RELSET_1, XBOOLE_0, XBOOLE_1, FUNCOP_1, TREES_3, PARTFUN1,
      FINSEQ_3, FINSEQ_2, XTUPLE_0;
 schemes CLASSES1, FUNCT_1, RELSET_1, DTCONSTR, XBOOLE_0;

begin

::
:: Preliminaries
::

theorem Th1:
  for I be set, J be non empty set, f be Function of I,J*, X be
ManySortedSet of J, p be Element of J*, x be set st x in I & p = f.x holds (X#
  * f).x = product (X * p)
proof
  let I be set, J be non empty set, f be Function of I,J*, X be ManySortedSet
  of J, p be Element of J*, x be set;
  assume
A1: x in I & p = f.x;
A2: dom f = I by FUNCT_2:def 1;
  then dom (X# * f) = dom f by PARTFUN1:def 2;
  hence (X# * f).x =(X# qua ManySortedSet of J*).p by A1,A2,FUNCT_1:12
    .= product (X * p) by FINSEQ_2:def 5;
end;

definition
  let I be set, A,B be ManySortedSet of I, C be ManySortedSubset of A;
  let F be ManySortedFunction of A,B;
  func F || C -> ManySortedFunction of C,B means
  :Def1:
  for i be set st i in I holds it.i = (F.i) | (C.i);
  existence
  proof
    defpred P[object,object] means $2 = (F.$1) | (C.$1);
A1: for i be object st i in I ex u be object st P[i,u];
    consider H be Function such that
A2: dom H = I & for i be object st i in I holds P[i,H.i] from CLASSES1:
    sch 1 (A1);
    reconsider H as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18;
    for i be object st i in I holds H.i is Function of C.i,B.i
    proof
      let i be object;
      assume
A3:   i in I;
      then reconsider f = F.i as Function of A.i,B.i by PBOOLE:def 15;
A4:   H.i = f | (C.i) by A2,A3;
      C c= A by PBOOLE:def 18;
      then
A5:   C.i c= A.i by A3;
      per cases;
      suppose
A6:     B.i is empty;
        then H.i = {} by A4;
        hence thesis by A6,FUNCT_2:def 1,RELSET_1:12;
      end;
      suppose
A8:     B.i is non empty;
        then
A9:     dom f = A.i by FUNCT_2:def 1;
A10:    rng (f|(C.i)) c= B.i by RELAT_1:def 19;
        dom (f|(C.i)) = dom f /\ (C.i) by RELAT_1:61
          .= C.i by A5,A9,XBOOLE_1:28;
        hence thesis by A4,A8,A10,FUNCT_2:def 1,RELSET_1:4;
      end;
    end;
    then reconsider H as ManySortedFunction of C,B by PBOOLE:def 15;
    take H;
    thus thesis by A2;
  end;
  uniqueness
  proof
    let X,Y be ManySortedFunction of C,B;
    assume that
A11: for i be set st i in I holds X.i = (F.i) | (C.i) and
A12: for i be set st i in I holds Y.i = (F.i) | (C.i);
    let i be object;
    assume
A13:  i in I;
    then X.i = (F.i)|(C.i) by A11;
    hence thesis by A12,A13;
  end;
end;

definition
  let I be set, X be ManySortedSet of I, i be object;
  assume
A1: i in I;
  func coprod(i,X) -> set means
  :Def2:
  for x be set holds x in it iff ex a be set st a in X.i & x = [a,i];
  existence
  proof
    defpred P[object] means ex a be set st a in X.i & $1 = [a,i];
    consider A be set such that
A2: for x be object holds x in A iff x in [:X.i,I:] & P[x] from XBOOLE_0:
    sch 1;
    take A;
    let x be set;
    thus x in A implies ex a be set st a in X.i & x = [a,i] by A2;
    given a be set such that
A3: a in X.i & x = [a,i];
    x in [:X.i,I:] by A1,A3,ZFMISC_1:87;
    hence thesis by A2,A3;
  end;
  uniqueness
  proof
    let A,B be set;
    assume that
A4: for x be set holds x in A iff ex a be set st a in X.i & x = [a,i] and
A5: for x be set holds x in B iff ex a be set st a in X.i & x = [a,i];
    thus A c= B
    proof
      let x be object;
      assume x in A;
      then ex a be set st a in X.i & x = [a,i] by A4;
      hence thesis by A5;
    end;
    let x be object;
    assume x in B;
    then ex a be set st a in X.i & x = [a,i] by A5;
    hence thesis by A4;
  end;
end;

notation
  let I be set, X be ManySortedSet of I;
  synonym coprod X for disjoin X;
end;

registration
  let I be set, X be ManySortedSet of I;
  cluster coprod X -> I-defined;
  coherence
  proof
    dom coprod X = dom X by CARD_3:def 3;
    then dom coprod X = I by PARTFUN1:def 2;
    hence thesis by RELAT_1:def 18;
  end;
end;

registration
  let I be set, X be ManySortedSet of I;
  cluster coprod X -> total;
  coherence
  proof
    dom coprod X = dom X by CARD_3:def 3;
    then dom coprod X = I by PARTFUN1:def 2;
    hence thesis by PARTFUN1:def 2;
  end;
end;

definition
  let I be set, X be ManySortedSet of I;
  redefine func coprod X means
  :Def3:
  dom it = I & for i be set st i in I holds it.i = coprod(i,X);
  compatibility
  proof
    let IT be Function;
    hereby
      assume
A1:   IT = disjoin X;
      hence dom IT = I by PARTFUN1:def 2;
      let i be set;
      assume
A2:   i in I;
      then i in dom X by PARTFUN1:def 2;
      then
A3:   IT.i = [:X.i,{i}:] by A1,CARD_3:def 3;
      now
        let x be set;
        hereby
          assume x in IT.i;
          then consider a,b being object such that
A4:       a in X.i and
A5:       b in {i} & x = [a,b] by A3,ZFMISC_1:def 2;
          reconsider a as set by TARSKI:1;
          take a;
          thus a in X.i by A4;
          thus x = [a,i] by A5,TARSKI:def 1;
        end;
        given a being set such that
A6:     a in X.i & x = [a,i];
        i in {i} by TARSKI:def 1;
        hence x in IT.i by A3,A6,ZFMISC_1:def 2;
      end;
      hence IT.i = coprod(i,X) by A2,Def2;
    end;
    assume that
A7: dom IT = I and
A8: for i be set st i in I holds IT.i = coprod(i,X);
A9: dom IT = dom X by A7,PARTFUN1:def 2;
    now
      let x be object;
      assume
A10:  x in dom X;
      then
A11:  x in I;
A12:  now
        let a be object;
        hereby
          assume a in coprod(x,X);
          then
A13:      ex b being set st b in X.x & a = [b,x] by A11,Def2;
          x in {x} by TARSKI:def 1;
          hence a in [:X.x,{x}:] by A13,ZFMISC_1:def 2;
        end;
        assume a in [:X.x,{x}:];
        then consider a1,a2 being object such that
A14:    a1 in X.x and
A15:    a2 in {x} and
A16:    a = [a1,a2] by ZFMISC_1:def 2;
        a2 = x by A15,TARSKI:def 1;
        hence a in coprod(x,X) by A11,A14,A16,Def2;
      end;
      thus IT.x = coprod(x,X) by A8,A10
        .= [:X.x,{x}:] by A12,TARSKI:2;
    end;
    hence thesis by A9,CARD_3:def 3;
  end;
end;

registration
  let I be set, X be non-empty ManySortedSet of I;
  cluster coprod X -> non-empty;
  coherence
  proof
    let x be object;
    assume
A1: x in I;
    then reconsider i = x as Element of I;
    consider a be object such that
A2: a in X.i by A1,XBOOLE_0:def 1;
    (coprod X).i = coprod(i,X) by A1,Def3;
    then [a,i] in (coprod X).i by A1,A2,Def2;
    hence thesis;
  end;
end;

registration
  let I be non empty set, X be non-empty ManySortedSet of I;
  cluster Union X -> non empty;
  coherence
  proof
    set i = the Element of I;
    consider a be object such that
A1: a in X.i by XBOOLE_0:def 1;
    dom X = I by PARTFUN1:def 2;
    then X.i in rng X by FUNCT_1:def 3;
    then a in union rng X by A1,TARSKI:def 4;
    hence thesis by CARD_3:def 4;
  end;
end;

theorem
  for I be set, X be ManySortedSet of I, i be set st i in I holds
  X.i <> {} iff (coprod X).i <> {}
proof
  let I be set, X be ManySortedSet of I, i be set;
  assume
A1: i in I;
  then
A2: (coprod X).i = coprod(i,X) by Def3;
  thus X.i <> {} implies (coprod X).i <> {}
  proof
    assume X.i <> {};
    then consider x be object such that
A3: x in X.i by XBOOLE_0:def 1;
    [x,i] in (coprod X).i by A1,A2,A3,Def2;
    hence thesis;
  end;
  assume (coprod X).i <> {};
  then consider a be object such that
A4: a in coprod(i,X) by A2,XBOOLE_0:def 1;
  ex x be set st x in X.i & a = [x,i] by A1,A4,Def2;
  hence thesis;
end;

begin

::
:: Free Many Sorted Universal Algebra - General Notions
::

reserve S for non void non empty ManySortedSign,
  U0 for MSAlgebra over S;

definition
  let S be non void non empty ManySortedSign, U0 be MSAlgebra over S;
  mode GeneratorSet of U0 -> MSSubset of U0 means
    :Def4:
    the Sorts of GenMSAlg (it) = the Sorts of U0;
  existence
  proof
    set A = the Sorts of U0;
    reconsider A as MSSubset of U0 by PBOOLE:def 18;
    take A;
    set G = GenMSAlg(A);
    the Sorts of G is MSSubset of U0 by MSUALG_2:def 9;
    then
A1: the Sorts of G c= A by PBOOLE:def 18;
    A is MSSubset of G by MSUALG_2:def 17;
    then A c= the Sorts of G by PBOOLE:def 18;
    hence thesis by A1,PBOOLE:146;
  end;
end;

theorem
  for S be non void non empty ManySortedSign, U0 be strict non-empty
  MSAlgebra over S, A be MSSubset of U0 holds A is GeneratorSet of U0 iff
  GenMSAlg(A) = U0
proof
  let S be non void non empty ManySortedSign, U0 be strict non-empty MSAlgebra
  over S, A be MSSubset of U0;
  thus A is GeneratorSet of U0 implies GenMSAlg(A) = U0
  proof
    reconsider U1 = U0 as MSSubAlgebra of U0 by MSUALG_2:5;
    assume A is GeneratorSet of U0;
    then the Sorts of GenMSAlg(A) = the Sorts of U1 by Def4;
    hence thesis by MSUALG_2:9;
  end;
  assume GenMSAlg(A) = U0;
  hence thesis by Def4;
end;

definition
  let S,U0;
  let IT be GeneratorSet of U0;
  attr IT is free means

  for U1 be non-empty MSAlgebra over S for f be
ManySortedFunction of IT,the Sorts of U1 ex h be ManySortedFunction of U0,U1 st
  h is_homomorphism U0,U1 & h || IT = f;
end;

definition
  let S be non void non empty ManySortedSign;
  let IT be MSAlgebra over S;
  attr IT is free means
  :Def6:
  ex G being GeneratorSet of IT st G is free;
end;

theorem Th4:
  for S be non void non empty ManySortedSign, X be ManySortedSet of
  the carrier of S holds Union coprod X misses [:the carrier' of S,{the carrier
  of S}:]
proof
  let S be non void non empty ManySortedSign, X be ManySortedSet of the
  carrier of S;
  assume Union (coprod X) /\ [:the carrier' of S,{the carrier of S}:] <> {};
  then consider x be object such that
A1: x in Union (coprod X) /\ [:the carrier' of S,{the carrier of S}:] by
XBOOLE_0:def 1;
  x in Union (coprod X) by A1,XBOOLE_0:def 4;
  then x in union rng (coprod X) by CARD_3:def 4;
  then consider A be set such that
A2: x in A and
A3: A in rng (coprod X) by TARSKI:def 4;
  consider s be object such that
A4: s in dom (coprod X) and
A5: (coprod X).s = A by A3,FUNCT_1:def 3;
  reconsider s as SortSymbol of S by A4;
  A = coprod(s,X) by A5,Def3;
  then
A6: ex a be set st a in X.s & x = [a,s] by A2,Def2;
  x in [:the carrier' of S,{the carrier of S}:] by A1,XBOOLE_0:def 4;
  then s in {the carrier of S} by A6,ZFMISC_1:87;
  then s in the carrier of S & s = the carrier of S by TARSKI:def 1;
  hence contradiction;
end;

begin

::
:: Construction of Free Many Sorted Algebras for Given Signature
::

definition
  let S be non void non empty ManySortedSign, X be ManySortedSet of the
  carrier of S;

  func REL(X) -> Relation of ([:the carrier' of S,{the carrier of S}:] \/
Union (coprod X)), (([:the carrier' of S,{the carrier of S}:] \/ Union (coprod
  X))*) means
  :Def7:
  for a be Element of [:the carrier' of S,{the carrier of S}:]
\/ Union (coprod X), b be Element of ([:the carrier' of S,{the carrier of S}:]
  \/ Union (coprod X))* holds [a,b] in it iff a in [:the carrier' of S,{the
  carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = a holds
  len b = len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the
carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the
carrier of S] = b.x holds the_result_sort_of o1 = (the_arity_of o).x) & (b.x in
  Union (coprod X) implies b.x in coprod((the_arity_of o).x,X));
  existence
  proof
    set O = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod X);
    defpred P[Element of O,Element of O*] means $1 in [:the carrier' of S,{the
carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = $1 holds
len $2 = len (the_arity_of o) & for x be set st x in dom $2 holds ($2.x in [:
the carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1
,the carrier of S] = $2.x holds the_result_sort_of o1 = (the_arity_of o).x) & (
    $2.x in Union (coprod X) implies $2.x in coprod((the_arity_of o).x,X));
    consider R be Relation of O,O* such that
A1: for a be Element of O, b be Element of O* holds [a,b] in R iff P[a
    ,b] from RELSET_1:sch 2;
    take R;
    let a be Element of O, b be Element of O*;
    thus [a,b] in R implies a in [:the carrier' of S,{the carrier of S}:] &
    for o be OperSymbol of S st [o,the carrier of S] = a holds len b = len (
the_arity_of o) & for x be set st x in dom b holds (b.x in [:the carrier' of S,
{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S]
= b.x holds the_result_sort_of o1 = (the_arity_of o).x) & (b.x in Union (coprod
    X) implies b.x in coprod((the_arity_of o).x,X)) by A1;
    assume a in [:the carrier' of S,{the carrier of S}:] & for o be
OperSymbol of S st [o,the carrier of S] = a holds len b = len (the_arity_of o)
& for x be set st x in dom b holds (b.x in [:the carrier' of S,{the carrier of
    S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds
the_result_sort_of o1 = (the_arity_of o).x) & (b.x in Union ( coprod X) implies
    b.x in coprod(( the_arity_of o).x,X));
    hence thesis by A1;
  end;
  uniqueness
  proof
    set O = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod X);
    let R,P be Relation of O,O*;
    assume that
A2: for a be Element of O, b be Element of O* holds [a,b] in R iff a
in [:the carrier' of S,{the carrier of S}:] & for o be OperSymbol of S st [o,
the carrier of S] = a holds len b = len (the_arity_of o) & for x be set st x in
dom b holds (b.x in [:the carrier' of S,{the carrier of S}:] implies for o1 be
OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 = (
    the_arity_of o).x) & (b.x in Union (coprod X) implies b.x in coprod((
    the_arity_of o).x,X)) and
A3: for a be Element of O, b be Element of O* holds [a,b] in P iff a
in [:the carrier' of S,{the carrier of S}:] & for o be OperSymbol of S st [o,
the carrier of S] = a holds len b = len (the_arity_of o) & for x be set st x in
dom b holds (b.x in [:the carrier' of S,{the carrier of S}:] implies for o1 be
OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 = (
    the_arity_of o).x) & (b.x in Union (coprod X) implies b.x in coprod((
    the_arity_of o).x,X));
    for x,y be object holds [x,y] in R iff [x,y] in P
    proof
      let x,y be object;
      thus [x,y] in R implies [x,y] in P
      proof
        assume
A4:     [x,y] in R;
        then reconsider a = x as Element of O by ZFMISC_1:87;
        reconsider b = y as Element of O* by A4,ZFMISC_1:87;
        [a,b] in R by A4;
        then
A5:     a in [:the carrier' of S,{the carrier of S}:] by A2;
        for o be OperSymbol of S st [o,the carrier of S] = a holds len b =
len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the carrier'
of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier
of S ] = b.x holds the_result_sort_of o1 = (the_arity_of o).x) & (b.x in Union
        ( coprod X) implies b.x in coprod((the_arity_of o).x,X)) by A2,A4;
        hence thesis by A3,A5;
      end;
      assume
A6:   [x,y] in P;
      then reconsider a = x as Element of O by ZFMISC_1:87;
      reconsider b = y as Element of O* by A6,ZFMISC_1:87;
      [a,b] in P by A6;
      then
A7:   a in [:the carrier' of S,{the carrier of S}:] by A3;
      for o be OperSymbol of S st [o,the carrier of S] = a holds len b =
len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the carrier'
of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier
of S ] = b.x holds the_result_sort_of o1 = (the_arity_of o).x) & (b.x in Union
      ( coprod X) implies b.x in coprod((the_arity_of o).x,X)) by A3,A6;
      hence thesis by A2,A7;
    end;
    hence thesis by RELAT_1:def 2;
  end;
end;

reserve S for non void non empty ManySortedSign,
  X for ManySortedSet of the carrier of S,
  o for OperSymbol of S,
  b for Element of ([:the carrier' of S,{the
  carrier of S}:] \/ Union (coprod X))*;

theorem Th5:
  [[o,the carrier of S],b] in REL(X) iff len b = len (the_arity_of
o) & for x be set st x in dom b holds (b.x in [:the carrier' of S,{the carrier
of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds
the_result_sort_of o1 = (the_arity_of o).x) & (b.x in Union (coprod X) implies
  b.x in coprod((the_arity_of o).x,X))
proof
  defpred P[OperSymbol of S,Element of ([:the carrier' of S,{the carrier of S}
  :] \/ Union (coprod X))*] means len $2 = len (the_arity_of $1) & for x be set
st x in dom $2 holds ($2.x in [:the carrier' of S,{the carrier of S}:] implies
  for o1 be OperSymbol of S st [o1,the carrier of S] = $2.x holds
  the_result_sort_of o1 = (the_arity_of $1).x) & ($2.x in Union (coprod X)
  implies b.x in coprod((the_arity_of $1).x,X));
  set a = [o,the carrier of S];
  the carrier of S in {the carrier of S} by TARSKI:def 1;
  then
A1: a in [:the carrier' of S,{the carrier of S}:] by ZFMISC_1:87;
  then reconsider
  a as Element of [:the carrier' of S,{the carrier of S}:] \/ Union
  (coprod X) by XBOOLE_0:def 3;
  thus [[o,the carrier of S],b] in REL(X) implies P[o,b]
  proof
    assume [[o,the carrier of S],b] in REL(X);
    then for o1 be OperSymbol of S st [o1,the carrier of S] = a holds P[o1,b]
    by Def7;
    hence thesis;
  end;
  assume
A2: P[o,b];
  now
    let o1 be OperSymbol of S;
    assume [o1,the carrier of S] = a;
    then o1 = o by XTUPLE_0:1;
    hence P[o1,b] by A2;
  end;
  hence thesis by A1,Def7;
end;

definition
  let S be non void non empty ManySortedSign, X be ManySortedSet of the
  carrier of S;
  func DTConMSA(X) -> DTConstrStr equals
  DTConstrStr (# [:the carrier' of S,{
    the carrier of S}:] \/ Union (coprod X), REL(X) #);
  correctness;
end;

registration
  let S be non void non empty ManySortedSign, X be ManySortedSet of the
  carrier of S;
  cluster DTConMSA(X) -> strict non empty;
  coherence;
end;

theorem Th6:
  for S be non void non empty ManySortedSign, X be ManySortedSet of
  the carrier of S holds NonTerminals(DTConMSA(X))c= [:the carrier' of S,{the
carrier of S}:] & Union (coprod X) c= Terminals (DTConMSA(X)) & (X is non-empty
implies NonTerminals(DTConMSA(X)) = [:the carrier' of S,{the carrier of S}:] &
  Terminals (DTConMSA(X)) = Union (coprod X))
proof
  let S be non void non empty ManySortedSign, X be ManySortedSet of the
  carrier of S;
  set D = DTConMSA(X), A = [:the carrier' of S,{the carrier of S}:] \/ Union (
  coprod (X qua ManySortedSet of the carrier of S));
A1: the carrier of D = (Terminals D) \/ (NonTerminals D) by LANG1:1;
  thus
A2: NonTerminals D c= [:the carrier' of S,{the carrier of S}:]
  proof
    let x be object;
    assume x in NonTerminals D;
    then
    x in { s where s is Symbol of D: ex n being FinSequence st s ==> n} by
LANG1:def 3;
    then consider s be Symbol of D such that
A3: s = x and
A4: ex n being FinSequence st s ==> n;
    consider n be FinSequence such that
A5: s ==> n by A4;
    [s,n] in the Rules of D by A5,LANG1:def 1;
    then reconsider n as Element of A* by ZFMISC_1:87;
    reconsider s as Element of A;
    [s,n] in REL X by A5,LANG1:def 1;
    hence thesis by A3,Def7;
  end;
A6: Union(coprod X) misses [:the carrier' of S,{the carrier of S}:] by Th4;
  thus
A7: Union (coprod X) c= Terminals (DTConMSA(X))
  proof
    let x be object;
    assume
A8: x in Union (coprod X);
    then x in A by XBOOLE_0:def 3;
    then x in Terminals D or x in NonTerminals D by A1,XBOOLE_0:def 3;
    hence thesis by A6,A2,A8,XBOOLE_0:3;
  end;
  assume
A9: X is non-empty;
  thus NonTerminals D c= [:the carrier' of S,{the carrier of S}:] by A2;
  thus
A10: [:the carrier' of S,{the carrier of S}:] c= NonTerminals D
  proof
    let x be object;
    assume
A11: x in [:the carrier' of S,{the carrier of S}:];
    then consider
    o being OperSymbol of S, x2 being Element of {the carrier of S}
    such that
A12: x = [o,x2] by DOMAIN_1:1;
    set O = the_arity_of o;
    defpred P[object,object] means $2 in coprod (O.$1,X);
A13: for a be object st a in Seg len O ex b be object st P[a,b]
    proof
      let a be object;
      assume a in Seg len O;
      then a in dom O by FINSEQ_1:def 3;
      then
A14:  O.a in rng O by FUNCT_1:def 3;
A15:  rng O c= the carrier of S by FINSEQ_1:def 4;
      then consider x be object such that
A16:  x in X.(O.a) by A9,A14,XBOOLE_0:def 1;
      take [x,O.a];
      thus thesis by A14,A15,A16,Def2;
    end;
    consider b be Function such that
A17: dom b = Seg len O &
for a be object st a in Seg len O holds P[a,b.a]
    from CLASSES1:sch 1(A13);
    reconsider b as FinSequence by A17,FINSEQ_1:def 2;
    rng b c= A
    proof
      let a be object;
A18:  rng O c= the carrier of S by FINSEQ_1:def 4;
      assume a in rng b;
      then consider c be object such that
A19:  c in dom b and
A20:  b.c = a by FUNCT_1:def 3;
      dom O = Seg len O by FINSEQ_1:def 3;
      then
A21:  O.c in rng O by A17,A19,FUNCT_1:def 3;
      dom coprod(X) = the carrier of S by PARTFUN1:def 2;
      then (coprod(X)).(O.c) in rng coprod(X) by A21,A18,FUNCT_1:def 3;
      then
A22:  coprod(O.c,X) in rng coprod(X) by A21,A18,Def3;
      a in coprod(O.c,X) by A17,A19,A20;
      then a in union rng coprod(X) by A22,TARSKI:def 4;
      then a in Union coprod(X) by CARD_3:def 4;
      hence thesis by XBOOLE_0:def 3;
    end;
    then reconsider b as FinSequence of A by FINSEQ_1:def 4;
    reconsider b as Element of A* by FINSEQ_1:def 11;
A23: now
      let c be set;
      assume
A24:  c in dom b;
      dom O = Seg len O by FINSEQ_1:def 3;
      then
A25:  O.c in rng O by A17,A24,FUNCT_1:def 3;
A26:  rng O c= the carrier of S by FINSEQ_1:def 4;
      dom coprod(X) = the carrier of S by PARTFUN1:def 2;
      then (coprod(X)).(O.c) in rng coprod(X) by A25,A26,FUNCT_1:def 3;
      then
A27:  coprod(O.c,X) in rng coprod(X) by A25,A26,Def3;
      P[c,b.c] by A17,A24;
      then b.c in union rng coprod(X) by A27,TARSKI:def 4;
      then b.c in Union coprod(X) by CARD_3:def 4;
      hence b.c in [:the carrier' of S,{the carrier of S}:] implies for o1 be
OperSymbol of S st [o1,the carrier of S] = b.c holds the_result_sort_of o1 = O.
      c by A6,XBOOLE_0:3;
      assume b.c in Union (coprod X);
      thus b.c in coprod(O.c,X) by A17,A24;
    end;
A28: the carrier of S = x2 by TARSKI:def 1;
    then reconsider
    xa = [o,the carrier of S] as Element of (the carrier of D) by A11,A12,
XBOOLE_0:def 3;
    len b = len O by A17,FINSEQ_1:def 3;
    then [xa,b] in REL(X) by A23,Th5;
    then xa ==> b by LANG1:def 1;
    then xa in { t where t is Symbol of D: ex n be FinSequence st t ==> n};
    hence thesis by A12,A28,LANG1:def 3;
  end;
A29: (Terminals D) misses (NonTerminals D) by DTCONSTR:8;
  thus Terminals D c= Union (coprod X)
  proof
    let x be object;
    assume x in Terminals D;
    then x in A & not x in [:the carrier' of S,{the carrier of S}:] by A1,A29
,A10,XBOOLE_0:3,def 3;
    hence thesis by XBOOLE_0:def 3;
  end;
  thus thesis by A7;
end;

reserve x for set;

registration
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S;
  cluster DTConMSA(X) -> with_terminals with_nonterminals
    with_useful_nonterminals;
  coherence
  proof
    set D = DTConMSA(X), A = [:the carrier' of S,{the carrier of S}:] \/ Union
    (coprod (X qua ManySortedSet of the carrier of S));
A1: Terminals D = Union (coprod X) by Th6;
A2: NonTerminals D = [:the carrier' of S,{the carrier of S}:] by Th6;
A3: Union (coprod X) misses [:the carrier' of S,{the carrier of S}:] by Th4;
    for nt being Symbol of D st nt in NonTerminals D ex p being
    FinSequence of TS(D) st nt ==> roots p
    proof
      let nt be Symbol of D;
      assume nt in NonTerminals D;
      then consider
      o being OperSymbol of S, x2 being Element of {the carrier of S}
      such that
A4:   nt = [o,x2] by A2,DOMAIN_1:1;
      set O = the_arity_of o;
      defpred P[object,object] means $2 in coprod(O.$1,X);
A5:   for a be object st a in Seg len O ex b be object st P[a,b]
      proof
        let a be object;
        assume a in Seg len O;
        then a in dom O by FINSEQ_1:def 3;
        then
A6:     O.a in rng O by FUNCT_1:def 3;
A7:     rng O c= the carrier of S by FINSEQ_1:def 4;
        then consider x be object such that
A8:     x in X.(O.a) by A6,XBOOLE_0:def 1;
        take [x,O.a];
        thus thesis by A6,A7,A8,Def2;
      end;
      consider b be Function such that
A9:   dom b = Seg len O & for a be object st a in Seg len O holds P[a,b.
      a] from CLASSES1:sch 1(A5);
      reconsider b as FinSequence by A9,FINSEQ_1:def 2;
A10:  rng b c= A
      proof
        let a be object;
A11:    rng O c= the carrier of S by FINSEQ_1:def 4;
        assume a in rng b;
        then consider c be object such that
A12:    c in dom b and
A13:    b.c = a by FUNCT_1:def 3;
        dom O = Seg len O by FINSEQ_1:def 3;
        then
A14:    O.c in rng O by A9,A12,FUNCT_1:def 3;
        dom coprod(X) = the carrier of S by PARTFUN1:def 2;
        then (coprod(X)).(O.c) in rng coprod(X) by A14,A11,FUNCT_1:def 3;
        then
A15:    coprod(O.c,X) in rng coprod(X) by A14,A11,Def3;
        a in coprod (O.c,X) by A9,A12,A13;
        then a in union rng coprod(X) by A15,TARSKI:def 4;
        then a in Union coprod(X) by CARD_3:def 4;
        hence thesis by XBOOLE_0:def 3;
      end;
      then reconsider b as FinSequence of A by FINSEQ_1:def 4;
      reconsider b as Element of A* by FINSEQ_1:def 11;
      deffunc F(object)=root-tree (b.$1);
      consider f be Function such that
A16:  dom f = dom b &
for x being object st x in dom b holds f.x = F(x) from
      FUNCT_1:sch 3;
      reconsider f as FinSequence by A9,A16,FINSEQ_1:def 2;
      rng f c= TS(D)
      proof
        let x be object;
A17:    rng O c= the carrier of S by FINSEQ_1:def 4;
        assume x in rng f;
        then consider y be object such that
A18:    y in dom f and
A19:    f.y = x by FUNCT_1:def 3;
        dom O = Seg len O by FINSEQ_1:def 3;
        then
A20:    O.y in rng O by A9,A16,A18,FUNCT_1:def 3;
        dom coprod(X) = the carrier of S by PARTFUN1:def 2;
        then (coprod(X)).(O.y) in rng coprod(X) by A20,A17,FUNCT_1:def 3;
        then
A21:    coprod(O.y,X) in rng coprod(X) by A20,A17,Def3;
        b.y in rng b by A16,A18,FUNCT_1:def 3;
        then reconsider a = b.y as Symbol of D by A10;
        P[y,b.y] by A9,A16,A18;
        then b.y in union rng coprod(X) by A21,TARSKI:def 4;
        then
A22:    a in Terminals D by A1,CARD_3:def 4;
        x = root-tree(b.y) by A16,A18,A19;
        hence thesis by A22,DTCONSTR:def 1;
      end;
      then reconsider f as FinSequence of TS(D) by FINSEQ_1:def 4;
A23:  for x being object st x in dom b holds (roots f).x = b.x
      proof
        let x be object;
        assume
A24:    x in dom b;
        then reconsider i = x as Nat;
        f.x = root-tree (b.x) & ex T be DecoratedTree st T = f.i & (roots
        f).i = T .{} by A16,A24,TREES_3:def 18;
        hence thesis by TREES_4:3;
      end;
A25:  now
        let c be set;
        assume
A26:    c in dom b;
        dom O = Seg len O by FINSEQ_1:def 3;
        then
A27:    O.c in rng O by A9,A26,FUNCT_1:def 3;
A28:    rng O c= the carrier of S by FINSEQ_1:def 4;
        dom coprod(X) = the carrier of S by PARTFUN1:def 2;
        then (coprod(X)).(O.c) in rng coprod(X) by A27,A28,FUNCT_1:def 3;
        then
A29:    coprod(O.c,X) in rng coprod(X) by A27,A28,Def3;
        P[c,b.c] by A9,A26;
        then b.c in union rng coprod(X) by A29,TARSKI:def 4;
        then b.c in Union coprod(X) by CARD_3:def 4;
        hence
        b.c in [:the carrier' of S,{the carrier of S}:] implies for o1 be
OperSymbol of S st [o1,the carrier of S] = b.c holds the_result_sort_of o1 = O.
        c by A3,XBOOLE_0:3;
        assume b.c in Union (coprod X);
        thus b.c in coprod(O.c,X) by A9,A26;
      end;
      the carrier of S = x2 & len b = len O by A9,FINSEQ_1:def 3,TARSKI:def 1;
      then [nt,b] in REL(X) by A4,A25,Th5;
      then
A30:  nt ==> b by LANG1:def 1;
      take f;
      dom (roots f) = dom f by TREES_3:def 18;
      hence thesis by A30,A16,A23,FUNCT_1:2;
    end;
    hence thesis by A1,A2,DTCONSTR:def 3,def 4,def 5;
  end;
end;

theorem Th7:
  for S be non void non empty ManySortedSign, X be ManySortedSet of
  the carrier of S, t be set holds (t in Terminals DTConMSA(X) & X is non-empty
  implies ex s be SortSymbol of S, x be set st x in X.s & t = [x,s]) & for s be
  SortSymbol of S, x be set st x in X.s holds [x,s] in Terminals DTConMSA(X)
proof
  let S be non void non empty ManySortedSign, X be ManySortedSet of the
  carrier of S, t be set;
  set D = DTConMSA(X);
A1: Union (coprod X) c= Terminals (DTConMSA(X)) by Th6;
A2: Union (coprod X) = union rng (coprod X) by CARD_3:def 4;
  thus t in Terminals D & X is non-empty implies ex s be SortSymbol of S, x be
  set st x in X.s & t = [x,s]
  proof
    assume that
A3: t in Terminals D and
A4: X is non-empty;
    Terminals D = Union (coprod X) by A4,Th6;
    then consider A be set such that
A5: t in A and
A6: A in rng(coprod X) by A2,A3,TARSKI:def 4;
    consider s be object such that
A7: s in dom (coprod X) and
A8: (coprod X).s = A by A6,FUNCT_1:def 3;
    reconsider s as SortSymbol of S by A7;
    (coprod X).s = coprod(s,X) by Def3;
    then consider x be set such that
A9: x in X.s & t = [x,s] by A5,A8,Def2;
    take s;
    take x;
    thus thesis by A9;
  end;
  let s be SortSymbol of S, x be set such that
A10: x in X.s;
  set t = [x,s];
  dom(coprod X) = the carrier of S by PARTFUN1:def 2;
  then
A11: (coprod X).s in rng (coprod X) by FUNCT_1:def 3;
  t in coprod(s,X) by A10,Def2;
  then t in (coprod X).s by Def3;
  then t in Union (coprod X) by A2,A11,TARSKI:def 4;
  hence thesis by A1;
end;

definition
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, o be OperSymbol of S;
  func Sym(o,X) ->Symbol of DTConMSA(X) equals
  [o,the carrier of S];
  coherence
  proof
    the carrier of S in {the carrier of S} by TARSKI:def 1;
    then [o,the carrier of S] in [:the carrier' of S,{the carrier of S}:] by
ZFMISC_1:87;
    then [o,the carrier of S] in NonTerminals (DTConMSA X) by Th6;
    hence thesis;
  end;
end;

definition
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, s be SortSymbol of S;
  func FreeSort(X,s) -> Subset of TS(DTConMSA(X)) equals
  {a where a is Element
of TS(DTConMSA(X)): (ex x be set st x in X.s & a = root-tree [x,s]) or ex o be
  OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = s};
  coherence
  proof
    set A = {a where a is Element of TS(DTConMSA(X)): (ex x be set st x in X.s
& a = root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] = a.
    {} & the_result_sort_of o = s};
    A c= TS(DTConMSA(X))
    proof
      let x be object;
      assume x in A;
      then
      ex a be Element of TS(DTConMSA(X)) st x = a &( (ex x be set st x in X
.s & a = root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] =
      a.{} & the_result_sort_of o = s);
      hence thesis;
    end;
    hence thesis;
  end;
end;

registration
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, s be SortSymbol of S;
  cluster FreeSort(X,s) -> non empty;
  coherence
  proof
    dom coprod(X) = the carrier of S by PARTFUN1:def 2;
    then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 3;
    then
A1: coprod(s,X) in rng coprod(X) by Def3;
    set A = {a where a is Element of TS(DTConMSA(X)): (ex x be set st x in X.s
& a = root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] = a.
    {} & the_result_sort_of o = s};
    consider x be object such that
A2: x in X.s by XBOOLE_0:def 1;
    set a = [x,s];
A3: (Terminals (DTConMSA(X))) = Union (coprod X) by Th6;
    a in coprod(s,X) by A2,Def2;
    then a in union rng coprod(X) by A1,TARSKI:def 4;
    then
A4: a in Terminals (DTConMSA X) by A3,CARD_3:def 4;
    then reconsider a as Symbol of DTConMSA(X);
    reconsider b = root-tree a as Element of TS(DTConMSA X) by A4,
DTCONSTR:def 1;
    b in A by A2;
    hence thesis;
  end;
end;

definition
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S;
  func FreeSort(X) -> ManySortedSet of the carrier of S means
  :Def11:
  for s be SortSymbol of S holds it.s = FreeSort(X,s);
  existence
  proof
    deffunc F(Element of S)=FreeSort(X,$1);
    consider f be Function such that
A1: dom f = the carrier of S & for d be Element of S holds f.d =F(d)
    from FUNCT_1:sch 4;
    reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2
,RELAT_1:def 18;
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let A,B be ManySortedSet of the carrier of S;
    assume that
A2: for s be SortSymbol of S holds A.s = FreeSort(X,s) and
A3: for s be SortSymbol of S holds B.s = FreeSort(X,s);
    for i be object st i in the carrier of S holds A.i = B.i
    proof
      let i be object;
      assume i in the carrier of S;
      then reconsider s = i as SortSymbol of S;
      A.s = FreeSort(X,s) by A2;
      hence thesis by A3;
    end;
    hence thesis;
  end;
end;

registration
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S;
  cluster FreeSort(X) -> non-empty;
  coherence
  proof
    let i be object;
    assume i in the carrier of S;
    then reconsider s = i as SortSymbol of S;
    (FreeSort(X)).s = FreeSort(X,s) by Def11;
    hence thesis;
  end;
end;

theorem Th8:
  for S be non void non empty ManySortedSign, X be non-empty
  ManySortedSet of the carrier of S, o be OperSymbol of S, x be set st x in ((
  FreeSort X)# * (the Arity of S)).o holds x is FinSequence of TS(DTConMSA(X))
proof
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, o be OperSymbol of S, x be set;
  set D = DTConMSA(X), ar = the_arity_of o, cr = the carrier of S;
A1: (the Arity of S).o = ar by MSUALG_1:def 1;
  rng ar c= cr & dom ((FreeSort X)) = cr by FINSEQ_1:def 4,PARTFUN1:def 2;
  then
A2: dom ((FreeSort X) * ar) = dom ar by RELAT_1:27;
  assume x in ((FreeSort X)# * (the Arity of S)).o;
  then x in product ((FreeSort X) * ar) by A1,Th1;
  then consider f be Function such that
A3: x = f and
A4: dom f = dom ((FreeSort X) * ar) and
A5: for y be object st y in dom ((FreeSort X)* ar) holds f.y in ((FreeSort
  X) * ar).y by CARD_3:def 5;
  dom ar = Seg len ar by FINSEQ_1:def 3;
  then reconsider f as FinSequence by A4,A2,FINSEQ_1:def 2;
  rng f c= TS D
  proof
    let a be object;
    assume a in rng f;
    then consider b be object such that
A6: b in dom f and
A7: f.b = a by FUNCT_1:def 3;
A8: a in ((FreeSort X) * ar).b by A4,A5,A6,A7;
    reconsider b as Nat by A6;
    ((FreeSort X) * ar).b = (FreeSort X).(ar.b) by A4,A6,FUNCT_1:12
      .= (FreeSort X). (ar/.b) by A4,A2,A6,PARTFUN1:def 6
      .= FreeSort(X,ar/.b) by Def11
      .= { s where s is Element of TS D: (ex x be set st x in X.(ar/.b) & s
= root-tree [x,ar/.b]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = s
    .{} & the_result_sort_of o1=ar/.b};
    then
    ex e be Element of TS D st a = e &( (ex x be set st x in X.(ar/.b) & e
= root-tree [x,(ar/.b)]) or ex o be OperSymbol of S st [o,the carrier of S] = e
    .{} & the_result_sort_of o=ar/.b) by A8;
    hence thesis;
  end;
  then reconsider f as FinSequence of TS(D) by FINSEQ_1:def 4;
  f = x by A3;
  hence thesis;
end;

theorem Th9:
  for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S, o be OperSymbol of S, p be FinSequence of TS
(DTConMSA(X)) holds p in ((FreeSort X)# * (the Arity of S)).o iff dom p = dom (
  the_arity_of o) & for n be Nat st n in dom p holds p.n in FreeSort(X,(
  the_arity_of o)/.n)
proof
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, o be OperSymbol of S, p be FinSequence of TS(DTConMSA(X));
  set AR = the Arity of S, cr = the carrier of S, ar = the_arity_of o;
  thus p in ((FreeSort X)# * AR).o implies dom p = dom (the_arity_of o) & for
  n be Nat st n in dom p holds p.n in FreeSort(X,(the_arity_of o)/.n)
  proof
A1: AR.o = ar by MSUALG_1:def 1;
A2: rng ar c= cr & dom ((FreeSort X)) = cr by FINSEQ_1:def 4,PARTFUN1:def 2;
    then
A3: dom ((FreeSort X) * ar) = dom ar by RELAT_1:27;
    assume p in ((FreeSort X)# * (the Arity of S)).o;
    then
A4: p in product ((FreeSort X) * ar) by A1,Th1;
    then
A5: dom p = dom ((FreeSort X) * ar) by CARD_3:9;
    hence dom p = dom ar by A2,RELAT_1:27;
    let n be Nat;
    assume
A6: n in dom p;
    then ((FreeSort X) * ar).n = (FreeSort X).(ar.n) by A5,FUNCT_1:12
      .= (FreeSort X). (ar/.n) by A5,A3,A6,PARTFUN1:def 6
      .= FreeSort(X,ar/.n) by Def11;
    hence thesis by A4,A5,A6,CARD_3:9;
  end;
  assume that
A7: dom p = dom (the_arity_of o) and
A8: for n be Nat st n in dom p holds p.n in FreeSort(X,(the_arity_of o) /.n);
  rng ar c= cr & dom ((FreeSort X)) = cr by FINSEQ_1:def 4,PARTFUN1:def 2;
  then
A9: dom p = dom ((FreeSort X) * ar) by A7,RELAT_1:27;
A10: for x be object st x in dom((FreeSort X) * ar) holds p.x in ((FreeSort X)
  * ar).x
  proof
    let x be object;
    assume
A11: x in dom ((FreeSort X) * ar);
    then reconsider n = x as Nat;
    FreeSort(X,ar/.n) = (FreeSort X). (ar/.n) by Def11
      .= (FreeSort X).(ar.n) by A7,A9,A11,PARTFUN1:def 6
      .= ((FreeSort X) * ar).x by A11,FUNCT_1:12;
    hence thesis by A8,A9,A11;
  end;
  AR.o = ar by MSUALG_1:def 1;
  then ((FreeSort X)# * AR).o = product ((FreeSort X) * ar) by Th1;
  hence thesis by A9,A10,CARD_3:9;
end;

theorem Th10:
  for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S, o be OperSymbol of S, p be FinSequence of TS
  (DTConMSA(X)) holds Sym(o,X) ==> roots p iff p in ((FreeSort X)# * (the Arity
  of S)).o
proof
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, o be OperSymbol of S, p be FinSequence of TS(DTConMSA(X));
  set D = DTConMSA(X), ar = the_arity_of o;
  set r = roots p, OU = [:the carrier' of S,{the carrier of S}:] \/ Union (
  coprod X);
A1: dom p = dom r by TREES_3:def 18;
  thus Sym(o,X) ==> roots p implies p in ((FreeSort X)# * (the Arity of S)).o
  proof
    assume Sym(o,X) ==> roots p;
    then
A2: [[o,the carrier of S],roots p] in REL(X) by LANG1:def 1;
    then reconsider
    r = roots p as Element of ([:the carrier' of S,{the carrier of
    S}:] \/ Union (coprod X))* by ZFMISC_1:87;
A3: dom p = dom r by TREES_3:def 18;
A4: dom r = Seg len r & Seg len ar = dom ar by FINSEQ_1:def 3;
A5: len r = len ar by A2,Th5;
    for n be Nat st n in dom p holds p.n in FreeSort(X,ar/.n)
    proof
      let n be Nat;
      set s = ar/.n;
      assume
A6:   n in dom p;
      then consider T be DecoratedTree such that
A7:   T = p.n and
A8:   r.n = T.{} by TREES_3:def 18;
      rng p c= TS D & p.n in rng p by A6,FINSEQ_1:def 4,FUNCT_1:def 3;
      then reconsider T as Element of TS(D) by A7;
A9:   rng r c= [:the carrier' of S,{the carrier of S}:] \/ Union (coprod
      X) & r.n in rng r by A3,A6,FINSEQ_1:def 4,FUNCT_1:def 3;
      per cases by A9,XBOOLE_0:def 3;
      suppose
A10:    r.n in [:the carrier' of S,{the carrier of S}:];
        then consider
        o1 being OperSymbol of S, x2 being Element of {the carrier of
        S} such that
A11:    r.n = [o1,x2] by DOMAIN_1:1;
A12:    x2 = the carrier of S by TARSKI:def 1;
        then the_result_sort_of o1 = ar.n by A2,A3,A6,A10,A11,Th5
          .= ar/.n by A5,A3,A4,A6,PARTFUN1:def 6;
        then (ex x be set st x in X.s & T = root-tree [x,s]) or ex o be
OperSymbol of S st [o,the carrier of S] = T.{} & the_result_sort_of o = s by A8
,A11,A12;
        hence thesis by A7;
      end;
      suppose
A13:    r.n in Union (coprod X);
        then r.n in coprod(ar.n,X) by A2,A3,A6,Th5;
        then r.n in coprod(s,X) by A5,A3,A4,A6,PARTFUN1:def 6;
        then
A14:    ex a be set st a in X.s & r.n = [a,s] by Def2;
        reconsider t = r.n as Terminal of D by A13,Th6;
        T = root-tree t by A8,DTCONSTR:9;
        hence thesis by A7,A14;
      end;
    end;
    hence thesis by A5,A3,A4,Th9;
  end;
A15: dom r = Seg len r by FINSEQ_1:def 3;
  reconsider r as FinSequence of OU;
  reconsider r as Element of OU* by FINSEQ_1:def 11;
  assume
A16: p in ((FreeSort X)# * (the Arity of S)).o;
  then
A17: dom p = dom ar by Th9;
A18: Union (coprod X) misses [:the carrier' of S,{the carrier of S}:] by Th4;
A19: for x be set st x in dom r holds (r.x in [:the carrier' of S,{the
carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = r.
x holds the_result_sort_of o1 = ar.x) & (r.x in Union (coprod X) implies r.x in
  coprod(ar.x,X))
  proof
    let x be set;
    assume
A20: x in dom r;
    then reconsider n = x as Nat;
A21: ex T be DecoratedTree st T = p.n & r.n = T.{} by A1,A20,TREES_3:def 18;
    set s = ar/.n;
    p.n in FreeSort(X,s) by A16,A1,A20,Th9;
    then consider a be Element of TS D such that
A22: a = p.n and
A23: (ex x be set st x in X.s & a = root-tree [x,s]) or ex o be
    OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = s;
A24: s = ar.n by A17,A1,A20,PARTFUN1:def 6;
    thus r.x in [:the carrier' of S,{the carrier of S}:] implies for o1 be
OperSymbol of S st [o1,the carrier of S] = r.x holds the_result_sort_of o1 = ar
    .x
    proof
      assume
A25:  r.x in [:the carrier' of S,{the carrier of S}:];
A26:  now
        dom coprod(X) = the carrier of S by PARTFUN1:def 2;
        then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 3;
        then
A27:    coprod(s,X) in rng coprod(X) by Def3;
        given y be set such that
A28:    y in X.s & a = root-tree [y,s];
        r.x = [y,s] & [y,s] in coprod(s,X) by A22,A21,A28,Def2,TREES_4:3;
        then r.x in union rng coprod(X) by A27,TARSKI:def 4;
        then r.x in Union (coprod X) by CARD_3:def 4;
        hence contradiction by A18,A25,XBOOLE_0:3;
      end;
      let o1 be OperSymbol of S;
      assume [o1,the carrier of S] = r.x;
      hence thesis by A22,A23,A21,A24,A26,XTUPLE_0:1;
    end;
    assume
A29: r.x in Union (coprod X);
    now
      given o1 be OperSymbol of S such that
A30:  [o1,the carrier of S] = a.{} and
      the_result_sort_of o1 = s;
      the carrier of S in {the carrier of S} by TARSKI:def 1;
      then [o1,the carrier of S] in [:the carrier' of S,{the carrier of S}:]
      by ZFMISC_1:87;
      hence contradiction by A18,A22,A21,A29,A30,XBOOLE_0:3;
    end;
    then consider y be set such that
A31: y in X.s and
A32: a = root-tree [y,s] by A23;
    r.x = [y,s] by A22,A21,A32,TREES_4:3;
    hence thesis by A24,A31,Def2;
  end;
  len r = len ar by A17,A1,A15,FINSEQ_1:def 3;
  then [[o,the carrier of S],r] in REL X by A19,Th5;
  hence thesis by LANG1:def 1;
end;

theorem Th11:
  for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S holds union rng (FreeSort X) = TS (DTConMSA(X
  ))
proof
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S;
  set D = DTConMSA(X);
A1: dom (FreeSort X) = the carrier of S by PARTFUN1:def 2;
  thus union rng (FreeSort X) c= TS D
  proof
    let x be object;
    assume x in union rng (FreeSort X);
    then consider A be set such that
A2: x in A and
A3: A in rng (FreeSort X) by TARSKI:def 4;
    consider s be object such that
A4: s in dom (FreeSort X) and
A5: (FreeSort X).s = A by A3,FUNCT_1:def 3;
    reconsider s as SortSymbol of S by A4;
    A = FreeSort(X,s) by A5,Def11
      .= {a where a is Element of TS(D): (ex x be set st x in X.s & a =
root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = a.{} &
    the_result_sort_of o1 = s};
    then ex a be Element of TS(D) st a = x &( (ex x be set st x in X.s & a =
root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] =a.{} &
    the_result_sort_of o1 = s) by A2;
    hence thesis;
  end;
  let x be object;
  assume x in TS D;
  then reconsider t = x as Element of TS(D);
A6: rng t c= the carrier of D & the carrier of D = (Terminals D) \/ (
  NonTerminals D) by LANG1:1,RELAT_1:def 19;
  {} in dom t by TREES_1:22;
  then
A7: t.{} in rng t by FUNCT_1:def 3;
A8: NonTerminals D = [:the carrier' of S,{the carrier of S}:] by Th6;
A9: Terminals D = Union (coprod X) by Th6;
  per cases by A7,A6,XBOOLE_0:def 3;
  suppose
A10: t.{} in Terminals D;
    then reconsider a = t.{} as Terminal of D;
    a in union rng(coprod X) by A9,A10,CARD_3:def 4;
    then consider A be set such that
A11: a in A and
A12: A in rng(coprod X) by TARSKI:def 4;
    consider s be object such that
A13: s in dom(coprod X) and
A14: (coprod X).s = A by A12,FUNCT_1:def 3;
    reconsider s as SortSymbol of S by A13;
    A = coprod(s,X) by A14,Def3;
    then t = root-tree a & ex b be set st b in X.s & a = [b,s] by A11,Def2,
DTCONSTR:9;
    then t in FreeSort(X,s);
    then
A15: t in (FreeSort X).s by Def11;
    (FreeSort X).s in rng (FreeSort X) by A1,FUNCT_1:def 3;
    hence thesis by A15,TARSKI:def 4;
  end;
  suppose
    t.{} in NonTerminals D;
    then reconsider a = t.{} as NonTerminal of D;
    consider o being OperSymbol of S, x2 being Element of {the carrier of S}
    such that
A16: a = [o,x2] by A8,DOMAIN_1:1;
    set rs = the_result_sort_of o;
    x2 = the carrier of S by TARSKI:def 1;
    then t in FreeSort(X,rs) by A16;
    then
A17: t in (FreeSort X).rs by Def11;
    (FreeSort X).rs in rng (FreeSort X) by A1,FUNCT_1:def 3;
    hence thesis by A17,TARSKI:def 4;
  end;
end;

theorem Th12:
  for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S, s1,s2 be SortSymbol of S st s1 <> s2 holds (
  FreeSort X).s1 misses (FreeSort X).s2
proof
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, s1,s2 be SortSymbol of S;
  assume that
A1: s1 <> s2 and
A2: (FreeSort X).s1 /\ (FreeSort X).s2 <> {};
  consider x being object such that
A3: x in (FreeSort X).s1 /\ (FreeSort X).s2 by A2,XBOOLE_0:def 1;
  set D = DTConMSA(X);
A4: (FreeSort X).s1 = FreeSort(X,s1) by Def11;
A5: (FreeSort X).s2 = FreeSort(X,s2) by Def11;
  x in (FreeSort X).s2 by A3,XBOOLE_0:def 4;
  then consider b be Element of TS D such that
A6: b = x and
A7: (ex x2 be set st x2 in X.s2 & b = root-tree [x2,s2]) or ex o2 be
  OperSymbol of S st [o2,the carrier of S]=b.{} & the_result_sort_of o2 = s2
by A5;
  x in (FreeSort X).s1 by A3,XBOOLE_0:def 4;
  then consider a be Element of TS D such that
A8: a = x and
A9: (ex x1 be set st x1 in X.s1 & a = root-tree [x1,s1]) or ex o1 be
OperSymbol of S st [o1,the carrier of S] = a.{} & the_result_sort_of o1 = s1
by A4;
  per cases by A9;
  suppose
    ex x1 be set st x1 in X.s1 & a = root-tree [x1,s1];
    then consider x1 be set such that
    x1 in X.s1 and
A10: a = root-tree [x1,s1];
    now
      per cases by A7;
      case
        ex x2 be set st x2 in X.s2 & b = root-tree [x2,s2];
        then consider x2 be set such that
        x2 in X.s2 and
A11:    b = root-tree [x2,s2];
        [x1,s1] = [x2,s2] by A8,A6,A10,A11,TREES_4:4;
        hence contradiction by A1,XTUPLE_0:1;
      end;
      case
        ex o2 be OperSymbol of S st [o2,the carrier of S]=b.{} &
        the_result_sort_of o2 = s2;
        then consider o2 be OperSymbol of S such that
A12:    [o2,the carrier of S] = b.{} and
        the_result_sort_of o2 = s2;
        [o2,the carrier of S] = [x1,s1] by A8,A6,A10,A12,TREES_4:3;
        then
A13:    the carrier of S = s1 by XTUPLE_0:1;
        for X be set holds not X in X;
        hence contradiction by A13;
      end;
    end;
    hence contradiction;
  end;
  suppose
    ex o1 be OperSymbol of S st [o1,the carrier of S] = a.{} &
    the_result_sort_of o1 = s1;
    then consider o1 be OperSymbol of S such that
A14: [o1,the carrier of S] = a.{} and
A15: the_result_sort_of o1 = s1;
    now
      per cases by A7;
      case
        ex x2 be set st x2 in X.s2 & b = root-tree [x2,s2];
        then consider x2 be set such that
        x2 in X.s2 and
A16:    b = root-tree [x2,s2];
        [o1,the carrier of S] = [x2,s2] by A8,A6,A14,A16,TREES_4:3;
        then
A17:    the carrier of S = s2 by XTUPLE_0:1;
        for X be set holds not X in X;
        hence contradiction by A17;
      end;
      case
        ex o2 be OperSymbol of S st [o2,the carrier of S]=b.{} &
        the_result_sort_of o2 = s2;
        hence contradiction by A1,A8,A6,A14,A15,XTUPLE_0:1;
      end;
    end;
    hence contradiction;
  end;
end;

definition
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, o be OperSymbol of S;
  func DenOp(o,X) -> Function of ((FreeSort X)# * (the Arity of S)).o, ((
  FreeSort X) * (the ResultSort of S)).o means
  :Def12:
  for p be FinSequence of TS
  (DTConMSA(X)) st Sym(o,X) ==> roots p holds it.p = (Sym(o,X))-tree p;
  existence
  proof
    set AL = ((FreeSort X)# * (the Arity of S)).o, AX = ((FreeSort X) * (the
    ResultSort of S)).o, D = DTConMSA(X), O = the carrier' of S, rs =
    the_result_sort_of o, RS = the ResultSort of S;
    defpred P[object,object] means
for p be FinSequence of TS D st p = $1 holds $2 =
    (Sym(o,X))-tree p;
A1: for x be object st x in AL ex y be object st y in AX & P[x,y]
    proof
      let x be object;
      assume
A2:   x in AL;
      then reconsider p = x as FinSequence of TS(D) by Th8;
      Sym(o,X) ==> roots p by A2,Th10;
      then reconsider a = (Sym(o,X))-tree p as Element of TS D by
DTCONSTR:def 1;
      take y = (Sym(o,X))-tree p;
      o in O;
      then o in dom ((FreeSort X) * RS) by PARTFUN1:def 2;
      then
A3:   AX =(FreeSort X).(RS.o) by FUNCT_1:12
        .= (FreeSort X).rs by MSUALG_1:def 2
        .= FreeSort(X,rs) by Def11;
      a.{} = Sym(o,X) by TREES_4:def 4;
      hence y in AX by A3;
      thus thesis;
    end;
    consider f be Function such that
A4: dom f = AL & rng f c= AX & for x be object st x in AL holds P[x,f.x]
    from FUNCT_1:sch 6(A1);
    reconsider g = f as Function of AL,rng f by A4,FUNCT_2:1;
    reconsider g as Function of AL,AX by A4,FUNCT_2:2;
    take g;
    let p be FinSequence of TS D;
    assume Sym(o,X) ==> roots p;
    then p in AL by Th10;
    hence thesis by A4;
  end;
  uniqueness
  proof
    set AL = ((FreeSort X)# * (the Arity of S)).o, AX = ((FreeSort X) * (the
    ResultSort of S)).o, D = DTConMSA(X);
    let f,g be Function of AL, AX;
    assume that
A5: for p be FinSequence of TS D st Sym(o,X) ==> roots p holds f.p =
    (Sym(o,X))-tree p and
A6: for p be FinSequence of TS D st Sym(o,X) ==> roots p holds g.p =
    (Sym(o,X))-tree p;
A7: for x be object st x in AL holds f.x = g.x
    proof
      let x be object;
      assume
A8:   x in AL;
      then reconsider p = x as FinSequence of TS(D) by Th8;
A9:   Sym(o,X) ==> roots p by A8,Th10;
      then f.p = (Sym(o,X))-tree p by A5;
      hence thesis by A6,A9;
    end;
    thus thesis by A7;
  end;
end;

definition
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S;
  func FreeOper(X) -> ManySortedFunction of (FreeSort X)# * (the Arity of S),
  (FreeSort X) * (the ResultSort of S) means
  :Def13:
  for o be OperSymbol of S holds it.o = DenOp(o,X);
  existence
  proof
    defpred P[object,object] means
for o be OperSymbol of S st $1 = o holds $2 =
    DenOp(o,X);
    set Y = the carrier' of S;
A1: for x be object st x in Y ex y be object st P[x,y]
    proof
      let x be object;
      assume x in Y;
      then reconsider o = x as OperSymbol of S;
      take DenOp(o,X);
      thus thesis;
    end;
    consider f be Function such that
A2: dom f = Y & for x be object st x in Y holds P[x,f.x] from CLASSES1:
    sch 1( A1);
    reconsider f as ManySortedSet of Y by A2,PARTFUN1:def 2,RELAT_1:def 18;
    for x be object st x in dom f holds f.x is Function
    proof
      let x be object;
      assume x in dom f;
      then reconsider o = x as OperSymbol of S;
      f.o = DenOp(o,X) by A2;
      hence thesis;
    end;
    then reconsider f as ManySortedFunction of Y by FUNCOP_1:def 6;
    for x be object st x in Y holds f.x is Function of ((FreeSort X)# * (the
    Arity of S)).x, ((FreeSort X) * (the ResultSort of S)).x
    proof
      let x be object;
      assume x in Y;
      then reconsider o = x as OperSymbol of S;
      f.o = DenOp(o,X) by A2;
      hence thesis;
    end;
    then reconsider
    f as ManySortedFunction of (FreeSort X)# * (the Arity of S), (
    FreeSort X) * (the ResultSort of S) by PBOOLE:def 15;
    take f;
    let o be OperSymbol of S;
    thus thesis by A2;
  end;
  uniqueness
  proof
    let A,B be ManySortedFunction of (FreeSort X)# * (the Arity of S), (
    FreeSort X) * (the ResultSort of S);
    assume that
A3: for o be OperSymbol of S holds A.o = DenOp(o,X) and
A4: for o be OperSymbol of S holds B.o = DenOp(o,X);
    for i be object st i in the carrier' of S holds A.i = B.i
    proof
      let i be object;
      assume i in the carrier' of S;
      then reconsider s = i as OperSymbol of S;
      A.s = DenOp(s,X) by A3;
      hence thesis by A4;
    end;
    hence thesis;
  end;
end;

definition
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S;
  func FreeMSA(X) -> MSAlgebra over S equals
  MSAlgebra (# FreeSort(X),
    FreeOper(X) #);
  coherence;
end;

registration
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S;
  cluster FreeMSA(X) -> strict non-empty;
  coherence by MSUALG_1:def 3;
end;

definition
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, s be SortSymbol of S;
  func FreeGen(s,X) -> Subset of (FreeSort(X)).s means
  :Def15:
  for x be set holds x in it iff ex a be set st a in X.s & x = root-tree [a,s];
  existence
  proof
    defpred P[object] means ex a be set st a in X.s & $1 = root-tree [a,s];
    set D = DTConMSA(X);
    consider A be set such that
A1: for x being object holds x in A iff x in (FreeSort(X)).s & P[x]
from XBOOLE_0:
    sch 1;
    A c= (FreeSort(X)).s
    by A1;
    then reconsider A as Subset of (FreeSort(X)).s;
    for x holds x in A iff P[x]
    proof
      dom coprod(X) = the carrier of S by PARTFUN1:def 2;
      then (coprod(X)).s in rng coprod(X) by FUNCT_1:def 3;
      then
A2:   coprod(s,X) in rng coprod(X) by Def3;
A3:   Terminals D = Union (coprod X) by Th6;
      let x;
      thus x in A implies P[x] by A1;
      set A = {aa where aa is Element of TS(D): (ex x be set st x in X.s & aa
= root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = aa.{}
      & the_result_sort_of o1 = s};
      assume
A4:   P[x];
      then consider a be set such that
A5:   a in X.s and
A6:   x = root-tree [a,s];
A7:   (FreeSort X).s = FreeSort(X,s) by Def11;
      set sa = [a,s];
      sa in coprod(s,X) by A5,Def2;
      then sa in union rng coprod(X) by A2,TARSKI:def 4;
      then
A8:   sa in Terminals D by A3,CARD_3:def 4;
      then reconsider sa as Symbol of D;
      reconsider b = root-tree sa as Element of TS(D) by A8,DTCONSTR:def 1;
      b in A by A5;
      hence thesis by A1,A4,A6,A7;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let A,B be Subset of (FreeSort(X)).s;
    assume that
A9: for x be set holds x in A iff ex a be set st a in X.s & x =
    root-tree [a,s] and
A10: for x be set holds x in B iff ex a be set st a in X.s & x =
    root-tree [a,s];
    thus A c= B
    proof
      let x be object;
      assume x in A;
      then ex a be set st a in X.s & x = root-tree [a,s] by A9;
      hence thesis by A10;
    end;
    let x be object;
    assume x in B;
    then ex a be set st a in X.s & x = root-tree [a,s] by A10;
    hence thesis by A9;
  end;
end;

registration
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, s be SortSymbol of S;
  cluster FreeGen(s,X) -> non empty;
  coherence
  proof
    consider x being object such that
A1: x in X.s by XBOOLE_0:def 1;
    ex a be set st a in X.s & root-tree [x,s] = root-tree [a,s] by A1;
    hence thesis by Def15;
  end;
end;

theorem Th13:
  for S be non void non empty ManySortedSign, X be non-empty
ManySortedSet of the carrier of S, s be SortSymbol of S holds FreeGen(s,X) = {
root-tree t where t is Symbol of DTConMSA(X): t in Terminals DTConMSA(X) & t`2
  = s}
proof
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, s be SortSymbol of S;
  set D = DTConMSA(X), A = {root-tree t where t is Symbol of D : t in
  Terminals D & t`2 = s};
  thus FreeGen(s,X) c= A
  proof
    let x be object;
    assume x in FreeGen(s,X);
    then consider a be set such that
A1: a in X.s and
A2: x = root-tree [a,s] by Def15;
A3: [a,s] in Terminals D by A1,Th7;
    then reconsider t = [a,s] as Symbol of D;
    t`2 = s;
    hence thesis by A2,A3;
  end;
  let x be object;
  assume x in A;
  then consider t be Symbol of D such that
A4: x = root-tree t and
A5: t in Terminals D and
A6: t`2 = s;
  consider s1 be SortSymbol of S, a be set such that
A7: a in X.s1 and
A8: t = [a,s1] by A5,Th7;
  s = s1 by A6,A8;
  hence thesis by A4,A7,A8,Def15;
end;

definition
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S;
  func FreeGen(X) -> GeneratorSet of FreeMSA(X) means
  :Def16:
  for s be SortSymbol of S holds it.s = FreeGen(s,X);
  existence
  proof
    deffunc F(Element of S)=FreeGen($1,X);
    set FM = FreeMSA(X), D = DTConMSA(X);
    consider f be Function such that
A1: dom f = the carrier of S & for s be Element of S holds f.s = F(s)
    from FUNCT_1:sch 4;
    reconsider f as ManySortedSet of the carrier of S by A1,PARTFUN1:def 2
,RELAT_1:def 18;
    f c= the Sorts of FM
    proof
      let x be object;
      assume x in the carrier of S;
      then reconsider s = x as SortSymbol of S;
      f.s = FreeGen(s,X) by A1;
      hence thesis;
    end;
    then reconsider f as MSSubset of FM by PBOOLE:def 18;
    the Sorts of GenMSAlg(f) = the Sorts of FM
    proof
      defpred P[set] means $1 in union rng (the Sorts of GenMSAlg(f));
      the Sorts of GenMSAlg(f) is MSSubset of FM by MSUALG_2:def 9;
      then
A2:   the Sorts of GenMSAlg(f) c= the Sorts of FM by PBOOLE:def 18;
A3:   for nt being Symbol of D, ts being FinSequence of TS(D) st nt ==>
roots ts & for t being DecoratedTree of the carrier of D st t in rng ts holds P
      [t] holds P[nt-tree ts]
      proof
        set G = GenMSAlg(f), OU = [:the carrier' of S,{the carrier of S}:] \/
        Union (coprod (X qua ManySortedSet of the carrier of S));
        let nt be Symbol of D, ts be FinSequence of TS(D);
        assume that
A4:     nt ==> roots ts and
A5:     for t being DecoratedTree of the carrier of D st t in rng ts
        holds P[t];
        reconsider sy = nt as Element of OU;
A6:     [nt,roots ts] in the Rules of D by A4,LANG1:def 1;
        then reconsider rt = roots ts as Element of OU* by ZFMISC_1:87;
        [sy,rt] in REL(X) by A4,LANG1:def 1;
        then sy in [:the carrier' of S,{the carrier of S}:] by Def7;
        then consider
        o being OperSymbol of S, x2 being Element of {the carrier of
        S} such that
A7:     sy = [o,x2] by DOMAIN_1:1;
        set ar = the_arity_of o, rs = the_result_sort_of o;
A8:     x2 = the carrier of S by TARSKI:def 1;
        [nt,roots ts] in REL(X) by A4,LANG1:def 1;
        then
A9:     len rt = len ar by A7,A8,Th5;
        reconsider B = the Sorts of G as MSSubset of FM by MSUALG_2:def 9;
A10:    dom B = the carrier of S by PARTFUN1:def 2;
A11:    dom (roots ts) = dom ts by TREES_3:def 18;
        rng ar c= the carrier of S by FINSEQ_1:def 4;
        then
A12:    dom (B * ar) = dom ar by A10,RELAT_1:27;
A13:    Seg len rt = dom rt & Seg len ar = dom ar by FINSEQ_1:def 3;
        then
A14:    dom ts = dom ar by A6,A7,A8,A11,Th5;
A15:    for x being object st x in dom (B * ar) holds ts.x in (B * ar).x
        proof
          let x be object;
          assume
A16:      x in dom (B * ar);
          then reconsider n = x as Nat;
A17:      ts.n in rng ts by A12,A11,A9,A13,A16,FUNCT_1:def 3;
          rng ts c= TS D by FINSEQ_1:def 4;
          then reconsider T = ts.x as Element of TS(D) by A17;
          P[T] by A5,A17;
          then consider A be set such that
A18:      T in A and
A19:      A in rng (the Sorts of G) by TARSKI:def 4;
          set b = ar/.n, A1 = {a where a is Element of TS D: (ex x be set st x
in X.b & a = root-tree [x,b]) or ex o be OperSymbol of S st [o,the carrier of S
          ] = a.{} & the_result_sort_of o = b};
A20:      A1 = FreeSort(X,b) .= (FreeSort X).b by Def11;
A21:      ex t be DecoratedTree st t = ts.n & rt.n = t.{} by A12,A11,A9,A13,A16
,TREES_3:def 18;
          consider s be object such that
A22:      s in dom(the Sorts of G) and
A23:      (the Sorts of G).s = A by A19,FUNCT_1:def 3;
          reconsider s as SortSymbol of S by A22;
A24:      rng rt c= [:the carrier' of S,{the carrier of S}:] \/ Union (
coprod X) & rt. n in rng rt by A12,A9,A13,A16,FINSEQ_1:def 4,FUNCT_1:def 3;
A25:      now
            per cases by A24,XBOOLE_0:def 3;
            suppose
A26:          rt.n in [:the carrier' of S,{the carrier of S}:];
              then consider o1 being OperSymbol of S, x2 being Element of {the
              carrier of S} such that
A27:          rt.n = [o1,x2] by DOMAIN_1:1;
A28:          x2 = the carrier of S by TARSKI:def 1;
              then
              the_result_sort_of o1 = ar.n by A6,A7,A8,A12,A11,A14,A16,A26,A27
,Th5
                .= b by A12,A16,PARTFUN1:def 6;
              hence T in (FreeSort X).b by A20,A21,A27,A28;
            end;
            suppose
A29:          rt.n in Union (coprod X);
              then rt.n in coprod(ar.n,X) by A6,A7,A8,A12,A11,A14,A16,Th5;
              then rt.n in coprod(b,X) by A12,A16,PARTFUN1:def 6;
              then
A30:          ex a be set st a in X.b & rt.n = [a,b] by Def2;
              reconsider tt = rt.n as Terminal of D by A29,Th6;
              T = root-tree tt by A21,DTCONSTR:9;
              hence T in (FreeSort X).b by A20,A30;
            end;
          end;
A31:      now
            assume b <> s;
            then
A32:        (FreeSort X).s misses (FreeSort X).b by Th12;
            (the Sorts of G).s c= (the Sorts of FM).s by A2;
            hence contradiction by A18,A23,A25,A32,XBOOLE_0:3;
          end;
          (B * ar).x = B.(ar.n) by A16,FUNCT_1:12
            .= B.(ar/.n) by A12,A16,PARTFUN1:def 6;
          hence thesis by A18,A23,A31;
        end;
        set AR = the Arity of S, RS = the ResultSort of S, BH = B# * the Arity
        of S, O = the carrier' of S;
A33:    Den(o,FM) = (FreeOper X).o by MSUALG_1:def 6
          .= DenOp(o,X) by Def13;
A34:    Sym(o,X) = [o,the carrier of S] & nt = [o,the carrier of S] by A7,
TARSKI:def 1;
        AR.o = ar by MSUALG_1:def 1;
        then BH.o = product (B * ar) by Th1;
        then
A35:    ts in BH.o by A12,A11,A9,A13,A15,CARD_3:9;
        dom DenOp(o,X) = ((FreeSort X)# * AR).o by FUNCT_2:def 1;
        then ts in dom DenOp(o,X) by A4,A34,Th10;
        then ts in (dom DenOp(o,X)) /\ (BH.o) by A35,XBOOLE_0:def 4;
        then
A36:    ts in dom (DenOp(o,X) | (BH.o)) by RELAT_1:61;
        then (DenOp(o,X) | (BH.o)).ts = (DenOp(o,X)).ts by FUNCT_1:47
          .= nt-tree ts by A4,A34,Def12;
        then
A37:    nt-tree ts in rng ((Den(o,FM))|(BH.o)) by A33,A36,FUNCT_1:def 3;
        RS.o = rs & dom (B * RS) = O by MSUALG_1:def 2,PARTFUN1:def 2;
        then
A38:    (B * RS).o = B.rs by FUNCT_1:12;
        B is opers_closed by MSUALG_2:def 9;
        then B is_closed_on o by MSUALG_2:def 6;
        then
A39:    rng ((Den(o,FM))|(BH.o)) c= (B * RS).o by MSUALG_2:def 5;
        B.rs in rng B by A10,FUNCT_1:def 3;
        hence thesis by A39,A37,A38,TARSKI:def 4;
      end;
A40:  for s be Symbol of D st s in Terminals D holds P[root-tree s]
      proof
        let t be Symbol of D;
        assume t in Terminals D;
        then t in Union (coprod X) by Th6;
        then t in union rng(coprod X) by CARD_3:def 4;
        then consider A be set such that
A41:    t in A and
A42:    A in rng (coprod X) by TARSKI:def 4;
        consider s be object such that
A43:    s in dom (coprod X) and
A44:    (coprod X).s = A by A42,FUNCT_1:def 3;
        reconsider s as SortSymbol of S by A43;
        A = coprod(s,X) by A44,Def3;
        then ex a be set st a in X.s & t = [a,s] by A41,Def2;
        then
A45:    root-tree t in FreeGen(s,X) by Def15;
        f is MSSubset of GenMSAlg(f) by MSUALG_2:def 17;
        then f c= the Sorts of GenMSAlg(f) by PBOOLE:def 18;
        then f.s c= (the Sorts of GenMSAlg(f)).s;
        then
A46:    FreeGen(s,X) c= (the Sorts of GenMSAlg(f)).s by A1;
        dom (the Sorts of GenMSAlg(f)) = the carrier of S by PARTFUN1:def 2;
        then
        (the Sorts of GenMSAlg(f)).s in rng (the Sorts of GenMSAlg(f)) by
FUNCT_1:def 3;
        hence thesis by A46,A45,TARSKI:def 4;
      end;
A47:  for t being DecoratedTree of the carrier of D st t in TS D holds P[
      t] from DTCONSTR:sch 7(A40,A3);
A48:  union rng(the Sorts of FM) c= union rng (the Sorts of GenMSAlg(f))
      proof
        set D = DTConMSA(X);
        let x be object;
        assume x in union rng(the Sorts of FM);
        then consider A be set such that
A49:    x in A and
A50:    A in rng(the Sorts of FM) by TARSKI:def 4;
        consider s be object such that
A51:    s in dom (FreeSort X) and
A52:    (FreeSort X).s = A by A50,FUNCT_1:def 3;
        reconsider s as SortSymbol of S by A51;
        A = FreeSort(X,s) by A52,Def11
          .= {a where a is Element of TS(D): (ex x be set st x in X.s & a =
root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] = a.{} &
        the_result_sort_of o1 = s};
        then ex a be Element of TS(D) st a = x &( (ex x be set st x in X.s & a
= root-tree [x,s]) or ex o1 be OperSymbol of S st [o1,the carrier of S] =a.{} &
        the_result_sort_of o1 = s) by A49;
        hence thesis by A47;
      end;
      let x be Element of S;
      reconsider s = x as SortSymbol of S;
      thus (the Sorts of GenMSAlg(f)).x c= (the Sorts of FM).x
           by A2;
        let a be object;
        assume
A53:    a in (the Sorts of FM).x;
        the carrier of S = dom (the Sorts of FM) by PARTFUN1:def 2;
        then (the Sorts of FM).s in rng (the Sorts of FM) by FUNCT_1:def 3;
        then a in union rng (the Sorts of FM) by A53,TARSKI:def 4;
        then consider A be set such that
A54:    a in A and
A55:    A in rng (the Sorts of GenMSAlg(f)) by A48,TARSKI:def 4;
        consider b be object such that
A56:    b in dom (the Sorts of GenMSAlg(f)) and
A57:    (the Sorts of GenMSAlg(f)).b = A by A55,FUNCT_1:def 3;
        reconsider b as SortSymbol of S by A56;
        now
          assume b <> s;
          then (FreeSort X).s misses (FreeSort X).b by Th12;
          then
A58:      (FreeSort X).s /\ (FreeSort X).b = {};
          (the Sorts of GenMSAlg(f)).b c= (the Sorts of FM).b by A2;
          hence contradiction by A53,A54,A57,A58,XBOOLE_0:def 4;
        end;
        hence thesis by A54,A57;
    end;
    then reconsider f as GeneratorSet of FM by Def4;
    take f;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let A,B be GeneratorSet of FreeMSA(X);
    assume that
A59: for s be SortSymbol of S holds A.s = FreeGen(s,X) and
A60: for s be SortSymbol of S holds B.s = FreeGen(s,X);
    for i be object st i in the carrier of S holds A.i = B.i
    proof
      let i be object;
      assume i in the carrier of S;
      then reconsider s = i as SortSymbol of S;
      A.s = FreeGen(s,X) by A59;
      hence thesis by A60;
    end;
    hence thesis;
  end;
end;

theorem
  for S be non void non empty ManySortedSign, X be non-empty
  ManySortedSet of the carrier of S holds FreeGen(X)is non-empty
proof
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S;
  let x be object;
  assume x in the carrier of S;
  then reconsider s = x as SortSymbol of S;
  (FreeGen(X)).s = FreeGen(s,X) by Def16;
  hence thesis;
end;

theorem
  for S be non void non empty ManySortedSign, X be non-empty
  ManySortedSet of the carrier of S holds union rng FreeGen(X) = {root-tree t
  where t is Symbol of DTConMSA(X): t in Terminals DTConMSA(X)}
proof
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S;
  set D = DTConMSA(X), A = union rng FreeGen(X), B = {root-tree t where t is
  Symbol of D : t in Terminals D};
  thus A c= B
  proof
    let x be object;
    assume x in A;
    then consider C be set such that
A1: x in C and
A2: C in rng FreeGen(X) by TARSKI:def 4;
    consider s be object such that
A3: s in dom FreeGen(X) and
A4: (FreeGen(X)).s = C by A2,FUNCT_1:def 3;
    reconsider s as SortSymbol of S by A3;
    C = FreeGen(s,X) by A4,Def16
      .= {root-tree t where t is Symbol of D : t in Terminals D & t`2 = s}
    by Th13;
    then
    ex t be Symbol of D st x = root-tree t & t in Terminals D & t`2 = s by A1;
    hence thesis;
  end;
  let x be object;
  assume x in B;
  then consider t be Symbol of D such that
A5: x = root-tree t and
A6: t in Terminals D;
  consider s be SortSymbol of S, a be set such that
  a in X.s and
A7: t = [a,s] by A6,Th7;
  t`2 = s by A7;
  then
  x in {root-tree tt where tt is Symbol of D : tt in Terminals D & tt`2 =
  s} by A5,A6;
  then x in FreeGen(s,X) by Th13;
  then
A8: x in (FreeGen(X)).s by Def16;
  dom FreeGen(X) = the carrier of S by PARTFUN1:def 2;
  then (FreeGen(X)).s in rng (FreeGen(X)) by FUNCT_1:def 3;
  hence thesis by A8,TARSKI:def 4;
end;

definition
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, s be SortSymbol of S;
  func Reverse(s,X) -> Function of FreeGen(s,X),X.s means
  :Def17:
  for t be
Symbol of DTConMSA(X) st root-tree t in FreeGen(s,X) holds it.(root-tree t) = t
  `1;
  existence
  proof
    set A = FreeGen(s,X), D = DTConMSA(X);
    defpred P[object,object] means
for t be Symbol of D st $1 = root-tree t holds $2
    = t`1;
A1: for x be object st x in A ex a be object st a in X.s & P[x,a]
    proof
      let x be object;
      assume x in A;
      then
      x in {root-tree t where t is Symbol of D: t in Terminals D & t`2 = s
      } by Th13;
      then consider t be Symbol of D such that
A2:   x = root-tree t and
A3:   t in Terminals D and
A4:   t`2 = s;
      consider s1 be SortSymbol of S, a be set such that
A5:   a in X.s1 and
A6:   t = [a,s1] by A3,Th7;
      take a;
      thus a in X.s by A4,A5,A6;
      let t1 be Symbol of D;
      assume x = root-tree t1;
      then t = t1 by A2,TREES_4:4;
      hence thesis by A6;
    end;
    consider f be Function such that
A7: dom f = A & rng f c= X.s & for x be object st x in A holds P[x,f.x]
    from FUNCT_1:sch 6(A1);
    reconsider f as Function of A,X.s by A7,FUNCT_2:2;
    take f;
    let t be Symbol of D;
    assume root-tree t in A;
    hence thesis by A7;
  end;
  uniqueness
  proof
    set D = DTConMSA(X), C = {root-tree t where t is Symbol of D : t in
    Terminals D & t`2 = s};
    let A,B be Function of FreeGen(s,X),X.s;
    assume that
A8: for t be Symbol of DTConMSA(X) st root-tree t in FreeGen(s,X)
    holds A.(root-tree t) = t`1 and
A9: for t be Symbol of DTConMSA(X) st root-tree t in FreeGen(s,X)
    holds B.(root-tree t) = t`1;
A10: FreeGen(s,X) = C by Th13;
A11: for i be object st i in C holds A.i = B.i
    proof
      let i be object;
      assume
A12:  i in C;
      then consider t be Symbol of D such that
A13:  i = root-tree t and
      t in Terminals D and
      t`2 = s;
      A.(root-tree t) = t`1 by A8,A10,A12,A13;
      hence thesis by A9,A10,A12,A13;
    end;
    dom A = C & dom B = C by A10,FUNCT_2:def 1;
    hence thesis by A11,FUNCT_1:2;
  end;
end;

definition
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S;
  func Reverse(X) -> ManySortedFunction of FreeGen(X),X means
  :Def18:
  for s be SortSymbol of S holds it.s = Reverse(s,X);
  existence
  proof
    defpred P[object,object] means
for s be SortSymbol of S st s = $1 holds $2 =
    Reverse(s,X);
    set I = the carrier of S, FG = FreeGen(X);
A1: for i be object st i in I ex u be object st P[i,u]
    proof
      let i be object;
      assume i in I;
      then reconsider s = i as SortSymbol of S;
      take Reverse(s,X);
      let s1 be SortSymbol of S;
      assume s1 = i;
      hence thesis;
    end;
    consider H be Function such that
A2: dom H = I & for i be object st i in I holds P[i,H.i] from CLASSES1:
    sch 1 (A1);
    reconsider H as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18;
    for x be object st x in dom H holds H.x is Function
    proof
      let i be object;
      assume i in dom H;
      then reconsider s = i as SortSymbol of S;
      H.s = Reverse(s,X) by A2;
      hence thesis;
    end;
    then reconsider H as ManySortedFunction of I by FUNCOP_1:def 6;
    for i be object st i in I holds H.i is Function of FG.i,X.i
    proof
      let i be object;
      assume i in I;
      then reconsider s = i as SortSymbol of S;
      (FreeGen X).s = FreeGen(s,X) & H.i = Reverse(s,X) by A2,Def16;
      hence thesis;
    end;
    then reconsider H as ManySortedFunction of FG,X by PBOOLE:def 15;
    take H;
    let s be SortSymbol of S;
    thus thesis by A2;
  end;
  uniqueness
  proof
    let A,B be ManySortedFunction of FreeGen(X),X;
    assume that
A3: for s be SortSymbol of S holds A.s = Reverse(s,X) and
A4: for s be SortSymbol of S holds B.s = Reverse(s,X);
    for i be object st i in the carrier of S holds A.i = B.i
    proof
      let i be object;
      assume i in the carrier of S;
      then reconsider s = i as SortSymbol of S;
      A.s = Reverse(s,X) by A3;
      hence thesis by A4;
    end;
    hence thesis;
  end;
end;

definition
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, A be non-empty ManySortedSet of the carrier of S, F be
  ManySortedFunction of FreeGen(X), A, t be Symbol of DTConMSA(X);
  assume
A1: t in Terminals (DTConMSA(X));
  func pi(F,A,t) -> Element of Union A means
  :Def19:
  for f be Function st f = F.(t`2) holds it = f.(root-tree t);
  existence
  proof
    set FG = FreeGen(X), D = DTConMSA(X);
    consider s be SortSymbol of S, x be set such that
    x in X.s and
A2: t = [x,s] by A1,Th7;
    FG.s = FreeGen(s,X) by Def16;
    then
A3: dom (F.s) = FreeGen(s,X) by FUNCT_2:def 1
      .= {root-tree tt where tt is Symbol of D: tt in Terminals D & tt`2 = s
    } by Th13;
    t`2 = s by A2;
    then root-tree t in dom (F.s) by A1,A3;
    then
A4: (F.s).(root-tree t) in rng (F.s) by FUNCT_1:def 3;
    dom A = the carrier of S by PARTFUN1:def 2;
    then rng (F.s) c= A.s & A.s in rng A by FUNCT_1:def 3,RELAT_1:def 19;
    then (F.s).(root-tree t) in union rng A by A4,TARSKI:def 4;
    then reconsider eu = (F.s).(root-tree t) as Element of Union A by
CARD_3:def 4;
    take eu;
    let f be Function;
    assume f = F.(t`2);
    hence thesis by A2;
  end;
  uniqueness
  proof
    consider s be SortSymbol of S, x be set such that
    x in X.s and
A5: t = [x,s] by A1,Th7;
    reconsider f = F.s as Function;
    let a,b be Element of Union A;
    assume that
A6: for f be Function st f = F.(t`2) holds a = f.(root-tree t) and
A7: for f be Function st f = F.(t`2) holds b = f.(root-tree t);
A8: f = F.(t`2) by A5;
    then a = f.(root-tree t) by A6;
    hence thesis by A7,A8;
  end;
end;

definition
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S, t be Symbol of DTConMSA(X);
  assume
A1: ex p be FinSequence st t ==> p;
  func @(X,t) -> OperSymbol of S means
  :Def20:
  [it,the carrier of S] = t;
  existence
  proof
    set D = DTConMSA(X), OU = [:the carrier' of S,{the carrier of S}:] \/
    Union (coprod (X qua ManySortedSet of the carrier of S));
    reconsider a = t as Element of OU;
    consider p be FinSequence such that
A2: t ==> p by A1;
    [t,p] in the Rules of D by A2,LANG1:def 1;
    then reconsider p as Element of OU* by ZFMISC_1:87;
    [a,p] in REL(X) by A2,LANG1:def 1;
    then a in [:the carrier' of S,{the carrier of S}:] by Def7;
    then consider
    o being OperSymbol of S, x2 being Element of {the carrier of S}
    such that
A3: a = [o,x2] by DOMAIN_1:1;
    take o;
    thus thesis by A3,TARSKI:def 1;
  end;
  uniqueness by XTUPLE_0:1;
end;

definition
  let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S
  , o be OperSymbol of S, p be FinSequence;
  assume
A1: p in Args(o,U0);
  func pi(o,U0,p) -> Element of Union (the Sorts of U0) equals
  :Def21:
  Den(o,
  U0).p;
  coherence
  proof
    set F = Den(o,U0), S0 = the Sorts of U0;
    dom F = Args(o,U0) by FUNCT_2:def 1;
    then rng F c= Result(o,U0) & F.p in rng F by A1,FUNCT_1:def 3
,RELAT_1:def 19;
    then F.p in union rng S0 by TARSKI:def 4;
    hence thesis by CARD_3:def 4;
  end;
end;

theorem Th16:
  for S be non void non empty ManySortedSign, X be non-empty
  ManySortedSet of the carrier of S holds FreeGen(X) is free
proof
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S;
  set D = DTConMSA(X), FA = FreeMSA(X), FG = FreeGen(X);
  let U1 be non-empty MSAlgebra over S, F be ManySortedFunction of FG,the
  Sorts of U1;
  set SA =the Sorts of FA, AR = the Arity of S, S1 = the Sorts of U1, O = the
  carrier' of S, RS = the ResultSort of S, DU = Union (the Sorts of U1);
  deffunc TermVal(Symbol of D) = pi(F,the Sorts of U1,$1);
  deffunc NTermVal(Symbol of D, FinSequence, FinSequence) = pi(@(X,$1),U1,$3);
  consider G being Function of TS(D), DU such that
A1: for t being Symbol of D st t in Terminals D holds G.(root-tree t) =
  TermVal(t) and
A2: for nt be Symbol of D, ts be FinSequence of TS(D) st nt ==> roots ts
  holds G.(nt-tree ts) = NTermVal(nt,roots ts,G * ts) from DTCONSTR:sch 8;
  deffunc F(object) = G | ((the Sorts of FA).$1);
  consider h be Function such that
A3: dom h = the carrier of S & for s be object st s in the carrier of S
  holds h.s = F(s) from FUNCT_1:sch 3;
  reconsider h as ManySortedSet of the carrier of S by A3,PARTFUN1:def 2
,RELAT_1:def 18;
  for s be object st s in dom h holds h.s is Function
  proof
    let s be object;
    assume s in dom h;
    then h.s = G | ((the Sorts of FA).s) by A3;
    hence thesis;
  end;
  then reconsider h as ManySortedFunction of the carrier of S by FUNCOP_1:def 6
;
  defpred P[set] means for s be SortSymbol of S st $1 in (the Sorts of FA).s
  holds (h.s).$1 in (the Sorts of U1).s;
A4: for nt being Symbol of D, ts being FinSequence of TS(D) st nt ==> roots
  ts & for t being DecoratedTree of the carrier of D st t in rng ts holds P[t]
  holds P[nt-tree ts]
  proof
    let nt be Symbol of D, ts be FinSequence of TS(D);
    assume that
A5: nt ==> roots ts and
A6: for t being DecoratedTree of the carrier of D st t in rng ts holds P[t];
    set p = G * ts, o = @(X,nt), ar = the_arity_of o, rs = the_result_sort_of
    o, OU = [:the carrier' of S,{the carrier of S}:] \/ Union (coprod (X qua
    ManySortedSet of the carrier of S)), rt = roots ts;
A7: [o,the carrier of S] = nt by A5,Def20;
    then
A8: [[o,the carrier of S],rt] in the Rules of D by A5,LANG1:def 1;
A9: [o,the carrier of S] = Sym(o,X);
    then
A10: (DenOp(o,X)).ts = nt-tree ts by A5,A7,Def12;
    dom (DenOp (o,X)) = ((FreeSort X)# * AR).o by FUNCT_2:def 1;
    then ts in dom (DenOp(o,X)) by A5,A7,A9,Th10;
    then
    rng (DenOp (o,X)) c= ((FreeSort X) * RS).o & nt-tree ts in rng (DenOp
    (o,X)) by A10,FUNCT_1:def 3,RELAT_1:def 19;
    then
A11: nt-tree ts in (SA * RS).o;
    set ppi = pi(o,U1,p);
A12: rng RS c= the carrier of S by RELAT_1:def 19;
A13: rng ar c= the carrier of S by FINSEQ_1:def 4;
    reconsider rt as Element of OU* by A8,ZFMISC_1:87;
A14: len rt = len ar by A8,Th5;
A15: dom rt = Seg len rt by FINSEQ_1:def 3;
    dom SA = the carrier of S by PARTFUN1:def 2;
    then
A16: dom(SA* ar) = dom ar by A13,RELAT_1:27;
A17: ar = AR.o by MSUALG_1:def 1;
    dom S1 = the carrier of S by PARTFUN1:def 2;
    then
A18: dom(S1* ar) = dom ar by A13,RELAT_1:27;
A19: dom rt = dom ts & Seg len ar = dom ar by FINSEQ_1:def 3,TREES_3:def 18;
A20: dom p = dom ts by FINSEQ_3:120;
    then
A21: dom p = dom (S1 * ar) by A18,A8,A15,A19,Th5;
A22: for x being object st x in dom (S1 * ar) holds p.x in (S1 * ar).x
    proof
      let x be object;
      assume
A23:  x in dom (S1 * ar);
      then reconsider n = x as Nat;
A24:  ts.n in rng ts by A18,A14,A15,A19,A23,FUNCT_1:def 3;
      rng ts c= TS D by FINSEQ_1:def 4;
      then reconsider t = ts.n as Element of TS(D) by A24;
A25:  p.n = G.(ts.n) by A21,A23,FINSEQ_3:120;
      ar.x in rng ar by A18,A23,FUNCT_1:def 3;
      then reconsider s = ar.x as SortSymbol of S by A13;
A26:  h.s = G | (SA.s) by A3;
      dom SA = the carrier of S by PARTFUN1:def 2;
      then
A27:  SA.s in rng SA by FUNCT_1:def 3;
      dom G = TS D by FUNCT_2:def 1
        .= union rng SA by Th11;
      then
A28:  dom (h.s) = SA.s by A26,A27,RELAT_1:62,ZFMISC_1:74;
      ts in ((FreeSort X)# * AR).o by A5,A7,A9,Th10;
      then ts in product ((FreeSort X) * ar) by A17,Th1;
      then ts.x in ((FreeSort X) * ar).x by A18,A16,A23,CARD_3:9;
      then
A29:  ts.x in (FreeSort X).(ar.x) by A18,A16,A23,FUNCT_1:12;
      then (h.s).t in S1.s by A6,A24;
      then G.t in S1.s by A29,A26,A28,FUNCT_1:47;
      hence thesis by A23,A25,FUNCT_1:12;
    end;
    dom S1 = the carrier of S by PARTFUN1:def 2;
    then
A30: dom (S1 *RS) = dom RS by A12,RELAT_1:27;
    let s be SortSymbol of S;
A31: dom Den(o,U1) = Args(o,U1) by FUNCT_2:def 1;
A32: dom RS = O by FUNCT_2:def 1;
    dom SA = the carrier of S by PARTFUN1:def 2;
    then dom (SA * RS) = dom RS by A12,RELAT_1:27;
    then nt-tree ts in SA.(RS.o) by A32,A11,FUNCT_1:12;
    then
A33: nt-tree ts in SA.rs by MSUALG_1:def 2;
    Args(o,U1) = (S1# * AR).o by MSUALG_1:def 4
      .= product (S1 * ar) by A17,Th1;
    then
A34: p in Args(o,U1) by A20,A18,A14,A15,A19,A22,CARD_3:9;
    then pi(o,U1,p) = Den(o,U1).p by Def21;
    then rng Den(o,U1) c= Result(o,U1) & ppi in rng Den(o,U1) by A34,A31,
FUNCT_1:def 3,RELAT_1:def 19;
    then
A35: ppi in Result(o,U1);
    assume
A36: nt-tree ts in SA.s;
A37: rs = s by A33,A36,XBOOLE_0:3,Th12;
    G.(nt-tree ts) = ppi by A2,A5;
    then
A38: ppi = (G | (SA.rs)).(nt-tree ts) by A33,FUNCT_1:49;
    Result(o,U1) = (S1 *RS).o by MSUALG_1:def 5
      .= S1.(RS.o) by A30,A32,FUNCT_1:12
      .= S1.rs by MSUALG_1:def 2;
    hence thesis by A3,A35,A38,A37;
  end;
A39: for t being Symbol of D st t in Terminals D holds P[root-tree t]
  proof
    let t be Symbol of D;
    assume
A40: t in Terminals D;
    then consider s be SortSymbol of S, x be set such that
    x in X.s and
A41: t = [x,s] by Th7;
    set E = {root-tree tt where tt is Symbol of D: tt in Terminals D & tt`2 =
    s}, a = root-tree t;
A42: t`2 = s by A41;
    then
A43: a in E by A40;
    let s1 be SortSymbol of S;
    reconsider f = F.s as Function of FG.s,S1.s;
A44: dom f = FG.s by FUNCT_2:def 1;
A45: E = FreeGen(s,X) by Th13;
    then FG.s = E by Def16;
    then
A46: rng f c= S1.s & f.a in rng f by A43,A44,FUNCT_1:def 3,RELAT_1:def 19;
    assume
A47: a in SA.s1;
A48: now
      a in (FreeSort X).s /\ (FreeSort X).s1 by A43,A45,A47,XBOOLE_0:def 4;
      then
A49:  (FreeSort X).s meets (FreeSort X).s1;
      assume s <> s1;
      hence contradiction by A49,Th12;
    end;
    h.s = G | (SA.s) by A3;
    then (h.s).a = G.a by A43,A45,FUNCT_1:49
      .= pi(F,S1,t) by A1,A40
      .= f.a by A40,A42,Def19;
    hence thesis by A46,A48;
  end;
A50: for t being DecoratedTree of the carrier of D st t in TS(D) holds P[t]
  from DTCONSTR:sch 7(A39,A4);
  for s be object st s in the carrier of S holds h.s is Function of (the
  Sorts of FA).s, (the Sorts of U1).s
  proof
    let x be object;
    assume x in the carrier of S;
    then reconsider s = x as SortSymbol of S;
A51: dom G = TS D by FUNCT_2:def 1
      .= union rng SA by Th11;
    dom SA = the carrier of S by PARTFUN1:def 2;
    then
A52: SA.s in rng SA by FUNCT_1:def 3;
A53: h.s = G | (SA.s) by A3;
    then
A54: dom (h.s) = SA.s by A51,A52,RELAT_1:62,ZFMISC_1:74;
A55: SA.s c= dom G by A51,A52,ZFMISC_1:74;
    rng (h.s) c= S1.s
    proof
      let a be object;
      assume a in rng (h.s);
      then consider T be object such that
A56:  T in dom (h.s) and
A57:  (h.s).T = a by FUNCT_1:def 3;
      reconsider T as Element of TS(D) by A55,A54,A56,FUNCT_2:def 1;
      T in SA.s by A53,A51,A52,A56,RELAT_1:62,ZFMISC_1:74;
      hence thesis by A50,A57;
    end;
    hence thesis by A54,FUNCT_2:def 1,RELSET_1:4;
  end;
  then reconsider h as ManySortedFunction of FA,U1 by PBOOLE:def 15;
  take h;
  thus h is_homomorphism FA,U1
  proof
    rng RS c= the carrier of S & dom SA = the carrier of S by PARTFUN1:def 2
,RELAT_1:def 19;
    then
A58: dom RS = O & dom (SA * RS) = dom RS by FUNCT_2:def 1,RELAT_1:27;
    let o be OperSymbol of S such that
    Args(o,FA) <> {};
    let x be Element of Args(o,FA);
    set rs = the_result_sort_of o, DA = Den(o,FA), D1 = Den(o,U1), OU = [:the
carrier' of S,{the carrier of S}:] \/ Union (coprod (X qua ManySortedSet of the
    carrier of S)), ar = the_arity_of o;
A59: ar = AR.o by MSUALG_1:def 1;
A60: Args(o,FA) = ((FreeSort X)# * AR).o by MSUALG_1:def 4;
    then reconsider p = x as FinSequence of TS(D) by Th8;
A61: Sym(o,X) ==> roots p by A60,Th10;
    then
A62: @(X,Sym(o,X)) = o by Def20;
A63: dom (G *p) = dom p by FINSEQ_3:120;
A64: x in ((FreeSort X)# * AR).o by A60;
A65: for a be object st a in dom p holds (G*p).a = (h#x).a
    proof
      rng ar c= the carrier of S & dom SA = the carrier of S by FINSEQ_1:def 4
,PARTFUN1:def 2;
      then
A66:  dom(SA* ar) = dom ar by RELAT_1:27;
      set rt = roots p;
      let a be object;
      assume
A67:  a in dom p;
      then reconsider n = a as Nat;
A68:  [[o,the carrier of S],rt] in the Rules of D by A61,LANG1:def 1;
      then reconsider rt as Element of OU* by ZFMISC_1:87;
A69:  len rt = len ar by A68,Th5;
A70:  (G*p).n = G.(x.n) & (h#x).n = (h.(ar/.n)).(x.n) by A63,A67,FINSEQ_3:120
,MSUALG_3:def 6;
A71:  h.(ar/.n) = G | (SA.(ar/.n)) by A3;
A72:  Seg len rt = dom rt by FINSEQ_1:def 3;
A73:  dom rt = dom p & Seg len ar = dom ar by FINSEQ_1:def 3,TREES_3:def 18;
      p in product((FreeSort X) * ar) by A64,A59,Th1;
      then
A74:  p.n in ((FreeSort X) * ar).n by A67,A66,A69,A72,A73,CARD_3:9;
      ((FreeSort X) * ar).n = SA.(ar.n) by A67,A66,A69,A72,A73,FUNCT_1:12
        .= SA.(ar/.n) by A67,A69,A72,A73,PARTFUN1:def 6;
      hence thesis by A70,A71,A74,FUNCT_1:49;
    end;
    dom (h#x) = dom ar by MSUALG_3:6;
    then
A75: G*p = h#x by A63,A65,FUNCT_1:2,MSUALG_3:6;
A76: h.rs = G | (SA.rs) by A3;
A77: dom (DenOp (o,X)) = ((FreeSort X)# * AR).o by FUNCT_2:def 1;
    (DenOp(o,X)).p = (Sym(o,X))-tree p by A61,Def12;
    then rng (DenOp (o,X)) c= ((FreeSort X) * RS).o & (Sym(o,X))-tree p in
    rng (DenOp (o,X)) by A60,A77,FUNCT_1:def 3,RELAT_1:def 19;
    then (Sym(o,X))-tree p in (SA * RS).o;
    then (Sym(o,X))-tree p in SA.(RS.o) by A58,FUNCT_1:12;
    then
A78: (Sym(o,X))-tree p in SA.rs by MSUALG_1:def 2;
    dom SA = the carrier of S by PARTFUN1:def 2;
    then
A79: SA.rs in rng SA by FUNCT_1:def 3;
    dom G = TS D by FUNCT_2:def 1
      .= union rng SA by Th11;
    then
A80: dom (h.rs) = SA.rs by A76,A79,RELAT_1:62,ZFMISC_1:74;
    DA = (FreeOper(X)).o by MSUALG_1:def 6
      .= DenOp(o,X) by Def13;
    then DA.x = (Sym(o,X))-tree p by A61,Def12;
    hence (h.rs).(DA.x) = G.((Sym(o,X))-tree p) by A78,A76,A80,FUNCT_1:47
      .= pi(@(X,Sym(o,X)),U1,G*p) by A2,A61
      .= D1.(h#x) by A62,A75,Def21;
  end;
  for x being object st x in the carrier of S holds (h || FG).x = F.x
  proof
    set hf = h || FG;
    let x be object;
    assume x in the carrier of S;
    then reconsider s = x as SortSymbol of S;
A81: dom (h.s) = SA.s by FUNCT_2:def 1;
A82: dom (hf.s) = FG.s by FUNCT_2:def 1;
A83: FG.s = FreeGen(s,X) by Def16;
A84: hf.s = (h.s) | (FG.s) by Def1;
A85: for a be object st a in FG.s holds (hf.s).a = (F.s).a
    proof
      let a be object;
A86:  h.s = G | (SA.s) by A3;
      assume
A87:  a in FG.s;
      then a in {root-tree t where t is Symbol of D: t in Terminals D & t`2 =
      s } by A83,Th13;
      then consider t be Symbol of D such that
A88:  a = root-tree t & t in Terminals D and
A89:  t`2 = s;
      thus (hf.s).a = (h.s).a by A84,A82,A87,FUNCT_1:47
        .= G.a by A81,A83,A87,A86,FUNCT_1:47
        .= pi(F,S1,t) by A1,A88
        .= (F.s).a by A88,A89,Def19;
    end;
    dom (F.s) = FG.s by FUNCT_2:def 1;
    hence thesis by A82,A85,FUNCT_1:2;
  end;
  hence thesis;
end;

theorem Th17:
  for S be non void non empty ManySortedSign, X be non-empty
  ManySortedSet of the carrier of S holds FreeMSA(X) is free
proof
  let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of
  the carrier of S;
  take FreeGen(X);
  thus thesis by Th16;
end;

registration
  let S be non void non empty ManySortedSign;
  cluster free strict for non-empty MSAlgebra over S;
  existence
  proof
    set U1 = the non-empty MSAlgebra over S;
    set X = the Sorts of U1;
    take FreeMSA(X);
    thus thesis by Th17;
  end;
end;

registration
  let S be non void non empty ManySortedSign, U0 be free MSAlgebra over S;
  cluster free for GeneratorSet of U0;
  existence by Def6;
end;

theorem Th18:
  for S be non void non empty ManySortedSign, U1 be non-empty
  MSAlgebra over S ex U0 be strict free non-empty MSAlgebra over S, F be
  ManySortedFunction of U0,U1 st F is_epimorphism U0,U1
proof
  let S be non void non empty ManySortedSign, U1 be non-empty MSAlgebra over S;
  set S1 = the Sorts of U1, FA = FreeMSA(S1), FG = FreeGen(S1);
  reconsider fa = FA as strict free non-empty MSAlgebra over S by Th17;
  set f = Reverse(S1);
  take fa;
  FG is free by Th16;
  then consider F be ManySortedFunction of FA,U1 such that
A1: F is_homomorphism FA,U1 and
A2: F || FG = f;
  reconsider a = F as ManySortedFunction of fa,U1;
  take a;
  thus a is_homomorphism fa,U1 by A1;
  thus a is "onto"
  proof
    let s be set;
    assume s in the carrier of S;
    then reconsider s0 = s as SortSymbol of S;
    reconsider g = a.s as Function of (the Sorts of fa).s0, S1.s0 by
PBOOLE:def 15;
A3: f.s0 = g | (FG.s0) by A2,Def1;
    then
A4: rng (f.s0) c= rng g by RELAT_1:70;
    thus rng (a.s) c= S1.s by A3,RELAT_1:def 19;
    let x be object;
    set D = DTConMSA(S1), t = [x,s0];
    assume x in S1.s;
    then
A5: t in Terminals D by Th7;
    then reconsider t as Symbol of D;
    t`2 = s0;
    then root-tree t in {root-tree tt where tt is Symbol of D : tt in
    Terminals D & tt`2 = s0} by A5;
    then
A6: root-tree t in FreeGen(s0,S1) by Th13;
A7: f.s0 = Reverse(s0,S1) by Def18;
    then dom (f.s0) = FreeGen(s0,S1) by FUNCT_2:def 1;
    then
A8: (f.s0).(root-tree t) in rng (f.s0) by A6,FUNCT_1:def 3;
    (f.s0).(root-tree t) = t`1 by A7,A6,Def17
      .= x;
    hence thesis by A4,A8;
  end;
end;

theorem
  for S be non void non empty ManySortedSign, U1 be strict non-empty
  MSAlgebra over S ex U0 be strict free non-empty MSAlgebra over S, F be
  ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 & Image F = U1
proof
  let S be non void non empty ManySortedSign, U1 be strict non-empty MSAlgebra
  over S;
  consider U0 be strict free non-empty MSAlgebra over S, F be
  ManySortedFunction of U0,U1 such that
A1: F is_epimorphism U0,U1 by Th18;
  Image F = U1 by A1,MSUALG_3:19;
  hence thesis by A1;
end;

subset_name: curated


TITLE: Confusing definitions of matrix coherence in linear algebra.
QUESTION [2 upvotes]: I am having two different definitions of matrix coherence.
Wikipedia (and its assorted references) defines it as follows: "the coherence or mutual coherence of a matrix A is defined as the maximum absolute value of the cross-correlations between the columns of A."
However, there are machine learning paper(s) that define it as "Matrix coherence measures the extent to which the
singular vectors of a matrix are correlated with the
standard basis".
Are these two different definitions of two different quantities, or is there some relation between the two?

REPLY [1 votes]: Note that the "the cross-correlations between the columns of A" corresponds to find the singular values of the Gramian of A =AA`. The maximum of the singular values gives you a singular vector such that when you do the internal product with the columns of A you will get which row has the maximum coherence. So, in a way both descriptions will lead to identify the max coherence row of A.


TITLE: Haag's theorem and causal perturbation theory
QUESTION [8 upvotes]: I don't know if this question had been asked before.
By Haag's theorem, interaction picture for quantum field theory cannot exist under some condition. While it is proven that under renormalization, those conditions are not met so interaction picture can still be used.
Now causal perturbation theory is a rigorous way of treating infinities in QFT without renormalization. So in Causal perturbation theory, can interaction picture be applied in this case? I mean when one cannot use renormalization, there is a chance that Haag's theorem is valid in this case.
Edited:
My question arise when I read the statement "renormalisation bypasses Haag’s theorem
" in  Klaczynski's work (https://arxiv.org/abs/1602.00662) on page 71.
The main argument is that the renormalized Lagrangian is not unitary equivalent to original one . I am not familiar with Causal perturbation theory, so the thing I want to know is in the treatment of causal perturbation theory, will unitarily break in some way? Thus making Haag's theorm not hold?

REPLY [5 votes]: Haag's theorem is a result about ground states (more generally, pure states that are invariant under the Poincaré group) and their induced GNS representation of canonical (anti)commutation relations.
It says that two invariant states are either equal or disjoint, where disjoint means that there is no unitary map relating the two corresponding irreducible representations of the algebra of canonical spacetime fields.
The physical consequence is that free and interacting theories, having usually distinct ground states (vacua), are represented in inequivalent ways (do not have "the same Hilbert space", stated in a rougher way).
In order to do scattering theory, in particular to write the S-matrix, one has therefore to do something different from what the naïve ideas suggest. In principle, this could be a serious obstacle to a mathematically rigorous approach to perturbative QFT, but actually it has already been overcome long ago by Haag  himself. The so-called Haag-Ruelle scattering theory (for a reference, one may consult the books by Reed-Simon, vol 3 or 4 I don't remember, and references therein contained) takes into account this problem successfully: an S-matrix is written, and also LSZ formulas are proved.
Of course in Haag-Ruelle scattering theory it is assumed that both the free and the interacting theories are well-defined in a rigorous way (i.e. satisfying the so-called Wightman axioms, or the Osterwalder-Schrader euclidean version).
I am not familiar with the so-called causal perturbation theory. But to me it seems just a way to try and understand the correlation functions of the interacting theory, knowing which the whole theory can be reconstructed (as shown also by Wightman). This is the aim of constructive QFT that was developed mostly in the 60s-70s by Glimm, Jaffe, Simon and others. Using this approach, some interacting theories could be well-defined, such as $P(\phi)_2, \phi^4_3$ and Yukawa in 3 spacetime dimensions. However, the relevant theories in 4 spacetime dimensions have not yet been rigorously dealt with.
To sum up, once the interacting theory is known rigorously, either by tools of causal perturbation theory or by other means, then applying Haag-Ruelle scattering theory would overcome the mathematical difficulties of having inequivalent representations and allows to construct the S-matrix and derive the LSZ formulas, thus putting on solid grounds the perturbation theory used by physicists. Of course, one may see things turned around, and say that the success of predictions based on perturbation theory assures that there is a rigorous, unambiguous, underlying theory. I am sure that this was and still is the point of view driving people to study the rigorous aspects of QFT.


TITLE: How to find the 3D point from projection point?
QUESTION [0 upvotes]: I can calculate projection point on monitor of a 3D polygon using the following equation.
$x'=x/(1+z/d)\\y'=y/(1+z/d)$.
Where $(x,y,z)$ is the $3D$ points and $(x',y')$ is projection points on the monitor. And $d$ is distance between COP(center of projection) and PP(Projection plane/monitor).
Now, I have $3$ points of polygon $(x_1,y_1,z_1),(x_2,y_2,z_2),(x_3,y_3,z_3)$. Using the above equation I can find out $(x'_1,y'_1),(x'_2,y'_2),(x'_3,y'_3)$ on the monitor. After find out the projection point of corner of polygon I can find out all projection points of the polygon.
Now, my question is if I choose a point $(x_p,y_p)$ on the projected polygon that is on the PP, how can I find out the original $3D$ point of this point?
[I need this to implement polygon filling algorithm with shading in computer graphics.]

REPLY [1 votes]: Suppose the $3D$ co-ordinate of COP, projection point, and original object point are $(x_c,y_c,z_c)$, $(x',y',z')$, and $(x_3,y_3,z_3)$.
$\frac{x_c-x'}{x'-x_3}=\frac{y_c-y'}{y'-y_3}=\frac{z_c-z'}{z'-z_3}=k'=\frac{1}{k}$
So, $x_3=x'-k(x_c-x'),\\y_3=y'-k(y_c-y'),\\z_3=z'-k(z_c-z')$
Where $z'=0$ if the PP is on the origin.
To calculate value of k, we have to use the general equation of plane $Ax+By+Cz+d=0$. Substituting $(x,y,z)$ with $(x_3,y_3,z_3)$ we find
$A\{x'-k(x_c-x')\}+B\{y'-k(y_c-y')\}+C\{z'-k(z_c-z')\}+d=0$
$Ax'-Ak(x_c-x')+By'-Bk(y_c-y')+Cz'-Ck(z_c-z')+d=0$
$-k\{A(x_c-x')+Bk(y_c-y')+Ck(z_c-z')\}+Ax'+By'+Cz'+d=0$
$k=\frac{Ax'+By'+Cz'+d}{A(x_c-x')+Bk(y_c-y')+Ck(z_c-z')}$
To know the value of $A,B,C,d$ see this answer


TITLE: Topological type $x_0^2+x_1^2+x_2^2+ x_3^2+x_4^2 = 0$ in $\mathbb P^4$
QUESTION [2 upvotes]: Let's consider projective variety $V$ given by th equation $x_0^2+x_1^2+x_2^2+ x_3^2+x_4^2 = 0 \ $ in $\mathbb CP^4$.
I was wondering what is the Picard group of $V$ ? Or cohomology ring of $V$ ?

REPLY [5 votes]: More generally, the cohomology of any smooth hypersurface in $\mathbb{C}P^n$ is described in the paper 'Topology of nonsingular complex hypersurfaces' by Kulkarni and Wood.  It depends only on $n$ and the degree of the hypersurface.  (In fact, any two smooth hypersurfaces of the same degree are even diffeomorphic.)  The proof is basically Morse theory.