:: Basic Notation of Universal Algebra
:: by Jaros{\l}aw Kotowicz, Beata Madras and Ma{\l}gorzata Korolkiewicz
::
:: Received December 29, 1992
:: Copyright (c) 1992-2011 Association of Mizar Users

begin

definition

attr c₁ is strict ;
struct UAStr -> 1-sorted ;
aggr UAStr(# carrier, charact #) -> UAStr ;
sel charact c₁ -> PFuncFinSequence of the carrier of c₁;

end;

registration

cluster non empty strict UAStr ;
existence
ex b₁ being UAStr st
( not b₁ is empty & b₁ is strict )

proof end;

end;

registration

let D be non empty set ;
let c be PFuncFinSequence of D;
cluster UAStr(# D,c #) -> non empty ;
coherence
not UAStr(# D,c #) is empty ;

end;

definition

let IT be UAStr ;
canceled;
canceled;
canceled;
canceled;
canceled;
canceled;
attr IT is partial means :Def7: :: UNIALG_1:def 7
the charact of IT is homogeneous ;
attr IT is quasi_total means :Def8: :: UNIALG_1:def 8
the charact of IT is quasi_total ;
attr IT is non-empty means :Def9: :: UNIALG_1:def 9
( the charact of IT <> {} & the charact of IT is non-empty );

end;

:: deftheorem UNIALG_1:def 1 :
canceled;

:: deftheorem UNIALG_1:def 2 :
canceled;

:: deftheorem UNIALG_1:def 3 :
canceled;

:: deftheorem UNIALG_1:def 4 :
canceled;

:: deftheorem UNIALG_1:def 5 :
canceled;

:: deftheorem UNIALG_1:def 6 :
canceled;

:: deftheorem Def7 defines partial UNIALG_1:def 7 :
for IT being UAStr holds
( IT is partial iff the charact of IT is homogeneous );

:: deftheorem Def8 defines quasi_total UNIALG_1:def 8 :
for IT being UAStr holds
( IT is quasi_total iff the charact of IT is quasi_total );

:: deftheorem Def9 defines non-empty UNIALG_1:def 9 :
for IT being UAStr holds
( IT is non-empty iff ( the charact of IT <> {} & the charact of IT is non-empty ) );

registration

cluster non empty strict partial quasi_total non-empty UAStr ;
existence
ex b₁ being UAStr st
( b₁ is quasi_total & b₁ is partial & b₁ is non-empty & b₁ is strict & not b₁ is empty )

proof end;

end;

registration

let U1 be partial UAStr ;
cluster the charact of U1 -> homogeneous ;
coherence
the charact of U1 is homogeneous by Def7;

end;

registration

let U1 be quasi_total UAStr ;
cluster the charact of U1 -> quasi_total ;
coherence
the charact of U1 is quasi_total by Def8;

end;

registration

let U1 be non-empty UAStr ;
cluster the charact of U1 -> non-empty non empty ;
coherence
( the charact of U1 is non-empty & not the charact of U1 is empty ) by Def9;

end;

definition

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

end;

theorem :: UNIALG_1:1

canceled;

theorem :: UNIALG_1:2

canceled;

theorem :: UNIALG_1:3

canceled;

theorem :: UNIALG_1:4

canceled;

theorem Th5: :: UNIALG_1:5

for n being Nat
for U1 being non empty partial non-empty UAStr 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

proof end;

definition

canceled;
let U1 be non empty partial non-empty UAStr ;
func signature U1 -> FinSequence of NAT means :: UNIALG_1:def 11
( len it = len the charact of U1 & ( for n being Nat st n in dom it holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
it . n = arity h ) );
existence
ex b₁ being FinSequence of NAT st
( len b₁ = len the charact of U1 & ( for n being Nat st n in dom b₁ holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
b₁ . n = arity h ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of NAT st len b₁ = len the charact of U1 & ( for n being Nat st n in dom b₁ holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
b₁ . n = arity h ) & len b₂ = len the charact of U1 & ( for n being Nat st n in dom b₂ holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
b₂ . n = arity h ) holds
b₁ = b₂

proof end;

end;

:: deftheorem UNIALG_1:def 10 :
canceled;

:: deftheorem defines signature UNIALG_1:def 11 :
for U1 being non empty partial non-empty UAStr
for b₂ being FinSequence of NAT holds
( b₂ = signature U1 iff ( len b₂ = len the charact of U1 & ( for n being Nat st n in dom b₂ holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
b₂ . n = arity h ) ) );

begin

registration

let U0 be Universal_Algebra;
cluster the charact of U0 -> Function-yielding ;
coherence
the charact of U0 is Function-yielding ;

end;