deffunc H1( Element of QC-WFF A) -> Element of omega = len (@ $1);
deffunc H2( Element of QC-WFF A) -> FinSequence of QC-WFF A = list_of_immediate_constituents $1;
consider W being finite-branching DecoratedTree of QC-WFF A such that
A1: ( W . {} = p & ( for x being Element of dom W
for w being Element of QC-WFF A st w = W . x holds
succ (W,x) = H2(w) ) ) from TREES_9:sch 2();
 A2: for t, t9 being Element of dom W
for d being Element of QC-WFF A st t9 in succ t & d = W . t9 holds
H1(d) < H1(W . t)
proof
let t, t9 be Element of dom W; :: thesis: for d being Element of QC-WFF A st t9 in succ t & d = W . t9 holds
H1(d) < H1(W . t)
let d be Element of QC-WFF A; :: thesis: ( t9 in succ t & d = W . t9 implies H1(d) < H1(W . t) )
assume that
A3: t9 in succ t and
A4: d = W . t9 ; :: thesis: H1(d) < H1(W . t)
consider n being Nat such that
A5: t9 = t ^ <*n*> and
t ^ <*n*> in dom W by A3;
A6: W . t9 = (succ (W,t)) . (n + 1) by A5, TREES_9:40
.= (list_of_immediate_constituents (W . t)) . (n + 1) by A1 ;
dom (list_of_immediate_constituents (W . t)) = dom (succ (W,t)) by A1
.= dom (t succ) by TREES_9:38 ;
then n + 1 in dom (list_of_immediate_constituents (W . t)) by A5, TREES_9:39;
hence H1(d) < H1(W . t) by A4, A6, Th3, QC_LANG2:51; :: thesis: verum
end;
W is finite from TREES_9:sch 3(A2);
 then reconsider W = W as finite DecoratedTree of QC-WFF A ;
take W ; :: thesis: ( W . {} = p & ( for x being Element of dom W holds succ (W,x) = list_of_immediate_constituents (W . x) ) )
thus ( W . {} = p & ( for x being Element of dom W holds succ (W,x) = list_of_immediate_constituents (W . x) ) ) by A1; :: thesis: verum