let S be non empty non void ManySortedSign ; for V being V16() ManySortedSet of the carrier of S
for t being Term of S,V
for p being Node of t holds t | p is Term of S,V
let V be V16() ManySortedSet of the carrier of S; for t being Term of S,V
for p being Node of t holds t | p is Term of S,V
let t be Term of S,V; for p being Node of t holds t | p is Term of S,V
defpred S1[ set ] means for q being Node of t st q = $1 holds
t | q is Term of S,V;
A1:
for p being Node of t
for n being Element of NAT st S1[p] & p ^ <*n*> in dom t holds
S1[p ^ <*n*>]
proof
let p be
Node of
t;
for n being Element of NAT st S1[p] & p ^ <*n*> in dom t holds
S1[p ^ <*n*>]let n be
Element of
NAT ;
( S1[p] & p ^ <*n*> in dom t implies S1[p ^ <*n*>] )
assume that A2:
for
q being
Node of
t st
q = p holds
t | q is
Term of
S,
V
and A3:
p ^ <*n*> in dom t
;
S1[p ^ <*n*>]
reconsider u =
t | p as
Term of
S,
V by A2;
A4:
dom u = (dom t) | p
by TREES_2:def 11;
A5:
<*n*> in (dom t) | p
by A3, TREES_1:def 9;
( ex
s being
SortSymbol of
S ex
v being
Element of
V . s st
u . {} = [v,s] or
u . {} in [:the carrier' of S,{the carrier of S}:] )
by Th2;
then consider o being
OperSymbol of
S,
x2 being
Element of
{the carrier of S} such that A8:
u . {} = [o,x2]
by A6, DOMAIN_1:9;
x2 = the
carrier of
S
by TARSKI:def 1;
then consider a being
ArgumentSeq of
Sym o,
V such that A9:
u = [o,the carrier of S] -tree a
by A8, Th10;
consider i being
Element of
NAT ,
T being
DecoratedTree,
r being
Node of
T such that A10:
i < len a
and
T = a . (i + 1)
and A11:
<*n*> = <*i*> ^ r
by A5, A4, A9, TREES_4:11;
A12:
n =
<*n*> . 1
by FINSEQ_1:57
.=
i
by A11, FINSEQ_1:58
;
then A13:
u | <*n*> = a . (n + 1)
by A9, A10, TREES_4:def 4;
let q be
Node of
t;
( q = p ^ <*n*> implies t | q is Term of S,V )
assume A14:
q = p ^ <*n*>
;
t | q is Term of S,V
n + 1
in dom a
by A10, A12, Lm9;
then
ex
t being
Term of
S,
V st
(
t = u | <*n*> &
t = a /. (n + 1) &
the_sort_of t = (the_arity_of o) . (n + 1) &
the_sort_of t = (the_arity_of o) /. (n + 1) )
by A13, Lm8;
hence
t | q is
Term of
S,
V
by A14, TREES_9:3;
verum
end;
A15:
S1[ {} ]
by TREES_9:1;
for p being Node of t holds S1[p]
from TREES_2:sch 1(A15, A1);
hence
for p being Node of t holds t | p is Term of S,V
; verum