begin
:: deftheorem Def2 defines IFXFinSequence ALGSTR_4:def 1 :
theorem Th1:
:: deftheorem Def3 defines extends ALGSTR_4:def 2 :
begin
:: deftheorem Def4 defines compatible ALGSTR_4:def 3 :
theorem Th2:
definition
let M be
multMagma ;
let R be
compatible Equivalence_Relation of
M;
func ClassOp R -> BinOp of
(Class R) means :
Def5:
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 b1 being BinOp of (Class R) holds verum;
existence
( ( for b1 being BinOp of (Class R) holds verum ) & ( not M is empty implies ex b1 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
b1 . x,y = Class R,(v * w) ) & ( M is empty implies ex b1 being BinOp of (Class R) st b1 = {} ) );
uniqueness
for b1, b2 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
b1 . 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
b2 . x,y = Class R,(v * w) ) implies b1 = b2 ) & ( M is empty & b1 = {} & b2 = {} implies b1 = b2 ) );
end;
:: deftheorem Def5 defines ClassOp ALGSTR_4:def 4 :
:: deftheorem defines ./. ALGSTR_4:def 5 :
:: deftheorem Def7 defines nat_hom ALGSTR_4:def 6 :
:: deftheorem defines equ_rel ALGSTR_4:def 7 :
theorem Th3:
definition
let X,
Y be
set ;
let f be
Function of
X,
Y;
func equ_kernel f -> Equivalence_Relation of
X means :
Def9:
for
x,
y being
set holds
(
[x,y] in it iff (
x in X &
y in X &
f . x = f . y ) );
existence
ex b1 being Equivalence_Relation of X st
for x, y being set holds
( [x,y] in b1 iff ( x in X & y in X & f . x = f . y ) )
uniqueness
for b1, b2 being Equivalence_Relation of X st ( for x, y being set holds
( [x,y] in b1 iff ( x in X & y in X & f . x = f . y ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in X & y in X & f . x = f . y ) ) ) holds
b1 = b2
end;
:: deftheorem Def9 defines equ_kernel ALGSTR_4:def 8 :
theorem Th4:
theorem Th5:
begin
:: deftheorem Def10 defines multSubmagma ALGSTR_4:def 9 :
theorem Th6:
theorem Th7:
:: deftheorem Def11 defines stable ALGSTR_4:def 10 :
theorem Th8:
theorem Th9:
theorem
theorem Th11:
theorem Th12:
theorem
:: deftheorem defines the_mult_induced_by ALGSTR_4:def 11 :
:: deftheorem Def13 defines the_submagma_generated_by ALGSTR_4:def 12 :
theorem Th14:
theorem Th15:
begin
definition
let X be
set ;
defpred S1[
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
S1[
e,
u]
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
S1[
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 ))
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 H1(
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:
(
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 b1 being Function of NAT ,(bool (the_universe_of (X \/ NAT ))) st
( b1 . 0 = {} & b1 . 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 = [:(b1 . p),(b1 . (n - p)):] ) & b1 . n = Union (disjoin fs) ) ) )
uniqueness
for b1, b2 being Function of NAT ,(bool (the_universe_of (X \/ NAT ))) st b1 . 0 = {} & b1 . 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 = [:(b1 . p),(b1 . (n - p)):] ) & b1 . n = Union (disjoin fs) ) ) & b2 . 0 = {} & b2 . 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 = [:(b2 . p),(b2 . (n - p)):] ) & b2 . n = Union (disjoin fs) ) ) holds
b1 = b2
end;
:: deftheorem Def14 defines free_magma_seq ALGSTR_4:def 13 :
:: deftheorem defines free_magma ALGSTR_4:def 14 :
theorem
theorem
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
:: deftheorem defines free_magma_carrier ALGSTR_4:def 15 :
Lm1:
for X being set
for n being natural number st n > 0 holds
[:(free_magma X,n),{n}:] c= free_magma_carrier X
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem
definition
let X be
set ;
func free_magma_mult X -> BinOp of
(free_magma_carrier X) means :
Def17:
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 b1 being BinOp of (free_magma_carrier X) holds verum;
existence
( ( for b1 being BinOp of (free_magma_carrier X) holds verum ) & ( not X is empty implies ex b1 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
b1 . v,w = [[[(v `1 ),(w `1 )],(v `2 )],(n + m)] ) & ( X is empty implies ex b1 being BinOp of (free_magma_carrier X) st b1 = {} ) );
uniqueness
for b1, b2 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
b1 . 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
b2 . v,w = [[[(v `1 ),(w `1 )],(v `2 )],(n + m)] ) implies b1 = b2 ) & ( X is empty & b1 = {} & b2 = {} implies b1 = b2 ) );
end;
:: deftheorem Def17 defines free_magma_mult ALGSTR_4:def 16 :
:: deftheorem defines free_magma ALGSTR_4:def 17 :
theorem
:: deftheorem Def19 defines length ALGSTR_4:def 18 :
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem Th34:
theorem
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:
for
x being
set st
x in dom it holds
it . x = [x,n] if n > 0 otherwise it = {} ;
correctness
consistency
for b1 being Function of (free_magma X,n),(free_magma X) holds verum;
existence
( ( for b1 being Function of (free_magma X,n),(free_magma X) holds verum ) & ( n > 0 implies ex b1 being Function of (free_magma X,n),(free_magma X) st
for x being set st x in dom b1 holds
b1 . x = [x,n] ) & ( not n > 0 implies ex b1 being Function of (free_magma X,n),(free_magma X) st b1 = {} ) );
uniqueness
for b1, b2 being Function of (free_magma X,n),(free_magma X) holds
( ( n > 0 & ( for x being set st x in dom b1 holds
b1 . x = [x,n] ) & ( for x being set st x in dom b2 holds
b2 . x = [x,n] ) implies b1 = b2 ) & ( not n > 0 & b1 = {} & b2 = {} implies b1 = b2 ) );
end;
:: deftheorem Def20 defines canon_image ALGSTR_4:def 19 :
Th36:
for X being set
for n being natural number holds canon_image X,n is one-to-one
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] ) )
theorem Th37:
theorem
theorem Th39:
definition
let X be non
empty set ;
let M be non
empty multMagma ;
let n,
m be non
zero natural 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:
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 b1 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
b1 . x = (f . y) * (g . z)
uniqueness
for b1, b2 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
b1 . 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
b2 . x = (f . y) * (g . z) ) holds
b1 = b2
end;
:: deftheorem Def21 defines [: ALGSTR_4:def 20 :
for
X being non
empty set for
M being non
empty multMagma for
n,
m being non
zero natural number for
f being
Function of
(free_magma X,n),
M for
g being
Function of
(free_magma X,m),
M for
b7 being
Function of
[:[:(free_magma X,n),(free_magma X,m):],{n}:],
M holds
(
b7 = [: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
b7 . x = (f . y) * (g . z) );
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem
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:
(
it is
multiplicative &
it extends ((canon_image Y,1) * f) * ((canon_image X,1) " ) );
existence
ex b1 being Function of (free_magma X),(free_magma Y) st
( b1 is multiplicative & b1 extends ((canon_image Y,1) * f) * ((canon_image X,1) " ) )
uniqueness
for b1, b2 being Function of (free_magma X),(free_magma Y) st b1 is multiplicative & b1 extends ((canon_image Y,1) * f) * ((canon_image X,1) " ) & b2 is multiplicative & b2 extends ((canon_image Y,1) * f) * ((canon_image X,1) " ) holds
b1 = b2
end;
:: deftheorem Def22 defines free_magmaF ALGSTR_4:def 21 :
theorem Th45:
theorem Th46:
theorem Th47:
theorem
theorem