:: UNIALG_1 semantic presentation

begin

definition
attrc1 is strict ;
struct UAStr  ->  1-sorted ;
aggrUAStr(# carrier, charact #) ->  UAStr ;
sel charact c1 ->  PFuncFinSequence of the carrier of c1;
end;

registration
cluster non empty strict for UAStr ;
existence
 ex b1 being UAStr st
( not b1 is empty & b1 is strict )
proof
set D = the non empty set ;
set c = the PFuncFinSequence of the non empty set ;
take  UAStr(# the non empty set , the PFuncFinSequence of the non empty set #) ; ::_thesis: ( not UAStr(# the non empty set , the PFuncFinSequence of the non empty set #) is empty & UAStr(# the non empty set , the PFuncFinSequence of the non empty set #) is strict )
thus  not the carrier of UAStr(# the non empty set , the PFuncFinSequence of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: UAStr(# the non empty set , the PFuncFinSequence of the non empty set #) is strict
thus  UAStr(# the non empty set , the PFuncFinSequence of the non empty set #) is strict ; ::_thesis: verum
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 ;
attrIT is partial  means :Def1: :: UNIALG_1:def 1
 the charact of IT is homogeneous ;
attrIT is quasi_total  means :Def2: :: UNIALG_1:def 2
 the charact of IT is quasi_total ;
attrIT 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 b1 being UAStr st
( b1 is quasi_total & b1 is partial & b1 is non-empty & b1 is strict & not b1 is empty )
proof
set A = the non empty set ;
set a = the Element of the non empty set ;
reconsider w = (<*> the non empty set ) .--> the Element of the non empty set as Element of PFuncs (( the non empty set *), the non empty set ) by MARGREL1:19;
set U1 = UAStr(# the non empty set ,<*w*> #);
take  UAStr(# the non empty set ,<*w*> #) ; ::_thesis: ( UAStr(# the non empty set ,<*w*> #) is quasi_total & UAStr(# the non empty set ,<*w*> #) is partial & UAStr(# the non empty set ,<*w*> #) is non-empty & UAStr(# the non empty set ,<*w*> #) is strict & not UAStr(# the non empty set ,<*w*> #) is empty )
A1: ( the charact of UAStr(# the non empty set ,<*w*> #) is non-empty & the charact of UAStr(# the non empty set ,<*w*> #) <> {} ) by MARGREL1:20;
 ( the charact of UAStr(# the non empty set ,<*w*> #) is quasi_total & the charact of UAStr(# the non empty set ,<*w*> #) is homogeneous ) by MARGREL1:20;
hence  ( UAStr(# the non empty set ,<*w*> #) is quasi_total & UAStr(# the non empty set ,<*w*> #) is partial & UAStr(# the non empty set ,<*w*> #) is non-empty & UAStr(# the non empty set ,<*w*> #) is strict & not UAStr(# the non empty set ,<*w*> #) is empty ) by A1, Def1, Def2, Def3; ::_thesis: verum
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
let n be Nat; ::_thesis: 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
let U1 be non empty partial non-empty UAStr ; ::_thesis: ( n in dom the charact of U1 implies the charact of U1 . n is PartFunc of ( the carrier of U1 *), the carrier of U1 )
set o = the charact of U1;
assume  n in dom the charact of U1 ; ::_thesis: the charact of U1 . n is PartFunc of ( the carrier of U1 *), the carrier of U1
then A1: the charact of U1 . n in rng the charact of U1 by FUNCT_1:def_3;
 rng the charact of U1 c= PFuncs (( the carrier of U1 *), the carrier of U1) by FINSEQ_1:def_4;
hence  the charact of U1 . n is PartFunc of ( the carrier of U1 *), the carrier of U1 by A1, PARTFUN1:47; ::_thesis: verum
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 b1 being FinSequence of NAT st
( len b1 = len the charact of U1 & ( for n being Nat st n in dom b1 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
b1 . n = arity h ) )
proof
defpred S1[ Nat, set ] means  for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . $1 holds
$2 = arity h;
A1: now__::_thesis:_for_m_being_Nat_st_m_in_Seg_(len_the_charact_of_U1)_holds_
ex_n_being_Element_of_NAT_st_S1[m,n]
let m be Nat; ::_thesis: ( m in Seg (len the charact of U1) implies ex n being Element of NAT st S1[m,n] )
assume  m in Seg (len the charact of U1) ; ::_thesis: ex n being Element of NAT st S1[m,n]
then  m in dom the charact of U1 by FINSEQ_1:def_3;
then reconsider H = the charact of U1 . m as non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 by Th1;
reconsider n = arity H as Element of NAT ;
take n = n; ::_thesis: S1[m,n]
thus  S1[m,n] ; ::_thesis: verum
end;
consider p being FinSequence of NAT  such that
A2: dom p = Seg (len the charact of U1) and
A3: for m being Nat st m in Seg (len the charact of U1) holds
S1[m,p . m] from FINSEQ_1:sch_5(A1);
take  p ; ::_thesis: ( len p = len the charact of U1 & ( for n being Nat st n in dom p 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
p . n = arity h ) )
thus  len p = len the charact of U1 by A2, FINSEQ_1:def_3; ::_thesis: for n being Nat st n in dom p 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
p . n = arity h
let n be Nat; ::_thesis: ( n in dom p implies for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
p . n = arity h )
assume A4: n in dom p ; ::_thesis: for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
p . n = arity h
let h be non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1; ::_thesis: ( h = the charact of U1 . n implies p . n = arity h )
assume  h = the charact of U1 . n ; ::_thesis: p . n = arity h
hence  p . n = arity h by A2, A3, A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being FinSequence of NAT st len b1 = len the charact of U1 & ( for n being Nat st n in dom b1 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
b1 . n = arity h ) & len b2 = len the charact of U1 & ( for n being Nat st n in dom b2 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
b2 . n = arity h ) holds
b1 = b2
proof
let x, y be FinSequence of NAT ; ::_thesis: ( len x = len the charact of U1 & ( for n being Nat st n in dom x 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
x . n = arity h ) & len y = len the charact of U1 & ( for n being Nat st n in dom y 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
y . n = arity h ) implies x = y )
assume that
A5: len x = len the charact of U1 and
A6: for n being Nat st n in dom x 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
x . n = arity h and
A7: len y = len the charact of U1 and
A8: for n being Nat st n in dom y 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
y . n = arity h ; ::_thesis: x = y
now__::_thesis:_for_m_being_Nat_st_1_<=_m_&_m_<=_len_x_holds_
x_._m_=_y_._m
let m be Nat; ::_thesis: ( 1 <= m & m <= len x implies x . m = y . m )
assume  ( 1 <= m & m <= len x ) ; ::_thesis: x . m = y . m
then A9: m in Seg (len x) by FINSEQ_1:1;
then  m in dom the charact of U1 by A5, FINSEQ_1:def_3;
then reconsider h = the charact of U1 . m as non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 by Th1;
 m in dom x by A9, FINSEQ_1:def_3;
then A10: x . m = arity h by A6;
 m in dom y by A5, A7, A9, FINSEQ_1:def_3;
hence  x . m = y . m by A8, A10; ::_thesis: verum
end;
hence  x = y by A5, A7, FINSEQ_1:14; ::_thesis: verum
end;
end;

:: deftheorem  defines signature UNIALG_1:def_4_:_
 for U1 being non empty partial non-empty UAStr
for b2 being FinSequence of NAT holds
( b2 = signature U1 iff ( len b2 = len the charact of U1 & ( for n being Nat st n in dom b2 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
b2 . 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;