:: Basic Notation of Universal Algebra
:: by Jaros{\l}aw Kotowicz, Beata Madras and Ma{\l}gorzata Korolkiewicz
::
:: Received December 29, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSEQ_1, PARTFUN1, RELAT_1, NAT_1, FUNCT_2, TARSKI, XBOOLE_0,
SUBSET_1, FUNCOP_1, FUNCT_1, STRUCT_0, NUMBERS, INCPROJ, XXREAL_0,
UNIALG_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, RELAT_1,
FUNCT_1, CARD_3, FINSEQ_1, FINSEQ_2, FUNCOP_1, STRUCT_0, PARTFUN1,
XXREAL_0, MARGREL1;
constructors PARTFUN1, FUNCOP_1, XXREAL_0, FINSEQ_2, STRUCT_0, CARD_3,
MARGREL1;
registrations ORDINAL1, RELSET_1, PARTFUN1, FUNCOP_1, XXREAL_0, STRUCT_0,
FUNCT_1, FINSEQ_1, MARGREL1;
requirements NUMERALS, BOOLE, SUBSET;
begin
reserve
n for Nat;
definition
struct (1-sorted) UAStr (# carrier -> set, charact -> PFuncFinSequence of
the carrier #);
end;
registration
cluster non empty strict for UAStr;
end;
registration
let D be non empty set, c be PFuncFinSequence of D;
cluster UAStr (#D,c #) -> non empty;
end;
definition
let IT be UAStr;
attr IT is partial means
:: UNIALG_1:def 1
the charact of IT is homogeneous;
attr IT is quasi_total means
:: UNIALG_1:def 2
the charact of IT is quasi_total;
attr IT is non-empty means
:: UNIALG_1:def 3
the charact of IT <> {} & the charact of IT is non-empty;
end;
registration
cluster quasi_total partial non-empty strict non empty for UAStr;
end;
registration
let U1 be partial UAStr;
cluster the charact of U1 -> homogeneous;
end;
registration
let U1 be quasi_total UAStr;
cluster the charact of U1 -> quasi_total;
end;
registration
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;
theorem :: UNIALG_1:1
n in dom the charact of U1 implies (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 4
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;
begin :: Addenda
:: from MSSUBLAT, 2007.05.13, A.T.
registration
let U0 be Universal_Algebra;
cluster the charact of U0 -> Function-yielding;
end;