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 q being DTree-yielding FinSequence st len q = len p & ( 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 ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,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 q being DTree-yielding FinSequence st len q = len p & ( 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 ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,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 q being DTree-yielding FinSequence st len q = len p & ( 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 ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,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 q being DTree-yielding FinSequence st len q = len p & ( 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 ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f )
let o be OperSymbol of S; for p being ArgumentSeq of o,A,V
for q being DTree-yielding FinSequence st len q = len p & ( 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 ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f )
let p be ArgumentSeq of o,A,V; for q being DTree-yielding FinSequence st len q = len p & ( 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 ) ) holds
ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f )
A1:
Sym (o,( the Sorts of A (\/) V)) = [o, the carrier of S]
by MSAFREE:def 9;
A2:
dom (doms p) = dom p
by TREES_3:37;
A3:
tree (doms p) = dom ([o, the carrier of S] -tree p)
by TREES_4:10;
A4:
dom p = Seg (len p)
by FINSEQ_1:def 3;
let q be DTree-yielding FinSequence; ( len q = len p & ( 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 ) ) implies ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f ) )
assume that
A5:
len q = len p
and
A6:
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 )
; ex vt being finite DecoratedTree st
( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f )
A7:
dom q = Seg (len q)
by FINSEQ_1:def 3;
now for x being object st x in dom (doms q) holds
(doms q) . x is finite Treelet x be
object ;
( x in dom (doms q) implies (doms q) . x is finite Tree )A8:
rng p c= S -Terms ( the Sorts of A (\/) V)
by FINSEQ_1:def 4;
assume A9:
x in dom (doms q)
;
(doms q) . x is finite Treethen A10:
x in dom q
by TREES_3:37;
then
p . x in rng p
by A5, A4, A7, FUNCT_1:def 3;
then reconsider t =
p . x as
c-Term of
A,
V by A8;
reconsider i =
x as
Nat by A9;
consider vt being
finite DecoratedTree such that A11:
vt = q . i
and
vt is_an_evaluation_of t,
f
by A5, A6, A4, A7, A10;
(doms q) . x = dom vt
by A10, A11, FUNCT_6:22;
hence
(doms q) . x is
finite Tree
;
verum end;
then reconsider r = doms q as FinTree-yielding FinSequence by TREES_3:23;
set vt = ((Den (o,A)) . (roots q)) -tree q;
A17:
len (doms q) = len q
by TREES_3:38;
A18:
dom (((Den (o,A)) . (roots q)) -tree q) = tree r
by TREES_4:10;
then reconsider vt = ((Den (o,A)) . (roots q)) -tree q as finite DecoratedTree by FINSET_1:10;
take
vt
; ( vt = ((Den (o,A)) . (roots q)) -tree q & vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f )
thus
vt = ((Den (o,A)) . (roots q)) -tree q
; vt is_an_evaluation_of (Sym (o,( the Sorts of A (\/) V))) -tree p,f
dom (doms q) = dom q
by TREES_3:37;
hence
dom vt = dom ((Sym (o,( the Sorts of A (\/) V))) -tree p)
by A1, A5, A4, A7, A18, A3, A2, A12, FINSEQ_1:13; MSATERM:def 9 for p being Node of vt holds
( ( for s being SortSymbol of S
for v being Element of V . s st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . p = [v,s] holds
vt . p = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . p = [x,s] holds
vt . p = x ) & ( for o being OperSymbol of S st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . p = [o, the carrier of S] holds
vt . p = (Den (o,A)) . (succ (vt,p)) ) )
let n be Node of vt; ( ( for s being SortSymbol of S
for v being Element of V . s st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [v,s] holds
vt . n = (f . s) . v ) & ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [x,s] holds
vt . n = x ) & ( for o being OperSymbol of S st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [o, the carrier of S] holds
vt . n = (Den (o,A)) . (succ (vt,n)) ) )
A19:
([o, the carrier of S] -tree p) . {} = [o, the carrier of S]
by TREES_4:def 4;
hereby ( ( for s being SortSymbol of S
for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [x,s] holds
vt . n = x ) & ( for o being OperSymbol of S st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [o, the carrier of S] holds
vt . n = (Den (o,A)) . (succ (vt,n)) ) )
let s be
SortSymbol of
S;
for v being Element of V . s st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [v,s] holds
vt . n = (f . s) . vlet v be
Element of
V . s;
( ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [v,s] implies vt . n = (f . s) . v )assume A20:
((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [v,s]
;
vt . n = (f . s) . vthen consider w being
FinSequence of
NAT ,
i being
Element of
NAT such that A21:
n = <*i*> ^ w
by FINSEQ_2:130;
A22:
w in (doms q) . (i + 1)
by A18, A21, TREES_3:48;
A23:
i < len p
by A5, A18, A17, A21, TREES_3:48;
then reconsider t =
p . (i + 1) as
c-Term of
A,
V by Lm2;
consider e being
finite DecoratedTree such that A24:
e = q . (i + 1)
and A25:
e is_an_evaluation_of t,
f
by A6, A23, Lm9;
i + 1
in dom p
by A23, Lm9;
then reconsider w =
w as
Node of
e by A5, A4, A7, A22, A24, FUNCT_6:22;
dom e = dom t
by A25;
then A26:
t . w = [v,s]
by A20, A21, A23, TREES_4:12;
thus vt . n =
e . w
by A5, A21, A23, A24, TREES_4:12
.=
(f . s) . v
by A25, A26
;
verum
end;
hereby for o being OperSymbol of S st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [o, the carrier of S] holds
vt . n = (Den (o,A)) . (succ (vt,n))
let s be
SortSymbol of
S;
for x being Element of the Sorts of A . s st ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [x,s] holds
vt . n = xlet x be
Element of the
Sorts of
A . s;
( ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [x,s] implies vt . n = x )assume A27:
((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [x,s]
;
vt . n = xthen consider w being
FinSequence of
NAT ,
i being
Element of
NAT such that A28:
n = <*i*> ^ w
by FINSEQ_2:130;
A29:
w in (doms q) . (i + 1)
by A18, A28, TREES_3:48;
A30:
i < len p
by A5, A18, A17, A28, TREES_3:48;
then reconsider t =
p . (i + 1) as
c-Term of
A,
V by Lm2;
consider e being
finite DecoratedTree such that A31:
e = q . (i + 1)
and A32:
e is_an_evaluation_of t,
f
by A6, A30, Lm9;
i + 1
in dom p
by A30, Lm9;
then reconsider w =
w as
Node of
e by A5, A4, A7, A29, A31, FUNCT_6:22;
dom e = dom t
by A32;
then A33:
t . w = [x,s]
by A27, A28, A30, TREES_4:12;
thus vt . n =
e . w
by A5, A28, A30, A31, TREES_4:12
.=
x
by A32, A33
;
verum
end;
let o1 be OperSymbol of S; ( ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [o1, the carrier of S] implies vt . n = (Den (o1,A)) . (succ (vt,n)) )
assume A34:
((Sym (o,( the Sorts of A (\/) V))) -tree p) . n = [o1, the carrier of S]
; vt . n = (Den (o1,A)) . (succ (vt,n))
per cases
( n = {} or n <> {} )
;
suppose A35:
n = {}
;
vt . n = (Den (o1,A)) . (succ (vt,n))then ((Sym (o,( the Sorts of A (\/) V))) -tree p) . n =
Sym (
o,
( the Sorts of A (\/) V))
by TREES_4:def 4
.=
[o, the carrier of S]
by MSAFREE:def 9
;
then A36:
o = o1
by A34, XTUPLE_0:1;
succ (
vt,
n)
= roots q
by A35, TREES_9:30;
hence
vt . n = (Den (o1,A)) . (succ (vt,n))
by A35, A36, TREES_4:def 4;
verum end; suppose
n <> {}
;
vt . n = (Den (o1,A)) . (succ (vt,n))then consider w being
FinSequence of
NAT ,
i being
Element of
NAT such that A37:
n = <*i*> ^ w
by FINSEQ_2:130;
reconsider ii =
<*i*> as
Node of
vt by A37, TREES_1:21;
A38:
w in (doms q) . (i + 1)
by A18, A37, TREES_3:48;
A39:
i < len p
by A5, A18, A17, A37, TREES_3:48;
then reconsider t =
p . (i + 1) as
c-Term of
A,
V by Lm2;
consider e being
finite DecoratedTree such that A40:
e = q . (i + 1)
and A41:
e is_an_evaluation_of t,
f
by A6, A39, Lm9;
A42:
e = vt | ii
by A5, A39, A40, TREES_4:def 4;
i + 1
in dom p
by A39, Lm9;
then reconsider w =
w as
Node of
e by A5, A4, A7, A38, A40, FUNCT_6:22;
dom e = dom t
by A41;
then
t . w = [o1, the carrier of S]
by A34, A37, A39, TREES_4:12;
then e . w =
(Den (o1,A)) . (succ (e,w))
by A41
.=
(Den (o1,A)) . (succ (vt,n))
by A37, A42, TREES_9:31
;
hence
vt . n = (Den (o1,A)) . (succ (vt,n))
by A5, A37, A39, A40, TREES_4:12;
verum end; end;