:: UNIALG_2 semantic presentation

for n being Nat
for D being non empty set
for D1 being non empty Subset of D holds (n -tuples_on D) /\ (n -tuples_on D1) = n -tuples_on D1

proof end;

theorem Th2: :: UNIALG_2:2

for D being non empty set
for h being non empty homogeneous quasi_total PartFunc of D * ,D holds dom h = (arity h) -tuples_on D

proof end;

definition

let D be non empty set ;
mode PFuncsDomHQN of D -> non empty set means :Def1: :: UNIALG_2:def 1
for x being Element of it holds x is non empty homogeneous quasi_total PartFunc of D * ,D;
existence

proof end;

end;

:: deftheorem Def1 defines PFuncsDomHQN UNIALG_2:def 1 :

definition

let D be non empty set ;
let P be PFuncsDomHQN of D;
:: original: Element
redefine mode Element of P -> non empty homogeneous quasi_total PartFunc of D * ,D;
coherence by Def1;

end;

definition

let U1 be Universal_Algebra;
mode PFuncsDomHQN of U1 is PFuncsDomHQN of the carrier of U1;

end;

definition

let U1 be UAStr ;
mode PartFunc of U1 is PartFunc of the carrier of U1 * ,the carrier of U1;

end;

definition

let U1, U2 be Universal_Algebra;
pred U1,U2 are_similar means :Def2: :: UNIALG_2:def 2
signature U1 = signature U2;
symmetry ;
reflexivity ;

end;

:: deftheorem Def2 defines are_similar UNIALG_2:def 2 :

theorem :: UNIALG_2:3

for U1, U2 being Universal_Algebra st U1,U2 are_similar holds
len the charact of U1 = len the charact of U2

proof end;

theorem :: UNIALG_2:4

for U1, U2, U3 being Universal_Algebra st U1,U2 are_similar & U2,U3 are_similar holds
U1,U3 are_similar

proof end;

theorem :: UNIALG_2:5

for U0 being Universal_Algebra holds rng the charact of U0 is non empty Subset of (PFuncs (the carrier of U0 * ),the carrier of U0) by FINSEQ_1:27, FINSEQ_1:def 4;

definition

let U0 be Universal_Algebra;
func Operations U0 -> PFuncsDomHQN of U0 equals :: UNIALG_2:def 3
rng the charact of U0;
coherence

proof end;

end;

:: deftheorem defines Operations UNIALG_2:def 3 :

definition

let U1 be Universal_Algebra;
mode operation of U1 is Element of Operations U1;

end;

theorem Th6: :: UNIALG_2:6

for U0 being Universal_Algebra
for n being set st n in dom the charact of U0 holds
the charact of U0 . n is operation of U0 by FUNCT_1:def 5;

definition

let U0 be Universal_Algebra;
let A be Subset of U0;
let o be operation of U0;
pred A is_closed_on o means :Def4: :: UNIALG_2:def 4
for s being FinSequence of A st len s = arity o holds
o . s in A;

end;

:: deftheorem Def4 defines is_closed_on UNIALG_2:def 4 :

definition

let U0 be Universal_Algebra;
let A be Subset of U0;
attr A is opers_closed means :Def5: :: UNIALG_2:def 5
for o being operation of U0 holds A is_closed_on o;

end;

:: deftheorem Def5 defines opers_closed UNIALG_2:def 5 :

definition

let U0 be Universal_Algebra;
let A be non empty Subset of U0;
let o be operation of U0;
assume A1: A is_closed_on o ;
func o /. A -> non empty homogeneous quasi_total PartFunc of A * ,A equals :Def6: :: UNIALG_2:def 6
o | ((arity o) -tuples_on A);
coherence

proof end;

end;

:: deftheorem Def6 defines /. UNIALG_2:def 6 :

definition

let U0 be Universal_Algebra;
let A be non empty Subset of U0;
func Opers U0,A -> PFuncFinSequence of A means :Def7: :: UNIALG_2:def 7
( dom it = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom it & o = the charact of U0 . n holds
it . n = o /. A ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines Opers UNIALG_2:def 7 :

theorem Th7: :: UNIALG_2:7

for U0 being Universal_Algebra
for B being non empty Subset of U0 st B = the carrier of U0 holds
( B is opers_closed & ( for o being operation of U0 holds o /. B = o ) )

proof end;

theorem :: UNIALG_2:8

for U1 being Universal_Algebra
for A being non empty Subset of U1
for o being operation of U1 st A is_closed_on o holds
arity (o /. A) = arity o

proof end;

definition

let U0 be Universal_Algebra;
mode SubAlgebra of U0 -> Universal_Algebra means :Def8: :: UNIALG_2:def 8
( the carrier of it is Subset of U0 & ( for B being non empty Subset of U0 st B = the carrier of it holds
( the charact of it = Opers U0,B & B is opers_closed ) ) );
existence

proof end;

end;

:: deftheorem Def8 defines SubAlgebra UNIALG_2:def 8 :

registration

let U0 be Universal_Algebra;
cluster strict SubAlgebra of U0;
existence

proof end;

end;

theorem Th9: :: UNIALG_2:9

for U0, U1 being Universal_Algebra
for o0 being operation of U0
for o1 being operation of U1
for n being Nat st U0 is SubAlgebra of U1 & n in dom the charact of U0 & o0 = the charact of U0 . n & o1 = the charact of U1 . n holds
arity o0 = arity o1

proof end;

theorem Th10: :: UNIALG_2:10

for U0, U1 being Universal_Algebra st U0 is SubAlgebra of U1 holds
dom the charact of U0 = dom the charact of U1

proof end;

theorem :: UNIALG_2:11

for U0 being Universal_Algebra holds U0 is SubAlgebra of U0

proof end;

theorem :: UNIALG_2:12

for U0, U1, U2 being Universal_Algebra st U0 is SubAlgebra of U1 & U1 is SubAlgebra of U2 holds
U0 is SubAlgebra of U2

proof end;

theorem Th13: :: UNIALG_2:13

for U1, U2 being Universal_Algebra st U1 is strict SubAlgebra of U2 & U2 is strict SubAlgebra of U1 holds
U1 = U2

proof end;

theorem Th14: :: UNIALG_2:14

for U0 being Universal_Algebra
for U1, U2 being SubAlgebra of U0 st the carrier of U1 c= the carrier of U2 holds
U1 is SubAlgebra of U2

proof end;

theorem Th15: :: UNIALG_2:15

for U0 being Universal_Algebra
for U1, U2 being strict SubAlgebra of U0 st the carrier of U1 = the carrier of U2 holds
U1 = U2

proof end;

theorem :: UNIALG_2:16

for U1, U2 being Universal_Algebra st U1 is SubAlgebra of U2 holds
U1,U2 are_similar

proof end;

theorem Th17: :: UNIALG_2:17

for U0 being Universal_Algebra
for A being non empty Subset of U0 holds UAStr(# A,(Opers U0,A) #) is strict Universal_Algebra

proof end;

definition

let U0 be Universal_Algebra;
let A be non empty Subset of U0;
assume A1: A is opers_closed ;
func UniAlgSetClosed A -> strict SubAlgebra of U0 equals :Def9: :: UNIALG_2:def 9
UAStr(# A,(Opers U0,A) #);
coherence

proof end;

end;

:: deftheorem Def9 defines UniAlgSetClosed UNIALG_2:def 9 :

definition

let U0 be Universal_Algebra;
let U1, U2 be SubAlgebra of U0;
assume A1: the carrier of U1 meets the carrier of U2 ;
func U1 /\ U2 -> strict SubAlgebra of U0 means :Def10: :: UNIALG_2:def 10
( the carrier of it = the carrier of U1 /\ the carrier of U2 & ( for B being non empty Subset of U0 st B = the carrier of it holds
( the charact of it = Opers U0,B & B is opers_closed ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines /\ UNIALG_2:def 10 :

definition

let U0 be Universal_Algebra;
func Constants U0 -> Subset of U0 equals :: UNIALG_2:def 11
{ a where a is Element of U0 : ex o being operation of U0 st
( arity o = 0 & a in rng o ) } ;
coherence

proof end;

end;

:: deftheorem defines Constants UNIALG_2:def 11 :

definition

let IT be Universal_Algebra;
attr IT is with_const_op means :Def12: :: UNIALG_2:def 12
ex o being operation of IT st arity o = 0;

end;

:: deftheorem Def12 defines with_const_op UNIALG_2:def 12 :

registration

cluster strict with_const_op UAStr ;
existence

proof end;

end;

registration

let U0 be with_const_op Universal_Algebra;
cluster Constants U0 -> non empty ;
coherence

proof end;

end;

theorem Th18: :: UNIALG_2:18

for U0 being Universal_Algebra
for U1 being SubAlgebra of U0 holds Constants U0 is Subset of U1

proof end;

theorem :: UNIALG_2:19

for U0 being with_const_op Universal_Algebra
for U1 being SubAlgebra of U0 holds Constants U0 is non empty Subset of U1 by Th18;

theorem Th20: :: UNIALG_2:20

for U0 being with_const_op Universal_Algebra
for U1, U2 being SubAlgebra of U0 holds the carrier of U1 meets the carrier of U2

proof end;

definition

let U0 be Universal_Algebra;
let A be Subset of U0;
assume A1: ( Constants U0 <> {} or A <> {} ) ;
func GenUnivAlg A -> strict SubAlgebra of U0 means :Def13: :: UNIALG_2:def 13
( A c= the carrier of it & ( for U1 being SubAlgebra of U0 st A c= the carrier of U1 holds
it is SubAlgebra of U1 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines GenUnivAlg UNIALG_2:def 13 :

theorem :: UNIALG_2:21

for U0 being strict Universal_Algebra holds GenUnivAlg ([#] the carrier of U0) = U0

proof end;

theorem Th22: :: UNIALG_2:22

for U0 being Universal_Algebra
for U1 being strict SubAlgebra of U0
for B being non empty Subset of U0 st B = the carrier of U1 holds
GenUnivAlg B = U1

proof end;

definition

let U0 be Universal_Algebra;
let U1, U2 be SubAlgebra of U0;
func U1 "\/" U2 -> strict SubAlgebra of U0 means :Def14: :: UNIALG_2:def 14
for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds
it = GenUnivAlg A;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines "\/" UNIALG_2:def 14 :

theorem Th23: :: UNIALG_2:23

for U0 being Universal_Algebra
for U1 being SubAlgebra of U0
for A, B being Subset of U0 st ( A <> {} or Constants U0 <> {} ) & B = A \/ the carrier of U1 holds
(GenUnivAlg A) "\/" U1 = GenUnivAlg B

proof end;

theorem Th24: :: UNIALG_2:24

for U0 being Universal_Algebra
for U1, U2 being SubAlgebra of U0 holds U1 "\/" U2 = U2 "\/" U1

proof end;

theorem Th25: :: UNIALG_2:25

for U0 being with_const_op Universal_Algebra
for U1, U2 being strict SubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = U1

proof end;

theorem Th26: :: UNIALG_2:26

for U0 being with_const_op Universal_Algebra
for U1, U2 being strict SubAlgebra of U0 holds (U1 /\ U2) "\/" U2 = U2

proof end;

definition

let U0 be Universal_Algebra;
func Sub U0 -> set means :Def15: :: UNIALG_2:def 15
for x being set holds
( x in it iff x is strict SubAlgebra of U0 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines Sub UNIALG_2:def 15 :

registration

let U0 be Universal_Algebra;
cluster Sub U0 -> non empty ;
coherence

proof end;

end;

definition

let U0 be Universal_Algebra;
func UniAlg_join U0 -> BinOp of Sub U0 means :Def16: :: UNIALG_2:def 16
for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
it . x,y = U1 "\/" U2;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines UniAlg_join UNIALG_2:def 16 :

definition

let U0 be Universal_Algebra;
func UniAlg_meet U0 -> BinOp of Sub U0 means :Def17: :: UNIALG_2:def 17
for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
it . x,y = U1 /\ U2;
existence

proof end;