deffunc H1( Element of S) -> Subset of (the Sorts of (FreeOSA X) . $1) = OSFreeGen $1,X;
set FM = FreeOSA X;
set D = DTConOSA X;
set PTA = ParsedTermsOSA X;
set SO = the Sorts of (FreeOSA X);
set NH = OSNat_Hom (ParsedTermsOSA X),(LCongruence X);
reconsider NH1 = OSNat_Hom (ParsedTermsOSA X),(LCongruence X) as ManySortedFunction of (ParsedTermsOSA X),(FreeOSA X) ;
A1:
NH1 is order-sorted
by OSALG_4:16;
reconsider SOS = the Sorts of (FreeOSA X) as OrderSortedSet of S ;
consider f being Function such that
A2:
( dom f = the carrier of S & ( for s being Element of S holds f . s = H1(s) ) )
from FUNCT_1:sch 4();
reconsider f = f as ManySortedSet of the carrier of S by A2, PARTFUN1:def 4, RELAT_1:def 18;
A3:
f c= the Sorts of (FreeOSA X)
then reconsider f = f as MSSubset of (FreeOSA X) by PBOOLE:def 23;
OSCl f c= SOS
by A3, OSALG_2:13;
then
OSCl f is ManySortedSubset of the Sorts of (FreeOSA X)
by PBOOLE:def 23;
then reconsider O = OSCl f as OSSubset of FreeOSA X by OSALG_2:def 2;
O is OSSubset of GenOSAlg O
by OSALG_2:def 13;
then A4:
O c= the Sorts of (GenOSAlg O)
by PBOOLE:def 23;
f c= O
by OSALG_2:12;
then A5:
f c= the Sorts of (GenOSAlg O)
by A4, PBOOLE:15;
A6:
NH1 is_epimorphism ParsedTermsOSA X, FreeOSA X
by OSALG_4:16;
then A7:
NH1 is "onto"
by MSUALG_3:def 10;
A8:
NH1 is_homomorphism ParsedTermsOSA X, FreeOSA X
by A6, MSUALG_3:def 10;
A9:
the Sorts of (GenOSAlg O) = the Sorts of (FreeOSA X)
proof
defpred S1[
set ]
means for
s1 being
Element of
S st $1
in dom (NH1 . s1) holds
(NH1 . s1) . $1
in the
Sorts of
(GenOSAlg O) . s1;
reconsider O2 = the
Sorts of
(GenOSAlg O) as
OrderSortedSet of
S by OSALG_1:17;
the
Sorts of
(GenOSAlg O) is
MSSubset of
(FreeOSA X)
by MSUALG_2:def 10;
hence
the
Sorts of
(GenOSAlg O) c= the
Sorts of
(FreeOSA X)
by PBOOLE:def 23;
PBOOLE:def 13 the Sorts of (FreeOSA X) c= the Sorts of (GenOSAlg O)
A10:
for
nt being
Symbol of
(DTConOSA X) for
ts being
FinSequence of
TS (DTConOSA X) st
nt ==> roots ts & ( for
t being
DecoratedTree of the
carrier of
(DTConOSA X) st
t in rng ts holds
S1[
t] ) holds
S1[
nt -tree ts]
proof
set G =
GenOSAlg O;
set OU =
[:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X));
let nt be
Symbol of
(DTConOSA X);
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S1[t] ) holds
S1[nt -tree ts]let ts be
FinSequence of
TS (DTConOSA X);
( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S1[t] ) implies S1[nt -tree ts] )
assume that A11:
nt ==> roots ts
and A12:
for
t being
DecoratedTree of the
carrier of
(DTConOSA X) st
t in rng ts holds
S1[
t]
;
S1[nt -tree ts]
[nt,(roots ts)] in the
Rules of
(DTConOSA X)
by A11, LANG1:def 1;
then reconsider rt =
roots ts as
Element of
([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:106;
reconsider sy =
nt as
Element of
[:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) ;
[sy,rt] in OSREL X
by A11, LANG1:def 1;
then
sy in [:the carrier' of S,{the carrier of S}:]
by Def4;
then consider o being
Element of the
carrier' of
S,
x2 being
Element of
{the carrier of S} such that A13:
sy = [o,x2]
by DOMAIN_1:9;
let s1 be
Element of
S;
( nt -tree ts in dom (NH1 . s1) implies (NH1 . s1) . (nt -tree ts) in the Sorts of (GenOSAlg O) . s1 )
assume
nt -tree ts in dom (NH1 . s1)
;
(NH1 . s1) . (nt -tree ts) in the Sorts of (GenOSAlg O) . s1
then
nt -tree ts in the
Sorts of
(ParsedTermsOSA X) . s1
;
then
nt -tree ts in ParsedTerms X,
s1
by Def8;
then consider a1 being
Element of
TS (DTConOSA X) such that A14:
nt -tree ts = a1
and A15:
( ex
s2 being
Element of
S ex
x being
set st
(
s2 <= s1 &
x in X . s2 &
a1 = root-tree [x,s2] ) or ex
o being
OperSymbol of
S st
(
[o,the carrier of S] = a1 . {} &
the_result_sort_of o <= s1 ) )
;
A16:
Seg (len rt) = dom rt
by FINSEQ_1:def 3;
A17:
x2 = the
carrier of
S
by TARSKI:def 1;
for
s2 being
Element of
S for
x being
set holds
( not
s2 <= s1 or not
x in X . s2 or not
a1 = root-tree [x,s2] )
then consider o1 being
OperSymbol of
S such that A19:
[o1,the carrier of S] = a1 . {}
and A20:
the_result_sort_of o1 <= s1
by A15;
set ar =
the_arity_of o;
set rs =
the_result_sort_of o;
A21:
dom (roots ts) = dom ts
by TREES_3:def 18;
[nt,(roots ts)] in OSREL X
by A11, LANG1:def 1;
then A22:
len rt = len (the_arity_of o)
by A13, A17, Th2;
A23:
Seg (len (the_arity_of o)) = dom (the_arity_of o)
by FINSEQ_1:def 3;
reconsider B = the
Sorts of
(GenOSAlg O) as
MSSubset of
(FreeOSA X) by MSUALG_2:def 10;
A24:
dom (B * (the_arity_of o)) = dom (the_arity_of o)
by PARTFUN1:def 4;
set AR = the
Arity of
S;
set RS = the
ResultSort of
S;
set BH =
(B # ) * the
Arity of
S;
set Op = the
carrier' of
S;
the
Arity of
S . o = the_arity_of o
by MSUALG_1:def 6;
then A25:
((B # ) * the Arity of S) . o = product (B * (the_arity_of o))
by MSAFREE:1;
reconsider rs1 =
the_result_sort_of o,
s11 =
s1 as
Element of
S ;
reconsider B1 =
B as
OrderSortedSet of
S by OSALG_1:17;
A26:
the
ResultSort of
S . o = the_result_sort_of o
by MSUALG_1:def 7;
B is
opers_closed
by MSUALG_2:def 10;
then
B is_closed_on o
by MSUALG_2:def 7;
then A27:
rng ((Den o,(FreeOSA X)) | (((B # ) * the Arity of S) . o)) c= (B * the ResultSort of S) . o
by MSUALG_2:def 6;
A28:
OSSym o,
X = [o,the carrier of S]
;
A29:
nt = [o,the carrier of S]
by A13, TARSKI:def 1;
then A30:
ts in (((ParsedTerms X) # ) * the Arity of S) . o
by A11, A28, Th7;
then reconsider ts1 =
ts as
Element of
Args o,
(ParsedTermsOSA X) by MSUALG_1:def 9;
Den o,
(ParsedTermsOSA X) =
(PTOper X) . o
by MSUALG_1:def 11
.=
PTDenOp o,
X
by Def10
;
then A31:
(Den o,(ParsedTermsOSA X)) . ts = nt -tree ts
by A11, A28, A29, Def9;
A32:
dom (the Sorts of (ParsedTermsOSA X) * (the_arity_of o)) = dom (the_arity_of o)
by PARTFUN1:def 4;
A33:
for
x being
set st
x in dom (B * (the_arity_of o)) holds
(NH1 # ts1) . x in (B * (the_arity_of o)) . x
proof
let x be
set ;
( x in dom (B * (the_arity_of o)) implies (NH1 # ts1) . x in (B * (the_arity_of o)) . x )
assume A34:
x in dom (B * (the_arity_of o))
;
(NH1 # ts1) . x in (B * (the_arity_of o)) . x
reconsider x1 =
x as
Nat by A34;
A35:
ts . x1 in rng ts
by A24, A21, A22, A16, A23, A34, FUNCT_1:def 5;
rng ts c= TS (DTConOSA X)
by FINSEQ_1:def 4;
then reconsider t =
ts . x as
Element of
TS (DTConOSA X) by A35;
ts1 . x in (the Sorts of (ParsedTermsOSA X) * (the_arity_of o)) . x
by A24, A32, A34, MSUALG_3:6;
then
ts1 . x in the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o) . x)
by A24, A32, A34, FUNCT_1:22;
then
ts1 . x in the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o) /. x)
by A24, A34, PARTFUN1:def 8;
then
ts1 . x1 in dom (NH1 . ((the_arity_of o) /. x1))
by FUNCT_2:def 1;
then
(NH1 . ((the_arity_of o) /. x1)) . t in the
Sorts of
(GenOSAlg O) . ((the_arity_of o) /. x1)
by A12, A35;
then A36:
(NH1 . ((the_arity_of o) /. x1)) . (ts1 . x1) in B . ((the_arity_of o) . x)
by A24, A34, PARTFUN1:def 8;
(NH1 # ts1) . x1 = (NH1 . ((the_arity_of o) /. x1)) . (ts1 . x1)
by A24, A21, A22, A16, A23, A34, MSUALG_3:def 8;
hence
(NH1 # ts1) . x in (B * (the_arity_of o)) . x
by A34, A36, FUNCT_1:22;
verum
end;
NH1 # ts1 in Args o,
(FreeOSA X)
;
then A37:
NH1 # ts1 in dom (Den o,(FreeOSA X))
by FUNCT_2:def 1;
[o1,the carrier of S] = [o,x2]
by A13, A14, A19, TREES_4:def 4;
then A38:
o1 = o
by ZFMISC_1:33;
then A39:
B1 . rs1 c= B1 . s11
by A20, OSALG_1:def 18;
dom (NH1 # ts1) = dom (the_arity_of o)
by MSUALG_3:6;
then
NH1 # ts1 in ((B # ) * the Arity of S) . o
by A25, A24, A33, CARD_3:18;
then
(Den o,(FreeOSA X)) . (NH1 # ts1) in rng ((Den o,(FreeOSA X)) | (((B # ) * the Arity of S) . o))
by A37, FUNCT_1:73;
then A40:
(Den o,(FreeOSA X)) . (NH1 # ts1) in (B * the ResultSort of S) . o
by A27;
ts in Args o,
(ParsedTermsOSA X)
by A30, MSUALG_1:def 9;
then
(Den o,(ParsedTermsOSA X)) . ts in Result o,
(ParsedTermsOSA X)
by FUNCT_2:7;
then
(Den o,(ParsedTermsOSA X)) . ts in (the Sorts of (ParsedTermsOSA X) * the ResultSort of S) . o
by MSUALG_1:def 10;
then
(Den o,(ParsedTermsOSA X)) . ts in the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o)
by A26, FUNCT_2:21;
then
nt -tree ts in dom (NH1 . (the_result_sort_of o))
by A31, FUNCT_2:def 1;
then A41:
(NH1 . s11) . (nt -tree ts) = (NH1 . rs1) . (nt -tree ts)
by A1, A20, A38, OSALG_3:def 1;
(NH1 . (the_result_sort_of o)) . ((Den o,(ParsedTermsOSA X)) . ts1) = (Den o,(FreeOSA X)) . (NH1 # ts1)
by A8, MSUALG_3:def 9;
then
(NH1 . (the_result_sort_of o)) . (nt -tree ts) in B . (the_result_sort_of o)
by A26, A31, A40, FUNCT_2:21;
hence
(NH1 . s1) . (nt -tree ts) in the
Sorts of
(GenOSAlg O) . s1
by A39, A41;
verum
end;
let x be
set ;
PBOOLE:def 5 ( not x in the carrier of S or the Sorts of (FreeOSA X) . x c= the Sorts of (GenOSAlg O) . x )
assume A42:
x in the
carrier of
S
;
the Sorts of (FreeOSA X) . x c= the Sorts of (GenOSAlg O) . x
then reconsider s =
x as
SortSymbol of
S ;
A43:
for
s being
Symbol of
(DTConOSA X) st
s in Terminals (DTConOSA X) holds
S1[
root-tree s]
proof
let t be
Symbol of
(DTConOSA X);
( t in Terminals (DTConOSA X) implies S1[ root-tree t] )
assume A44:
t in Terminals (DTConOSA X)
;
S1[ root-tree t]
let s1 be
Element of
S;
( root-tree t in dom (NH1 . s1) implies (NH1 . s1) . (root-tree t) in the Sorts of (GenOSAlg O) . s1 )
assume
root-tree t in dom (NH1 . s1)
;
(NH1 . s1) . (root-tree t) in the Sorts of (GenOSAlg O) . s1
then
root-tree t in the
Sorts of
(ParsedTermsOSA X) . s1
;
then
root-tree t in ParsedTerms X,
s1
by Def8;
then consider a being
Element of
TS (DTConOSA X) such that A45:
root-tree t = a
and A46:
( ex
s2 being
Element of
S ex
x being
set st
(
s2 <= s1 &
x in X . s2 &
a = root-tree [x,s2] ) or ex
o being
OperSymbol of
S st
(
[o,the carrier of S] = a . {} &
the_result_sort_of o <= s1 ) )
;
for
o being
OperSymbol of
S holds
( not
[o,the carrier of S] = a . {} or not
the_result_sort_of o <= s1 )
then consider s2 being
Element of
S,
x being
set such that A49:
s2 <= s1
and A50:
x in X . s2
and A51:
a = root-tree [x,s2]
by A46;
reconsider s11 =
s1,
s21 =
s2 as
Element of
S ;
a in ParsedTerms X,
s2
by A50, A51;
then
a in (ParsedTerms X) . s2
by Def8;
then
root-tree [x,s2] in dom (NH1 . s2)
by A51, FUNCT_2:def 1;
then A52:
(NH1 . s21) . (root-tree [x,s2]) = (NH1 . s11) . (root-tree [x,s2])
by A1, A49, OSALG_3:def 1;
f . s2 c= the
Sorts of
(GenOSAlg O) . s2
by A5, PBOOLE:def 5;
then A53:
OSFreeGen s2,
X c= the
Sorts of
(GenOSAlg O) . s2
by A2;
O2 . s21 c= O2 . s11
by A49, OSALG_1:def 18;
then A54:
OSFreeGen s2,
X c= the
Sorts of
(GenOSAlg O) . s1
by A53, XBOOLE_1:1;
(NH1 . s2) . (root-tree [x,s2]) in OSFreeGen s2,
X
by A50, Def26;
hence
(NH1 . s1) . (root-tree t) in the
Sorts of
(GenOSAlg O) . s1
by A45, A51, A52, A54;
verum
end;
A55:
for
t being
DecoratedTree of the
carrier of
(DTConOSA X) st
t in TS (DTConOSA X) holds
S1[
t]
from DTCONSTR:sch 7(A43, A10);
the
Sorts of
(FreeOSA X) . s c= the
Sorts of
(GenOSAlg O) . s
proof
let x1 be
set ;
TARSKI:def 3 ( not x1 in the Sorts of (FreeOSA X) . s or x1 in the Sorts of (GenOSAlg O) . s )
assume A56:
x1 in the
Sorts of
(FreeOSA X) . s
;
x1 in the Sorts of (GenOSAlg O) . s
A57: the
Sorts of
(ParsedTermsOSA X) . s =
ParsedTerms X,
s
by Def8
.=
{ a where a is Element of TS (DTConOSA X) : ( ex s2 being Element of S ex x being set st
( s2 <= s & x in X . s2 & a = root-tree [x,s2] ) or ex o1 being OperSymbol of S st
( [o1,the carrier of S] = a . {} & the_result_sort_of o1 <= s ) ) }
;
rng (NH1 . x) = the
Sorts of
(FreeOSA X) . x
by A7, A42, MSUALG_3:def 3;
then consider x2 being
set such that A58:
x2 in dom (NH1 . s)
and A59:
x1 = (NH1 . s) . x2
by A56, FUNCT_1:def 5;
x2 in the
Sorts of
(ParsedTermsOSA X) . s
by A58;
then
ex
a being
Element of
TS (DTConOSA X) st
(
a = x2 & ( ex
s2 being
Element of
S ex
x being
set st
(
s2 <= s &
x in X . s2 &
a = root-tree [x,s2] ) or ex
o1 being
OperSymbol of
S st
(
[o1,the carrier of S] = a . {} &
the_result_sort_of o1 <= s ) ) )
by A57;
hence
x1 in the
Sorts of
(GenOSAlg O) . s
by A55, A58, A59;
verum
end;
hence
the
Sorts of
(FreeOSA X) . x c= the
Sorts of
(GenOSAlg O) . x
;
verum
end;
f is OSGeneratorSet of FreeOSA X
then reconsider f = f as OSGeneratorSet of FreeOSA X ;
take
f
; for s being Element of S holds f . s = OSFreeGen s,X
thus
for s being Element of S holds f . s = OSFreeGen s,X
by A2; verum