let S be locally_directed OrderSortedSign; for X being V2() ManySortedSet of S
for U1 being non-empty monotone OSAlgebra of S
for f being ManySortedFunction of PTVars X, the Sorts of U1 ex h being ManySortedFunction of (ParsedTermsOSA X),U1 st
( h is_homomorphism ParsedTermsOSA X,U1 & h is order-sorted & h || (PTVars X) = f )
let X be V2() ManySortedSet of S; for U1 being non-empty monotone OSAlgebra of S
for f being ManySortedFunction of PTVars X, the Sorts of U1 ex h being ManySortedFunction of (ParsedTermsOSA X),U1 st
( h is_homomorphism ParsedTermsOSA X,U1 & h is order-sorted & h || (PTVars X) = f )
set D = DTConOSA X;
set PTA = ParsedTermsOSA X;
set PV = PTVars X;
set SPTA = the Sorts of (ParsedTermsOSA X);
let U1 be non-empty monotone OSAlgebra of S; for f being ManySortedFunction of PTVars X, the Sorts of U1 ex h being ManySortedFunction of (ParsedTermsOSA X),U1 st
( h is_homomorphism ParsedTermsOSA X,U1 & h is order-sorted & h || (PTVars X) = f )
let F be ManySortedFunction of PTVars X, the Sorts of U1; ex h being ManySortedFunction of (ParsedTermsOSA X),U1 st
( h is_homomorphism ParsedTermsOSA X,U1 & h is order-sorted & h || (PTVars X) = F )
set SA = the Sorts of (ParsedTermsOSA X);
set AR = the Arity of S;
set S1 = the Sorts of U1;
set O = the carrier' of S;
set RS = the ResultSort of S;
reconsider SAO = the Sorts of (ParsedTermsOSA X), S1O = the Sorts of U1 as OrderSortedSet of S by OSALG_1:17;
deffunc H1( Symbol of (DTConOSA X)) -> Element of Union the Sorts of U1 = pi (F, the Sorts of U1,$1);
deffunc H2( Symbol of (DTConOSA X), set , FinSequence) -> Element of Union the Sorts of U1 = pi ((@ (X,$1)),U1,$3);
consider G being Function of (TS (DTConOSA X)),(Union the Sorts of U1) such that
A1:
for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
G . (root-tree t) = H1(t)
and
A2:
for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
G . (nt -tree ts) = H2(nt, roots ts,G * ts)
from DTCONSTR:sch 8();
deffunc H3( object ) -> Element of bool [:(TS (DTConOSA X)),(Union the Sorts of U1):] = G | ( the Sorts of (ParsedTermsOSA X) . $1);
consider h being Function such that
A3:
( dom h = the carrier of S & ( for s being object st s in the carrier of S holds
h . s = H3(s) ) )
from FUNCT_1:sch 3();
reconsider h = h as ManySortedSet of the carrier of S by A3, PARTFUN1:def 2, RELAT_1:def 18;
for s being object st s in dom h holds
h . s is Function
then reconsider h = h as ManySortedFunction of the carrier of S by FUNCOP_1:def 6;
defpred S1[ set ] means for s being Element of S st $1 in the Sorts of (ParsedTermsOSA X) . s holds
(h . s) . $1 in the Sorts of U1 . s;
A4:
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
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 A5:
nt ==> roots ts
and A6:
for
t being
DecoratedTree of the
carrier of
(DTConOSA X) st
t in rng ts holds
S1[
t]
;
S1[nt -tree ts]
set p =
G * ts;
set o =
@ (
X,
nt);
set ar =
the_arity_of (@ (X,nt));
set rs =
the_result_sort_of (@ (X,nt));
set OU =
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
set rt =
roots ts;
A7:
[(@ (X,nt)), the carrier of S] = nt
by A5, Def15;
then A8:
[[(@ (X,nt)), the carrier of S],(roots ts)] in the
Rules of
(DTConOSA X)
by A5, LANG1:def 1;
let s be
Element of
S;
( nt -tree ts in the Sorts of (ParsedTermsOSA X) . s implies (h . s) . (nt -tree ts) in the Sorts of U1 . s )
reconsider s2 =
s as
Element of
S ;
assume A9:
nt -tree ts in the
Sorts of
(ParsedTermsOSA X) . s
;
(h . s) . (nt -tree ts) in the Sorts of U1 . s
consider op being
OperSymbol of
S such that A10:
nt = [op, the carrier of S]
and
ts in Args (
op,
(ParsedTermsOSA X))
and
nt -tree ts = (Den (op,(ParsedTermsOSA X))) . ts
and A11:
for
s1 being
Element of
S holds
(
nt -tree ts in the
Sorts of
(ParsedTermsOSA X) . s1 iff
the_result_sort_of op <= s1 )
by A5, Th12;
op = @ (
X,
nt)
by A5, A10, Def15;
then
the_result_sort_of (@ (X,nt)) <= s
by A9, A11;
then A12:
S1O . (the_result_sort_of (@ (X,nt))) c= S1O . s2
by OSALG_1:def 16;
A13:
rng (Den ((@ (X,nt)),U1)) c= Result (
(@ (X,nt)),
U1)
by RELAT_1:def 19;
A14:
dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt)))
by PARTFUN1:def 2;
A15:
[(@ (X,nt)), the carrier of S] = OSSym (
(@ (X,nt)),
X)
;
then A16:
(PTDenOp ((@ (X,nt)),X)) . ts = nt -tree ts
by A5, A7, Def9;
A17:
dom ( the Sorts of (ParsedTermsOSA X) * (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt)))
by PARTFUN1:def 2;
dom (PTDenOp ((@ (X,nt)),X)) = (((ParsedTerms X) #) * the Arity of S) . (@ (X,nt))
by FUNCT_2:def 1;
then
ts in dom (PTDenOp ((@ (X,nt)),X))
by A5, A7, A15, Th7;
then A18:
nt -tree ts in rng (PTDenOp ((@ (X,nt)),X))
by A16, FUNCT_1:def 3;
A19:
h . (the_result_sort_of (@ (X,nt))) = G | ( the Sorts of (ParsedTermsOSA X) . (the_result_sort_of (@ (X,nt))))
by A3;
A20:
Seg (len (the_arity_of (@ (X,nt)))) = dom (the_arity_of (@ (X,nt)))
by FINSEQ_1:def 3;
A21:
rng (the_arity_of (@ (X,nt))) c= the
carrier of
S
by FINSEQ_1:def 4;
A22:
the_arity_of (@ (X,nt)) = the
Arity of
S . (@ (X,nt))
by MSUALG_1:def 1;
A23:
dom (roots ts) = dom ts
by TREES_3:def 18;
reconsider rt =
roots ts as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A8, ZFMISC_1:87;
A24:
len rt = len (the_arity_of (@ (X,nt)))
by A8, Th2;
A25:
dom rt = Seg (len rt)
by FINSEQ_1:def 3;
A26:
dom (G * ts) = dom ts
by FINSEQ_3:120;
then A27:
dom (G * ts) = dom ( the Sorts of U1 * (the_arity_of (@ (X,nt))))
by A23, A14, A8, A25, A20, Th2;
A28:
for
x being
object st
x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) holds
(G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x
proof
let x be
object ;
( x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) implies (G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x )
assume A29:
x in dom ( the Sorts of U1 * (the_arity_of (@ (X,nt))))
;
(G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x
then reconsider n =
x as
Nat ;
A30:
ts . n in rng ts
by A23, A14, A24, A25, A20, A29, FUNCT_1:def 3;
rng ts c= TS (DTConOSA X)
by FINSEQ_1:def 4;
then reconsider t =
ts . n as
Element of
TS (DTConOSA X) by A30;
A31:
(G * ts) . n = G . (ts . n)
by A27, A29, FINSEQ_3:120;
(the_arity_of (@ (X,nt))) . x in rng (the_arity_of (@ (X,nt)))
by A14, A29, FUNCT_1:def 3;
then reconsider s =
(the_arity_of (@ (X,nt))) . x as
Element of
S by A21;
A32:
h . s = G | ( the Sorts of (ParsedTermsOSA X) . s)
by A3;
dom the
Sorts of
(ParsedTermsOSA X) = the
carrier of
S
by PARTFUN1:def 2;
then A33:
the
Sorts of
(ParsedTermsOSA X) . s in rng the
Sorts of
(ParsedTermsOSA X)
by FUNCT_1:def 3;
dom G =
TS (DTConOSA X)
by FUNCT_2:def 1
.=
union (rng the Sorts of (ParsedTermsOSA X))
by Th8
;
then A34:
dom (h . s) = the
Sorts of
(ParsedTermsOSA X) . s
by A32, A33, RELAT_1:62, ZFMISC_1:74;
ts in (((ParsedTerms X) #) * the Arity of S) . (@ (X,nt))
by A5, A7, A15, Th7;
then
ts in product ((ParsedTerms X) * (the_arity_of (@ (X,nt))))
by A22, MSAFREE:1;
then
ts . x in ((ParsedTerms X) * (the_arity_of (@ (X,nt)))) . x
by A14, A17, A29, CARD_3:9;
then A35:
ts . x in (ParsedTerms X) . ((the_arity_of (@ (X,nt))) . x)
by A14, A17, A29, FUNCT_1:12;
then
(h . s) . t in the
Sorts of
U1 . s
by A6, A30;
then
G . t in the
Sorts of
U1 . s
by A35, A32, A34, FUNCT_1:47;
hence
(G * ts) . x in ( the Sorts of U1 * (the_arity_of (@ (X,nt)))) . x
by A29, A31, FUNCT_1:12;
verum
end;
set ppi =
pi (
(@ (X,nt)),
U1,
(G * ts));
A36:
dom (Den ((@ (X,nt)),U1)) = Args (
(@ (X,nt)),
U1)
by FUNCT_2:def 1;
A37:
dom the
ResultSort of
S = the
carrier' of
S
by FUNCT_2:def 1;
Args (
(@ (X,nt)),
U1) =
(( the Sorts of U1 #) * the Arity of S) . (@ (X,nt))
by MSUALG_1:def 4
.=
product ( the Sorts of U1 * (the_arity_of (@ (X,nt))))
by A22, MSAFREE:1
;
then A38:
G * ts in Args (
(@ (X,nt)),
U1)
by A26, A23, A14, A24, A25, A20, A28, CARD_3:9;
then
pi (
(@ (X,nt)),
U1,
(G * ts))
= (Den ((@ (X,nt)),U1)) . (G * ts)
by MSAFREE:def 21;
then
pi (
(@ (X,nt)),
U1,
(G * ts))
in rng (Den ((@ (X,nt)),U1))
by A38, A36, FUNCT_1:def 3;
then A39:
pi (
(@ (X,nt)),
U1,
(G * ts))
in Result (
(@ (X,nt)),
U1)
by A13;
h . s = G | ( the Sorts of (ParsedTermsOSA X) . s)
by A3;
then A40:
(h . s) . (nt -tree ts) = G . (nt -tree ts)
by A9, FUNCT_1:49;
A41:
rng the
ResultSort of
S c= the
carrier of
S
by RELAT_1:def 19;
dom the
Sorts of
(ParsedTermsOSA X) = the
carrier of
S
by PARTFUN1:def 2;
then A42:
dom ( the Sorts of (ParsedTermsOSA X) * the ResultSort of S) = dom the
ResultSort of
S
by A41, RELAT_1:27;
dom the
Sorts of
U1 = the
carrier of
S
by PARTFUN1:def 2;
then A43:
dom ( the Sorts of U1 * the ResultSort of S) = dom the
ResultSort of
S
by A41, RELAT_1:27;
rng (PTDenOp ((@ (X,nt)),X)) c= ((ParsedTerms X) * the ResultSort of S) . (@ (X,nt))
by RELAT_1:def 19;
then
nt -tree ts in ( the Sorts of (ParsedTermsOSA X) * the ResultSort of S) . (@ (X,nt))
by A18;
then
nt -tree ts in the
Sorts of
(ParsedTermsOSA X) . ( the ResultSort of S . (@ (X,nt)))
by A37, A42, FUNCT_1:12;
then A44:
nt -tree ts in the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of (@ (X,nt)))
by MSUALG_1:def 2;
G . (nt -tree ts) = pi (
(@ (X,nt)),
U1,
(G * ts))
by A2, A5;
then A45:
pi (
(@ (X,nt)),
U1,
(G * ts))
= (G | ( the Sorts of (ParsedTermsOSA X) . (the_result_sort_of (@ (X,nt))))) . (nt -tree ts)
by A44, FUNCT_1:49;
Result (
(@ (X,nt)),
U1) =
( the Sorts of U1 * the ResultSort of S) . (@ (X,nt))
by MSUALG_1:def 5
.=
the
Sorts of
U1 . ( the ResultSort of S . (@ (X,nt)))
by A43, A37, FUNCT_1:12
.=
the
Sorts of
U1 . (the_result_sort_of (@ (X,nt)))
by MSUALG_1:def 2
;
then
(h . (the_result_sort_of (@ (X,nt)))) . (nt -tree ts) in the
Sorts of
U1 . s
by A39, A45, A19, A12;
hence
(h . s) . (nt -tree ts) in the
Sorts of
U1 . s
by A44, A19, A40, FUNCT_1:49;
verum
end;
A46:
for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
S1[ root-tree t]
proof
let t be
Symbol of
(DTConOSA X);
( t in Terminals (DTConOSA X) implies S1[ root-tree t] )
assume A47:
t in Terminals (DTConOSA X)
;
S1[ root-tree t]
then consider s being
Element of
S,
x being
set such that A48:
x in X . s
and A49:
t = [x,s]
by Th4;
reconsider s =
s as
SortSymbol of
S ;
set E =
{ (root-tree tt) where tt is Symbol of (DTConOSA X) : ( tt in Terminals (DTConOSA X) & tt `2 = s ) } ;
set a =
root-tree t;
A50:
t `2 = s
by A49;
then A51:
root-tree t in { (root-tree tt) where tt is Symbol of (DTConOSA X) : ( tt in Terminals (DTConOSA X) & tt `2 = s ) }
by A47;
reconsider f =
F . s as
Function of
((PTVars X) . s),
( the Sorts of U1 . s) ;
A52:
dom f = (PTVars X) . s
by FUNCT_2:def 1;
A53:
rng f c= the
Sorts of
U1 . s
by RELAT_1:def 19;
A54:
{ (root-tree tt) where tt is Symbol of (DTConOSA X) : ( tt in Terminals (DTConOSA X) & tt `2 = s ) } = PTVars (
s,
X)
by Th28;
then
(PTVars X) . s = { (root-tree tt) where tt is Symbol of (DTConOSA X) : ( tt in Terminals (DTConOSA X) & tt `2 = s ) }
by Def24;
then
f . (root-tree t) in rng f
by A51, A52, FUNCT_1:def 3;
then A55:
f . (root-tree t) in the
Sorts of
U1 . s
by A53;
let s1 be
Element of
S;
( root-tree t in the Sorts of (ParsedTermsOSA X) . s1 implies (h . s1) . (root-tree t) in the Sorts of U1 . s1 )
reconsider s0 =
s,
s11 =
s1 as
Element of
S ;
assume A56:
root-tree t in the
Sorts of
(ParsedTermsOSA X) . s1
;
(h . s1) . (root-tree t) in the Sorts of U1 . s1
then
s <= s1
by A48, A49, Th10;
then A57:
S1O . s0 c= S1O . s11
by OSALG_1:def 16;
A58:
h . s = G | ( the Sorts of (ParsedTermsOSA X) . s)
by A3;
then A59:
(h . s) . (root-tree t) =
G . (root-tree t)
by A51, A54, FUNCT_1:49
.=
pi (
F, the
Sorts of
U1,
t)
by A1, A47
.=
f . (root-tree t)
by A47, A50, Def28
;
h . s1 = G | ( the Sorts of (ParsedTermsOSA X) . s1)
by A3;
then (h . s1) . (root-tree t) =
G . (root-tree t)
by A56, FUNCT_1:49
.=
f . (root-tree t)
by A51, A54, A58, A59, FUNCT_1:49
;
hence
(h . s1) . (root-tree t) in the
Sorts of
U1 . s1
by A55, A57;
verum
end;
A60:
for t being DecoratedTree of the carrier of (DTConOSA X) st t in TS (DTConOSA X) holds
S1[t]
from DTCONSTR:sch 7(A46, A4);
for s being object st s in the carrier of S holds
h . s is Function of ( the Sorts of (ParsedTermsOSA X) . s),( the Sorts of U1 . s)
proof
let x be
object ;
( x in the carrier of S implies h . x is Function of ( the Sorts of (ParsedTermsOSA X) . x),( the Sorts of U1 . x) )
assume
x in the
carrier of
S
;
h . x is Function of ( the Sorts of (ParsedTermsOSA X) . x),( the Sorts of U1 . x)
then reconsider s =
x as
Element of
S ;
A61:
dom G =
TS (DTConOSA X)
by FUNCT_2:def 1
.=
union (rng the Sorts of (ParsedTermsOSA X))
by Th8
;
dom the
Sorts of
(ParsedTermsOSA X) = the
carrier of
S
by PARTFUN1:def 2;
then A62:
the
Sorts of
(ParsedTermsOSA X) . s in rng the
Sorts of
(ParsedTermsOSA X)
by FUNCT_1:def 3;
A63:
h . s = G | ( the Sorts of (ParsedTermsOSA X) . s)
by A3;
then A64:
dom (h . s) = the
Sorts of
(ParsedTermsOSA X) . s
by A61, A62, RELAT_1:62, ZFMISC_1:74;
A65:
the
Sorts of
(ParsedTermsOSA X) . s c= dom G
by A61, A62, ZFMISC_1:74;
rng (h . s) c= the
Sorts of
U1 . s
hence
h . x is
Function of
( the Sorts of (ParsedTermsOSA X) . x),
( the Sorts of U1 . x)
by A64, FUNCT_2:def 1, RELSET_1:4;
verum
end;
then reconsider h = h as ManySortedFunction of (ParsedTermsOSA X),U1 by PBOOLE:def 15;
take
h
; ( h is_homomorphism ParsedTermsOSA X,U1 & h is order-sorted & h || (PTVars X) = F )
thus
h is_homomorphism ParsedTermsOSA X,U1
( h is order-sorted & h || (PTVars X) = F )proof
A68:
dom the
Sorts of
(ParsedTermsOSA X) = the
carrier of
S
by PARTFUN1:def 2;
rng the
ResultSort of
S c= the
carrier of
S
by RELAT_1:def 19;
then A69:
dom ( the Sorts of (ParsedTermsOSA X) * the ResultSort of S) = dom the
ResultSort of
S
by A68, RELAT_1:27;
let op be
Element of the
carrier' of
S;
MSUALG_3:def 7 ( Args (op,(ParsedTermsOSA X)) = {} or for b1 being Element of Args (op,(ParsedTermsOSA X)) holds (h . (the_result_sort_of op)) . ((Den (op,(ParsedTermsOSA X))) . b1) = (Den (op,U1)) . (h # b1) )
assume
Args (
op,
(ParsedTermsOSA X))
<> {}
;
for b1 being Element of Args (op,(ParsedTermsOSA X)) holds (h . (the_result_sort_of op)) . ((Den (op,(ParsedTermsOSA X))) . b1) = (Den (op,U1)) . (h # b1)
reconsider o =
op as
OperSymbol of
S ;
let x be
Element of
Args (
op,
(ParsedTermsOSA X));
(h . (the_result_sort_of op)) . ((Den (op,(ParsedTermsOSA X))) . x) = (Den (op,U1)) . (h # x)
set rs =
the_result_sort_of o;
set DA =
Den (
o,
(ParsedTermsOSA X));
set D1 =
Den (
o,
U1);
set OU =
[: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X));
set ar =
the_arity_of o;
A70:
the_arity_of o = the
Arity of
S . o
by MSUALG_1:def 1;
A71:
Args (
o,
(ParsedTermsOSA X))
= (((ParsedTerms X) #) * the Arity of S) . o
by MSUALG_1:def 4;
then reconsider p =
x as
FinSequence of
TS (DTConOSA X) by Th5;
A72:
OSSym (
o,
X)
==> roots p
by A71, Th7;
then A73:
@ (
X,
(OSSym (o,X)))
= o
by Def15;
A74:
dom (G * p) = dom p
by FINSEQ_3:120;
A75:
x in (((ParsedTerms X) #) * the Arity of S) . o
by A71;
A76:
for
a being
object st
a in dom p holds
(G * p) . a = (h # x) . a
proof
set rt =
roots p;
let a be
object ;
( a in dom p implies (G * p) . a = (h # x) . a )
A77:
dom ( the Sorts of (ParsedTermsOSA X) * (the_arity_of o)) = dom (the_arity_of o)
by PARTFUN1:def 2;
A78:
[[o, the carrier of S],(roots p)] in the
Rules of
(DTConOSA X)
by A72, LANG1:def 1;
assume A79:
a in dom p
;
(G * p) . a = (h # x) . a
then reconsider n =
a as
Nat ;
A80:
(h # x) . n = (h . ((the_arity_of o) /. n)) . (x . n)
by A79, MSUALG_3:def 6;
A81:
(G * p) . n = G . (x . n)
by A74, A79, FINSEQ_3:120;
A82:
h . ((the_arity_of o) /. n) = G | ( the Sorts of (ParsedTermsOSA X) . ((the_arity_of o) /. n))
by A3;
A83:
dom (roots p) = dom p
by TREES_3:def 18;
reconsider rt =
roots p as
Element of
([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A78, ZFMISC_1:87;
A84:
len rt = len (the_arity_of o)
by A78, Th2;
A85:
Seg (len rt) = dom rt
by FINSEQ_1:def 3;
A86:
Seg (len (the_arity_of o)) = dom (the_arity_of o)
by FINSEQ_1:def 3;
p in product ((ParsedTerms X) * (the_arity_of o))
by A75, A70, MSAFREE:1;
then A87:
p . n in ((ParsedTerms X) * (the_arity_of o)) . n
by A79, A77, A83, A84, A85, A86, CARD_3:9;
((ParsedTerms X) * (the_arity_of o)) . n =
the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o) . n)
by A79, A77, A83, A84, A85, A86, FUNCT_1:12
.=
the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o) /. n)
by A79, A83, A84, A85, A86, PARTFUN1:def 6
;
hence
(G * p) . a = (h # x) . a
by A81, A80, A82, A87, FUNCT_1:49;
verum
end;
dom (h # x) = dom (the_arity_of o)
by MSUALG_3:6;
then A88:
G * p = h # x
by A74, A76, FUNCT_1:2, MSUALG_3:6;
A89:
h . (the_result_sort_of o) = G | ( the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o))
by A3;
A90:
rng (PTDenOp (o,X)) c= ((ParsedTerms X) * the ResultSort of S) . o
by RELAT_1:def 19;
A91:
dom (PTDenOp (o,X)) = (((ParsedTerms X) #) * the Arity of S) . o
by FUNCT_2:def 1;
(PTDenOp (o,X)) . p = (OSSym (o,X)) -tree p
by A72, Def9;
then
(OSSym (o,X)) -tree p in rng (PTDenOp (o,X))
by A71, A91, FUNCT_1:def 3;
then A92:
(OSSym (o,X)) -tree p in ( the Sorts of (ParsedTermsOSA X) * the ResultSort of S) . o
by A90;
dom the
Sorts of
(ParsedTermsOSA X) = the
carrier of
S
by PARTFUN1:def 2;
then A93:
the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o) in rng the
Sorts of
(ParsedTermsOSA X)
by FUNCT_1:def 3;
dom the
ResultSort of
S = the
carrier' of
S
by FUNCT_2:def 1;
then
(OSSym (o,X)) -tree p in the
Sorts of
(ParsedTermsOSA X) . ( the ResultSort of S . o)
by A69, A92, FUNCT_1:12;
then A94:
(OSSym (o,X)) -tree p in the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o)
by MSUALG_1:def 2;
dom G =
TS (DTConOSA X)
by FUNCT_2:def 1
.=
union (rng the Sorts of (ParsedTermsOSA X))
by Th8
;
then A95:
dom (h . (the_result_sort_of o)) = the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o)
by A89, A93, RELAT_1:62, ZFMISC_1:74;
Den (
o,
(ParsedTermsOSA X)) =
(PTOper X) . o
by MSUALG_1:def 6
.=
PTDenOp (
o,
X)
by Def10
;
then
(Den (o,(ParsedTermsOSA X))) . x = (OSSym (o,X)) -tree p
by A72, Def9;
then (h . (the_result_sort_of o)) . ((Den (o,(ParsedTermsOSA X))) . x) =
G . ((OSSym (o,X)) -tree p)
by A94, A89, A95, FUNCT_1:47
.=
pi (
(@ (X,(OSSym (o,X)))),
U1,
(G * p))
by A2, A72
.=
(Den (o,U1)) . (h # x)
by A73, A88, MSAFREE:def 21
;
hence
(h . (the_result_sort_of op)) . ((Den (op,(ParsedTermsOSA X))) . x) = (Den (op,U1)) . (h # x)
;
verum
end;
thus
h is order-sorted
h || (PTVars X) = F
for x being object st x in the carrier of S holds
(h || (PTVars X)) . x = F . x
proof
set hf =
h || (PTVars X);
let x be
object ;
( x in the carrier of S implies (h || (PTVars X)) . x = F . x )
assume
x in the
carrier of
S
;
(h || (PTVars X)) . x = F . x
then reconsider s =
x as
Element of
S ;
A100:
dom (h . s) = the
Sorts of
(ParsedTermsOSA X) . s
by FUNCT_2:def 1;
A101:
dom ((h || (PTVars X)) . s) = (PTVars X) . s
by FUNCT_2:def 1;
A102:
(PTVars X) . s = PTVars (
s,
X)
by Def24;
A103:
(h || (PTVars X)) . s = (h . s) | ((PTVars X) . s)
by MSAFREE:def 1;
A104:
for
a being
object st
a in (PTVars X) . s holds
((h || (PTVars X)) . s) . a = (F . s) . a
proof
let a be
object ;
( a in (PTVars X) . s implies ((h || (PTVars X)) . s) . a = (F . s) . a )
A105:
h . s = G | ( the Sorts of (ParsedTermsOSA X) . s)
by A3;
assume A106:
a in (PTVars X) . s
;
((h || (PTVars X)) . s) . a = (F . s) . a
then
a in { (root-tree t) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) }
by A102, Th28;
then consider t being
Symbol of
(DTConOSA X) such that A107:
a = root-tree t
and A108:
t in Terminals (DTConOSA X)
and A109:
t `2 = s
;
thus ((h || (PTVars X)) . s) . a =
(h . s) . a
by A103, A101, A106, FUNCT_1:47
.=
G . a
by A100, A102, A106, A105, FUNCT_1:47
.=
pi (
F, the
Sorts of
U1,
t)
by A1, A107, A108
.=
(F . s) . a
by A107, A108, A109, Def28
;
verum
end;
dom (F . s) = (PTVars X) . s
by FUNCT_2:def 1;
hence
(h || (PTVars X)) . x = F . x
by A101, A104, FUNCT_1:2;
verum
end;
hence
h || (PTVars X) = F
; verum