:: Basic Notation of Universal Algebra
:: by Jaros{\l}aw Kotowicz, Beata Madras and Ma{\l}gorzata Korolkiewicz
::
:: Received December 29, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users
begin
definition
attr
c
1
is
strict
;
struct
UAStr
->
1-sorted
;
aggr
UAStr
(#
carrier
,
charact
#)
->
UAStr
;
sel
charact
c
1
->
PFuncFinSequence
of the
carrier
of
c
1
;
end;
registration
cluster
non
empty
strict
for
UAStr
;
existence
ex
b
1
being
UAStr
st
( not
b
1
is
empty
&
b
1
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
;
attr
IT
is
partial
means
:
Def1
:
:: UNIALG_1:def 1
the
charact
of
IT
is
homogeneous
;
attr
IT
is
quasi_total
means
:
Def2
:
:: UNIALG_1:def 2
the
charact
of
IT
is
quasi_total
;
attr
IT
is
non-empty
means
:
Def3
:
:: UNIALG_1:def 3
( the
charact
of
IT
<>
{}
& the
charact
of
IT
is
non-empty
);
end;
::
deftheorem
Def1
defines
partial
UNIALG_1:def 1 :
for
IT
being
UAStr
holds
(
IT
is
partial
iff the
charact
of
IT
is
homogeneous
);
::
deftheorem
Def2
defines
quasi_total
UNIALG_1:def 2 :
for
IT
being
UAStr
holds
(
IT
is
quasi_total
iff the
charact
of
IT
is
quasi_total
);
::
deftheorem
Def3
defines
non-empty
UNIALG_1:def 3 :
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
for
UAStr
;
existence
ex
b
1
being
UAStr
st
(
b
1
is
quasi_total
&
b
1
is
partial
&
b
1
is
non-empty
&
b
1
is
strict
& not
b
1
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
Def1
;
end;
registration
let
U1
be
quasi_total
UAStr
;
cluster
the
charact
of
U1
->
quasi_total
;
coherence
the
charact
of
U1
is
quasi_total
by
Def2
;
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
Def3
;
end;
definition
mode
Universal_Algebra
is
non
empty
partial
quasi_total
non-empty
UAStr
;
end;
theorem
Th1
:
:: UNIALG_1:1
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 4
(
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
1
being
FinSequence
of
NAT
st
(
len
b
1
=
len
the
charact
of
U1
& ( for
n
being
Nat
st
n
in
dom
b
1
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
1
.
n
=
arity
h
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
FinSequence
of
NAT
st
len
b
1
=
len
the
charact
of
U1
& ( for
n
being
Nat
st
n
in
dom
b
1
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
1
.
n
=
arity
h
) &
len
b
2
=
len
the
charact
of
U1
& ( for
n
being
Nat
st
n
in
dom
b
2
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
2
.
n
=
arity
h
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
defines
signature
UNIALG_1:def 4 :
for
U1
being non
empty
partial
non-empty
UAStr
for
b
2
being
FinSequence
of
NAT
holds
(
b
2
=
signature
U1
iff (
len
b
2
=
len
the
charact
of
U1
& ( for
n
being
Nat
st
n
in
dom
b
2
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
2
.
n
=
arity
h
) ) );
begin
:: from MSSUBLAT, 2007.05.13, A.T.
registration
let
U0
be
Universal_Algebra
;
cluster
the
charact
of
U0
->
Function-yielding
;
coherence
the
charact
of
U0
is
Function-yielding
;
end;