Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### Basic Notation of Universal Algebra

by
Jaroslaw Kotowicz,
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;
```