let n be Nat; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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))); :: thesis: ( 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 } ) ; :: thesis: 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
proof
let a be object ; :: according to MEMBERED:def 6 :: thesis: ( not a in { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } or a is natural )
assume a in { (height t1) where t1 is Element of (Free (S,X)) : t1 in rng p } ; :: thesis: a is natural
then ex t1 being Element of (Free (S,X)) st
( a = height t1 & t1 in rng p ) ;
hence a is natural ; :: thesis: verum
end;
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 :: thesis: for q being FinSequence of NAT st q in dom (o -term p) holds
len q <= n + 1
let q be FinSequence of NAT ; :: thesis: ( q in dom (o -term p) implies len b1 <= n + 1 )
assume q in dom (o -term p) ; :: thesis: len b1 <= n + 1
per 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 q = {} ; :: thesis: len b1 <= n + 1
hence len q <= n + 1 ; :: thesis: verum
end;
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 ) ; :: thesis: len b1 <= n + 1
then 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; :: thesis: verum
end;
end;
end;
hence height (o -term p) = n + 1 by A12, A11, TREES_1:def 12; :: thesis: verum