:: by Beata Perkowska

::

:: Received October 20, 1993

:: Copyright (c) 1993-2016 Association of Mizar Users

definition
end;

:: deftheorem Def1 defines disjoint_with_NAT FREEALG:def 1 :

for IT being set holds

( IT is disjoint_with_NAT iff IT misses NAT );

for IT being set holds

( IT is disjoint_with_NAT iff IT misses NAT );

registration
end;

Lm1: ( not 0 in rng <*1*> & 0 in rng <*0*> )

proof end;

notation
end;

definition
end;

:: deftheorem Def2 defines with_zero FREEALG:def 2 :

for IT being Relation holds

( not IT is with_zero iff not 0 in rng IT );

for IT being Relation holds

( not IT is with_zero iff not 0 in rng IT );

registration

ex b_{1} being FinSequence of NAT st

( not b_{1} is empty & b_{1} is with_zero )

ex b_{1} being FinSequence of NAT st

( not b_{1} is empty & b_{1} is without_zero )
end;

cluster non empty Relation-like with_zero NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like for FinSequence of NAT ;

existence ex b

( not b

proof end;

cluster non empty Relation-like without_zero NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like for FinSequence of NAT ;

existence ex b

( not b

proof end;

definition

let U1 be Universal_Algebra;

let n be Nat;

assume A1: n in dom the charact of U1 ;

coherence

the charact of U1 . n is operation of U1 by A1, FUNCT_1:def 3;

end;
let n be Nat;

assume A1: n in dom the charact of U1 ;

coherence

the charact of U1 . n is operation of U1 by A1, FUNCT_1:def 3;

:: deftheorem Def3 defines oper FREEALG:def 3 :

for U1 being Universal_Algebra

for n being Nat st n in dom the charact of U1 holds

oper (n,U1) = the charact of U1 . n;

for U1 being Universal_Algebra

for n being Nat st n in dom the charact of U1 holds

oper (n,U1) = the charact of U1 . n;

definition

let U0 be Universal_Algebra;

ex b_{1} being Subset of U0 st

for A being Subset of U0 st A is opers_closed & b_{1} c= A holds

A = the carrier of U0

end;
mode GeneratorSet of U0 -> Subset of U0 means :: FREEALG:def 4

for A being Subset of U0 st A is opers_closed & it c= A holds

A = the carrier of U0;

existence for A being Subset of U0 st A is opers_closed & it c= A holds

A = the carrier of U0;

ex b

for A being Subset of U0 st A is opers_closed & b

A = the carrier of U0

proof end;

:: deftheorem defines GeneratorSet FREEALG:def 4 :

for U0 being Universal_Algebra

for b_{2} being Subset of U0 holds

( b_{2} is GeneratorSet of U0 iff for A being Subset of U0 st A is opers_closed & b_{2} c= A holds

A = the carrier of U0 );

for U0 being Universal_Algebra

for b

( b

A = the carrier of U0 );

Lm2: for A being Universal_Algebra

for B being Subset of A st B is opers_closed holds

Constants A c= B

proof end;

Lm3: for A being Universal_Algebra

for B being Subset of A st ( B <> {} or Constants A <> {} ) holds

( B is GeneratorSet of A iff the carrier of (GenUnivAlg B) = the carrier of A )

proof end;

definition

let U0 be Universal_Algebra;

let IT be GeneratorSet of U0;

end;
let IT be GeneratorSet of U0;

attr IT is free means :: FREEALG:def 5

for U1 being Universal_Algebra st U0,U1 are_similar holds

for f being Function of IT, the carrier of U1 ex h being Function of U0,U1 st

( h is_homomorphism & h | IT = f );

for U1 being Universal_Algebra st U0,U1 are_similar holds

for f being Function of IT, the carrier of U1 ex h being Function of U0,U1 st

( h is_homomorphism & h | IT = f );

:: deftheorem defines free FREEALG:def 5 :

for U0 being Universal_Algebra

for IT being GeneratorSet of U0 holds

( IT is free iff for U1 being Universal_Algebra st U0,U1 are_similar holds

for f being Function of IT, the carrier of U1 ex h being Function of U0,U1 st

( h is_homomorphism & h | IT = f ) );

for U0 being Universal_Algebra

for IT being GeneratorSet of U0 holds

( IT is free iff for U1 being Universal_Algebra st U0,U1 are_similar holds

for f being Function of IT, the carrier of U1 ex h being Function of U0,U1 st

( h is_homomorphism & h | IT = f ) );

:: deftheorem Def6 defines free FREEALG:def 6 :

for IT being Universal_Algebra holds

( IT is free iff ex G being GeneratorSet of IT st G is free );

for IT being Universal_Algebra holds

( IT is free iff ex G being GeneratorSet of IT st G is free );

registration
end;

registration

let U0 be free Universal_Algebra;

existence

ex b_{1} being GeneratorSet of U0 st b_{1} is free
by Def6;

end;
existence

ex b

theorem :: FREEALG:1

for U0 being strict Universal_Algebra

for A being Subset of U0 st ( Constants U0 <> {} or A <> {} ) holds

( A is GeneratorSet of U0 iff GenUnivAlg A = U0 )

for A being Subset of U0 st ( Constants U0 <> {} or A <> {} ) holds

( A is GeneratorSet of U0 iff GenUnivAlg A = U0 )

proof end;

::

:: Construction of a Decorated Tree Structure for Free Universal Algebra

::

:: Construction of a Decorated Tree Structure for Free Universal Algebra

::

definition

let f be non empty FinSequence of NAT ;

let X be set ;

ex b_{1} being Relation of ((dom f) \/ X),(((dom f) \/ X) *) st

for a being Element of (dom f) \/ X

for b being Element of ((dom f) \/ X) * holds

( [a,b] in b_{1} iff ( a in dom f & f . a = len b ) )

for b_{1}, b_{2} being Relation of ((dom f) \/ X),(((dom f) \/ X) *) st ( for a being Element of (dom f) \/ X

for b being Element of ((dom f) \/ X) * holds

( [a,b] in b_{1} iff ( a in dom f & f . a = len b ) ) ) & ( for a being Element of (dom f) \/ X

for b being Element of ((dom f) \/ X) * holds

( [a,b] in b_{2} iff ( a in dom f & f . a = len b ) ) ) holds

b_{1} = b_{2}

end;
let X be set ;

func REL (f,X) -> Relation of ((dom f) \/ X),(((dom f) \/ X) *) means :Def7: :: FREEALG:def 7

for a being Element of (dom f) \/ X

for b being Element of ((dom f) \/ X) * holds

( [a,b] in it iff ( a in dom f & f . a = len b ) );

existence for a being Element of (dom f) \/ X

for b being Element of ((dom f) \/ X) * holds

( [a,b] in it iff ( a in dom f & f . a = len b ) );

ex b

for a being Element of (dom f) \/ X

for b being Element of ((dom f) \/ X) * holds

( [a,b] in b

proof end;

uniqueness for b

for b being Element of ((dom f) \/ X) * holds

( [a,b] in b

for b being Element of ((dom f) \/ X) * holds

( [a,b] in b

b

proof end;

:: deftheorem Def7 defines REL FREEALG:def 7 :

for f being non empty FinSequence of NAT

for X being set

for b_{3} being Relation of ((dom f) \/ X),(((dom f) \/ X) *) holds

( b_{3} = REL (f,X) iff for a being Element of (dom f) \/ X

for b being Element of ((dom f) \/ X) * holds

( [a,b] in b_{3} iff ( a in dom f & f . a = len b ) ) );

for f being non empty FinSequence of NAT

for X being set

for b

( b

for b being Element of ((dom f) \/ X) * holds

( [a,b] in b

definition

let f be non empty FinSequence of NAT ;

let X be set ;

coherence

DTConstrStr(# ((dom f) \/ X),(REL (f,X)) #) is strict DTConstrStr ;

;

end;
let X be set ;

func DTConUA (f,X) -> strict DTConstrStr equals :: FREEALG:def 8

DTConstrStr(# ((dom f) \/ X),(REL (f,X)) #);

correctness DTConstrStr(# ((dom f) \/ X),(REL (f,X)) #);

coherence

DTConstrStr(# ((dom f) \/ X),(REL (f,X)) #) is strict DTConstrStr ;

;

:: deftheorem defines DTConUA FREEALG:def 8 :

for f being non empty FinSequence of NAT

for X being set holds DTConUA (f,X) = DTConstrStr(# ((dom f) \/ X),(REL (f,X)) #);

for f being non empty FinSequence of NAT

for X being set holds DTConUA (f,X) = DTConstrStr(# ((dom f) \/ X),(REL (f,X)) #);

registration
end;

theorem Th2: :: FREEALG:2

for f being non empty FinSequence of NAT

for X being set holds

( Terminals (DTConUA (f,X)) c= X & NonTerminals (DTConUA (f,X)) = dom f )

for X being set holds

( Terminals (DTConUA (f,X)) c= X & NonTerminals (DTConUA (f,X)) = dom f )

proof end;

theorem Th3: :: FREEALG:3

for f being non empty FinSequence of NAT

for X being disjoint_with_NAT set holds Terminals (DTConUA (f,X)) = X

for X being disjoint_with_NAT set holds Terminals (DTConUA (f,X)) = X

proof end;

registration

let f be non empty FinSequence of NAT ;

let X be set ;

coherence

DTConUA (f,X) is with_nonterminals by Th2;

end;
let X be set ;

coherence

DTConUA (f,X) is with_nonterminals by Th2;

registration

let f be non empty with_zero FinSequence of NAT ;

let X be set ;

coherence

( DTConUA (f,X) is with_nonterminals & DTConUA (f,X) is with_useful_nonterminals )

end;
let X be set ;

coherence

( DTConUA (f,X) is with_nonterminals & DTConUA (f,X) is with_useful_nonterminals )

proof end;

registration

let f be non empty FinSequence of NAT ;

let D be non empty disjoint_with_NAT set ;

coherence

( DTConUA (f,D) is with_terminals & DTConUA (f,D) is with_nonterminals & DTConUA (f,D) is with_useful_nonterminals )

end;
let D be non empty disjoint_with_NAT set ;

coherence

( DTConUA (f,D) is with_terminals & DTConUA (f,D) is with_nonterminals & DTConUA (f,D) is with_useful_nonterminals )

proof end;

definition

let f be non empty FinSequence of NAT ;

let X be set ;

let n be Nat;

assume A1: n in dom f ;

coherence

n is Symbol of (DTConUA (f,X)) by A1, XBOOLE_0:def 3;

end;
let X be set ;

let n be Nat;

assume A1: n in dom f ;

coherence

n is Symbol of (DTConUA (f,X)) by A1, XBOOLE_0:def 3;

:: deftheorem Def9 defines Sym FREEALG:def 9 :

for f being non empty FinSequence of NAT

for X being set

for n being Nat st n in dom f holds

Sym (n,f,X) = n;

for f being non empty FinSequence of NAT

for X being set

for n being Nat st n in dom f holds

Sym (n,f,X) = n;

::

:: Construction of Free Universal Algebra for Non Empty Set of Generators and

:: Given Signature

:: Construction of Free Universal Algebra for Non Empty Set of Generators and

:: Given Signature

definition

let f be non empty FinSequence of NAT ;

let D be non empty disjoint_with_NAT set ;

let n be Nat;

assume A1: n in dom f ;

ex b_{1} being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st

( dom b_{1} = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b_{1} holds

b_{1} . p = (Sym (n,f,D)) -tree p ) )

for b_{1}, b_{2} being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st dom b_{1} = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b_{1} holds

b_{1} . p = (Sym (n,f,D)) -tree p ) & dom b_{2} = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b_{2} holds

b_{2} . p = (Sym (n,f,D)) -tree p ) holds

b_{1} = b_{2}

end;
let D be non empty disjoint_with_NAT set ;

let n be Nat;

assume A1: n in dom f ;

func FreeOpNSG (n,f,D) -> non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) means :Def10: :: FREEALG:def 10

( dom it = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom it holds

it . p = (Sym (n,f,D)) -tree p ) );

existence ( dom it = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom it holds

it . p = (Sym (n,f,D)) -tree p ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def10 defines FreeOpNSG FREEALG:def 10 :

for f being non empty FinSequence of NAT

for D being non empty disjoint_with_NAT set

for n being Nat st n in dom f holds

for b_{4} being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) holds

( b_{4} = FreeOpNSG (n,f,D) iff ( dom b_{4} = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b_{4} holds

b_{4} . p = (Sym (n,f,D)) -tree p ) ) );

for f being non empty FinSequence of NAT

for D being non empty disjoint_with_NAT set

for n being Nat st n in dom f holds

for b

( b

b

definition

let f be non empty FinSequence of NAT ;

let D be non empty disjoint_with_NAT set ;

ex b_{1} being PFuncFinSequence of (TS (DTConUA (f,D))) st

( len b_{1} = len f & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = FreeOpNSG (n,f,D) ) )

for b_{1}, b_{2} being PFuncFinSequence of (TS (DTConUA (f,D))) st len b_{1} = len f & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = FreeOpNSG (n,f,D) ) & len b_{2} = len f & ( for n being Nat st n in dom b_{2} holds

b_{2} . n = FreeOpNSG (n,f,D) ) holds

b_{1} = b_{2}

end;
let D be non empty disjoint_with_NAT set ;

func FreeOpSeqNSG (f,D) -> PFuncFinSequence of (TS (DTConUA (f,D))) means :Def11: :: FREEALG:def 11

( len it = len f & ( for n being Nat st n in dom it holds

it . n = FreeOpNSG (n,f,D) ) );

existence ( len it = len f & ( for n being Nat st n in dom it holds

it . n = FreeOpNSG (n,f,D) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def11 defines FreeOpSeqNSG FREEALG:def 11 :

for f being non empty FinSequence of NAT

for D being non empty disjoint_with_NAT set

for b_{3} being PFuncFinSequence of (TS (DTConUA (f,D))) holds

( b_{3} = FreeOpSeqNSG (f,D) iff ( len b_{3} = len f & ( for n being Nat st n in dom b_{3} holds

b_{3} . n = FreeOpNSG (n,f,D) ) ) );

for f being non empty FinSequence of NAT

for D being non empty disjoint_with_NAT set

for b

( b

b

definition

let f be non empty FinSequence of NAT ;

let D be non empty disjoint_with_NAT set ;

UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) is strict Universal_Algebra

end;
let D be non empty disjoint_with_NAT set ;

func FreeUnivAlgNSG (f,D) -> strict Universal_Algebra equals :: FREEALG:def 12

UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #);

coherence UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #);

UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #) is strict Universal_Algebra

proof end;

:: deftheorem defines FreeUnivAlgNSG FREEALG:def 12 :

for f being non empty FinSequence of NAT

for D being non empty disjoint_with_NAT set holds FreeUnivAlgNSG (f,D) = UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #);

for f being non empty FinSequence of NAT

for D being non empty disjoint_with_NAT set holds FreeUnivAlgNSG (f,D) = UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #);

theorem Th4: :: FREEALG:4

for f being non empty FinSequence of NAT

for D being non empty disjoint_with_NAT set holds signature (FreeUnivAlgNSG (f,D)) = f

for D being non empty disjoint_with_NAT set holds signature (FreeUnivAlgNSG (f,D)) = f

proof end;

definition

let f be non empty FinSequence of NAT ;

let D be non empty disjoint_with_NAT set ;

{ (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } is Subset of (FreeUnivAlgNSG (f,D))

end;
let D be non empty disjoint_with_NAT set ;

func FreeGenSetNSG (f,D) -> Subset of (FreeUnivAlgNSG (f,D)) equals :: FREEALG:def 13

{ (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } ;

coherence { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } ;

{ (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } is Subset of (FreeUnivAlgNSG (f,D))

proof end;

:: deftheorem defines FreeGenSetNSG FREEALG:def 13 :

for f being non empty FinSequence of NAT

for D being non empty disjoint_with_NAT set holds FreeGenSetNSG (f,D) = { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } ;

for f being non empty FinSequence of NAT

for D being non empty disjoint_with_NAT set holds FreeGenSetNSG (f,D) = { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } ;

theorem Th5: :: FREEALG:5

for f being non empty FinSequence of NAT

for D being non empty disjoint_with_NAT set holds not FreeGenSetNSG (f,D) is empty

for D being non empty disjoint_with_NAT set holds not FreeGenSetNSG (f,D) is empty

proof end;

definition

let f be non empty FinSequence of NAT ;

let D be non empty disjoint_with_NAT set ;

:: original: FreeGenSetNSG

redefine func FreeGenSetNSG (f,D) -> GeneratorSet of FreeUnivAlgNSG (f,D);

coherence

FreeGenSetNSG (f,D) is GeneratorSet of FreeUnivAlgNSG (f,D)

end;
let D be non empty disjoint_with_NAT set ;

:: original: FreeGenSetNSG

redefine func FreeGenSetNSG (f,D) -> GeneratorSet of FreeUnivAlgNSG (f,D);

coherence

FreeGenSetNSG (f,D) is GeneratorSet of FreeUnivAlgNSG (f,D)

proof end;

definition

let f be non empty FinSequence of NAT ;

let D be non empty disjoint_with_NAT set ;

let C be non empty set ;

let s be Symbol of (DTConUA (f,D));

let F be Function of (FreeGenSetNSG (f,D)),C;

assume A1: s in Terminals (DTConUA (f,D)) ;

coherence

F . (root-tree s) is Element of C

end;
let D be non empty disjoint_with_NAT set ;

let C be non empty set ;

let s be Symbol of (DTConUA (f,D));

let F be Function of (FreeGenSetNSG (f,D)),C;

assume A1: s in Terminals (DTConUA (f,D)) ;

coherence

F . (root-tree s) is Element of C

proof end;

:: deftheorem Def14 defines pi FREEALG:def 14 :

for f being non empty FinSequence of NAT

for D being non empty disjoint_with_NAT set

for C being non empty set

for s being Symbol of (DTConUA (f,D))

for F being Function of (FreeGenSetNSG (f,D)),C st s in Terminals (DTConUA (f,D)) holds

pi (F,s) = F . (root-tree s);

for f being non empty FinSequence of NAT

for D being non empty disjoint_with_NAT set

for C being non empty set

for s being Symbol of (DTConUA (f,D))

for F being Function of (FreeGenSetNSG (f,D)),C st s in Terminals (DTConUA (f,D)) holds

pi (F,s) = F . (root-tree s);

definition

let f be non empty FinSequence of NAT ;

let D be set ;

let s be Symbol of (DTConUA (f,D));

given p being FinSequence such that A1: s ==> p ;

coherence

s is Nat

end;
let D be set ;

let s be Symbol of (DTConUA (f,D));

given p being FinSequence such that A1: s ==> p ;

coherence

s is Nat

proof end;

:: deftheorem Def15 defines @ FREEALG:def 15 :

for f being non empty FinSequence of NAT

for D being set

for s being Symbol of (DTConUA (f,D)) st ex p being FinSequence st s ==> p holds

@ s = s;

for f being non empty FinSequence of NAT

for D being set

for s being Symbol of (DTConUA (f,D)) st ex p being FinSequence st s ==> p holds

@ s = s;

theorem Th6: :: FREEALG:6

for f being non empty FinSequence of NAT

for D being non empty disjoint_with_NAT set holds FreeGenSetNSG (f,D) is free

for D being non empty disjoint_with_NAT set holds FreeGenSetNSG (f,D) is free

proof end;

registration

let f be non empty FinSequence of NAT ;

let D be non empty disjoint_with_NAT set ;

coherence

FreeUnivAlgNSG (f,D) is free

end;
let D be non empty disjoint_with_NAT set ;

coherence

FreeUnivAlgNSG (f,D) is free

proof end;

definition

let f be non empty FinSequence of NAT ;

let D be non empty disjoint_with_NAT set ;

:: original: FreeGenSetNSG

redefine func FreeGenSetNSG (f,D) -> free GeneratorSet of FreeUnivAlgNSG (f,D);

coherence

FreeGenSetNSG (f,D) is free GeneratorSet of FreeUnivAlgNSG (f,D) by Th6;

end;
let D be non empty disjoint_with_NAT set ;

:: original: FreeGenSetNSG

redefine func FreeGenSetNSG (f,D) -> free GeneratorSet of FreeUnivAlgNSG (f,D);

coherence

FreeGenSetNSG (f,D) is free GeneratorSet of FreeUnivAlgNSG (f,D) by Th6;

::

:: Construction of Free Universal Algebra for Given Signature

:: (with at Last One Zero Argument Operation) and Set of Generators

::

:: Construction of Free Universal Algebra for Given Signature

:: (with at Last One Zero Argument Operation) and Set of Generators

::

definition

let f be non empty with_zero FinSequence of NAT ;

let D be disjoint_with_NAT set ;

let n be Nat;

assume A1: n in dom f ;

ex b_{1} being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st

( dom b_{1} = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b_{1} holds

b_{1} . p = (Sym (n,f,D)) -tree p ) )

for b_{1}, b_{2} being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) st dom b_{1} = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b_{1} holds

b_{1} . p = (Sym (n,f,D)) -tree p ) & dom b_{2} = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b_{2} holds

b_{2} . p = (Sym (n,f,D)) -tree p ) holds

b_{1} = b_{2}

end;
let D be disjoint_with_NAT set ;

let n be Nat;

assume A1: n in dom f ;

func FreeOpZAO (n,f,D) -> non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) means :Def16: :: FREEALG:def 16

( dom it = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom it holds

it . p = (Sym (n,f,D)) -tree p ) );

existence ( dom it = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom it holds

it . p = (Sym (n,f,D)) -tree p ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def16 defines FreeOpZAO FREEALG:def 16 :

for f being non empty with_zero FinSequence of NAT

for D being disjoint_with_NAT set

for n being Nat st n in dom f holds

for b_{4} being non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) holds

( b_{4} = FreeOpZAO (n,f,D) iff ( dom b_{4} = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom b_{4} holds

b_{4} . p = (Sym (n,f,D)) -tree p ) ) );

for f being non empty with_zero FinSequence of NAT

for D being disjoint_with_NAT set

for n being Nat st n in dom f holds

for b

( b

b

definition

let f be non empty with_zero FinSequence of NAT ;

let D be disjoint_with_NAT set ;

ex b_{1} being PFuncFinSequence of (TS (DTConUA (f,D))) st

( len b_{1} = len f & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = FreeOpZAO (n,f,D) ) )

for b_{1}, b_{2} being PFuncFinSequence of (TS (DTConUA (f,D))) st len b_{1} = len f & ( for n being Nat st n in dom b_{1} holds

b_{1} . n = FreeOpZAO (n,f,D) ) & len b_{2} = len f & ( for n being Nat st n in dom b_{2} holds

b_{2} . n = FreeOpZAO (n,f,D) ) holds

b_{1} = b_{2}

end;
let D be disjoint_with_NAT set ;

func FreeOpSeqZAO (f,D) -> PFuncFinSequence of (TS (DTConUA (f,D))) means :Def17: :: FREEALG:def 17

( len it = len f & ( for n being Nat st n in dom it holds

it . n = FreeOpZAO (n,f,D) ) );

existence ( len it = len f & ( for n being Nat st n in dom it holds

it . n = FreeOpZAO (n,f,D) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def17 defines FreeOpSeqZAO FREEALG:def 17 :

for f being non empty with_zero FinSequence of NAT

for D being disjoint_with_NAT set

for b_{3} being PFuncFinSequence of (TS (DTConUA (f,D))) holds

( b_{3} = FreeOpSeqZAO (f,D) iff ( len b_{3} = len f & ( for n being Nat st n in dom b_{3} holds

b_{3} . n = FreeOpZAO (n,f,D) ) ) );

for f being non empty with_zero FinSequence of NAT

for D being disjoint_with_NAT set

for b

( b

b

definition

let f be non empty with_zero FinSequence of NAT ;

let D be disjoint_with_NAT set ;

UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) is strict Universal_Algebra

end;
let D be disjoint_with_NAT set ;

func FreeUnivAlgZAO (f,D) -> strict Universal_Algebra equals :: FREEALG:def 18

UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #);

coherence UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #);

UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #) is strict Universal_Algebra

proof end;

:: deftheorem defines FreeUnivAlgZAO FREEALG:def 18 :

for f being non empty with_zero FinSequence of NAT

for D being disjoint_with_NAT set holds FreeUnivAlgZAO (f,D) = UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #);

for f being non empty with_zero FinSequence of NAT

for D being disjoint_with_NAT set holds FreeUnivAlgZAO (f,D) = UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #);

theorem Th7: :: FREEALG:7

for f being non empty with_zero FinSequence of NAT

for D being disjoint_with_NAT set holds signature (FreeUnivAlgZAO (f,D)) = f

for D being disjoint_with_NAT set holds signature (FreeUnivAlgZAO (f,D)) = f

proof end;

theorem Th8: :: FREEALG:8

for f being non empty with_zero FinSequence of NAT

for D being disjoint_with_NAT set holds FreeUnivAlgZAO (f,D) is with_const_op

for D being disjoint_with_NAT set holds FreeUnivAlgZAO (f,D) is with_const_op

proof end;

theorem Th9: :: FREEALG:9

for f being non empty with_zero FinSequence of NAT

for D being disjoint_with_NAT set holds Constants (FreeUnivAlgZAO (f,D)) <> {}

for D being disjoint_with_NAT set holds Constants (FreeUnivAlgZAO (f,D)) <> {}

proof end;

definition

let f be non empty with_zero FinSequence of NAT ;

let D be disjoint_with_NAT set ;

{ (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } is Subset of (FreeUnivAlgZAO (f,D))

end;
let D be disjoint_with_NAT set ;

func FreeGenSetZAO (f,D) -> Subset of (FreeUnivAlgZAO (f,D)) equals :: FREEALG:def 19

{ (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } ;

coherence { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } ;

{ (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } is Subset of (FreeUnivAlgZAO (f,D))

proof end;

:: deftheorem defines FreeGenSetZAO FREEALG:def 19 :

for f being non empty with_zero FinSequence of NAT

for D being disjoint_with_NAT set holds FreeGenSetZAO (f,D) = { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } ;

for f being non empty with_zero FinSequence of NAT

for D being disjoint_with_NAT set holds FreeGenSetZAO (f,D) = { (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } ;

definition

let f be non empty with_zero FinSequence of NAT ;

let D be disjoint_with_NAT set ;

:: original: FreeGenSetZAO

redefine func FreeGenSetZAO (f,D) -> GeneratorSet of FreeUnivAlgZAO (f,D);

coherence

FreeGenSetZAO (f,D) is GeneratorSet of FreeUnivAlgZAO (f,D)

end;
let D be disjoint_with_NAT set ;

:: original: FreeGenSetZAO

redefine func FreeGenSetZAO (f,D) -> GeneratorSet of FreeUnivAlgZAO (f,D);

coherence

FreeGenSetZAO (f,D) is GeneratorSet of FreeUnivAlgZAO (f,D)

proof end;

definition

let f be non empty with_zero FinSequence of NAT ;

let D be disjoint_with_NAT set ;

let C be non empty set ;

let s be Symbol of (DTConUA (f,D));

let F be Function of (FreeGenSetZAO (f,D)),C;

assume A1: s in Terminals (DTConUA (f,D)) ;

coherence

F . (root-tree s) is Element of C

end;
let D be disjoint_with_NAT set ;

let C be non empty set ;

let s be Symbol of (DTConUA (f,D));

let F be Function of (FreeGenSetZAO (f,D)),C;

assume A1: s in Terminals (DTConUA (f,D)) ;

coherence

F . (root-tree s) is Element of C

proof end;

:: deftheorem Def20 defines pi FREEALG:def 20 :

for f being non empty with_zero FinSequence of NAT

for D being disjoint_with_NAT set

for C being non empty set

for s being Symbol of (DTConUA (f,D))

for F being Function of (FreeGenSetZAO (f,D)),C st s in Terminals (DTConUA (f,D)) holds

pi (F,s) = F . (root-tree s);

for f being non empty with_zero FinSequence of NAT

for D being disjoint_with_NAT set

for C being non empty set

for s being Symbol of (DTConUA (f,D))

for F being Function of (FreeGenSetZAO (f,D)),C st s in Terminals (DTConUA (f,D)) holds

pi (F,s) = F . (root-tree s);

theorem Th10: :: FREEALG:10

for f being non empty with_zero FinSequence of NAT

for D being disjoint_with_NAT set holds FreeGenSetZAO (f,D) is free

for D being disjoint_with_NAT set holds FreeGenSetZAO (f,D) is free

proof end;

registration

let f be non empty with_zero FinSequence of NAT ;

let D be disjoint_with_NAT set ;

coherence

FreeUnivAlgZAO (f,D) is free

end;
let D be disjoint_with_NAT set ;

coherence

FreeUnivAlgZAO (f,D) is free

proof end;

definition

let f be non empty with_zero FinSequence of NAT ;

let D be disjoint_with_NAT set ;

:: original: FreeGenSetZAO

redefine func FreeGenSetZAO (f,D) -> free GeneratorSet of FreeUnivAlgZAO (f,D);

coherence

FreeGenSetZAO (f,D) is free GeneratorSet of FreeUnivAlgZAO (f,D) by Th10;

end;
let D be disjoint_with_NAT set ;

:: original: FreeGenSetZAO

redefine func FreeGenSetZAO (f,D) -> free GeneratorSet of FreeUnivAlgZAO (f,D);

coherence

FreeGenSetZAO (f,D) is free GeneratorSet of FreeUnivAlgZAO (f,D) by Th10;

registration

existence

ex b_{1} being Universal_Algebra st

( b_{1} is strict & b_{1} is free & b_{1} is with_const_op )

end;
ex b

( b

proof end;

:: Free Universal Algebra - General Notions

::