let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
let A be non-empty MSAlgebra over S; for V being Variables of A
for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
let V be Variables of A; for f being ManySortedFunction of V, the Sorts of A
for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
let f be ManySortedFunction of V, the Sorts of A; for o being OperSymbol of S
for p being ArgumentSeq of o,A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
let o be OperSymbol of S; for p being ArgumentSeq of o,A,V
for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
let p be ArgumentSeq of o,A,V; for vt being finite DecoratedTree st vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f holds
ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
let vt be finite DecoratedTree; ( vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f implies ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) ) )
assume A1:
vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f
; ex q being DTree-yielding FinSequence st
( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
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
; ( len q = len p & vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
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; ( vt = ((Den (o,A)) . (roots q)) -tree q & ( for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) ) )
([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; for i being Nat
for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f )
let i be Nat; for t being c-Term of A,V st i in dom p & t = p . i holds
ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f )
let t be c-Term of A,V; ( i in dom p & t = p . i implies ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f ) )
assume that
A8:
i in dom p
and
A9:
t = p . i
; ex vt being finite DecoratedTree st
( vt = q . i & vt is_an_evaluation_of t,f )
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; ( e = q . i & e is_an_evaluation_of t,f )
len (doms p) = len p
by TREES_3:38;
hence
e = q . i
by A2, A7, A4, A10, A11, TREES_4:def 4; e is_an_evaluation_of t,f
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; verum