The abstract of the Mizar article:

Basic Notation of Universal Algebra

by

Jaroslaw Kotowicz,

Beata Madras, and

Malgorzata Korolkiewicz

Received December 29, 1992

MML identifier: UNIALG_1

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, PARTFUN1, RELAT_1, FUNCT_2, FUNCOP_1, BOOLE, FUNCT_1,
      ZF_REFLE, INCPROJ, UNIALG_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, NAT_1, RELAT_1,
      FUNCT_1, FINSEQ_1, FUNCOP_1, STRUCT_0, PARTFUN1;
 constructors FINSEQ_4, STRUCT_0, FUNCOP_1, PARTFUN1, XREAL_0, XCMPLX_0,
      MEMBERED, XBOOLE_0;
 clusters SUBSET_1, RELSET_1, STRUCT_0, PARTFUN1, FUNCOP_1, ARYTM_3, MEMBERED,
      ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements NUMERALS, BOOLE, SUBSET;


begin

reserve A,z for set,
        x,y for FinSequence of A,
        h for PartFunc of A*,A,
        n,m for Nat;

definition let A;
  let IT be PartFunc of A*,A;
attr IT is homogeneous means
:: UNIALG_1:def 1
 for x,y st x in dom IT & y in dom IT holds len x = len y;
end;

definition let A;
 let IT be PartFunc of A*,A;
attr IT is quasi_total means
:: UNIALG_1:def 2
   for x,y st len x = len y & x in dom IT holds y in dom IT;
end;

definition let A be non empty set;
cluster homogeneous quasi_total non empty PartFunc of A*,A;
end;

theorem :: UNIALG_1:1
 h is non empty iff dom h <> {};

theorem :: UNIALG_1:2
for A being non empty set, a being Element of A
holds {<*>A} -->a is homogeneous quasi_total non empty PartFunc of A*,A;

theorem :: UNIALG_1:3
for A being non empty set, a being Element of A
 holds {<*>A} -->a is Element of PFuncs(A*,A);

definition let A;
 mode PFuncFinSequence of A is FinSequence of PFuncs(A*,A);
 canceled;
end;

definition
  struct (1-sorted) UAStr (# carrier -> set,
                             charact -> PFuncFinSequence of the carrier #);
end;

definition
 cluster non empty strict UAStr;
end;

definition let D be non empty set, c be PFuncFinSequence of D;
 cluster UAStr (#D,c #) -> non empty;
end;

definition let A;
 let IT be PFuncFinSequence of A;
attr IT is homogeneous means
:: UNIALG_1:def 4
   for n,h st n in dom IT & h = IT.n holds h is homogeneous;
end;

definition let A;
 let IT be PFuncFinSequence of A;
 attr IT is quasi_total means
:: UNIALG_1:def 5
   for n,h st n in dom IT & h = IT.n holds h is quasi_total;
end;

definition let F be Function;
 redefine attr F is non-empty means
:: UNIALG_1:def 6
 for n being set st n in dom F holds F.n is non empty;
end;

definition let A be non empty set; let x be Element of PFuncs(A*,A);
 redefine func <*x*> -> PFuncFinSequence of A;
end;

definition let A be non empty set;
cluster homogeneous quasi_total non-empty PFuncFinSequence of A;
end;

definition let IT be UAStr;
attr IT is partial means
:: UNIALG_1:def 7
 the charact of IT is homogeneous;
attr IT is quasi_total means
:: UNIALG_1:def 8
 the charact of IT is quasi_total;
attr IT is non-empty means
:: UNIALG_1:def 9
 the charact of IT <> {} & the charact of IT is non-empty;
end;

reserve A for non empty set,
        h for PartFunc of A*,A ,
        x,y for FinSequence of A,
        a for Element of A;

theorem :: UNIALG_1:4
for x be Element of PFuncs(A*,A) st x = {<*>A} --> a holds
  <*x*> is homogeneous quasi_total non-empty;

definition
 cluster quasi_total partial non-empty strict non empty UAStr;
end;

definition let U1 be partial UAStr;
 cluster the charact of U1 -> homogeneous;
end;

definition let U1 be quasi_total UAStr;
 cluster the charact of U1 -> quasi_total;
end;

definition let U1 be non-empty UAStr;
 cluster the charact of U1 -> non-empty non empty;
end;

definition
mode Universal_Algebra is quasi_total partial non-empty non empty UAStr;
end;

reserve U1 for partial non-empty non empty UAStr;

definition
  let A;
  let f be homogeneous non empty PartFunc of A*,A;
func arity(f) -> Nat means
:: UNIALG_1:def 10
   x in dom f implies it = len x;
end;

theorem :: UNIALG_1:5
for U1 holds for n st n in dom the charact of(U1) holds
  (the charact of(U1)).n is
   PartFunc of (the carrier of U1)*,the carrier of U1;

definition let U1;
func signature U1 ->FinSequence of NAT means
:: UNIALG_1:def 11
   len it = len the charact of(U1) &
 for n st n in dom it holds
   for h be homogeneous non empty
   PartFunc of (the carrier of U1 )*,the carrier of U1
     st h = (the charact of(U1)).n
    holds it.n = arity(h);
end;