let S be non empty non void ManySortedSign ; :: thesis:
let A be non-empty MSAlgebra over S; :: thesis:
let V be Variables of A; :: thesis:
let f be ManySortedFunction of V, the Sorts of A; :: thesis:
let o be OperSymbol of S; :: thesis:
let p be ArgumentSeq of o,A,V; :: thesis:
let vt be finite DecoratedTree; :: thesis:
assume A1: vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f ; :: thesis:
reconsider r = {} as empty Element of dom vt by TREES_1:22;
consider x being set , q being DTree-yielding FinSequence such that
A2: vt = x -tree q by TREES_9:8;
A3: dom vt = tree (doms q) by A2, TREES_4:10;
take q ; :: thesis:
A4: len (doms q) = len q by TREES_3:38;
A5: Sym (o,( the Sorts of A (\/) V)) = [o, the carrier of S] by MSAFREE:def 9;
then A6: dom vt = dom ([o, the carrier of S] -tree p) by A1;
then dom vt = tree (doms p) by TREES_4:10;
then A7: doms q = doms p by A3, TREES_3:50;
hence len q = len p by A4, TREES_3:38; :: thesis:
([o, the carrier of S] -tree p) . r = [o, the carrier of S] by TREES_4:def 4;
then vt . r = (Den (o,A)) . (succ (vt,r)) by A5, A1
.= (Den (o,A)) . (roots q) by A2, TREES_9:30 ;
hence vt = ((Den (o,A)) . (roots q)) -tree q by A2, TREES_4:def 4; :: thesis:
let i be Nat; :: thesis:
let t be c-Term of A,V; :: thesis:
assume that
A8: i in dom p and
A9: t = p . i ; :: thesis:
reconsider u = {} as Node of t by TREES_1:22;
consider k being Element of NAT such that
A10: i = k + 1 and
A11: k < len p by A8, Lm1;
<*k*> ^ u = <*k*> by FINSEQ_1:34;
then reconsider r = <*k*> as Node of vt by A6, A9, A10, A11, TREES_4:11;
take e = vt | r; :: thesis:
len (doms p) = len p by TREES_3:38;
hence e = q . i by A2, A7, A4, A10, A11, TREES_4:def 4; :: thesis:
reconsider r1 = r as Node of ([o, the carrier of S] -tree p) by A5, A1;
t = ([o, the carrier of S] -tree p) | r1 by A9, A10, A11, TREES_4:def 4;
hence e is_an_evaluation_of t,f by A5, A1, Th34; :: thesis: