Volume 4, 1992

University of Bialystok

Copyright (c) 1992 Association of Mizar Users

### 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;

Back to top