let S be locally_directed OrderSortedSign; :: thesis:
let X be non-empty ManySortedSet of S; :: thesis:
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:
let F be ManySortedFunction of PTVars X, the Sorts of U1; :: thesis:
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 H₁( Symbol of (DTConOSA X)) -> Element of Union the Sorts of U1 = pi (F, the Sorts of U1,$1);
deffunc H₂( 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) = H₁(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) = H₂(nt, roots ts,G * ts) from DTCONSTR:sch 8();
deffunc H₃( 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 = H₃(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

proof

let s be object ; :: thesis:
assume s in dom h ; :: thesis:
then h . s = G | ( the Sorts of (ParsedTermsOSA X) . s) by A3;
hence h . s is Function ; :: thesis:

end;

then reconsider h = h as ManySortedFunction of the carrier of S by FUNCOP_1:def 6;
defpred S₁[ 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
S₁[t] ) holds
S₁[nt -tree ts]

proof

let nt be Symbol of (DTConOSA X); :: thesis:
let ts be FinSequence of TS (DTConOSA X); :: thesis:
assume that
A5: nt ==> roots ts and
A6: for t being DecoratedTree of the carrier of (DTConOSA X) st t in rng ts holds
S₁[t] ; :: thesis:
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; :: thesis:
reconsider s2 = s as Element of S ;
assume A9: nt -tree ts in the Sorts of (ParsedTermsOSA X) . s ; :: thesis:
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

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; :: thesis:

end;

A46: for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
S₁[ root-tree t]

proof

let t be Symbol of (DTConOSA X); :: thesis:
assume A47: t in Terminals (DTConOSA X) ; :: thesis:
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; :: thesis:
reconsider s0 = s, s11 = s1 as Element of S ;
assume A56: root-tree t in the Sorts of (ParsedTermsOSA X) . s1 ; :: thesis:
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; :: thesis:

end;

A60: for t being DecoratedTree of the carrier of (DTConOSA X) st t in TS (DTConOSA X) holds
S₁[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 ; :: thesis:
assume x in the carrier of S ; :: thesis:
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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in rng (h . s) ; :: thesis:
then consider T being object such that
A66: T in dom (h . s) and
A67: (h . s) . T = a by FUNCT_1:def 3;
reconsider T = T as Element of TS (DTConOSA X) by A65, A64, A66, FUNCT_2:def 1;
T in the Sorts of (ParsedTermsOSA X) . s by A63, A61, A62, A66, RELAT_1:62, ZFMISC_1:74;
hence a in the Sorts of U1 . s by A60, A67; :: thesis:

end;

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; :: thesis:

end;

then reconsider h = h as ManySortedFunction of (ParsedTermsOSA X),U1 by PBOOLE:def 15;
take h ; :: thesis:
thus h is_homomorphism ParsedTermsOSA X,U1 :: thesis:

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; :: according to MSUALG_3:def 7 :: thesis:
assume Args (op,(ParsedTermsOSA X)) <> {} ; :: thesis:
reconsider o = op as OperSymbol of S ;
let x be Element of Args (op,(ParsedTermsOSA X)); :: thesis:
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 ; :: thesis:
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 ; :: thesis:
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; :: thesis:

end;

end;

thus h is order-sorted :: thesis:

proof

let s1, s2 be Element of S; :: according to OSALG_3:def 1 :: thesis:
assume s1 <= s2 ; :: thesis:
then A96: SAO . s1 c= SAO . s2 by OSALG_1:def 16;
let a1 be set ; :: thesis:
assume A97: a1 in dom (h . s1) ; :: thesis:
A98: a1 in SAO . s1 by A97;
then a1 in the Sorts of (ParsedTermsOSA X) . s2 by A96;
hence a1 in dom (h . s2) by FUNCT_2:def 1; :: thesis:
A99: h . s2 = G | ( the Sorts of (ParsedTermsOSA X) . s2) by A3;
h . s1 = G | ( the Sorts of (ParsedTermsOSA X) . s1) by A3;
hence (h . s1) . a1 = G . a1 by A97, FUNCT_1:49
.= (h . s2) . a1 by A96, A98, A99, FUNCT_1:49 ;
:: thesis:

end;

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 ; :: thesis:
assume x in the carrier of S ; :: thesis:
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 ; :: thesis:
A105: h . s = G | ( the Sorts of (ParsedTermsOSA X) . s) by A3;
assume A106: a in (PTVars X) . s ; :: thesis:
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 ; :: thesis:

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; :: thesis:

end;

hence h || (PTVars X) = F ; :: thesis: