:: UNIALG_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let A be set ;
let IT be PartFunc of A * ,A;
attr IT is homogeneous means :Def1: :: UNIALG_1:def 1
for x, y being FinSequence of A st x in dom IT & y in dom IT holds
len x = len y;
end;

:: deftheorem Def1 defines homogeneous UNIALG_1:def 1 :
for A being set
for IT being PartFunc of A * ,A holds
( IT is homogeneous iff for x, y being FinSequence of A st x in dom IT & y in dom IT holds
len x = len y );

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 A be non empty set ;
cluster non empty homogeneous quasi_total M5(A * ,A);
existence
ex b1 being PartFunc of A * ,A st
( b1 is homogeneous & b1 is quasi_total & not b1 is empty )
proof end;
end;

theorem :: UNIALG_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being set
for h being PartFunc of A * ,A holds
( not h is empty iff dom h <> {} ) by RELAT_1:60, RELAT_1:64;

theorem Th2: :: UNIALG_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being non empty set
for a being Element of A holds {(<*> A)} --> a is Element of PFuncs (A * ),A
proof end;

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

definition
attr c1 is strict;
struct UAStr -> 1-sorted ;
aggr UAStr(# carrier, charact #) -> UAStr ;
sel charact c1 -> PFuncFinSequence of the carrier of c1;
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 D be non empty set ;
let c be PFuncFinSequence of D;
cluster UAStr(# D,c #) -> non empty ;
coherence
not UAStr(# D,c #) is empty
proof end;
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 non-empty homogeneous quasi_total FinSequence of PFuncs (A * ),A;
existence
ex b1 being PFuncFinSequence of A st
( b1 is homogeneous & b1 is quasi_total & b1 is non-empty )
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 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 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 A be non empty set ;
let f be non empty homogeneous PartFunc of A * ,A;
func arity f -> Nat means :: UNIALG_1:def 10
for x being FinSequence of A st x in dom f holds
it = len x;
existence
ex b1 being Nat st
for x being FinSequence of A st x in dom f holds
b1 = len x
proof end;
uniqueness
for b1, b2 being Nat st ( for x being FinSequence of A st x in dom f holds
b1 = len x ) & ( for x being FinSequence of A st x in dom f holds
b2 = len x ) holds
b1 = b2
proof end;
end;

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

theorem Th5: :: UNIALG_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for U1 being non empty partial non-empty UAStr
for n being Nat 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 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 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 end;
end;

:: deftheorem defines signature UNIALG_1:def 11 :
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 ) ) );