The abstract of the Mizar article:

A Scheme for Extensions of Homomorphisms of Many Sorted Algebras

by

Andrzej Trybulec

Received December 13, 1994

MML identifier: MSAFREE1

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, CARD_3, RELAT_1, PROB_1, LANG1, DTCONSTR, TREES_4,
      FINSEQ_1, TDGROUP, TREES_2, TREES_3, AMI_1, MSUALG_1, PBOOLE, FREEALG,
      BOOLE, MSAFREE, QC_LANG1, ZF_REFLE, TARSKI, MATRIX_1, PROB_2, PRALG_1,
      FINSEQ_4, MCART_1, ALG_1, MSAFREE1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, RELAT_1, FUNCT_1,
      FUNCT_2, STRUCT_0, MCART_1, FINSEQ_1, MULTOP_1, PROB_2, CARD_3, FINSEQ_4,
      TREES_2, TREES_3, TREES_4, AMI_1, LANG1, DTCONSTR, PROB_1, PBOOLE,
      MSUALG_1, MSAFREE, MSUALG_3;
 constructors MULTOP_1, PROB_2, AMI_1, MSAFREE, MSUALG_3, FINSOP_1, FINSEQ_4,
      MEMBERED, XBOOLE_0;
 clusters PBOOLE, MSAFREE, PRALG_1, DTCONSTR, AMI_1, MSUALG_1, MSUALG_3,
      FUNCT_1, RELSET_1, STRUCT_0, TREES_3, FINSEQ_1, SUBSET_1, ARYTM_3,
      ZFMISC_1, XBOOLE_0;
 requirements BOOLE, SUBSET;


begin

theorem :: MSAFREE1:1
 for f,g being Function st g in product f
  holds rng g c= Union f;

scheme DTConstrUniq{DT()->non empty DTConstrStr, D()->non empty set,
                   G(set) -> Element of D(),
                   H(set, set, set) -> Element of D(),
                   f1, f2() -> Function of TS(DT()), D()
                   }:
 f1() = f2()
provided
 for t being Symbol of DT() st t in Terminals DT()
            holds f1().(root-tree t) = G(t) and
 for nt being Symbol of DT(),
          ts being FinSequence of TS(DT()) st nt ==> roots ts
        for x being FinSequence of D() st x = f1() * ts
              holds f1().(nt-tree ts) = H(nt, ts, x) and
 for t being Symbol of DT() st t in Terminals DT()
            holds f2().(root-tree t) = G(t) and
 for nt being Symbol of DT(),
          ts being FinSequence of TS(DT()) st nt ==> roots ts
        for x being FinSequence of D() st x = f2() * ts
              holds f2().(nt-tree ts) = H(nt, ts, x);

theorem :: MSAFREE1:2  :: MSAFREE:5
 for S being non void non empty ManySortedSign,
     X being ManySortedSet of the carrier of S
 for o,b being set st [o,b] in REL(X) holds
  o in [:the OperSymbols of S,{the carrier of S}:] &
   b in ([:the OperSymbols of S,{the carrier of S}:] \/ Union coprod X)*;

theorem :: MSAFREE1:3  :: MSAFREE:5
   for S being non void non empty ManySortedSign,
     X being ManySortedSet of the carrier of S
 for o being OperSymbol of S, b being FinSequence st
      [[o,the carrier of S],b] in REL(X) holds
   len b = len (the_arity_of o) &
   for x be set st x in dom b holds
    (b.x in [:the OperSymbols 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));

definition let D be set;
 redefine mode FinSequence of D -> Element of D*;
end;

definition let I be non empty set, M be non-empty ManySortedSet of I;
 cluster rng M -> non empty with_non-empty_elements;
end;

definition let D be non empty with_non-empty_elements set;
 cluster union D -> non empty;
end;

definition let I be set;
 cluster empty-yielding -> disjoint_valued ManySortedSet of I;
end;

definition let I be set;
 cluster disjoint_valued ManySortedSet of I;
end;

definition let I be non empty set;
 let X be disjoint_valued ManySortedSet of I;
 let D be non-empty ManySortedSet of I;
 let F be ManySortedFunction of X,D;
 func Flatten F -> Function of Union X, Union D means
:: MSAFREE1:def 1
  for i being Element of I, x being set st x in X.i
   holds it.x = F.i.x;
end;

theorem :: MSAFREE1:4
 for I being non empty set,
     X being disjoint_valued ManySortedSet of I,
     D being non-empty ManySortedSet of I
 for F1,F2 be ManySortedFunction of X,D st Flatten F1 = Flatten F2
  holds F1 = F2;

definition let S be non empty ManySortedSign;
 let A be MSAlgebra over S;
 attr A is disjoint_valued means
:: MSAFREE1:def 2
 the Sorts of A is disjoint_valued;
end;

definition let S be non empty ManySortedSign;
 func SingleAlg S -> strict MSAlgebra over S means
:: MSAFREE1:def 3
 for i being set st i in the carrier of S
    holds (the Sorts of it).i = {i};
end;

definition let S be non empty ManySortedSign;
 cluster non-empty disjoint_valued MSAlgebra over S;
end;

definition let S be non empty ManySortedSign;
 cluster SingleAlg S -> non-empty disjoint_valued;
end;

definition let S be non empty ManySortedSign;
 let A be disjoint_valued MSAlgebra over S;
 cluster the Sorts of A -> disjoint_valued;
end;

theorem :: MSAFREE1:5
 for S being non void non empty ManySortedSign, o being OperSymbol of S,
     A1 be non-empty disjoint_valued MSAlgebra over S,
     A2 be non-empty MSAlgebra over S,
     f be ManySortedFunction of A1,A2,
     a be Element of Args(o,A1)
  holds (Flatten f)*a = f#a;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S;
 cluster FreeSort X -> disjoint_valued;
end;

scheme FreeSortUniq{ S() -> non void non empty ManySortedSign,
             X,D() -> non-empty ManySortedSet of the carrier of S(),
             G(set) -> Element of Union D(),
             H(set, set, set) -> Element of Union D(),
             f1, f2() -> ManySortedFunction of FreeSort X(), D()
           }:
 f1() = f2()
provided
 for o being OperSymbol of S(),
       ts being Element of Args(o,FreeMSA X())
    for x being FinSequence of Union D() st x = (Flatten f1()) * ts holds
      f1().(the_result_sort_of o).(Den(o,FreeMSA X()).ts)
        = H(o, ts, x)
    and
 for s being SortSymbol of S(), y be set st y in FreeGen(s,X())
            holds f1().s.y = G(y) and
 for o being OperSymbol of S(), ts being Element of Args(o,FreeMSA X())
    for x being FinSequence of Union D() st x = (Flatten f2()) * ts holds
      f2().(the_result_sort_of o).(Den(o,FreeMSA X()).ts)
       = H(o, ts, x)
    and
 for s being SortSymbol of S(), y be set st y in FreeGen(s,X())
            holds f2().s.y = G(y);

definition let S be non void non empty ManySortedSign;
 let X be non-empty ManySortedSet of the carrier of S;
 cluster FreeMSA X -> non-empty;
end;

definition let S be non void non empty ManySortedSign;
 let o be OperSymbol of S; let A be non-empty MSAlgebra over S;
 cluster Args(o,A) -> non empty;
 cluster Result(o,A) -> non empty;
end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S;
 cluster the Sorts of FreeMSA X -> disjoint_valued;
end;

definition
 let S be non void non empty ManySortedSign,
     X be non-empty ManySortedSet of the carrier of S;
 cluster FreeMSA X -> disjoint_valued;
end;

scheme ExtFreeGen{ S() -> non void non empty ManySortedSign,
             X() -> non-empty ManySortedSet of the carrier of S(),
             MSA() -> non-empty MSAlgebra over S(),
             P[set,set,set],
             IT1, IT2() -> ManySortedFunction of FreeMSA X(), MSA()
            }:
   IT1() = IT2()
 provided
  IT1() is_homomorphism FreeMSA X(), MSA() and
  for s being SortSymbol of S(), x,y being set st y in FreeGen(s,X())
      holds IT1().s.y = x iff P[s,x,y] and
  IT2() is_homomorphism FreeMSA X(), MSA() and
  for s being SortSymbol of S(), x,y being set st y in FreeGen(s,X())
      holds IT2().s.y = x iff P[s,x,y];