let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra of S
for V being Variables of A
for f being ManySortedFunction of V,the Sorts of A
for t being c-Term of A,V
for e being finite DecoratedTree st e is_an_evaluation_of t,f holds
for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
let A be non-empty MSAlgebra of S; :: thesis: for V being Variables of A
for f being ManySortedFunction of V,the Sorts of A
for t being c-Term of A,V
for e being finite DecoratedTree st e is_an_evaluation_of t,f holds
for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
let V be Variables of A; :: thesis: for f being ManySortedFunction of V,the Sorts of A
for t being c-Term of A,V
for e being finite DecoratedTree st e is_an_evaluation_of t,f holds
for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
let f be ManySortedFunction of V,the Sorts of A; :: thesis: for t being c-Term of A,V
for e being finite DecoratedTree st e is_an_evaluation_of t,f holds
for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
let t be c-Term of A,V; :: thesis: for e being finite DecoratedTree st e is_an_evaluation_of t,f holds
for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
let e be finite DecoratedTree; :: thesis: ( e is_an_evaluation_of t,f implies for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f )
assume that
A1: dom e = dom t and
A2: for p being Node of e holds
( ( for s being SortSymbol of S
for v being Element of V . s st t . p = [v,s] holds
e . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st t . p = [x,s] holds
e . p = x ) & ( for o being OperSymbol of S st t . p = [o,the carrier of S] holds
e . p = (Den o,A) . (succ e,p) ) ) ; :: according to MSATERM:def 9 :: thesis: for p being Node of t
for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
let p be Node of t; :: thesis: for n being Node of e st n = p holds
e | n is_an_evaluation_of t | p,f
let n be Node of e; :: thesis: ( n = p implies e | n is_an_evaluation_of t | p,f )
assume A3: n = p ; :: thesis: e | n is_an_evaluation_of t | p,f
set vt = e | n;
set tp = t | p;
A4: ( dom (e | n) = (dom e) | n & dom (t | p) = (dom t) | p ) by TREES_2:def 11;
hence dom (e | n) = dom (t | p) by A1, A3; :: according to MSATERM:def 9 :: thesis: for p being Node of (e | n) holds
( ( for s being SortSymbol of S
for v being Element of V . s st (t | p) . p = [v,s] holds
(e | n) . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st (t | p) . p = [x,s] holds
(e | n) . p = x ) & ( for o being OperSymbol of S st (t | p) . p = [o,the carrier of S] holds
(e | n) . p = (Den o,A) . (succ (e | n),p) ) )
let q be Node of (e | n); :: thesis: ( ( for s being SortSymbol of S
for v being Element of V . s st (t | p) . q = [v,s] holds
(e | n) . q = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st (t | p) . q = [x,s] holds
(e | n) . q = x ) & ( for o being OperSymbol of S st (t | p) . q = [o,the carrier of S] holds
(e | n) . q = (Den o,A) . (succ (e | n),q) ) )
reconsider nq = n ^ q as Node of e by A4, TREES_1:def 9;
reconsider pq = p ^ q as Node of t by A1, A3, A4, TREES_1:def 9;

hereby :: thesis: ( ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st (t | p) . q = [x,s] holds
(e | n) . q = x ) & ( for o being OperSymbol of S st (t | p) . q = [o,the carrier of S] holds
(e | n) . q = (Den o,A) . (succ (e | n),q) ) )

let s be SortSymbol of S; :: thesis: for v being Element of V . s st (t | p) . q = [v,s] holds
(e | n) . q = (f . s) . v
let v be Element of V . s; :: thesis: ( (t | p) . q = [v,s] implies (e | n) . q = (f . s) . v )
assume (t | p) . q = [v,s] ; :: thesis: (e | n) . q = (f . s) . v
then t . pq = [v,s] by A1, A3, A4, TREES_2:def 11;
then e . nq = (f . s) . v by A2, A3;
hence (e | n) . q = (f . s) . v by A4, TREES_2:def 11; :: thesis: verum

end;

hereby :: thesis: for o being OperSymbol of S st (t | p) . q = [o,the carrier of S] holds
(e | n) . q = (Den o,A) . (succ (e | n),q)

let s be SortSymbol of S; :: thesis: for x being Element of the Sorts of A . s st (t | p) . q = [x,s] holds
(e | n) . q = x
let x be Element of the Sorts of A . s; :: thesis: ( (t | p) . q = [x,s] implies (e | n) . q = x )
assume (t | p) . q = [x,s] ; :: thesis: (e | n) . q = x
then t . pq = [x,s] by A1, A3, A4, TREES_2:def 11;
then e . nq = x by A2, A3;
hence (e | n) . q = x by A4, TREES_2:def 11; :: thesis: verum

end;

let o be OperSymbol of S; :: thesis: ( (t | p) . q = [o,the carrier of S] implies (e | n) . q = (Den o,A) . (succ (e | n),q) )
assume (t | p) . q = [o,the carrier of S] ; :: thesis: (e | n) . q = (Den o,A) . (succ (e | n),q)
then t . pq = [o,the carrier of S] by A1, A3, A4, TREES_2:def 11;
then e . nq = (Den o,A) . (succ e,nq) by A2, A3;
then (e | n) . q = (Den o,A) . (succ e,(n ^ q)) by A4, TREES_2:def 11;
hence (e | n) . q = (Den o,A) . (succ (e | n),q) by TREES_9:32; :: thesis: verum