:: 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;
struct UAStr -> 1-sorted ;

aggr UAStr(# carrier, charact #) -> UAStr ;

sel charact c

registration
end;

registration
end;

:: deftheorem Def1 defines partial UNIALG_1:def 1 :

for IT being UAStr holds

( IT is partial iff the charact of IT is homogeneous );

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

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

for IT being UAStr holds

( IT is non-empty iff ( the charact of IT <> {} & the charact of IT is non-empty ) );

registration

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 )

end;
ex b

( b

proof end;

registration

let U1 be non-empty UAStr ;

coherence

( the charact of U1 is non-empty & not the charact of U1 is empty ) by Def3;

end;
coherence

( the charact of U1 is non-empty & not the charact of U1 is empty ) by Def3;

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

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 ;

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

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}

end;
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 ( 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 ) );

ex b

( len b

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

proof end;

uniqueness for b

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

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

b

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

for U1 being non empty partial non-empty UAStr

for b

( b

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

begin

:: from MSSUBLAT, 2007.05.13, A.T.