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

begin

definition

let IT be Relation;
attr IT is homogeneous means :Def1: :: UNIALG_1:def 1
dom IT is with_common_domain ;

end;

:: deftheorem Def1 defines homogeneous UNIALG_1:def 1 :

for IT being Relation holds
( IT is homogeneous iff dom IT is with_common_domain );

definition

let A be set ;
let IT be PartFunc of (A * ),A;
attr IT is quasi_total means :: UNIALG_1:def 2
for x, y being FinSequence of A st len x = len y & x in dom IT holds
y in dom IT;

end;

:: deftheorem defines quasi_total UNIALG_1:def 2 :

for A being set
for IT being PartFunc of (A * ),A holds
( IT is quasi_total iff for x, y being FinSequence of A st len x = len y & x in dom IT holds
y in dom IT );

registration

let f be Relation;
let X be with_common_domain set ;
cluster f | X -> homogeneous ;
coherence
f | X is homogeneous

proof end;

end;

registration

let A be non empty set ;
let f be PartFunc of (A * ),A;
cluster proj1 f -> FinSequence-membered ;
coherence
dom f is FinSequence-membered

proof end;

end;

registration

let A be non empty set ;
cluster Relation-like A * -defined A -valued Function-like non empty homogeneous quasi_total Element of K21(K22((A * ),A));
existence
ex b₁ being PartFunc of (A * ),A st
( b₁ is homogeneous & b₁ is quasi_total & not b₁ is empty )

proof end;

end;

registration

cluster Relation-like Function-like non empty homogeneous set ;
existence
ex b₁ being Function st
( b₁ is homogeneous & not b₁ is empty )

proof end;

end;

registration

let R be homogeneous Relation;
cluster proj1 R -> with_common_domain ;
coherence
dom R is with_common_domain by Def1;

end;

theorem :: UNIALG_1:1

canceled;

theorem Th2: :: UNIALG_1:2

for A being non empty set
for a being Element of A holds (<*> A) .--> a is non empty homogeneous quasi_total PartFunc of (A * ),A

proof end;

theorem Th3: :: UNIALG_1:3

for A being non empty set
for a being Element of A holds (<*> A) .--> a is Element of PFuncs (A * ),A

proof end;

registration

let A be set ;
let B be functional set ;
cluster Function-like -> Function-yielding Element of K21(K22(A,B));
coherence
for b₁ being PartFunc of A,B holds b₁ is Function-yielding

proof end;

end;

definition

let A be set ;
mode PFuncFinSequence of A is FinSequence of PFuncs (A * ),A;

end;

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 A be set ;
let IT be PFuncFinSequence of A;
canceled;
attr IT is homogeneous means :Def4: :: UNIALG_1:def 4
for n being Nat
for h being PartFunc of (A * ),A st n in dom IT & h = IT . n holds
h is homogeneous ;

end;

:: deftheorem UNIALG_1:def 3 :

canceled;

:: deftheorem Def4 defines homogeneous UNIALG_1:def 4 :

for A being set
for IT being PFuncFinSequence of A holds
( IT is homogeneous iff for n being Nat
for h being PartFunc of (A * ),A st n in dom IT & h = IT . n holds
h is homogeneous );

definition

let A be set ;
let IT be PFuncFinSequence of A;
attr IT is quasi_total means :Def5: :: UNIALG_1:def 5
for n being Nat
for h being PartFunc of (A * ),A st n in dom IT & h = IT . n holds
h is quasi_total ;

end;

:: deftheorem Def5 defines quasi_total UNIALG_1:def 5 :

for A being set
for IT being PFuncFinSequence of A holds
( IT is quasi_total iff for n being Nat
for h being PartFunc of (A * ),A st n in dom IT & h = IT . n holds
h is quasi_total );

definition

let A be non empty set ;
let x be Element of PFuncs (A * ),A;
:: original: <*
redefine func <*x*> -> PFuncFinSequence of A;
coherence
<*x*> is PFuncFinSequence of A

proof end;

end;

registration

let A be non empty set ;
cluster Relation-like non-empty NAT -defined PFuncs (A * ),A -valued Function-like Function-yielding V29() FinSequence-like FinSubsequence-like countable homogeneous quasi_total FinSequence of PFuncs (A * ),A;
existence
ex b₁ being PFuncFinSequence of A st
( b₁ is homogeneous & b₁ is quasi_total & b₁ is non-empty )

proof end;

end;

registration

let A be non empty set ;
let f be homogeneous PFuncFinSequence of A;
let i be set ;
cluster f . i -> homogeneous ;
coherence
f . i is homogeneous

proof end;

end;

definition

let IT be UAStr ;
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 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 ) );

theorem Th4: :: UNIALG_1:4

for A being non empty set
for a being Element of A
for x being Element of PFuncs (A * ),A st x = (<*> A) .--> a holds
( <*x*> is homogeneous & <*x*> is quasi_total & <*x*> is non-empty )

proof end;

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;

definition

let f be homogeneous Relation;
func arity f -> Nat means :: UNIALG_1:def 10
for x being FinSequence st x in dom f holds
it = len x if ex x being FinSequence st x in dom f
otherwise it = 0 ;
consistency
for b₁ being Nat holds verum ;
existence
( ( ex x being FinSequence st x in dom f implies ex b₁ being Nat st
for x being FinSequence st x in dom f holds
b₁ = len x ) & ( ( for x being FinSequence holds not x in dom f ) implies ex b₁ being Nat st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Nat holds
( ( ex x being FinSequence st x in dom f & ( for x being FinSequence st x in dom f holds
b₁ = len x ) & ( for x being FinSequence st x in dom f holds
b₂ = len x ) implies b₁ = b₂ ) & ( ( for x being FinSequence holds not x in dom f ) & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) )

proof end;

end;

:: deftheorem defines arity UNIALG_1:def 10 :

for f being homogeneous Relation
for b₂ being Nat holds
( ( ex x being FinSequence st x in dom f implies ( b₂ = arity f iff for x being FinSequence st x in dom f holds
b₂ = len x ) ) & ( ( for x being FinSequence holds not x in dom f ) implies ( b₂ = arity f iff b₂ = 0 ) ) );

definition

let f be homogeneous Function;
:: original: arity
redefine func arity f -> Element of NAT ;
coherence
arity f is Element of NAT by ORDINAL1:def 13;

end;

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

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