The Mizar abstract of MSAFREE3

Journal of Formalized Mathematics
Volume 13, 2001
University of Bialystok
Copyright (c) 2001 Association of Mizar Users
The abstract of the Mizar article:: Yet Another Construction of Free Algebra
by
Grzegorz Bancerek, and
Artur Kornilowicz
Received August 8, 2001
MML identifier: MSAFREE3
[ Mizar article, MML identifier index ]
environ

 vocabulary AMI_1, MSUALG_1, PROB_1, FUNCT_1, RELAT_1, PBOOLE, PRALG_1,
      MSUALG_3, FUNCT_6, CATALG_1, ZF_MODEL, MSUALG_2, MSAFREE, BOOLE,
      FUNCOP_1, ZF_REFLE, LANG1, FREEALG, TREES_4, MCART_1, QC_LANG1, MSATERM,
      UNIALG_2, TDGROUP, FINSEQ_1, MATRIX_1, DTCONSTR, TARSKI, FINSET_1,
      TREES_2, TREES_9, QC_LANG3, TREES_3, CARD_3, FINSEQ_4, MSUALG_6, PRELAMB;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, FUNCT_1,
      RELSET_1, STRUCT_0, NUMBERS, XREAL_0, NAT_1, MCART_1, FINSET_1, CARD_3,
      FINSEQ_1, PROB_1, TREES_1, TREES_2, FUNCT_6, TREES_3, TREES_4, DTCONSTR,
      LANG1, PBOOLE, TREES_9, MSUALG_1, MSUALG_2, PRALG_1, MSAFREE, PRE_CIRC,
      MSUALG_3, EXTENS_1, EQUATION, MSATERM, MSUALG_6, CATALG_1;
 constructors NAT_1, DOMAIN_1, MSAFREE1, TREES_9, PRE_CIRC, EXTENS_1, EQUATION,
      FINSEQ_4, MSATERM, MSUALG_6, CATALG_1;
 clusters SUBSET_1, RELSET_1, FUNCT_1, STRUCT_0, PBOOLE, MSUALG_1, MSUALG_2,
      FINSEQ_1, TREES_9, PRALG_1, CARD_1, MSAFREE, CANTOR_1, TREES_3, MSUALG_6,
      MSUALG_9, MSATERM, TREES_2, INDEX_1, INSTALG1, CATALG_1, MEMBERED,
      RELAT_1, NUMBERS, ORDINAL2;
 requirements BOOLE, SUBSET, NUMERALS;


begin

reserve X,x,y,z for set;

definition
 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;
 canceled;
end;

theorem :: MSAFREE3:1
 for f being Function st X c= dom f & f is one-to-one
  holds f"(f.:X) = X;

theorem :: MSAFREE3:2
   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 2
  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:3
 for S being non void Signature
 for X being non-empty 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:4
 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:5
 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:6
 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;

definition
 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:7
   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:8
 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:9
 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});

definition
 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 Element of Free(S, X);
end;

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

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

definition
 cluster -> non empty 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 3

  for s being set 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 4

  X /\ (S variables_in t);
end;

theorem :: MSAFREE3:10
 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:11
 for S being ManySortedSign, s,x being set holds
   (s in the carrier of S implies (S variables_in root-tree [x,s]).s = {x}) &
   for s' being set st s' <> s or not s in the carrier of S
    holds (S variables_in root-tree [x,s]).s' = {};

theorem :: MSAFREE3:12
 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:13
 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 s' being set st s' <> s or not x in X.s
    holds (X variables_in root-tree [x,s]).s' = {};

theorem :: MSAFREE3:14
 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: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 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 5

  S variables_in t;
end;

theorem :: MSAFREE3:16
 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 6

  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: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 s being SortSymbol of S st x in S-Terms(X,Y).s
  holds x is Term of S,Y;

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 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: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 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:20
 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:21
 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: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 S-Terms(X,Y) is opers_closed;

theorem :: MSAFREE3:23
 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:24
 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:25
 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:26
   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:27
 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:28
 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:29
 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:30
 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:31
 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:32
   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:33
 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:34
 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:35
 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:36
   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:37
   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:38
 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:39
 for S being non void Signature
 for A being feasible MSAlgebra over S
 for B being MSSubAlgebra of A
  holds B is feasible;

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

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

definition
 let S be non void Signature,
     X be ManySortedSet of the carrier of S;
 cluster Free(S, X) -> feasible free;
end;
The abstract of the Mizar article:

Yet Another Construction of Free Algebra
