let S be non empty non void ManySortedSign ; :: thesis: 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 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 over 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 )
set vt = e | n;
set tp = t | p;
A3: dom (e | n) = (dom e) | n by TREES_2:def 10;
assume A4: n = p ; :: thesis: e | n is_an_evaluation_of t | p,f
hence dom (e | n) = dom (t | p) by A1, A3, TREES_2:def 10; :: 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 A3, TREES_1:def 6;
reconsider pq = p ^ q as Node of t by A1, A4, A3, TREES_1:def 6;

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, A4, A3, TREES_2:def 10;
then e . nq = (f . s) . v by A2, A4;
hence (e | n) . q = (f . s) . v by A3, TREES_2:def 10; :: 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, A4, A3, TREES_2:def 10;
then e . nq = x by A2, A4;
hence (e | n) . q = x by A3, TREES_2:def 10; :: 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, A4, A3, TREES_2:def 10;
then e . nq = (Den (o,A)) . (succ (e,nq)) by A2, A4;
then (e | n) . q = (Den (o,A)) . (succ (e,(n ^ q))) by A3, TREES_2:def 10;
hence (e | n) . q = (Den (o,A)) . (succ ((e | n),q)) by TREES_9:31; :: thesis: verum