let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds
len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t))
let F be Element of QC-WFF A; :: thesis: for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds
len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t))
let t, t9 be Element of dom (tree_of_subformulae F); :: thesis: ( t is_a_proper_prefix_of t9 implies len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t)) )
set G = (tree_of_subformulae F) . t;
set H = (tree_of_subformulae F) . t9;
assume A1: t is_a_proper_prefix_of t9 ; :: thesis: len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t))
then A2: t is_a_prefix_of t9 ;
A3: now :: thesis: not len (@ ((tree_of_subformulae F) . t9)) = len (@ ((tree_of_subformulae F) . t))
consider r being FinSequence such that
A4: t9 = t ^ r by A2, TREES_1:1;
reconsider r = r as FinSequence of NAT by A4, FINSEQ_1:36;
A5: 1 <= len r
proof
reconsider t1 = {} as Element of dom (tree_of_subformulae F) by TREES_1:22;
( r <> {} & t1 is_a_prefix_of r ) by A1, A4, FINSEQ_1:34;
then A6: t1 is_a_proper_prefix_of r ;
len t1 = 0 ;
then 0 < len r by A6, TREES_1:6;
then 0 + 1 <= len r by NAT_1:13;
hence 1 <= len r ; :: thesis: verum
end;
defpred S1[ set , object ] means ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence ex m being Nat st
( m = $1 & r1 = r | (Seg m) & t1 = t ^ r1 & $2 = (tree_of_subformulae F) . t1 );
A7: for k being Nat st k in Seg (len r) holds
ex x being object st S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len r) implies ex x being object st S1[k,x] )
assume k in Seg (len r) ; :: thesis: ex x being object st S1[k,x]
r | (Seg k) is FinSequence by FINSEQ_1:15;
then consider r1 being FinSequence such that
A8: r1 = r | (Seg k) ;
r1 is_a_prefix_of r by A8, TREES_1:def 1;
then t ^ r1 in dom (tree_of_subformulae F) by A4, FINSEQ_6:13, TREES_1:20;
then consider t1 being Element of dom (tree_of_subformulae F) such that
A9: t1 = t ^ r1 ;
ex x being set st x = (tree_of_subformulae F) . t1 ;
hence ex x being object st S1[k,x] by A8, A9; :: thesis: verum
end;
ex L being FinSequence st
( dom L = Seg (len r) & ( for k being Nat st k in Seg (len r) holds
S1[k,L . k] ) ) from FINSEQ_1:sch 1(A7);
then consider L being FinSequence such that
dom L = Seg (len r) and
A10: for k being Nat st k in Seg (len r) holds
ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence ex m being Nat st
( m = k & r1 = r | (Seg m) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) ;
for k being Nat st 1 <= k & k <= len r holds
ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st
( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 )
proof
let k be Nat; :: thesis: ( 1 <= k & k <= len r implies ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st
( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) )
assume ( 1 <= k & k <= len r ) ; :: thesis: ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st
( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 )
then k in Seg (len r) by FINSEQ_1:1;
then ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence ex m being Nat st
( m = k & r1 = r | (Seg m) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) by A10;
hence ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st
( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) ; :: thesis: verum
end;
then consider t1 being Element of dom (tree_of_subformulae F), r1 being FinSequence such that
A11: r1 = r | (Seg 1) and
A12: t1 = t ^ r1 and
L . 1 = (tree_of_subformulae F) . t1 by A5;
set H1 = (tree_of_subformulae F) . t1;
A13: (tree_of_subformulae F) . t1 is_immediate_constituent_of (tree_of_subformulae F) . t
proof
ex m being Element of NAT st r1 = <*m*> by A5, A11, TREES_9:34;
hence (tree_of_subformulae F) . t1 is_immediate_constituent_of (tree_of_subformulae F) . t by A12, Th7; :: thesis: verum
end;
r1 is_a_prefix_of r by A11, TREES_1:def 1;
then t1 is_a_prefix_of t9 by A4, A12, FINSEQ_6:13;
then A14: len (@ ((tree_of_subformulae F) . t9)) <= len (@ ((tree_of_subformulae F) . t1)) by Th1, Th13;
assume len (@ ((tree_of_subformulae F) . t9)) = len (@ ((tree_of_subformulae F) . t)) ; :: thesis: contradiction
hence contradiction by A14, A13, QC_LANG2:51; :: thesis: verum
end;
len (@ ((tree_of_subformulae F) . t9)) <= len (@ ((tree_of_subformulae F) . t)) by A2, Th1, Th13;
hence len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t)) by A3, XXREAL_0:1; :: thesis: verum