:: PRALG_1 semantic presentation

theorem Th1: :: PRALG_1:1

for b₁, b₂ being non empty set
for b₃, b₄ being Nat st b₃ -tuples_on b₁ = b₄ -tuples_on b₂ holds
b₃ = b₄

proof end;

definition

let c₁, c₂ be non empty set ;
let c₃ be FinSequence of [:c₁,c₂:];
redefine func pr1 as pr1 c₃ -> FinSequence of a₁ means :Def1: :: PRALG_1:def 1
( len a₄ = len a₃ & ( for b₁ being Nat st b₁ in dom a₄ holds
a₄ . b₁ = (a₃ . b₁) `1 ) );
compatibility

proof end;

coherence

proof end;

redefine func pr2 as pr2 c₃ -> FinSequence of a₂ means :Def2: :: PRALG_1:def 2
( len a₄ = len a₃ & ( for b₁ being Nat st b₁ in dom a₄ holds
a₄ . b₁ = (a₃ . b₁) `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 c₁, c₂ be non empty set ;
let c₃ be non empty homogeneous quasi_total PartFunc of c₁ * ,c₁;
let c₄ be non empty homogeneous quasi_total PartFunc of c₂ * ,c₂;
assume E4: arity c₃ = arity c₄ ;
func [[:c₃,c₄:]] -> non empty homogeneous quasi_total PartFunc of [:a₁,a₂:] * ,[:a₁,a₂:] means :Def3: :: PRALG_1:def 3
( dom a₅ = (arity a₃) -tuples_on [:a₁,a₂:] & ( for b₁ being FinSequence of [:a₁,a₂:] st b₁ in dom a₅ holds
a₅ . b₁ = [(a₃ . (pr1 b₁)),(a₄ . (pr2 b₁))] ) );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁, c₂ be Universal_Algebra;
assume E5: c₁,c₂ are_similar ;
func Opers c₁,c₂ -> PFuncFinSequence of [:the carrier of a₁,the carrier of a₂:] means :Def4: :: PRALG_1:def 4
( len a₃ = len the charact of a₁ & ( for b₁ being Nat st b₁ in dom a₃ holds
for b₂ being non empty homogeneous quasi_total PartFunc of the carrier of a₁ * ,the carrier of a₁
for b₃ being non empty homogeneous quasi_total PartFunc of the carrier of a₂ * ,the carrier of a₂ st b₂ = the charact of a₁ . b₁ & b₃ = the charact of a₂ . b₁ holds
a₃ . b₁ = [[:b₂,b₃:]] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Opers PRALG_1:def 4 :

theorem Th2: :: PRALG_1:2

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

proof end;

definition

let c₁, c₂ be Universal_Algebra;
assume E7: c₁,c₂ are_similar ;
func [:c₁,c₂:] -> strict Universal_Algebra equals :Def5: :: PRALG_1:def 5
UAStr(# [:the carrier of a₁,the carrier of a₂:],(Opers a₁,a₂) #);
coherence by E7, Th2;

end;

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

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines Inv PRALG_1:def 6 :

theorem Th3: :: PRALG_1:3

for b₁, b₂ being non empty set holds rng (Inv b₁,b₂) = [:b₂,b₁:]

proof end;

theorem Th4: :: PRALG_1:4

for b₁, b₂ being non empty set holds Inv b₁,b₂ is one-to-one

proof end;

theorem Th5: :: PRALG_1:5

for b₁, b₂ being Universal_Algebra st b₁,b₂ are_similar holds
Inv the carrier of b₁,the carrier of b₂ is Function of the carrier of [:b₁,b₂:],the carrier of [:b₂,b₁:]

proof end;

theorem Th6: :: PRALG_1:6

for b₁, b₂ being Universal_Algebra st b₁,b₂ are_similar holds
for b₃ being operation of b₁
for b₄ being operation of b₂
for b₅ being operation of [:b₁,b₂:]
for b₆ being Nat st b₃ = the charact of b₁ . b₆ & b₄ = the charact of b₂ . b₆ & b₅ = the charact of [:b₁,b₂:] . b₆ & b₆ in dom the charact of b₁ holds
( arity b₅ = arity b₃ & arity b₅ = arity b₄ & b₅ = [[:b₃,b₄:]] )

proof end;

theorem Th7: :: PRALG_1:7

for b₁, b₂ being Universal_Algebra st b₁,b₂ are_similar holds
[:b₁,b₂:],b₁ are_similar

proof end;

theorem Th8: :: PRALG_1:8

for b₁, b₂, b₃, b₄ being Universal_Algebra st b₁ is SubAlgebra of b₂ & b₃ is SubAlgebra of b₄ & b₂,b₄ are_similar holds
[:b₁,b₃:] is SubAlgebra of [:b₂,b₄:]

proof end;

definition

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

proof end;

uniqueness by FUNCT_1:17;

end;

:: deftheorem Def7 defines TrivialOp PRALG_1:def 7 :

registration

let c₁ be natural number ;
cluster TrivialOp a₁ -> non empty homogeneous quasi_total ;
coherence

proof end;

end;

theorem Th9: :: PRALG_1:9

for b₁ being natural number holds arity (TrivialOp b₁) = b₁

proof end;

definition

let c₁ be FinSequence of NAT ;
func TrivialOps c₁ -> PFuncFinSequence of {{} } means :Def8: :: PRALG_1:def 8
( len a₂ = len a₁ & ( for b₁ being Nat st b₁ in dom a₂ holds
for b₂ being Nat st b₂ = a₁ . b₁ holds
a₂ . b₁ = TrivialOp b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines TrivialOps PRALG_1:def 8 :

theorem Th10: :: PRALG_1:10

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

proof end;

theorem Th11: :: PRALG_1:11

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

proof end;

registration

let c₁ be non empty set ;
cluster non empty FinSequence of a₁;
existence

proof end;

cluster non empty Element of a₁ * ;
existence

proof end;

end;

definition

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

end;

:: deftheorem Def9 defines Trivial_Algebra PRALG_1:def 9 :

definition

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

end;

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

definition

let c₁ be Function;
attr a₁ is 1-sorted-yielding means :Def11: :: PRALG_1:def 11
for b₁ being set st b₁ in dom a₁ holds
a₁ . b₁ 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 c₁ be set ;
cluster 1-sorted-yielding ManySortedSet of a₁;
existence

proof end;

end;

definition

let c₁ be Function;
attr a₁ is equal-signature means :Def12: :: PRALG_1:def 12
for b₁, b₂ being set st b₁ in dom a₁ & b₂ in dom a₁ holds
for b₃, b₄ being Universal_Algebra st b₃ = a₁ . b₁ & b₄ = a₁ . b₂ holds
signature b₃ = signature b₄;

end;

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

registration

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

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be 1-sorted-yielding ManySortedSet of c₁;
let c₃ be Element of c₁;
redefine func . as c₂ . c₃ -> 1-sorted ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be Univ_Alg-yielding ManySortedSet of c₁;
let c₃ be Element of c₁;
redefine func . as c₂ . c₃ -> Universal_Algebra;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be 1-sorted-yielding ManySortedSet of c₁;
func Carrier c₂ -> ManySortedSet of a₁ means :Def13: :: PRALG_1:def 13
for b₁ being set st b₁ in a₁ holds
ex b₂ being 1-sorted st
( b₂ = a₂ . b₁ & a₃ . b₁ = the carrier of b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines Carrier PRALG_1:def 13 :

registration

let c₁ be non empty set ;
let c₂ be Univ_Alg-yielding ManySortedSet of c₁;
cluster Carrier a₂ -> V3 ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be Univ_Alg-yielding equal-signature ManySortedSet of c₁;
func ComSign c₂ -> FinSequence of NAT means :Def14: :: PRALG_1:def 14
for b₁ being Element of a₁ holds a₃ = signature (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines ComSign PRALG_1:def 14 :

registration

let c₁ be non empty set ;
let c₂ be V3 ManySortedSet of c₁;
cluster product a₂ -> non empty ;
coherence ;

end;

definition

let c₁ be non empty set ;
let c₂ be V3 ManySortedSet of c₁;
mode ManySortedOperation of c₂ -> ManySortedFunction of a₁ means :Def15: :: PRALG_1:def 15
for b₁ being Element of a₁ holds a₃ . b₁ is non empty homogeneous quasi_total PartFunc of (a₂ . b₁) * ,a₂ . b₁;
existence

proof end;

end;

:: deftheorem Def15 defines ManySortedOperation PRALG_1:def 15 :

definition

let c₁ be non empty set ;
let c₂ be V3 ManySortedSet of c₁;
let c₃ be ManySortedOperation of c₂;
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> non empty homogeneous quasi_total PartFunc of (a₂ . a₄) * ,a₂ . a₄;
coherence by Def15;

end;

definition

let c₁ be Function;
attr a₁ is equal-arity means :Def16: :: PRALG_1:def 16
for b₁, b₂ being set st b₁ in dom a₁ & b₂ in dom a₁ holds
for b₃, b₄ being Function st a₁ . b₁ = b₃ & a₁ . b₂ = b₄ holds
for b₅, b₆ being Nat
for b₇, b₈ being non empty set st dom b₃ = b₅ -tuples_on b₇ & dom b₄ = b₆ -tuples_on b₈ holds
for b₉ being non empty homogeneous quasi_total PartFunc of b₇ * ,b₇
for b₁₀ being non empty homogeneous quasi_total PartFunc of b₈ * ,b₈ st b₃ = b₉ & b₄ = b₁₀ holds
arity b₉ = arity b₁₀;

end;

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

registration

let c₁ be non empty set ;
let c₂ be V3 ManySortedSet of c₁;
cluster equal-arity ManySortedOperation of a₂;
existence

proof end;

end;

theorem Th12: :: PRALG_1:12

for b₁ being non empty set
for b₂ being V3 ManySortedSet of b₁
for b₃ being ManySortedOperation of b₂ holds
( b₃ is equal-arity iff for b₄, b₅ being Element of b₁ holds arity (b₃ . b₄) = arity (b₃ . b₅) )

proof end;

definition

let c₁ be Function-yielding Function;
let c₂ be Function;
func c₁ .. c₂ -> Function means :Def17: :: PRALG_1:def 17
( dom a₃ = dom a₁ & ( for b₁ being set st b₁ in dom a₁ holds
a₃ . b₁ = (a₁ . b₁) . (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁ be set ;
let c₂ be ManySortedFunction of c₁;
let c₃ be ManySortedSet of c₁;
redefine func .. as c₂ .. c₃ -> ManySortedSet of a₁ means :Def18: :: PRALG_1:def 18
for b₁ being set st b₁ in a₁ holds
for b₂ being Function st b₂ = a₂ . b₁ holds
a₄ . b₁ = b₂ . (a₃ . b₁);
coherence

proof end;

compatibility

proof end;

end;

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

definition

let c₁ be non empty set ;
let c₂ be V3 ManySortedSet of c₁;
let c₃ be FinSequence of product c₂;
redefine func uncurry as uncurry c₃ -> ManySortedSet of [:(dom a₃),a₁:];
coherence

proof end;

end;

definition

let c₁, c₂ be set ;
let c₃ be ManySortedSet of [:c₁,c₂:];
redefine func ~ as ~ c₃ -> ManySortedSet of [:a₂,a₁:];
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be ManySortedSet of [:c₁,c₂:];
redefine func curry as curry c₃ -> ManySortedSet of a₁;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be V3 ManySortedSet of c₁;
let c₃ be equal-arity ManySortedOperation of c₂;
func ComAr c₃ -> Nat means :Def19: :: PRALG_1:def 19
for b₁ being Element of a₁ holds a₄ = arity (a₃ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines ComAr PRALG_1:def 19 :

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
func EmptySeq c₂ -> ManySortedSet of a₁ means :Def20: :: PRALG_1:def 20
for b₁ being set st b₁ in a₁ holds
a₃ . b₁ = {} (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines EmptySeq PRALG_1:def 20 :

definition

let c₁ be non empty set ;
let c₂ be V3 ManySortedSet of c₁;
let c₃ be equal-arity ManySortedOperation of c₂;
func [[:c₃:]] -> non empty homogeneous quasi_total PartFunc of (product a₂) * , product a₂ means :: PRALG_1:def 21
( dom a₄ = (ComAr a₃) -tuples_on (product a₂) & ( for b₁ being Element of (product a₂) * st b₁ in dom a₄ holds
( ( dom b₁ = {} implies a₄ . b₁ = a₃ .. (EmptySeq a₂) ) & ( dom b₁ <> {} implies for b₂ being non empty set
for b₃ being ManySortedSet of [:a₁,b₂:] st b₂ = dom b₁ & b₃ = ~ (uncurry b₁) holds
a₄ . b₁ = a₃ .. (curry b₃) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def21 defines [[: PRALG_1:def 21 :

definition

let c₁ be non empty set ;
let c₂ be Univ_Alg-yielding equal-signature ManySortedSet of c₁;
let c₃ be natural number ;
assume E26: c₃ in dom (ComSign c₂) ;
func ProdOp c₂,c₃ -> equal-arity ManySortedOperation of Carrier a₂ means :: PRALG_1:def 22
for b₁ being Element of a₁
for b₂ being operation of (a₂ . b₁) st the charact of (a₂ . b₁) . a₃ = b₂ holds
a₄ . b₁ = b₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines ProdOp PRALG_1:def 22 :

definition

let c₁ be non empty set ;
let c₂ be Univ_Alg-yielding equal-signature ManySortedSet of c₁;
func ProdOpSeq c₂ -> PFuncFinSequence of (product (Carrier a₂)) means :Def23: :: PRALG_1:def 23
( len a₃ = len (ComSign a₂) & ( for b₁ being Nat st b₁ in dom a₃ holds
a₃ . b₁ = [[:(ProdOp a₂,b₁):]] ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def23 defines ProdOpSeq PRALG_1:def 23 :

definition

let c₁ be non empty set ;
let c₂ be Univ_Alg-yielding equal-signature ManySortedSet of c₁;
func ProdUnivAlg c₂ -> strict Universal_Algebra equals :: PRALG_1:def 24
UAStr(# (product (Carrier a₂)),(ProdOpSeq a₂) #);
coherence

proof end;

end;

:: deftheorem Def24 defines ProdUnivAlg PRALG_1:def 24 :