let S be non empty non void ManySortedSign ; for V being non-empty 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 non-empty 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 Nat st S1[p] & p ^ <*n*> in dom t holds
S1[p ^ <*n*>]
proof
let p be
Node of
t;
for n being Nat st S1[p] & p ^ <*n*> in dom t holds
S1[p ^ <*n*>]let n be
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 10;
reconsider nn =
n as
Element of
NAT by ORDINAL1:def 12;
A5:
<*nn*> in (dom t) | p
by A3, TREES_1:def 6;
( 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:1;
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
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
.=
i
by A11, FINSEQ_1:41
;
then A13:
u | <*nn*> = a . (nn + 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 )
nn + 1
in dom a
by A10, A12, Lm9;
then
ex
t being
Term of
S,
V st
(
t = u | <*nn*> &
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
(
q = p ^ <*n*> implies
t | q is
Term of
S,
V )
by TREES_9:3;
verum
end;
A14:
S1[ {} ]
by TREES_9:1;
for p being Node of t holds S1[p]
from TREES_2:sch 1(A14, A1);
hence
for p being Node of t holds t | p is Term of S,V
; verum