:: UNIALG_1 semantic presentation

definition
let c1 be set ;
let c2 be PartFunc of c1 * ,c1;
attr a2 is homogeneous means :Def1: :: UNIALG_1:def 1
for b1, b2 being FinSequence of a1 st b1 in dom a2 & b2 in dom a2 holds
len b1 = len b2;
end;

:: deftheorem Def1 defines homogeneous UNIALG_1:def 1 :
for b1 being set
for b2 being PartFunc of b1 * ,b1 holds
( b2 is homogeneous iff for b3, b4 being FinSequence of b1 st b3 in dom b2 & b4 in dom b2 holds
len b3 = len b4 );

definition
let c1 be set ;
let c2 be PartFunc of c1 * ,c1;
attr a2 is quasi_total means :: UNIALG_1:def 2
for b1, b2 being FinSequence of a1 st len b1 = len b2 & b1 in dom a2 holds
b2 in dom a2;
end;

:: deftheorem Def2 defines quasi_total UNIALG_1:def 2 :
for b1 being set
for b2 being PartFunc of b1 * ,b1 holds
( b2 is quasi_total iff for b3, b4 being FinSequence of b1 st len b3 = len b4 & b3 in dom b2 holds
b4 in dom b2 );

registration
let c1 be non empty set ;
cluster non empty homogeneous quasi_total M5(a1 * ,a1);
existence
ex b1 being PartFunc of c1 * ,c1 st
( b1 is homogeneous & b1 is quasi_total & not b1 is empty )
proof end;
end;

theorem Th1: :: UNIALG_1:1
for b1 being set
for b2 being PartFunc of b1 * ,b1 holds
( not b2 is empty iff dom b2 <> {} ) by RELAT_1:60, RELAT_1:64;

theorem Th2: :: UNIALG_1:2
for b1 being non empty set
for b2 being Element of b1 holds {(<*> b1)} --> b2 is non empty homogeneous quasi_total PartFunc of b1 * ,b1
proof end;

theorem Th3: :: UNIALG_1:3
for b1 being non empty set
for b2 being Element of b1 holds {(<*> b1)} --> b2 is Element of PFuncs (b1 * ),b1
proof end;

definition
let c1 be set ;
mode PFuncFinSequence of a1 is FinSequence of PFuncs (a1 * ),a1;
end;

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

registration
cluster non empty strict UAStr ;
existence
ex b1 being UAStr st
( not b1 is empty & b1 is strict )
proof end;
end;

registration
let c1 be non empty set ;
let c2 be PFuncFinSequence of c1;
cluster UAStr(# a1,a2 #) -> non empty ;
coherence
not UAStr(# c1,c2 #) is empty
proof end;
end;

definition
let c1 be set ;
let c2 be PFuncFinSequence of c1;
canceled;
attr a2 is homogeneous means :Def4: :: UNIALG_1:def 4
for b1 being Nat
for b2 being PartFunc of a1 * ,a1 st b1 in dom a2 & b2 = a2 . b1 holds
b2 is homogeneous;
end;

:: deftheorem Def3 UNIALG_1:def 3 :
canceled;

:: deftheorem Def4 defines homogeneous UNIALG_1:def 4 :
for b1 being set
for b2 being PFuncFinSequence of b1 holds
( b2 is homogeneous iff for b3 being Nat
for b4 being PartFunc of b1 * ,b1 st b3 in dom b2 & b4 = b2 . b3 holds
b4 is homogeneous );

definition
let c1 be set ;
let c2 be PFuncFinSequence of c1;
attr a2 is quasi_total means :Def5: :: UNIALG_1:def 5
for b1 being Nat
for b2 being PartFunc of a1 * ,a1 st b1 in dom a2 & b2 = a2 . b1 holds
b2 is quasi_total;
end;

:: deftheorem Def5 defines quasi_total UNIALG_1:def 5 :
for b1 being set
for b2 being PFuncFinSequence of b1 holds
( b2 is quasi_total iff for b3 being Nat
for b4 being PartFunc of b1 * ,b1 st b3 in dom b2 & b4 = b2 . b3 holds
b4 is quasi_total );

definition
let c1 be non empty set ;
let c2 be Element of PFuncs (c1 * ),c1;
redefine func <* as <*c2*> -> PFuncFinSequence of a1;
coherence
<*c2*> is PFuncFinSequence of c1
proof end;
end;

registration
let c1 be non empty set ;
cluster non-empty homogeneous quasi_total FinSequence of PFuncs (a1 * ),a1;
existence
ex b1 being PFuncFinSequence of c1 st
( b1 is homogeneous & b1 is quasi_total & b1 is non-empty )
proof end;
end;

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

:: deftheorem Def6 UNIALG_1:def 6 :
canceled;

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

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

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

theorem Th4: :: UNIALG_1:4
for b1 being non empty set
for b2 being Element of b1
for b3 being Element of PFuncs (b1 * ),b1 st b3 = {(<*> b1)} --> b2 holds
( <*b3*> is homogeneous & <*b3*> is quasi_total & <*b3*> is non-empty )
proof end;

registration
cluster non empty strict partial quasi_total non-empty 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 end;
end;

registration
let c1 be partial UAStr ;
cluster the charact of a1 -> homogeneous ;
coherence
the charact of c1 is homogeneous by Def7;
end;

registration
let c1 be quasi_total UAStr ;
cluster the charact of a1 -> quasi_total ;
coherence
the charact of c1 is quasi_total by Def8;
end;

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

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

definition
let c1 be non empty set ;
let c2 be non empty homogeneous PartFunc of c1 * ,c1;
func arity c2 -> Nat means :: UNIALG_1:def 10
for b1 being FinSequence of a1 st b1 in dom a2 holds
a3 = len b1;
existence
ex b1 being Nat st
for b2 being FinSequence of c1 st b2 in dom c2 holds
b1 = len b2
proof end;
uniqueness
for b1, b2 being Nat st ( for b3 being FinSequence of c1 st b3 in dom c2 holds
b1 = len b3 ) & ( for b3 being FinSequence of c1 st b3 in dom c2 holds
b2 = len b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines arity UNIALG_1:def 10 :
for b1 being non empty set
for b2 being non empty homogeneous PartFunc of b1 * ,b1
for b3 being Nat holds
( b3 = arity b2 iff for b4 being FinSequence of b1 st b4 in dom b2 holds
b3 = len b4 );

theorem Th5: :: UNIALG_1:5
for b1 being non empty partial non-empty UAStr
for b2 being Nat st b2 in dom the charact of b1 holds
the charact of b1 . b2 is PartFunc of the carrier of b1 * ,the carrier of b1
proof end;

definition
let c1 be non empty partial non-empty UAStr ;
func signature c1 -> FinSequence of NAT means :: UNIALG_1:def 11
( len a2 = len the charact of a1 & ( for b1 being Nat st b1 in dom a2 holds
for b2 being non empty homogeneous PartFunc of the carrier of a1 * ,the carrier of a1 st b2 = the charact of a1 . b1 holds
a2 . b1 = arity b2 ) );
existence
ex b1 being FinSequence of NAT st
( len b1 = len the charact of c1 & ( for b2 being Nat st b2 in dom b1 holds
for b3 being non empty homogeneous PartFunc of the carrier of c1 * ,the carrier of c1 st b3 = the charact of c1 . b2 holds
b1 . b2 = arity b3 ) )
proof end;
uniqueness
for b1, b2 being FinSequence of NAT st len b1 = len the charact of c1 & ( for b3 being Nat st b3 in dom b1 holds
for b4 being non empty homogeneous PartFunc of the carrier of c1 * ,the carrier of c1 st b4 = the charact of c1 . b3 holds
b1 . b3 = arity b4 ) & len b2 = len the charact of c1 & ( for b3 being Nat st b3 in dom b2 holds
for b4 being non empty homogeneous PartFunc of the carrier of c1 * ,the carrier of c1 st b4 = the charact of c1 . b3 holds
b2 . b3 = arity b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines signature UNIALG_1:def 11 :
for b1 being non empty partial non-empty UAStr
for b2 being FinSequence of NAT holds
( b2 = signature b1 iff ( len b2 = len the charact of b1 & ( for b3 being Nat st b3 in dom b2 holds
for b4 being non empty homogeneous PartFunc of the carrier of b1 * ,the carrier of b1 st b4 = the charact of b1 . b3 holds
b2 . b3 = arity b4 ) ) );