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