:: Yet another construction of free algebra
::  by Grzegorz Bancerek and Artur Korni{\l}owicz
::
:: Received August 8, 2001
:: Copyright (c) 2001-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, STRUCT_0, MSUALG_1, CARD_3, RELAT_1, FUNCT_1, SUBSET_1,
      PBOOLE, MSUALG_3, TARSKI, FUNCT_6, MEMBER_1, CATALG_1, ZF_MODEL,
      MSUALG_2, MSAFREE, FUNCOP_1, CARD_1, LANG1, ZFMISC_1, TREES_4, MCART_1,
      MARGREL1, FINSEQ_1, MSATERM, UNIALG_2, DTCONSTR, FINSET_1, TREES_2,
      TREES_9, ZF_LANG1, TREES_3, TREES_A, NUMBERS, ARYTM_3, ORDINAL4,
      XXREAL_0, NAT_1, PARTFUN1, MSUALG_6, PRELAMB, SETLIM_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, DOMAIN_1, RELAT_1,
      FUNCT_1, RELSET_1, STRUCT_0, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, MCART_1,
      FINSET_1, CARD_3, FINSEQ_1, FINSEQ_2, TREES_1, TREES_2, FUNCT_6, TREES_3,
      TREES_4, DTCONSTR, LANG1, PBOOLE, TREES_9, MSUALG_1, MSUALG_2, MSAFREE,
      FUNCOP_1, MSUALG_3, EQUATION, MSATERM, MSUALG_6, CATALG_1, XXREAL_0;
 constructors DOMAIN_1, TREES_9, MSUALG_3, MSATERM, MSUALG_6, CATALG_1,
      EQUATION, SEQ_4, RELSET_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1,
      XREAL_0, FINSEQ_1, TREES_2, TREES_3, TREES_9, STRUCT_0, RELSET_1,
      MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE, MSATERM, INDEX_1, MSUALG_6,
      MSUALG_9, INSTALG1, CATALG_1, MSSUBFAM, PBOOLE, XTUPLE_0;
 requirements BOOLE, SUBSET, NUMERALS;


begin

reserve x,y,z for set;

registration
  let S be non empty non void ManySortedSign;
  let A be non empty MSAlgebra over S;
  cluster Union the Sorts of A -> non empty;
end;

definition
  let S be non empty non void ManySortedSign;
  let A be non empty MSAlgebra over S;
  mode Element of A is Element of Union the Sorts of A;
end;

theorem :: MSAFREE3:1
  for I being set, A being ManySortedSet of I for F being
  ManySortedFunction of I st F is "1-1" & A c= doms F holds F""(F.:.:A) = A;

definition
  let S be non void Signature;
  let X be ManySortedSet of the carrier of S;

  func Free(S, X) -> strict MSAlgebra over S means
:: MSAFREE3:def 1

  ex A being MSSubset
  of FreeMSA (X (\/) ((the carrier of S) --> {0})) st it = GenMSAlg A & A = (
  Reverse (X (\/) ((the carrier of S) --> {0})))""X;
end;

theorem :: MSAFREE3:2
  for S being non void Signature for X being ManySortedSet of the
carrier of S for s being SortSymbol of S holds [x,s] in the carrier of DTConMSA
  X iff x in X.s;

theorem :: MSAFREE3:3
  for S being non void Signature for Y being non-empty
ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds x in X.s & x in Y.s iff root-tree [x,s] in ((
  Reverse Y)""X).s;

theorem :: MSAFREE3:4
  for S being non void Signature for X being ManySortedSet of the
carrier of S for s being SortSymbol of S st x in X.s holds root-tree [x,s] in (
  the Sorts of Free(S, X)).s;

theorem :: MSAFREE3:5
  for S being non void Signature for X being ManySortedSet of the
carrier of S for o being OperSymbol of S st the_arity_of o = {} holds root-tree
  [o, the carrier of S] in (the Sorts of Free(S, X)).the_result_sort_of o;

registration
  let S be non void Signature;
  let X be non empty-yielding ManySortedSet of the carrier of S;
  cluster Free(S, X) -> non empty;
end;

theorem :: MSAFREE3:6
  for S being non void Signature for X being non-empty ManySortedSet of
  the carrier of S holds x is Element of FreeMSA X iff x is Term of S, X;

theorem :: MSAFREE3:7
  for S being non void Signature for X being non-empty
ManySortedSet of the carrier of S for s being SortSymbol of S for x being Term
  of S, X holds x in (the Sorts of FreeMSA X).s iff the_sort_of x = s;

theorem :: MSAFREE3:8
  for S being non void Signature for X being non empty-yielding
ManySortedSet of the carrier of S for x being Element of Free(S, X) holds x is
  Term of S, X (\/) ((the carrier of S) --> {0});

registration
  let S be non empty non void ManySortedSign;
  let X be non empty-yielding ManySortedSet of the carrier of S;
  cluster -> Relation-like Function-like for Element of Free(S, X);
end;

registration
  let S be non empty non void ManySortedSign;
  let X be non empty-yielding ManySortedSet of the carrier of S;
  cluster -> finite DecoratedTree-like for Element of Free(S, X);
end;

registration
  let S be non empty non void ManySortedSign;
  let X be non empty-yielding ManySortedSet of the carrier of S;
  cluster -> finite-branching for Element of Free(S, X);
end;

registration
  cluster -> non empty for DecoratedTree;
end;

definition
  let S be ManySortedSign;
  let t be non empty Relation;
  func S variables_in t -> ManySortedSet of the carrier of S means
:: MSAFREE3:def 2

  for s being object st s in the carrier of S
  holds it.s = {a`1 where a is Element of rng t: a`2 = s};
end;

definition
  let S be ManySortedSign;
  let X be ManySortedSet of the carrier of S;
  let t be non empty Relation;
  func X variables_in t -> ManySortedSubset of X equals
:: MSAFREE3:def 3
     X (/\) (S variables_in t);
end;

theorem :: MSAFREE3:9
  for S being ManySortedSign, X being ManySortedSet of the carrier
of S for t being non empty Relation, V being ManySortedSubset of X holds V = X
  variables_in t iff for s being set st s in the carrier of S holds V.s = (X.s)
  /\ {a`1 where a is Element of rng t: a`2 = s};

theorem :: MSAFREE3:10
  for S being ManySortedSign, s,x being object holds (s in the
  carrier of S implies (S variables_in root-tree [x,s]).s = {x}) &
 for s9 being object st s9 <> s or not s in the carrier of S
  holds (S variables_in root-tree [x,s]).s9 = {};

theorem :: MSAFREE3:11
  for S being ManySortedSign, s being set st s in the carrier of S
  for p being DTree-yielding FinSequence holds x in (S variables_in ([z, the
  carrier of S]-tree p)).s iff ex t being DecoratedTree st t in rng p & x in (S
  variables_in t).s;

theorem :: MSAFREE3:12
  for S being ManySortedSign for X being ManySortedSet of the
  carrier of S for s,x being set holds (x in X.s implies (X variables_in
root-tree [x,s]).s = {x}) & for s9 being set st s9 <> s or not x in X.s holds (
  X variables_in root-tree [x,s]).s9 = {};

theorem :: MSAFREE3:13
  for S being ManySortedSign for X being ManySortedSet of the
  carrier of S for s being set st s in the carrier of S for p being
  DTree-yielding FinSequence holds x in (X variables_in ([z, the carrier of S]
-tree p)).s iff ex t being DecoratedTree st t in rng p & x in (X variables_in t
  ).s;

theorem :: MSAFREE3:14
  for S being non void Signature for X being non-empty
ManySortedSet of the carrier of S for t being Term of S, X holds S variables_in
  t c= X;

definition
  let S be non void Signature;
  let X be non-empty ManySortedSet of the carrier of S;
  let t be Term of S, X;
  func variables_in t -> ManySortedSubset of X equals
:: MSAFREE3:def 4
  S variables_in t;
end;

theorem :: MSAFREE3:15
  for S being non void Signature for X being non-empty
ManySortedSet of the carrier of S for t being Term of S, X holds variables_in t
  = X variables_in t;

definition
  let S be non void Signature;
  let Y be non-empty ManySortedSet of the carrier of S;
  let X be ManySortedSet of the carrier of S;
  func S-Terms(X,Y) -> MSSubset of FreeMSA Y means
:: MSAFREE3:def 5

  for s being
  SortSymbol of S holds it.s = {t where t is Term of S,Y: the_sort_of t = s &
  variables_in t c= X};
end;

theorem :: MSAFREE3:16
  for S being non void Signature for Y being non-empty
ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S
  for s being SortSymbol of S st x in S-Terms(X,Y).s holds x is Term of S,Y;

theorem :: MSAFREE3:17
  for S being non void Signature for Y being non-empty
ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S
  for t being Term of S, Y for s being SortSymbol of S st t in S-Terms(X,Y).s
  holds the_sort_of t = s & variables_in t c= X;

theorem :: MSAFREE3:18
  for S being non void Signature for Y being non-empty
ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S
for s being SortSymbol of S holds root-tree [x,s] in (S-Terms(X,Y)).s iff x in
  X.s & x in Y.s;

theorem :: MSAFREE3:19
  for S being non void Signature for Y being non-empty
ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S
for o being OperSymbol of S for p being ArgumentSeq of Sym(o,Y) holds Sym(o,Y)
-tree p in (S-Terms(X,Y)).the_result_sort_of o iff rng p c= Union (S-Terms(X,Y)
  );

theorem :: MSAFREE3:20
  for S being non void Signature for X being non-empty
ManySortedSet of the carrier of S for A being MSSubset of FreeMSA X holds A is
  opers_closed iff for o being OperSymbol of S, p being ArgumentSeq of Sym(o,X)
  st rng p c= Union A holds Sym(o,X)-tree p in A.the_result_sort_of o;

theorem :: MSAFREE3:21
  for S being non void Signature for Y being non-empty
ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S
  holds S-Terms(X,Y) is opers_closed;

theorem :: MSAFREE3:22
  for S being non void Signature for Y being non-empty
ManySortedSet of the carrier of S for X being ManySortedSet of the carrier of S
  holds (Reverse Y)""X c= S-Terms(X,Y);

theorem :: MSAFREE3:23
  for S being non void Signature for X being ManySortedSet of the
carrier of S for t being Term of S, X (\/) ((the carrier of S)-->{0})
 for s being SortSymbol of S st
  t in S-Terms(X, X (\/) ((the carrier of S)-->{0})).s holds t
  in (the Sorts of Free(S, X)).s;

theorem :: MSAFREE3:24
  for S being non void Signature
  for X being ManySortedSet of the carrier of S
 holds the Sorts of Free(S, X)
   = S-Terms(X, X (\/) ((the carrier of S)-->{0}));

theorem :: MSAFREE3:25
  for S being non void Signature for X being ManySortedSet of the
  carrier of S holds
  (FreeMSA (X (\/) ((the carrier of S)-->{0})))|
   (S-Terms(X, X (\/) ((the carrier of S)-->{0}))) = Free(S, X);

theorem :: MSAFREE3:26
  for S being non void Signature for X,Y being non-empty
  ManySortedSet of the carrier of S for A being MSSubAlgebra of FreeMSA X for B
  being MSSubAlgebra of FreeMSA Y st the Sorts of A = the Sorts of B holds the
  MSAlgebra of A = the MSAlgebra of B;

theorem :: MSAFREE3:27
  for S being non void Signature for X being non empty-yielding
ManySortedSet of the carrier of S for Y being ManySortedSet of the carrier of S
  for t being Element of Free(S, X) holds S variables_in t c= X;

theorem :: MSAFREE3:28
  for S being non void Signature for X being non-empty
ManySortedSet of the carrier of S for t being Term of S,X holds variables_in t
  c= X;

theorem :: MSAFREE3:29
  for S being non void Signature for X,Y being non-empty
ManySortedSet of the carrier of S for t1 being Term of S,X, t2 being Term of S,
  Y st t1 = t2 holds the_sort_of t1 = the_sort_of t2;

theorem :: MSAFREE3:30
  for S being non void Signature for X,Y being non-empty
ManySortedSet of the carrier of S for t being Term of S,Y st variables_in t c=
  X holds t is Term of S,X;

theorem :: MSAFREE3:31
  for S being non void Signature for X being non-empty ManySortedSet of
  the carrier of S holds Free(S, X) = FreeMSA X;

theorem :: MSAFREE3:32
  for S being non void Signature for Y being non-empty
  ManySortedSet of the carrier of S for t being Term of S,Y for p being Element
  of dom t holds variables_in (t|p) c= variables_in t;

theorem :: MSAFREE3:33
  for S being non void Signature for X being non empty-yielding
ManySortedSet of the carrier of S for t being Element of Free(S, X) for p being
  Element of dom t holds t|p is Element of Free(S, X);

theorem :: MSAFREE3:34
  for S being non void Signature for X being non-empty
  ManySortedSet of the carrier of S for t being Term of S,X for a being Element
  of rng t holds a = [a`1,a`2];

theorem :: MSAFREE3:35
  for S being non void Signature for X being non empty-yielding
ManySortedSet of the carrier of S for t being Element of Free(S, X) for s being
SortSymbol of S holds (x in (S variables_in t).s implies [x,s] in rng t) & ([x,
  s] in rng t implies x in (S variables_in t).s & x in X.s);

theorem :: MSAFREE3:36
  for S being non void Signature for X being ManySortedSet of the
  carrier of S st for s being SortSymbol of S st X.s = {} ex o being OperSymbol
  of S st the_result_sort_of o = s & the_arity_of o = {} holds Free(S, X) is
  non-empty;

theorem :: MSAFREE3:37
  for S being non void non empty ManySortedSign for A being
  MSAlgebra over S for B being MSSubAlgebra of A for o being OperSymbol of S
  holds Args(o,B) c= Args(o,A);

theorem :: MSAFREE3:38
  for S being non void Signature for A being feasible MSAlgebra
  over S for B being MSSubAlgebra of A holds B is feasible;

registration
  let S be non void Signature, A be feasible MSAlgebra over S;
  cluster -> feasible for MSSubAlgebra of A;
end;

theorem :: MSAFREE3:39
  for S being non void Signature for X being ManySortedSet of the
  carrier of S holds Free(S, X) is feasible free;

registration
  let S be non void Signature, X be ManySortedSet of the carrier of S;
  cluster Free(S, X) -> feasible free;
end;