let A be QC-alphabet ; for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_prefix_of t9 holds
(tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t
let F be Element of QC-WFF A; for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_prefix_of t9 holds
(tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t
let t, t9 be Element of dom (tree_of_subformulae F); ( t is_a_prefix_of t9 implies (tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t )
assume
t is_a_prefix_of t9
; (tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t
then consider r being FinSequence such that
A1:
t9 = t ^ r
by TREES_1:1;
reconsider r = r as FinSequence of NAT by A1, FINSEQ_1:36;
consider n being Nat such that
A2:
n = len r
;
defpred S1[ set , object ] means ex G being QC-formula of A ex m, k1 being Nat ex r1 being FinSequence st
( G = $2 & m = $1 & m + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) );
A3:
for k being Nat st k in Seg (n + 1) holds
ex x being object st S1[k,x]
ex L being FinSequence st
( dom L = Seg (n + 1) & ( for k being Nat st k in Seg (n + 1) holds
S1[k,L . k] ) )
from FINSEQ_1:sch 1(A3);
then consider L being FinSequence such that
A7:
dom L = Seg (n + 1)
and
A8:
for k being Nat st k in Seg (n + 1) holds
ex G being QC-formula of A ex m, k1 being Nat ex r1 being FinSequence st
( G = L . k & m = k & m + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) )
;
A9:
len L = n + 1
by A7, FINSEQ_1:def 3;
A10:
for k being Nat st 1 <= k & k <= n + 1 holds
ex G being QC-formula of A ex k1 being Nat ex r1 being FinSequence st
( G = L . k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) )
A11:
for k being Nat st 1 <= k & k < n + 1 holds
ex H1, G1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 )
proof
let k be
Nat;
( 1 <= k & k < n + 1 implies ex H1, G1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 ) )
assume that A12:
1
<= k
and A13:
k < n + 1
;
ex H1, G1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 )
consider H1 being
QC-formula of
A,
k1 being
Nat,
r1 being
FinSequence such that A14:
H1 = L . k
and A15:
k + k1 = n + 1
and A16:
r1 = r | (Seg k1)
and A17:
H1 = (tree_of_subformulae F) . (t ^ r1)
by A10, A12, A13;
( 1
<= k + 1 &
k + 1
<= n + 1 )
by A12, A13, NAT_1:13;
then consider G1 being
QC-formula of
A,
k2 being
Nat,
r2 being
FinSequence such that A18:
G1 = L . (k + 1)
and A19:
(k + 1) + k2 = n + 1
and A20:
r2 = r | (Seg k2)
and A21:
G1 = (tree_of_subformulae F) . (t ^ r2)
by A10;
reconsider k1 =
k1,
k2 =
k2 as
Element of
NAT by ORDINAL1:def 12;
k1 + 1
<= n + 1
by A12, A15, XREAL_1:6;
then
k2 + 1
<= len r
by A2, A15, A19, XREAL_1:6;
then consider m being
Element of
NAT such that A22:
r1 = r2 ^ <*m*>
by A15, A16, A19, A20, TREES_9:33;
t ^ r2 in dom (tree_of_subformulae F)
then reconsider t2 =
t ^ r2 as
Element of
dom (tree_of_subformulae F) ;
A23:
t2 ^ <*m*> = t ^ r1
by A22, FINSEQ_1:32;
t2 ^ <*m*> in dom (tree_of_subformulae F)
then
H1 is_immediate_constituent_of G1
by A17, A21, A23, Th7;
hence
ex
H1,
G1 being
Element of
QC-WFF A st
(
L . k = H1 &
L . (k + 1) = G1 &
H1 is_immediate_constituent_of G1 )
by A14, A18;
verum
end;
A24:
0 + 1 <= n + 1
by NAT_1:13;
then consider G being QC-formula of A, k1 being Nat, r1 being FinSequence such that
A25:
G = L . 1
and
A26:
1 + k1 = n + 1
and
A27:
r1 = r | (Seg k1)
and
A28:
G = (tree_of_subformulae F) . (t ^ r1)
by A10;
A29:
L . (n + 1) = (tree_of_subformulae F) . t
dom r = Seg k1
by A2, A26, FINSEQ_1:def 3;
then
t9 = t ^ r1
by A1, A27;
hence
(tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t
by A24, A9, A25, A28, A29, A11, QC_LANG2:def 20; verum