:: Free Magmas
:: by Marco Riccardi
::
:: Received October 20, 2009
:: Copyright (c) 2009 Association of Mizar Users

begin

registration

let X be set ;
let f be Function of NAT ,X;
let n be natural number ;
cluster f | n -> T-Sequence-like ;
correctness
coherence
f | n is T-Sequence-like ;

proof end;

end;

definition

let X, x be set ;
func IFXFinSequence x,X -> XFinSequence of X equals :Def2: :: ALGSTR_4:def 1
x if x is XFinSequence of X
otherwise <%> X;
correctness
coherence
( ( x is XFinSequence of X implies x is XFinSequence of X ) & ( x is not XFinSequence of X implies <%> X is XFinSequence of X ) );
consistency
for b₁ being XFinSequence of X holds verum;
;

end;

:: deftheorem Def2 defines IFXFinSequence ALGSTR_4:def 1 :

for X, x being set holds
( ( x is XFinSequence of X implies IFXFinSequence x,X = x ) & ( x is not XFinSequence of X implies IFXFinSequence x,X = <%> X ) );

definition

let X be non empty set ;
let f be Function of (X ^omega ),X;
let c be XFinSequence of X;
:: original: .
redefine func f . c -> Element of X;
correctness
coherence
f . c is Element of X;

proof end;

end;

theorem Th1: :: ALGSTR_4:1

for X, Y, Z being set st Y c= the_universe_of X & Z c= the_universe_of X holds
[:Y,Z:] c= the_universe_of X

proof end;

scheme :: ALGSTR_4:sch 1
FuncRecursiveUniq{ F₁( set ) -> set , F₂() -> Function, F₃() -> Function } :

F₂() = F₃()

provided

A1: ( dom F₂() = NAT & ( for n being natural number holds F₂() . n = F₁((F₂() | n)) ) ) and
A2: ( dom F₃() = NAT & ( for n being natural number holds F₃() . n = F₁((F₃() | n)) ) )

proof end;

scheme :: ALGSTR_4:sch 2
FuncRecursiveExist{ F₁( set ) -> set } :

ex f being Function st
( dom f = NAT & ( for n being natural number holds f . n = F₁((f | n)) ) )

proof end;

scheme :: ALGSTR_4:sch 3
FuncRecursiveUniqu2{ F₁() -> non empty set , F₂( XFinSequence of F₁()) -> Element of F₁(), F₃() -> Function of NAT ,F₁(), F₄() -> Function of NAT ,F₁() } :

F₃() = F₄()

provided

A1: for n being natural number holds F₃() . n = F₂((F₃() | n)) and
A2: for n being natural number holds F₄() . n = F₂((F₄() | n))

proof end;

scheme :: ALGSTR_4:sch 4
FuncRecursiveExist2{ F₁() -> non empty set , F₂( XFinSequence of F₁()) -> Element of F₁() } :

ex f being Function of NAT ,F₁() st
for n being natural number holds f . n = F₂((f | n))

proof end;

definition

let f, g be Function;
pred f extends g means :Def3: :: ALGSTR_4:def 2
( dom g c= dom f & f tolerates g );

end;

:: deftheorem Def3 defines extends ALGSTR_4:def 2 :

for f, g being Function holds
( f extends g iff ( dom g c= dom f & f tolerates g ) );

registration

cluster empty multMagma ;
existence
ex b₁ being multMagma st b₁ is empty

proof end;

end;

begin

definition

let M be multMagma ;
let R be Equivalence_Relation of M;
attr R is compatible means :Def4: :: ALGSTR_4:def 3
for v, v', w, w' being Element of M st v in Class R,v' & w in Class R,w' holds
v * w in Class R,(v' * w');

end;

:: deftheorem Def4 defines compatible ALGSTR_4:def 3 :

for M being multMagma
for R being Equivalence_Relation of M holds
( R is compatible iff for v, v', w, w' being Element of M st v in Class R,v' & w in Class R,w' holds
v * w in Class R,(v' * w') );

registration

let M be multMagma ;
cluster nabla the carrier of M -> compatible ;
correctness
coherence
nabla the carrier of M is compatible ;

proof end;

end;

registration

let M be multMagma ;
cluster compatible Element of bool [:the carrier of M,the carrier of M:];
correctness
existence
ex b₁ being Equivalence_Relation of M st b₁ is compatible ;

proof end;

end;

theorem Th2: :: ALGSTR_4:2

for M being multMagma
for R being Equivalence_Relation of M holds
( R is compatible iff for v, v', w, w' being Element of M st Class R,v = Class R,v' & Class R,w = Class R,w' holds
Class R,(v * w) = Class R,(v' * w') )

proof end;

definition

let M be multMagma ;
let R be compatible Equivalence_Relation of M;
func ClassOp R -> BinOp of (Class R) means :Def5: :: ALGSTR_4:def 4
for x, y being Element of Class R
for v, w being Element of M st x = Class R,v & y = Class R,w holds
it . x,y = Class R,(v * w) if not M is empty
otherwise it = {} ;
correctness
consistency
for b₁ being BinOp of (Class R) holds verum;
existence
( ( for b₁ being BinOp of (Class R) holds verum ) & ( not M is empty implies ex b₁ being BinOp of (Class R) st
for x, y being Element of Class R
for v, w being Element of M st x = Class R,v & y = Class R,w holds
b₁ . x,y = Class R,(v * w) ) & ( M is empty implies ex b₁ being BinOp of (Class R) st b₁ = {} ) );
uniqueness
for b₁, b₂ being BinOp of (Class R) holds
( ( not M is empty & ( for x, y being Element of Class R
for v, w being Element of M st x = Class R,v & y = Class R,w holds
b₁ . x,y = Class R,(v * w) ) & ( for x, y being Element of Class R
for v, w being Element of M st x = Class R,v & y = Class R,w holds
b₂ . x,y = Class R,(v * w) ) implies b₁ = b₂ ) & ( M is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) );

proof end;

end;

:: deftheorem Def5 defines ClassOp ALGSTR_4:def 4 :

for M being multMagma
for R being compatible Equivalence_Relation of M
for b₃ being BinOp of (Class R) holds
( ( not M is empty implies ( b₃ = ClassOp R iff for x, y being Element of Class R
for v, w being Element of M st x = Class R,v & y = Class R,w holds
b₃ . x,y = Class R,(v * w) ) ) & ( M is empty implies ( b₃ = ClassOp R iff b₃ = {} ) ) );

definition

let M be multMagma ;
let R be compatible Equivalence_Relation of M;
func M ./. R -> multMagma equals :: ALGSTR_4:def 5
multMagma(# (Class R),(ClassOp R) #);
correctness
coherence
multMagma(# (Class R),(ClassOp R) #) is multMagma ;
;

end;

:: deftheorem defines ./. ALGSTR_4:def 5 :

for M being multMagma
for R being compatible Equivalence_Relation of M holds M ./. R = multMagma(# (Class R),(ClassOp R) #);

registration

let M be multMagma ;
let R be compatible Equivalence_Relation of M;
cluster M ./. R -> strict ;
correctness
coherence
M ./. R is strict ;
;

end;

registration

let M be non empty multMagma ;
let R be compatible Equivalence_Relation of M;
cluster M ./. R -> non empty ;
correctness
coherence
not M ./. R is empty ;
;

end;

definition

let M be non empty multMagma ;
let R be compatible Equivalence_Relation of M;
func nat_hom R -> Function of M,(M ./. R) means :Def7: :: ALGSTR_4:def 6
for v being Element of M holds it . v = Class R,v;
existence
ex b₁ being Function of M,(M ./. R) st
for v being Element of M holds b₁ . v = Class R,v

proof end;

uniqueness
for b₁, b₂ being Function of M,(M ./. R) st ( for v being Element of M holds b₁ . v = Class R,v ) & ( for v being Element of M holds b₂ . v = Class R,v ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines nat_hom ALGSTR_4:def 6 :

for M being non empty multMagma
for R being compatible Equivalence_Relation of M
for b₃ being Function of M,(M ./. R) holds
( b₃ = nat_hom R iff for v being Element of M holds b₃ . v = Class R,v );

registration

let M be non empty multMagma ;
let R be compatible Equivalence_Relation of M;
cluster nat_hom R -> multiplicative ;
correctness
coherence
nat_hom R is multiplicative ;

proof end;

end;

registration

let M be non empty multMagma ;
let R be compatible Equivalence_Relation of M;
cluster nat_hom R -> onto ;
correctness
coherence
nat_hom R is onto ;

proof end;

end;

definition

let M be multMagma ;
mode Relators of M is [:the carrier of M,the carrier of M:] -valued Function;

end;

definition

let M be multMagma ;
let r be Relators of M;
func equ_rel r -> Equivalence_Relation of M equals :: ALGSTR_4:def 7
meet { R where R is compatible Equivalence_Relation of M : for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class R,w } ;
correctness
coherence
meet { R where R is compatible Equivalence_Relation of M : for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class R,w } is Equivalence_Relation of M;

proof end;

end;

:: deftheorem defines equ_rel ALGSTR_4:def 7 :

for M being multMagma
for r being Relators of M holds equ_rel r = meet { R where R is compatible Equivalence_Relation of M : for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class R,w } ;

theorem Th3: :: ALGSTR_4:3

for M being multMagma
for r being Relators of M
for R being compatible Equivalence_Relation of M st ( for i being set
for v, w being Element of M st i in dom r & r . i = [v,w] holds
v in Class R,w ) holds
equ_rel r c= R

proof end;

registration

let M be multMagma ;
let r be Relators of M;
cluster equ_rel r -> compatible ;
coherence
equ_rel r is compatible

proof end;

end;

definition

let X, Y be set ;
let f be Function of X,Y;
func equ_kernel f -> Equivalence_Relation of X means :Def9: :: ALGSTR_4:def 8
for x, y being set holds
( [x,y] in it iff ( x in X & y in X & f . x = f . y ) );
existence
ex b₁ being Equivalence_Relation of X st
for x, y being set holds
( [x,y] in b₁ iff ( x in X & y in X & f . x = f . y ) )

proof end;

uniqueness
for b₁, b₂ being Equivalence_Relation of X st ( for x, y being set holds
( [x,y] in b₁ iff ( x in X & y in X & f . x = f . y ) ) ) & ( for x, y being set holds
( [x,y] in b₂ iff ( x in X & y in X & f . x = f . y ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines equ_kernel ALGSTR_4:def 8 :

for X, Y being set
for f being Function of X,Y
for b₄ being Equivalence_Relation of X holds
( b₄ = equ_kernel f iff for x, y being set holds
( [x,y] in b₄ iff ( x in X & y in X & f . x = f . y ) ) );

theorem Th4: :: ALGSTR_4:4

for M, N being non empty multMagma
for f being Function of M,N st f is multiplicative holds
equ_kernel f is compatible

proof end;

theorem Th5: :: ALGSTR_4:5

for N, M being non empty multMagma
for f being Function of M,N st f is multiplicative holds
ex r being Relators of M st equ_kernel f = equ_rel r

proof end;

begin

definition

let M be multMagma ;
mode multSubmagma of M -> multMagma means :Def10: :: ALGSTR_4:def 9
( the carrier of it c= the carrier of M & the multF of it = the multF of M || the carrier of it );
existence
ex b₁ being multMagma st
( the carrier of b₁ c= the carrier of M & the multF of b₁ = the multF of M || the carrier of b₁ )

proof end;

end;

:: deftheorem Def10 defines multSubmagma ALGSTR_4:def 9 :

for M, b₂ being multMagma holds
( b₂ is multSubmagma of M iff ( the carrier of b₂ c= the carrier of M & the multF of b₂ = the multF of M || the carrier of b₂ ) );

registration

let M be multMagma ;
cluster strict multSubmagma of M;
existence
ex b₁ being multSubmagma of M st b₁ is strict

proof end;

end;

registration

let M be non empty multMagma ;
cluster non empty multSubmagma of M;
existence
not for b₁ being multSubmagma of M holds b₁ is empty

proof end;

end;

theorem Th6: :: ALGSTR_4:6

for M being multMagma
for N, K being multSubmagma of M st N is multSubmagma of K & K is multSubmagma of N holds
multMagma(# the carrier of N,the multF of N #) = multMagma(# the carrier of K,the multF of K #)

proof end;

theorem Th7: :: ALGSTR_4:7

for M being multMagma
for N being multSubmagma of M st the carrier of N = the carrier of M holds
multMagma(# the carrier of N,the multF of N #) = multMagma(# the carrier of M,the multF of M #)

proof end;

definition

let M be multMagma ;
let A be Subset of M;
attr A is stable means :Def11: :: ALGSTR_4:def 10
for v, w being Element of M st v in A & w in A holds
v * w in A;

end;

:: deftheorem Def11 defines stable ALGSTR_4:def 10 :

for M being multMagma
for A being Subset of M holds
( A is stable iff for v, w being Element of M st v in A & w in A holds
v * w in A );

registration

let M be multMagma ;
cluster stable Element of bool the carrier of M;
correctness
existence
ex b₁ being Subset of M st b₁ is stable ;

proof end;

end;

theorem Th8: :: ALGSTR_4:8

for M being multMagma
for N being multSubmagma of M holds the carrier of N is stable Subset of M

proof end;

registration

let M be multMagma ;
let N be multSubmagma of M;
cluster the carrier of N -> stable Subset of M;
correctness
coherence
for b₁ being Subset of M st b₁ = the carrier of N holds
b₁ is stable ;
by Th8;

end;

theorem Th9: :: ALGSTR_4:9

for M being multMagma
for F being Function st ( for i being set st i in dom F holds
F . i is stable Subset of M ) holds
meet F is stable Subset of M

proof end;

theorem :: ALGSTR_4:10

for M being non empty multMagma
for A being Subset of M holds
( A is stable iff A * A c= A )

proof end;

theorem Th11: :: ALGSTR_4:11

for M, N being non empty multMagma
for f being Function of M,N
for X being stable Subset of M st f is multiplicative holds
f .: X is stable Subset of N

proof end;

theorem Th12: :: ALGSTR_4:12

for N, M being non empty multMagma
for f being Function of M,N
for Y being stable Subset of N st f is multiplicative holds
f " Y is stable Subset of M

proof end;

theorem :: ALGSTR_4:13

for N, M being non empty multMagma
for f, g being Function of M,N st f is multiplicative & g is multiplicative holds
{ v where v is Element of M : f . v = g . v } is stable Subset of M

proof end;

definition

let M be multMagma ;
let A be stable Subset of M;
func the_mult_induced_by A -> BinOp of A equals :: ALGSTR_4:def 11
the multF of M || A;
correctness
coherence
the multF of M || A is BinOp of A;

proof end;

end;

:: deftheorem defines the_mult_induced_by ALGSTR_4:def 11 :

for M being multMagma
for A being stable Subset of M holds the_mult_induced_by A = the multF of M || A;

definition

let M be multMagma ;
let A be Subset of M;
func the_submagma_generated_by A -> strict multSubmagma of M means :Def13: :: ALGSTR_4:def 12
( A c= the carrier of it & ( for N being strict multSubmagma of M st A c= the carrier of N holds
it is multSubmagma of N ) );
existence
ex b₁ being strict multSubmagma of M st
( A c= the carrier of b₁ & ( for N being strict multSubmagma of M st A c= the carrier of N holds
b₁ is multSubmagma of N ) )

proof end;

uniqueness
for b₁, b₂ being strict multSubmagma of M st A c= the carrier of b₁ & ( for N being strict multSubmagma of M st A c= the carrier of N holds
b₁ is multSubmagma of N ) & A c= the carrier of b₂ & ( for N being strict multSubmagma of M st A c= the carrier of N holds
b₂ is multSubmagma of N ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines the_submagma_generated_by ALGSTR_4:def 12 :

for M being multMagma
for A being Subset of M
for b₃ being strict multSubmagma of M holds
( b₃ = the_submagma_generated_by A iff ( A c= the carrier of b₃ & ( for N being strict multSubmagma of M st A c= the carrier of N holds
b₃ is multSubmagma of N ) ) );

theorem Th14: :: ALGSTR_4:14

for M being multMagma
for A being Subset of M holds
( A is empty iff the_submagma_generated_by A is empty )

proof end;

registration

let M be multMagma ;
let A be empty Subset of M;
cluster the_submagma_generated_by A -> empty strict ;
correctness
coherence
the_submagma_generated_by A is empty ;
by Th14;

end;

theorem Th15: :: ALGSTR_4:15

for M, N being non empty multMagma
for f being Function of M,N
for X being Subset of M st f is multiplicative holds
f .: the carrier of (the_submagma_generated_by X) = the carrier of (the_submagma_generated_by (f .: X))

proof end;

begin

definition

let X be set ;
defpred S₁[ set , set ] means for fs being XFinSequence of bool (the_universe_of (X \/ NAT )) st $1 = fs holds
( ( dom fs = 0 implies $2 = {} ) & ( dom fs = 1 implies $2 = X ) & ( for n being natural number st n >= 2 & dom fs = n holds
ex fs1 being FinSequence st
( len fs1 = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs1 . p = [:(fs . p),(fs . (n - p)):] ) & $2 = Union (disjoin fs1) ) ) );
A1: for e being set st e in (bool (the_universe_of (X \/ NAT ))) ^omega holds
ex u being set st S₁[e,u]

proof end;

consider F being Function such that
A11: ( dom F = (bool (the_universe_of (X \/ NAT ))) ^omega & ( for e being set st e in (bool (the_universe_of (X \/ NAT ))) ^omega holds
S₁[e,F . e] ) ) from CLASSES1:sch 1(A1);
for e being set st e in (bool (the_universe_of (X \/ NAT ))) ^omega holds
F . e in bool (the_universe_of (X \/ NAT ))

proof end;

then reconsider F = F as Function of ((bool (the_universe_of (X \/ NAT ))) ^omega ),(bool (the_universe_of (X \/ NAT ))) by A11, FUNCT_2:5;
deffunc H₁( XFinSequence of bool (the_universe_of (X \/ NAT ))) -> Element of bool (the_universe_of (X \/ NAT )) = F . $1;
func free_magma_seq X -> Function of NAT ,(bool (the_universe_of (X \/ NAT ))) means :Def14: :: ALGSTR_4:def 13
( it . 0 = {} & it . 1 = X & ( for n being natural number st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(it . p),(it . (n - p)):] ) & it . n = Union (disjoin fs) ) ) );
existence
ex b₁ being Function of NAT ,(bool (the_universe_of (X \/ NAT ))) st
( b₁ . 0 = {} & b₁ . 1 = X & ( for n being natural number st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(b₁ . p),(b₁ . (n - p)):] ) & b₁ . n = Union (disjoin fs) ) ) )

proof end;

uniqueness
for b₁, b₂ being Function of NAT ,(bool (the_universe_of (X \/ NAT ))) st b₁ . 0 = {} & b₁ . 1 = X & ( for n being natural number st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(b₁ . p),(b₁ . (n - p)):] ) & b₁ . n = Union (disjoin fs) ) ) & b₂ . 0 = {} & b₂ . 1 = X & ( for n being natural number st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(b₂ . p),(b₂ . (n - p)):] ) & b₂ . n = Union (disjoin fs) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines free_magma_seq ALGSTR_4:def 13 :

for X being set
for b₂ being Function of NAT ,(bool (the_universe_of (X \/ NAT ))) holds
( b₂ = free_magma_seq X iff ( b₂ . 0 = {} & b₂ . 1 = X & ( for n being natural number st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(b₂ . p),(b₂ . (n - p)):] ) & b₂ . n = Union (disjoin fs) ) ) ) );

definition

let X be set ;
let n be natural number ;
func free_magma X,n -> set equals :: ALGSTR_4:def 14
(free_magma_seq X) . n;
correctness
coherence
(free_magma_seq X) . n is set ;
;

end;

:: deftheorem defines free_magma ALGSTR_4:def 14 :

for X being set
for n being natural number holds free_magma X,n = (free_magma_seq X) . n;

registration

let X be non empty set ;
let n be natural non zero number ;
cluster free_magma X,n -> non empty ;
correctness
coherence
not free_magma X,n is empty ;

proof end;

end;

theorem :: ALGSTR_4:16

for X being set holds free_magma X,0 = {} by Def14;

theorem :: ALGSTR_4:17

for X being set holds free_magma X,1 = X by Def14;

theorem Th18: :: ALGSTR_4:18

for X being set holds free_magma X,2 = [:[:X,X:],{1}:]

proof end;

theorem :: ALGSTR_4:19

for X being set holds free_magma X,3 = [:[:X,[:[:X,X:],{1}:]:],{1}:] \/ [:[:[:[:X,X:],{1}:],X:],{2}:]

proof end;

theorem Th20: :: ALGSTR_4:20

for X being set
for n being natural number st n >= 2 holds
ex fs being FinSequence st
( len fs = n - 1 & ( for p being natural number st p >= 1 & p <= n - 1 holds
fs . p = [:(free_magma X,p),(free_magma X,(n -' p)):] ) & free_magma X,n = Union (disjoin fs) )

proof end;

theorem Th21: :: ALGSTR_4:21

for X, x being set
for n being natural number st n >= 2 & x in free_magma X,n holds
ex p, m being natural number st
( x `2 = p & 1 <= p & p <= n - 1 & (x `1 ) `1 in free_magma X,p & (x `1 ) `2 in free_magma X,m & n = p + m & x in [:[:(free_magma X,p),(free_magma X,m):],{p}:] )

proof end;

theorem Th22: :: ALGSTR_4:22

for X, x, y being set
for n, m being natural number st x in free_magma X,n & y in free_magma X,m holds
[[x,y],n] in free_magma X,(n + m)

proof end;

theorem Th23: :: ALGSTR_4:23

for X, Y being set
for n being natural number st X c= Y holds
free_magma X,n c= free_magma Y,n

proof end;

definition

let X be set ;
func free_magma_carrier X -> set equals :: ALGSTR_4:def 15
Union (disjoin ((free_magma_seq X) | NATPLUS ));
correctness
coherence
Union (disjoin ((free_magma_seq X) | NATPLUS )) is set ;
;

end;

:: deftheorem defines free_magma_carrier ALGSTR_4:def 15 :

for X being set holds free_magma_carrier X = Union (disjoin ((free_magma_seq X) | NATPLUS ));

Lm1: for X being set
for n being natural number st n > 0 holds
[:(free_magma X,n),{n}:] c= free_magma_carrier X

proof end;

theorem Th24: :: ALGSTR_4:24

for X being set holds
( X = {} iff free_magma_carrier X = {} )

proof end;

registration

let X be empty set ;
cluster free_magma_carrier X -> empty ;
correctness
coherence
free_magma_carrier X is empty ;
by Th24;

end;

registration

let X be non empty set ;
cluster free_magma_carrier X -> non empty ;
correctness
coherence
not free_magma_carrier X is empty ;
by Th24;
let w be Element of free_magma_carrier X;
cluster w `2 -> natural non zero number ;
correctness
coherence
for b<sub>1</sub> being number st b<sub>1</sub> = w `2 holds
( not b₁ is empty & b₁ is natural );

proof end;

end;

theorem Th25: :: ALGSTR_4:25

for X being non empty set
for w being Element of free_magma_carrier X holds w in [:(free_magma X,(w `2 )),{(w `2 )}:]

proof end;

theorem Th26: :: ALGSTR_4:26

for X being non empty set
for v, w being Element of free_magma_carrier X holds [[[(v `1 ),(w `1 )],(v `2 )],((v `2 ) + (w `2 ))] is Element of free_magma_carrier X

proof end;

theorem Th27: :: ALGSTR_4:27

for X, Y being set st X c= Y holds
free_magma_carrier X c= free_magma_carrier Y

proof end;

theorem :: ALGSTR_4:28

for X being set
for n being natural number st n > 0 holds
[:(free_magma X,n),{n}:] c= free_magma_carrier X by Lm1;

definition

let X be set ;
func free_magma_mult X -> BinOp of (free_magma_carrier X) means :Def17: :: ALGSTR_4:def 16
for v, w being Element of free_magma_carrier X
for n, m being natural number st n = v `2 & m = w `2 holds
it . v,w = [[[(v `1 ),(w `1 )],(v `2 )],(n + m)] if not X is empty
otherwise it = {} ;
correctness
consistency
for b<sub>1</sub> being BinOp of (free_magma_carrier X) holds verum;
existence
( ( for b<sub>1</sub> being BinOp of (free_magma_carrier X) holds verum ) & ( not X is empty implies ex b<sub>1</sub> being BinOp of (free_magma_carrier X) st
for v, w being Element of free_magma_carrier X
for n, m being natural number st n = v `2 & m = w `2 holds
b<sub>1</sub> . v,w = [[[(v `1 ),(w `1 )],(v `2 )],(n + m)] ) & ( X is empty implies ex b₁ being BinOp of (free_magma_carrier X) st b₁ = {} ) );
uniqueness
for b₁, b₂ being BinOp of (free_magma_carrier X) holds
( ( not X is empty & ( for v, w being Element of free_magma_carrier X
for n, m being natural number st n = v `2 & m = w `2 holds
b₁ . v,w = [[[(v `1 ),(w `1 )],(v `2 )],(n + m)] ) & ( for v, w being Element of free_magma_carrier X
for n, m being natural number st n = v `2 & m = w `2 holds
b<sub>2</sub> . v,w = [[[(v `1 ),(w `1 )],(v `2 )],(n + m)] ) implies b₁ = b₂ ) & ( X is empty & b₁ = {} & b₂ = {} implies b₁ = b₂ ) );

proof end;

end;

:: deftheorem Def17 defines free_magma_mult ALGSTR_4:def 16 :

for X being set
for b₂ being BinOp of (free_magma_carrier X) holds
( ( not X is empty implies ( b₂ = free_magma_mult X iff for v, w being Element of free_magma_carrier X
for n, m being natural number st n = v `2 & m = w `2 holds
b₂ . v,w = [[[(v `1 ),(w `1 )],(v `2 )],(n + m)] ) ) & ( X is empty implies ( b₂ = free_magma_mult X iff b₂ = {} ) ) );

definition

let X be set ;
func free_magma X -> multMagma equals :: ALGSTR_4:def 17
multMagma(# (free_magma_carrier X),(free_magma_mult X) #);
correctness
coherence
multMagma(# (free_magma_carrier X),(free_magma_mult X) #) is multMagma ;
;

end;

:: deftheorem defines free_magma ALGSTR_4:def 17 :

for X being set holds free_magma X = multMagma(# (free_magma_carrier X),(free_magma_mult X) #);

registration

let X be set ;
cluster free_magma X -> strict ;
correctness
coherence
free_magma X is strict ;
;

end;

registration

let X be empty set ;
cluster free_magma X -> empty ;
correctness
coherence
free_magma X is empty ;
;

end;

registration

let X be non empty set ;
cluster free_magma X -> non empty ;
correctness
coherence
not free_magma X is empty ;
;
let w be Element of (free_magma X);
cluster w `2 -> natural non zero number ;
correctness
coherence
for b<sub>1</sub> being number st b<sub>1</sub> = w `2 holds
( not b₁ is empty & b₁ is natural );
;
cluster w `1 -> Element of free_magma X,(w `2 );
correctness
coherence
for b₁ being Element of free_magma X,(w `2 ) st b<sub>1</sub> = w `1 holds
verum;
;

end;

theorem :: ALGSTR_4:29

for X being set
for S being Subset of X holds free_magma S is multSubmagma of free_magma X

proof end;

definition

let X be set ;
let w be Element of (free_magma X);
func length w -> natural number equals :Def19: :: ALGSTR_4:def 18
w `2 if not X is empty
otherwise 0 ;
correctness
coherence
( ( not X is empty implies w `2 is natural number ) & ( X is empty implies 0 is natural number ) );
consistency
for b₁ being natural number holds verum;
;

end;

:: deftheorem Def19 defines length ALGSTR_4:def 18 :

for X being set
for w being Element of (free_magma X) holds
( ( not X is empty implies length w = w `2 ) & ( X is empty implies length w = 0 ) );

theorem Th30: :: ALGSTR_4:30

for X being set holds X = { (w `1 ) where w is Element of (free_magma X) : length w = 1 }

proof end;

theorem Th31: :: ALGSTR_4:31

for X being set
for v, w being Element of (free_magma X) st not X is empty holds
v * w = [[[(v `1 ),(w `1 )],(v `2 )],((length v) + (length w))]

proof end;

theorem Th32: :: ALGSTR_4:32

for X being set
for v being Element of (free_magma X) st not X is empty holds
( v = [(v `1 ),(v `2 )] & length v >= 1 )

proof end;

theorem :: ALGSTR_4:33

for X being set
for v, w being Element of (free_magma X) holds length (v * w) = (length v) + (length w)

proof end;

theorem Th34: :: ALGSTR_4:34

for X being set
for w being Element of (free_magma X) st length w >= 2 holds
ex w1, w2 being Element of (free_magma X) st
( w = w1 * w2 & length w1 < length w & length w2 < length w )

proof end;

theorem :: ALGSTR_4:35

for X being set
for v1, v2, w1, w2 being Element of (free_magma X) st v1 * v2 = w1 * w2 holds
( v1 = w1 & v2 = w2 )

proof end;

definition

let X be set ;
let n be natural number ;
func canon_image X,n -> Function of (free_magma X,n),(free_magma X) means :Def20: :: ALGSTR_4:def 19
for x being set st x in dom it holds
it . x = [x,n] if n > 0
otherwise it = {} ;
correctness
consistency
for b₁ being Function of (free_magma X,n),(free_magma X) holds verum;
existence
( ( for b₁ being Function of (free_magma X,n),(free_magma X) holds verum ) & ( n > 0 implies ex b₁ being Function of (free_magma X,n),(free_magma X) st
for x being set st x in dom b₁ holds
b₁ . x = [x,n] ) & ( not n > 0 implies ex b₁ being Function of (free_magma X,n),(free_magma X) st b₁ = {} ) );
uniqueness
for b₁, b₂ being Function of (free_magma X,n),(free_magma X) holds
( ( n > 0 & ( for x being set st x in dom b₁ holds
b₁ . x = [x,n] ) & ( for x being set st x in dom b₂ holds
b₂ . x = [x,n] ) implies b₁ = b₂ ) & ( not n > 0 & b₁ = {} & b₂ = {} implies b₁ = b₂ ) );

proof end;

end;

:: deftheorem Def20 defines canon_image ALGSTR_4:def 19 :

for X being set
for n being natural number
for b₃ being Function of (free_magma X,n),(free_magma X) holds
( ( n > 0 implies ( b₃ = canon_image X,n iff for x being set st x in dom b₃ holds
b₃ . x = [x,n] ) ) & ( not n > 0 implies ( b₃ = canon_image X,n iff b₃ = {} ) ) );

Th36: for X being set
for n being natural number holds canon_image X,n is one-to-one

proof end;

registration

let X be set ;
let n be natural number ;
cluster canon_image X,n -> one-to-one ;
correctness
coherence
canon_image X,n is one-to-one ;
by Th36;

end;

registration

let X be non empty set ;
cluster canon_image X,1 -> Function of X,(free_magma X);
correctness
coherence
for b₁ being Function of X,(free_magma X) st b₁ = canon_image X,1 holds
verum;
;

end;

Lm2: for X being non empty set holds
( dom (canon_image X,1) = X & ( for x being set st x in X holds
(canon_image X,1) . x = [x,1] ) )

proof end;

theorem Th37: :: ALGSTR_4:36

for X being non empty set
for A being Subset of (free_magma X) st A = (canon_image X,1) .: X holds
free_magma X = the_submagma_generated_by A

proof end;

theorem :: ALGSTR_4:37

for X being non empty set
for R being compatible Equivalence_Relation of (free_magma X) holds (free_magma X) ./. R = the_submagma_generated_by ((nat_hom R) .: ((canon_image X,1) .: X))

proof end;

theorem Th39: :: ALGSTR_4:38

for X, Y being non empty set
for f being Function of X,Y holds (canon_image Y,1) * f is Function of X,(free_magma Y)

proof end;

definition

let X be non empty set ;
let M be non empty multMagma ;
let n, m be natural non zero number ;
let f be Function of (free_magma X,n),M;
let g be Function of (free_magma X,m),M;
func [:f,g:] -> Function of [:[:(free_magma X,n),(free_magma X,m):],{n}:],M means :Def21: :: ALGSTR_4:def 20
for x being Element of [:[:(free_magma X,n),(free_magma X,m):],{n}:]
for y being Element of free_magma X,n
for z being Element of free_magma X,m st y = (x `1 ) `1 & z = (x `1 ) `2 holds
it . x = (f . y) * (g . z);
existence
ex b₁ being Function of [:[:(free_magma X,n),(free_magma X,m):],{n}:],M st
for x being Element of [:[:(free_magma X,n),(free_magma X,m):],{n}:]
for y being Element of free_magma X,n
for z being Element of free_magma X,m st y = (x `1 ) `1 & z = (x `1 ) `2 holds
b₁ . x = (f . y) * (g . z)

proof end;

uniqueness
for b₁, b₂ being Function of [:[:(free_magma X,n),(free_magma X,m):],{n}:],M st ( for x being Element of [:[:(free_magma X,n),(free_magma X,m):],{n}:]
for y being Element of free_magma X,n
for z being Element of free_magma X,m st y = (x `1 ) `1 & z = (x `1 ) `2 holds
b₁ . x = (f . y) * (g . z) ) & ( for x being Element of [:[:(free_magma X,n),(free_magma X,m):],{n}:]
for y being Element of free_magma X,n
for z being Element of free_magma X,m st y = (x `1 ) `1 & z = (x `1 ) `2 holds
b₂ . x = (f . y) * (g . z) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def21 defines [: ALGSTR_4:def 20 :

for X being non empty set
for M being non empty multMagma
for n, m being natural non zero number
for f being Function of (free_magma X,n),M
for g being Function of (free_magma X,m),M
for b₇ being Function of [:[:(free_magma X,n),(free_magma X,m):],{n}:],M holds
( b₇ = [:f,g:] iff for x being Element of [:[:(free_magma X,n),(free_magma X,m):],{n}:]
for y being Element of free_magma X,n
for z being Element of free_magma X,m st y = (x `1 ) `1 & z = (x `1 ) `2 holds
b₇ . x = (f . y) * (g . z) );

theorem Th40: :: ALGSTR_4:39

for X being non empty set
for M being non empty multMagma
for f being Function of X,M ex h being Function of (free_magma X),M st
( h is multiplicative & h extends f * ((canon_image X,1) " ) )

proof end;

theorem Th41: :: ALGSTR_4:40

for X being non empty set
for M being non empty multMagma
for f being Function of X,M
for h, g being Function of (free_magma X),M st h is multiplicative & h extends f * ((canon_image X,1) " ) & g is multiplicative & g extends f * ((canon_image X,1) " ) holds
h = g

proof end;

theorem Th42: :: ALGSTR_4:41

for N, M being non empty multMagma
for f being Function of M,N
for H being non empty multSubmagma of N
for R being compatible Equivalence_Relation of M st f is multiplicative & the carrier of H = rng f & R = equ_kernel f holds
ex g being Function of (M ./. R),H st
( f = g * (nat_hom R) & g is bijective & g is multiplicative )

proof end;

theorem :: ALGSTR_4:42

for M, N being non empty multMagma
for R being compatible Equivalence_Relation of M
for g1, g2 being Function of (M ./. R),N st g1 * (nat_hom R) = g2 * (nat_hom R) holds
g1 = g2

proof end;

theorem :: ALGSTR_4:43

for M being non empty multMagma ex X being non empty set ex r being Relators of (free_magma X) ex g being Function of ((free_magma X) ./. (equ_rel r)),M st
( g is bijective & g is multiplicative )

proof end;

definition

let X, Y be non empty set ;
let f be Function of X,Y;
func free_magmaF f -> Function of (free_magma X),(free_magma Y) means :Def22: :: ALGSTR_4:def 21
( it is multiplicative & it extends ((canon_image Y,1) * f) * ((canon_image X,1) " ) );
existence
ex b₁ being Function of (free_magma X),(free_magma Y) st
( b₁ is multiplicative & b₁ extends ((canon_image Y,1) * f) * ((canon_image X,1) " ) )

proof end;

uniqueness
for b₁, b₂ being Function of (free_magma X),(free_magma Y) st b₁ is multiplicative & b₁ extends ((canon_image Y,1) * f) * ((canon_image X,1) " ) & b₂ is multiplicative & b₂ extends ((canon_image Y,1) * f) * ((canon_image X,1) " ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def22 defines free_magmaF ALGSTR_4:def 21 :

for X, Y being non empty set
for f being Function of X,Y
for b₄ being Function of (free_magma X),(free_magma Y) holds
( b₄ = free_magmaF f iff ( b₄ is multiplicative & b₄ extends ((canon_image Y,1) * f) * ((canon_image X,1) " ) ) );

registration

let X, Y be non empty set ;
let f be Function of X,Y;
cluster free_magmaF f -> multiplicative ;
coherence
free_magmaF f is multiplicative by Def22;

end;

theorem Th45: :: ALGSTR_4:44

for X, Y, Z being non empty set
for f being Function of X,Y
for g being Function of Y,Z holds free_magmaF (g * f) = (free_magmaF g) * (free_magmaF f)

proof end;

theorem Th46: :: ALGSTR_4:45

for X, Z, Y being non empty set
for f being Function of X,Y
for g being Function of X,Z st Y c= Z & f = g holds
free_magmaF f = free_magmaF g

proof end;

theorem Th47: :: ALGSTR_4:46

for Y, X being non empty set
for f being Function of X,Y holds free_magmaF (id X) = id (dom (free_magmaF f))

proof end;

theorem :: ALGSTR_4:47

for X, Y being non empty set
for f being Function of X,Y st f is one-to-one holds
free_magmaF f is one-to-one

proof end;

theorem :: ALGSTR_4:48

for X, Y being non empty set
for f being Function of X,Y st f is onto holds
free_magmaF f is onto

proof end;