let S be locally_directed OrderSortedSign; :: thesis: for X being V5() ManySortedSet of
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 V5() ManySortedSet of ; :: thesis: 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; :: thesis: 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; :: thesis: 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 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( set ) -> 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 set st s in the carrier of S holds
h . s = H3(s) ) )
from FUNCT_1:sch 3();
reconsider h = h as ManySortedSet of by A3, PARTFUN1:def 4, RELAT_1:def 18;
for s being set st s in dom h holds
h . s is Function
then reconsider h = h as ManySortedFunction of 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 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);
:: thesis: ( t in Terminals (DTConOSA X) implies S1[ root-tree t] )
assume A5:
t in Terminals (DTConOSA X)
;
:: thesis: S1[ root-tree t]
then consider s being
Element of
S,
x being
set such that A6:
(
x in X . s &
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;
A7:
t `2 = s
by A6, MCART_1:7;
then A8:
root-tree t in { (root-tree tt) where tt is Symbol of (DTConOSA X) : ( tt in Terminals (DTConOSA X) & tt `2 = s ) }
by A5;
A9:
(
{ (root-tree tt) where tt is Symbol of (DTConOSA X) : ( tt in Terminals (DTConOSA X) & tt `2 = s ) } = PTVars s,
X &
PTVars s,
X c= (ParsedTerms X) . s )
by Th29;
reconsider f =
F . s as
Function of
((PTVars X) . s),
(the Sorts of U1 . s) ;
A10:
(PTVars X) . s = { (root-tree tt) where tt is Symbol of (DTConOSA X) : ( tt in Terminals (DTConOSA X) & tt `2 = s ) }
by A9, Def25;
A11:
(
dom f = (PTVars X) . s &
rng f c= the
Sorts of
U1 . s )
by FUNCT_2:def 1, RELAT_1:def 19;
then
f . (root-tree t) in rng f
by A8, A10, FUNCT_1:def 5;
then A12:
f . (root-tree t) in the
Sorts of
U1 . s
by A11;
A13:
h . s = G | (the Sorts of (ParsedTermsOSA X) . s)
by A3;
then A14:
(h . s) . (root-tree t) =
G . (root-tree t)
by A8, A9, FUNCT_1:72
.=
pi F,the
Sorts of
U1,
t
by A1, A5
.=
f . (root-tree t)
by A5, A7, Def29
;
let s1 be
Element of
S;
:: thesis: ( 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 A15:
root-tree t in the
Sorts of
(ParsedTermsOSA X) . s1
;
:: thesis: (h . s1) . (root-tree t) in the Sorts of U1 . s1
then
s <= s1
by A6, Th10;
then A16:
S1O . s0 c= S1O . s11
by OSALG_1:def 18;
h . s1 = G | (the Sorts of (ParsedTermsOSA X) . s1)
by A3;
then (h . s1) . (root-tree t) =
G . (root-tree t)
by A15, FUNCT_1:72
.=
f . (root-tree t)
by A8, A9, A13, A14, FUNCT_1:72
;
hence
(h . s1) . (root-tree t) in the
Sorts of
U1 . s1
by A12, A16;
:: thesis: verum
end;
A17:
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 A18:
(
nt ==> roots ts & ( for
t being
DecoratedTree of st
t in rng ts holds
S1[
t] ) )
;
:: thesis: 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;
A19:
(
@ X,
nt in the
carrier' of
S &
the_arity_of (@ X,nt) = the
Arity of
S . (@ X,nt) )
by MSUALG_1:def 6;
A20:
Args (@ X,nt),
U1 =
((the Sorts of U1 # ) * the Arity of S) . (@ X,nt)
by MSUALG_1:def 9
.=
product (the Sorts of U1 * (the_arity_of (@ X,nt)))
by A19, MSAFREE:1
;
A21:
(
dom (G * ts) = dom ts &
len (G * ts) = len ts & ( for
n being
Nat st
n in dom (G * ts) holds
(G * ts) . n = G . (ts . n) ) )
by ALG_1:1;
A22:
dom (roots ts) = dom ts
by TREES_3:def 18;
A23:
[(@ X,nt),the carrier of S] = nt
by A18, Def16;
A24:
[(@ X,nt),the carrier of S] = OSSym (@ X,nt),
X
;
A25:
(
rng (the_arity_of (@ X,nt)) c= the
carrier of
S &
dom the
Sorts of
U1 = the
carrier of
S &
dom the
Sorts of
(ParsedTermsOSA X) = the
carrier of
S )
by FINSEQ_1:def 4, PARTFUN1:def 4;
A26:
(
dom (the Sorts of U1 * (the_arity_of (@ X,nt))) = dom (the_arity_of (@ X,nt)) &
dom (the Sorts of (ParsedTermsOSA X) * (the_arity_of (@ X,nt))) = dom (the_arity_of (@ X,nt)) )
by PARTFUN1:def 4;
A27:
[[(@ X,nt),the carrier of S],(roots ts)] in the
Rules of
(DTConOSA X)
by A18, A23, 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;
A28:
len rt = len (the_arity_of (@ X,nt))
by A27, Th2;
A29:
(
dom rt = Seg (len rt) &
Seg (len (the_arity_of (@ X,nt))) = dom (the_arity_of (@ X,nt)) )
by FINSEQ_1:def 3;
then A30:
dom (G * ts) = dom (the Sorts of U1 * (the_arity_of (@ X,nt)))
by A21, A22, A26, A27, Th2;
for
x being
set 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
set ;
:: thesis: ( 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 A31:
x in dom (the Sorts of U1 * (the_arity_of (@ X,nt)))
;
:: thesis: (G * ts) . x in (the Sorts of U1 * (the_arity_of (@ X,nt))) . x
then reconsider n =
x as
Nat ;
A32:
(G * ts) . n = G . (ts . n)
by A30, A31, ALG_1:1;
A33:
rng ts c= TS (DTConOSA X)
by FINSEQ_1:def 4;
A34:
ts . n in rng ts
by A22, A26, A28, A29, A31, FUNCT_1:def 5;
then reconsider t =
ts . n as
Element of
TS (DTConOSA X) by A33;
ts in (((ParsedTerms X) # ) * the Arity of S) . (@ X,nt)
by A18, A23, A24, Th7;
then
ts in product ((ParsedTerms X) * (the_arity_of (@ X,nt)))
by A19, MSAFREE:1;
then
ts . x in ((ParsedTerms X) * (the_arity_of (@ X,nt))) . x
by A26, A31, CARD_3:18;
then A35:
ts . x in (ParsedTerms X) . ((the_arity_of (@ X,nt)) . x)
by A26, A31, FUNCT_1:22;
(the_arity_of (@ X,nt)) . x in rng (the_arity_of (@ X,nt))
by A26, A31, FUNCT_1:def 5;
then reconsider s =
(the_arity_of (@ X,nt)) . x as
Element of
S by A25;
A36:
(h . s) . t in the
Sorts of
U1 . s
by A18, A34, A35;
A37:
h . s = G | (the Sorts of (ParsedTermsOSA X) . s)
by A3;
A38:
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 4;
then
the
Sorts of
(ParsedTermsOSA X) . s in rng the
Sorts of
(ParsedTermsOSA X)
by FUNCT_1:def 5;
then
dom (h . s) = the
Sorts of
(ParsedTermsOSA X) . s
by A37, A38, RELAT_1:91, ZFMISC_1:92;
then
G . t in the
Sorts of
U1 . s
by A35, A36, A37, FUNCT_1:70;
hence
(G * ts) . x in (the Sorts of U1 * (the_arity_of (@ X,nt))) . x
by A31, A32, FUNCT_1:22;
:: thesis: verum
end;
then A39:
G * ts in Args (@ X,nt),
U1
by A20, A21, A22, A26, A28, A29, CARD_3:18;
then A40:
pi (@ X,nt),
U1,
(G * ts) = (Den (@ X,nt),U1) . (G * ts)
by MSAFREE:def 23;
set ppi =
pi (@ X,nt),
U1,
(G * ts);
A41:
(
dom (Den (@ X,nt),U1) = Args (@ X,nt),
U1 &
rng (Den (@ X,nt),U1) c= Result (@ X,nt),
U1 )
by FUNCT_2:def 1, RELAT_1:def 19;
then
pi (@ X,nt),
U1,
(G * ts) in rng (Den (@ X,nt),U1)
by A39, A40, FUNCT_1:def 5;
then A42:
pi (@ X,nt),
U1,
(G * ts) in Result (@ X,nt),
U1
by A41;
(
dom the
Sorts of
U1 = the
carrier of
S &
rng the
ResultSort of
S c= the
carrier of
S &
dom the
Sorts of
(ParsedTermsOSA X) = the
carrier of
S )
by PARTFUN1:def 4, RELAT_1:def 19;
then A43:
(
dom (the Sorts of U1 * the ResultSort of S) = dom the
ResultSort of
S &
dom the
ResultSort of
S = the
carrier' of
S &
dom (the Sorts of (ParsedTermsOSA X) * the ResultSort of S) = dom the
ResultSort of
S )
by FUNCT_2:def 1, RELAT_1:46;
A44:
Result (@ X,nt),
U1 =
(the Sorts of U1 * the ResultSort of S) . (@ X,nt)
by MSUALG_1:def 10
.=
the
Sorts of
U1 . (the ResultSort of S . (@ X,nt))
by A43, FUNCT_1:22
.=
the
Sorts of
U1 . (the_result_sort_of (@ X,nt))
by MSUALG_1:def 7
;
A45:
G . (nt -tree ts) = pi (@ X,nt),
U1,
(G * ts)
by A2, A18;
A46:
(PTDenOp (@ X,nt),X) . ts = nt -tree ts
by A18, A23, A24, Def9;
A47:
(
dom (PTDenOp (@ X,nt),X) = (((ParsedTerms X) # ) * the Arity of S) . (@ X,nt) &
rng (PTDenOp (@ X,nt),X) c= ((ParsedTerms X) * the ResultSort of S) . (@ X,nt) )
by FUNCT_2:def 1, RELAT_1:def 19;
then
ts in dom (PTDenOp (@ X,nt),X)
by A18, A23, A24, Th7;
then
nt -tree ts in rng (PTDenOp (@ X,nt),X)
by A46, FUNCT_1:def 5;
then
nt -tree ts in (the Sorts of (ParsedTermsOSA X) * the ResultSort of S) . (@ X,nt)
by A47;
then
nt -tree ts in the
Sorts of
(ParsedTermsOSA X) . (the ResultSort of S . (@ X,nt))
by A43, FUNCT_1:22;
then A48:
nt -tree ts in the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of (@ X,nt))
by MSUALG_1:def 7;
then A49:
pi (@ X,nt),
U1,
(G * ts) = (G | (the Sorts of (ParsedTermsOSA X) . (the_result_sort_of (@ X,nt)))) . (nt -tree ts)
by A45, FUNCT_1:72;
let s be
Element of
S;
:: thesis: ( 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 ;
A50:
(
h . (the_result_sort_of (@ X,nt)) = G | (the Sorts of (ParsedTermsOSA X) . (the_result_sort_of (@ X,nt))) &
h . s = G | (the Sorts of (ParsedTermsOSA X) . s) )
by A3;
assume A51:
nt -tree ts in the
Sorts of
(ParsedTermsOSA X) . s
;
:: thesis: (h . s) . (nt -tree ts) in the Sorts of U1 . s
consider op being
OperSymbol of
S such that A52:
(
nt = [op,the carrier of S] &
ts in Args op,
(ParsedTermsOSA X) &
nt -tree ts = (Den op,(ParsedTermsOSA X)) . ts & ( 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 A18, Th12;
op = @ X,
nt
by A18, A52, Def16;
then
the_result_sort_of (@ X,nt) <= s
by A51, A52;
then
S1O . (the_result_sort_of (@ X,nt)) c= S1O . s2
by OSALG_1:def 18;
then A53:
(h . (the_result_sort_of (@ X,nt))) . (nt -tree ts) in the
Sorts of
U1 . s
by A42, A44, A49, A50;
(h . s) . (nt -tree ts) = G . (nt -tree ts)
by A50, A51, FUNCT_1:72;
hence
(h . s) . (nt -tree ts) in the
Sorts of
U1 . s
by A48, A50, A53, FUNCT_1:72;
:: thesis: verum
end;
A54:
for t being DecoratedTree of st t in TS (DTConOSA X) holds
S1[t]
from DTCONSTR:sch 7(A4, A17);
for s being set 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
set ;
:: thesis: ( 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
;
:: thesis: h . x is Function of (the Sorts of (ParsedTermsOSA X) . x),(the Sorts of U1 . x)
then reconsider s =
x as
Element of
S ;
A55:
h . s = G | (the Sorts of (ParsedTermsOSA X) . s)
by A3;
A56:
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 4;
then A57:
the
Sorts of
(ParsedTermsOSA X) . s in rng the
Sorts of
(ParsedTermsOSA X)
by FUNCT_1:def 5;
then A58:
the
Sorts of
(ParsedTermsOSA X) . s c= dom G
by A56, ZFMISC_1:92;
A59:
dom (h . s) = the
Sorts of
(ParsedTermsOSA X) . s
by A55, A56, A57, RELAT_1:91, ZFMISC_1:92;
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 A59, FUNCT_2:def 1, RELSET_1:11;
:: thesis: verum
end;
then reconsider h = h as ManySortedFunction of (ParsedTermsOSA X),U1 by PBOOLE:def 18;
take
h
; :: thesis: ( h is_homomorphism ParsedTermsOSA X,U1 & h is order-sorted & h || (PTVars X) = F )
thus
h is_homomorphism ParsedTermsOSA X,U1
:: thesis: ( h is order-sorted & h || (PTVars X) = F )proof
let op be
Element of the
carrier' of
S;
:: according to MSUALG_3:def 9 :: thesis: ( 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) <> {}
;
:: thesis: 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);
:: thesis: (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;
A61:
Den o,
(ParsedTermsOSA X) =
(PTOper X) . o
by MSUALG_1:def 11
.=
PTDenOp o,
X
by Def10
;
A62:
Args o,
(ParsedTermsOSA X) = (((ParsedTerms X) # ) * the Arity of S) . o
by MSUALG_1:def 9;
then A63:
x in (((ParsedTerms X) # ) * the Arity of S) . o
;
reconsider p =
x as
FinSequence of
TS (DTConOSA X) by A62, Th5;
A64:
OSSym o,
X ==> roots p
by A62, Th7;
then A65:
(Den o,(ParsedTermsOSA X)) . x = (OSSym o,X) -tree p
by A61, Def9;
A66:
(
o in the
carrier' of
S &
the_arity_of o = the
Arity of
S . o &
dom the
Arity of
S = the
carrier' of
S )
by FUNCT_2:def 1, MSUALG_1:def 6;
A67:
@ X,
(OSSym o,X) = o
by A64, Def16;
(
rng the
ResultSort of
S c= the
carrier of
S &
dom the
Sorts of
(ParsedTermsOSA X) = the
carrier of
S )
by PARTFUN1:def 4, RELAT_1:def 19;
then A68:
(
dom the
ResultSort of
S = the
carrier' of
S &
dom (the Sorts of (ParsedTermsOSA X) * the ResultSort of S) = dom the
ResultSort of
S )
by FUNCT_2:def 1, RELAT_1:46;
A69:
(PTDenOp o,X) . p = (OSSym o,X) -tree p
by A64, Def9;
A70:
(
dom (PTDenOp o,X) = (((ParsedTerms X) # ) * the Arity of S) . o &
rng (PTDenOp o,X) c= ((ParsedTerms X) * the ResultSort of S) . o )
by FUNCT_2:def 1, RELAT_1:def 19;
then
(OSSym o,X) -tree p in rng (PTDenOp o,X)
by A62, A69, FUNCT_1:def 5;
then
(OSSym o,X) -tree p in (the Sorts of (ParsedTermsOSA X) * the ResultSort of S) . o
by A70;
then
(OSSym o,X) -tree p in the
Sorts of
(ParsedTermsOSA X) . (the ResultSort of S . o)
by A68, FUNCT_1:22;
then A71:
(OSSym o,X) -tree p in the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o)
by MSUALG_1:def 7;
A72:
h . (the_result_sort_of o) = G | (the Sorts of (ParsedTermsOSA X) . (the_result_sort_of o))
by A3;
A73:
dom G =
TS (DTConOSA X)
by FUNCT_2:def 1
.=
union (rng the Sorts of (ParsedTermsOSA X))
by Th8
;
A74:
(
dom (G * p) = dom p &
len (G * p) = len p & ( for
n being
Nat st
n in dom (G * p) holds
(G * p) . n = G . (p . n) ) )
by ALG_1:1;
A75:
(
dom (h # x) = dom (the_arity_of o) &
dom x = dom (the_arity_of o) )
by MSUALG_3:6;
for
a being
set st
a in dom p holds
(G * p) . a = (h # x) . a
proof
let a be
set ;
:: thesis: ( a in dom p implies (G * p) . a = (h # x) . a )
assume A76:
a in dom p
;
:: thesis: (G * p) . a = (h # x) . a
then reconsider n =
a as
Nat ;
A77:
(G * p) . n = G . (x . n)
by A74, A76;
A78:
(h # x) . n = (h . ((the_arity_of o) /. n)) . (x . n)
by A76, MSUALG_3:def 8;
A79:
h . ((the_arity_of o) /. n) = G | (the Sorts of (ParsedTermsOSA X) . ((the_arity_of o) /. n))
by A3;
A80:
p in product ((ParsedTerms X) * (the_arity_of o))
by A63, A66, MSAFREE:1;
A81:
(
dom (the Sorts of U1 * (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;
set rt =
roots p;
A82:
dom (roots p) = dom p
by TREES_3:def 18;
A83:
[[o,the carrier of S],(roots p)] in the
Rules of
(DTConOSA X)
by A64, LANG1:def 1;
then reconsider rt =
roots p as
Element of
([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:106;
A84:
len rt = len (the_arity_of o)
by A83, Th2;
A85:
(
Seg (len rt) = dom rt &
Seg (len (the_arity_of o)) = dom (the_arity_of o) )
by FINSEQ_1:def 3;
then A86:
p . n in ((ParsedTerms X) * (the_arity_of o)) . n
by A76, A80, A81, A82, A84, CARD_3:18;
((ParsedTerms X) * (the_arity_of o)) . n =
the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o) . n)
by A76, A81, A82, A84, A85, FUNCT_1:22
.=
the
Sorts of
(ParsedTermsOSA X) . ((the_arity_of o) /. n)
by A76, A82, A84, A85, PARTFUN1:def 8
;
hence
(G * p) . a = (h # x) . a
by A77, A78, A79, A86, FUNCT_1:72;
:: thesis: verum
end;
then A87:
G * p = h # x
by A74, A75, FUNCT_1:9;
dom the
Sorts of
(ParsedTermsOSA X) = the
carrier of
S
by PARTFUN1:def 4;
then
the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o) in rng the
Sorts of
(ParsedTermsOSA X)
by FUNCT_1:def 5;
then
dom (h . (the_result_sort_of o)) = the
Sorts of
(ParsedTermsOSA X) . (the_result_sort_of o)
by A72, A73, RELAT_1:91, ZFMISC_1:92;
then (h . (the_result_sort_of o)) . ((Den o,(ParsedTermsOSA X)) . x) =
G . ((OSSym o,X) -tree p)
by A65, A71, A72, FUNCT_1:70
.=
pi (@ X,(OSSym o,X)),
U1,
(G * p)
by A2, A64
.=
(Den o,U1) . (h # x)
by A67, A87, MSAFREE:def 23
;
hence
(h . (the_result_sort_of op)) . ((Den op,(ParsedTermsOSA X)) . x) = (Den op,U1) . (h # x)
;
:: thesis: verum
end;
thus
h is order-sorted
:: thesis: h || (PTVars X) = F
for x being set st x in the carrier of S holds
(h || (PTVars X)) . x = F . x
proof
let x be
set ;
:: thesis: ( x in the carrier of S implies (h || (PTVars X)) . x = F . x )
assume
x in the
carrier of
S
;
:: thesis: (h || (PTVars X)) . x = F . x
then reconsider s =
x as
Element of
S ;
set hf =
h || (PTVars X);
A93:
(h || (PTVars X)) . s = (h . s) | ((PTVars X) . s)
by MSAFREE:def 1;
A94:
dom (h . s) = the
Sorts of
(ParsedTermsOSA X) . s
by FUNCT_2:def 1;
A95:
(PTVars X) . s = PTVars s,
X
by Def25;
A96:
dom ((h || (PTVars X)) . s) = (PTVars X) . s
by FUNCT_2:def 1;
A97:
dom (F . s) = (PTVars X) . s
by FUNCT_2:def 1;
for
a being
set st
a in (PTVars X) . s holds
((h || (PTVars X)) . s) . a = (F . s) . a
proof
let a be
set ;
:: thesis: ( a in (PTVars X) . s implies ((h || (PTVars X)) . s) . a = (F . s) . a )
assume A98:
a in (PTVars X) . s
;
:: thesis: ((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 A95, Th29;
then consider t being
Symbol of
(DTConOSA X) such that A99:
(
a = root-tree t &
t in Terminals (DTConOSA X) &
t `2 = s )
;
A100:
h . s = G | (the Sorts of (ParsedTermsOSA X) . s)
by A3;
thus ((h || (PTVars X)) . s) . a =
(h . s) . a
by A93, A96, A98, FUNCT_1:70
.=
G . a
by A94, A95, A98, A100, FUNCT_1:70
.=
pi F,the
Sorts of
U1,
t
by A1, A99
.=
(F . s) . a
by A99, Def29
;
:: thesis: verum
end;
hence
(h || (PTVars X)) . x = F . x
by A96, A97, FUNCT_1:9;
:: thesis: verum
end;
hence
h || (PTVars X) = F
by PBOOLE:3; :: thesis: verum