let n be Nat; for S being non empty non void ManySortedSign
for o being OperSymbol of S
for X being V5() ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) st the_arity_of o <> {} & n = union { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } holds
height (o -term p) = n + 1
let S be non empty non void ManySortedSign ; for o being OperSymbol of S
for X being V5() ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) st the_arity_of o <> {} & n = union { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } holds
height (o -term p) = n + 1
let o be OperSymbol of S; for X being V5() ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) st the_arity_of o <> {} & n = union { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } holds
height (o -term p) = n + 1
let X be V5() ManySortedSet of the carrier of S; for p being Element of Args (o,(Free (S,X))) st the_arity_of o <> {} & n = union { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } holds
height (o -term p) = n + 1
let p be Element of Args (o,(Free (S,X))); ( the_arity_of o <> {} & n = union { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } implies height (o -term p) = n + 1 )
set I = { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } ;
assume A1:
( the_arity_of o <> {} & n = union { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } )
; height (o -term p) = n + 1
set i0 = the Element of dom p;
A4:
dom p = dom (the_arity_of o)
by MSUALG_6:2;
reconsider i0 = the Element of dom p as Nat ;
reconsider t0 = p . i0 as Element of the Sorts of (Free (S,X)) . ((the_arity_of o) /. i0) by A4, A1, MSUALG_6:2;
t0 in rng p
by A4, A1, FUNCT_1:def 3;
then A5:
height t0 in { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p }
;
A2:
{ (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is natural-membered
deffunc H1( Element of (Free (S,X))) -> Nat = height $1;
A3:
rng p is finite
;
{ H1(t1) where t1 is Element of (Free (S,X)) : t1 in rng p } is finite
from FRAENKEL:sch 21(A3);
then reconsider I = { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } as non empty finite natural-membered set by A2, A5;
( n = max I & max I in I )
by A1, XXREAL_2:def 8;
then consider t1 being Element of (Free (S,X)) such that
A7:
( max I = height t1 & t1 in rng p )
;
consider a being FinSequence of NAT such that
A8:
( a in dom t1 & len a = max I )
by A7, TREES_1:def 12;
consider i1 being object such that
A9:
( i1 in dom p & t1 = p . i1 )
by A7, FUNCT_1:def 3;
reconsider i1 = i1 as Nat by A9;
consider i being Nat such that
A10:
i1 = 1 + i
by NAT_1:10, A9, FINSEQ_3:25;
i1 <= len p
by A9, FINSEQ_3:25;
then A11:
<*i*> ^ a in dom (o -term p)
by A8, A9, A10, NAT_1:13, TREES_4:11;
A12:
len (<*i*> ^ a) = 1 + n
by A1, A8, FINSEQ_5:8;
now for q being FinSequence of NAT st q in dom (o -term p) holds
len q <= n + 1let q be
FinSequence of
NAT ;
( q in dom (o -term p) implies len b1 <= n + 1 )assume
q in dom (o -term p)
;
len b1 <= n + 1per cases then
( q = {} or ex i being Nat ex T being DecoratedTree ex w being Node of T st
( i < len p & T = p . (i + 1) & q = <*i*> ^ w ) )
by TREES_4:11;
suppose
ex
i being
Nat ex
T being
DecoratedTree ex
w being
Node of
T st
(
i < len p &
T = p . (i + 1) &
q = <*i*> ^ w )
;
len b1 <= n + 1then consider i being
Nat,
t being
DecoratedTree,
w being
Node of
t such that B1:
(
i < len p &
t = p . (i + 1) &
q = <*i*> ^ w )
;
B0:
( 1
<= i + 1 &
i + 1
<= len p )
by B1, NAT_1:12, NAT_1:13;
then B2:
i + 1
in dom p
by FINSEQ_3:25;
reconsider t =
t as
Element of the
Sorts of
(Free (S,X)) . ((the_arity_of o) /. (i + 1)) by B0, B1, A4, MSUALG_6:2, FINSEQ_3:25;
t in rng p
by B2, B1, FUNCT_1:def 3;
then
height t in I
;
then
(
len w <= height t &
height t <= max I )
by XXREAL_2:def 8, TREES_1:def 12;
then
len w <= n
by A1, XXREAL_0:2;
then
1
+ (len w) <= n + 1
by XREAL_1:6;
hence
len q <= n + 1
by B1, FINSEQ_5:8;
verum end; end; end;
hence
height (o -term p) = n + 1
by A12, A11, TREES_1:def 12; verum