:: PRALG_1 semantic presentation

theorem Th1: :: PRALG_1:1

for D1, D2 being non empty set
for n, m being Nat st n -tuples_on D1 = m -tuples_on D2 holds
n = m

proof end;

definition

let A, B be non empty set ;
let h1 be FinSequence of [:A,B:];
:: original: pr1
redefine func pr1 h1 -> FinSequence of A means :Def1: :: PRALG_1:def 1
( len it = len h1 & ( for n being Nat st n in dom it holds
it . n = (h1 . n) `1 ) );
compatibility

proof end;

coherence

proof end;

:: original: pr2
redefine func pr2 h1 -> FinSequence of B means :Def2: :: PRALG_1:def 2
( len it = len h1 & ( for n being Nat st n in dom it holds
it . n = (h1 . n) `2 ) );
compatibility

proof end;

coherence

proof end;

end;

:: deftheorem Def1 defines pr1 PRALG_1:def 1 :

:: deftheorem Def2 defines pr2 PRALG_1:def 2 :

definition

let A, B be non empty set ;
let f1 be non empty homogeneous quasi_total PartFunc of A * ,A;
let f2 be non empty homogeneous quasi_total PartFunc of B * ,B;
assume A1: arity f1 = arity f2 ;
func [[:f1,f2:]] -> non empty homogeneous quasi_total PartFunc of [:A,B:] * ,[:A,B:] means :Def3: :: PRALG_1:def 3
( dom it = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom it holds
it . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines [[: PRALG_1:def 3 :

definition

let U1, U2 be Universal_Algebra;
assume A1: U1,U2 are_similar ;
func Opers U1,U2 -> PFuncFinSequence of [:the carrier of U1,the carrier of U2:] means :Def4: :: PRALG_1:def 4
( len it = len the charact of U1 & ( for n being Nat st n in dom it holds
for h1 being non empty homogeneous quasi_total PartFunc of the carrier of U1 * ,the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of the carrier of U2 * ,the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
it . n = [[:h1,h2:]] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Opers PRALG_1:def 4 :

theorem Th2: :: PRALG_1:2

for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
UAStr(# [:the carrier of U1,the carrier of U2:],(Opers U1,U2) #) is strict Universal_Algebra

proof end;

definition

let U1, U2 be Universal_Algebra;
assume A1: U1,U2 are_similar ;
func [:U1,U2:] -> strict Universal_Algebra equals :Def5: :: PRALG_1:def 5
UAStr(# [:the carrier of U1,the carrier of U2:],(Opers U1,U2) #);
coherence by A1, Th2;

end;

:: deftheorem Def5 defines [: PRALG_1:def 5 :

definition

let A, B be non empty set ;
func Inv A,B -> Function of [:A,B:],[:B,A:] means :Def6: :: PRALG_1:def 6
for a being Element of [:A,B:] holds it . a = [(a `2 ),(a `1 )];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Inv PRALG_1:def 6 :

theorem :: PRALG_1:3

for A, B being non empty set holds rng (Inv A,B) = [:B,A:]

proof end;

theorem :: PRALG_1:4

for A, B being non empty set holds Inv A,B is one-to-one

proof end;

theorem :: PRALG_1:5

for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
Inv the carrier of U1,the carrier of U2 is Function of the carrier of [:U1,U2:],the carrier of [:U2,U1:]

proof end;

theorem Th6: :: PRALG_1:6

for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
for o1 being operation of U1
for o2 being operation of U2
for o being operation of [:U1,U2:]
for n being Nat st o1 = the charact of U1 . n & o2 = the charact of U2 . n & o = the charact of [:U1,U2:] . n & n in dom the charact of U1 holds
( arity o = arity o1 & arity o = arity o2 & o = [[:o1,o2:]] )

proof end;

theorem :: PRALG_1:7

for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
[:U1,U2:],U1 are_similar

proof end;

theorem :: PRALG_1:8

for U1, U2, U3, U4 being Universal_Algebra st U1 is SubAlgebra of U2 & U3 is SubAlgebra of U4 & U2,U4 are_similar holds
[:U1,U3:] is SubAlgebra of [:U2,U4:]

proof end;

definition

let k be natural number ;
func TrivialOp k -> PartFunc of {{} } * ,{{} } means :Def7: :: PRALG_1:def 7
( dom it = {(k |-> {} )} & rng it = {{} } );
existence

proof end;

uniqueness by FUNCT_1:17;

end;

:: deftheorem Def7 defines TrivialOp PRALG_1:def 7 :

registration

let k be natural number ;
cluster TrivialOp k -> non empty homogeneous quasi_total ;
coherence

proof end;

end;

theorem :: PRALG_1:9

for k being natural number holds arity (TrivialOp k) = k

proof end;

definition

let f be FinSequence of NAT ;
func TrivialOps f -> PFuncFinSequence of {{} } means :Def8: :: PRALG_1:def 8
( len it = len f & ( for n being Nat st n in dom it holds
for m being Nat st m = f . n holds
it . n = TrivialOp m ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines TrivialOps PRALG_1:def 8 :

theorem Th10: :: PRALG_1:10

for f being FinSequence of NAT holds
( TrivialOps f is homogeneous & TrivialOps f is quasi_total & TrivialOps f is non-empty )

proof end;

theorem Th11: :: PRALG_1:11

for f being FinSequence of NAT st f <> {} holds
UAStr(# {{} },(TrivialOps f) #) is strict Universal_Algebra

proof end;

registration

let D be non empty set ;
cluster non empty FinSequence of D;
existence

proof end;

cluster non empty Element of D * ;
existence

proof end;

end;

definition

let f be non empty FinSequence of NAT ;
func Trivial_Algebra f -> strict Universal_Algebra equals :: PRALG_1:def 9
UAStr(# {{} },(TrivialOps f) #);
coherence by Th11;

end;

:: deftheorem defines Trivial_Algebra PRALG_1:def 9 :

definition

let IT be Function;
attr IT is Univ_Alg-yielding means :Def10: :: PRALG_1:def 10
for x being set st x in dom IT holds
IT . x is Universal_Algebra;

end;

:: deftheorem Def10 defines Univ_Alg-yielding PRALG_1:def 10 :

definition

let IT be Function;
attr IT is 1-sorted-yielding means :Def11: :: PRALG_1:def 11
for x being set st x in dom IT holds
IT . x is 1-sorted ;

end;

:: deftheorem Def11 defines 1-sorted-yielding PRALG_1:def 11 :

registration

cluster Univ_Alg-yielding set ;
existence

proof end;

end;

registration

cluster Univ_Alg-yielding -> 1-sorted-yielding set ;
coherence

proof end;

end;

registration

let I be set ;
cluster 1-sorted-yielding ManySortedSet of I;
existence

proof end;

end;

definition

let IT be Function;
attr IT is equal-signature means :Def12: :: PRALG_1:def 12
for x, y being set st x in dom IT & y in dom IT holds
for U1, U2 being Universal_Algebra st U1 = IT . x & U2 = IT . y holds
signature U1 = signature U2;

end;

:: deftheorem Def12 defines equal-signature PRALG_1:def 12 :

registration

let J be non empty set ;
cluster Univ_Alg-yielding 1-sorted-yielding equal-signature ManySortedSet of J;
existence

proof end;

end;

definition

let J be non empty set ;
let A be 1-sorted-yielding ManySortedSet of J;
let j be Element of J;
:: original: .
redefine func A . j -> 1-sorted ;
coherence

proof end;

end;

definition

let J be non empty set ;
let A be Univ_Alg-yielding ManySortedSet of J;
let j be Element of J;
:: original: .
redefine func A . j -> Universal_Algebra;
coherence

proof end;

end;

definition

let J be set ;
let A be 1-sorted-yielding ManySortedSet of J;
func Carrier A -> ManySortedSet of J means :Def13: :: PRALG_1:def 13
for j being set st j in J holds
ex R being 1-sorted st
( R = A . j & it . j = the carrier of R );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines Carrier PRALG_1:def 13 :

registration

let J be non empty set ;
let A be Univ_Alg-yielding ManySortedSet of J;
cluster Carrier A -> V3 ;
coherence

proof end;

end;

definition

let J be non empty set ;
let A be Univ_Alg-yielding equal-signature ManySortedSet of J;
func ComSign A -> FinSequence of NAT means :Def14: :: PRALG_1:def 14
for j being Element of J holds it = signature (A . j);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines ComSign PRALG_1:def 14 :

registration

let J be non empty set ;
let B be V3 ManySortedSet of J;
cluster product B -> non empty ;
coherence ;

end;

definition

let J be non empty set ;
let B be V3 ManySortedSet of J;
mode ManySortedOperation of B -> ManySortedFunction of J means :Def15: :: PRALG_1:def 15
for j being Element of J holds it . j is non empty homogeneous quasi_total PartFunc of (B . j) * ,B . j;
existence

proof end;

end;

:: deftheorem Def15 defines ManySortedOperation PRALG_1:def 15 :

definition

let J be non empty set ;
let B be V3 ManySortedSet of J;
let O be ManySortedOperation of B;
let j be Element of J;
:: original: .
redefine func O . j -> non empty homogeneous quasi_total PartFunc of (B . j) * ,B . j;
coherence by Def15;

end;

definition

let IT be Function;
attr IT is equal-arity means :Def16: :: PRALG_1:def 16
for x, y being set st x in dom IT & y in dom IT holds
for f, g being Function st IT . x = f & IT . y = g holds
for n, m being Nat
for X, Y being non empty set st dom f = n -tuples_on X & dom g = m -tuples_on Y holds
for o1 being non empty homogeneous quasi_total PartFunc of X * ,X
for o2 being non empty homogeneous quasi_total PartFunc of Y * ,Y st f = o1 & g = o2 holds
arity o1 = arity o2;

end;

:: deftheorem Def16 defines equal-arity PRALG_1:def 16 :

registration

let J be non empty set ;
let B be V3 ManySortedSet of J;
cluster equal-arity ManySortedOperation of B;
existence

proof end;

end;

theorem Th12: :: PRALG_1:12

for J being non empty set
for B being V3 ManySortedSet of J
for O being ManySortedOperation of B holds
( O is equal-arity iff for i, j being Element of J holds arity (O . i) = arity (O . j) )

proof end;

definition

let F be Function-yielding Function;
let f be Function;
func F .. f -> Function means :Def17: :: PRALG_1:def 17
( dom it = dom F & ( for x being set st x in dom F holds
it . x = (F . x) . (f . x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines .. PRALG_1:def 17 :

definition

let I be set ;
let f be ManySortedFunction of I;
let x be ManySortedSet of I;
:: original: ..
redefine func f .. x -> ManySortedSet of I means :Def18: :: PRALG_1:def 18
for i being set st i in I holds
for g being Function st g = f . i holds
it . i = g . (x . i);
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def18 defines .. PRALG_1:def 18 :

definition

let J be non empty set ;
let B be V3 ManySortedSet of J;
let p be FinSequence of product B;
:: original: uncurry
redefine func uncurry p -> ManySortedSet of [:(dom p),J:];
coherence

proof end;

end;

definition

let I, J be set ;
let X be ManySortedSet of [:I,J:];
:: original: ~
redefine func ~ X -> ManySortedSet of [:J,I:];
coherence

proof end;

end;

definition

let X be set ;
let Y be non empty set ;
let f be ManySortedSet of [:X,Y:];
:: original: curry
redefine func curry f -> ManySortedSet of X;
coherence

proof end;

end;

definition

let J be non empty set ;
let B be V3 ManySortedSet of J;
let O be equal-arity ManySortedOperation of B;
func ComAr O -> Nat means :Def19: :: PRALG_1:def 19
for j being Element of J holds it = arity (O . j);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines ComAr PRALG_1:def 19 :

definition

let I be set ;
let A be ManySortedSet of I;
func EmptySeq A -> ManySortedSet of I means :Def20: :: PRALG_1:def 20
for i being set st i in I holds
it . i = {} (A . i);
existence

proof end;