let A be QC-alphabet ; :: thesis: for F, G, H being Element of QC-WFF A holds
( ( F is_subformula_of G or F is_subformula_of H ) iff F is_proper_subformula_of G '&' H )
let F, G, H be Element of QC-WFF A; :: thesis: ( ( F is_subformula_of G or F is_subformula_of H ) iff F is_proper_subformula_of G '&' H )
( G is_immediate_constituent_of G '&' H & H is_immediate_constituent_of G '&' H ) ;
hence ( ( F is_subformula_of G or F is_subformula_of H ) implies F is_proper_subformula_of G '&' H ) by Th63; :: thesis: ( not F is_proper_subformula_of G '&' H or F is_subformula_of G or F is_subformula_of H )
given n being Nat, L being FinSequence such that A1: 1 <= n and
A2: len L = n and
A3: L . 1 = F and
A4: L . n = G '&' H and
A5: for k being Nat st 1 <= k & k < n holds
ex H1, F1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ; :: according to QC_LANG2:def 20,QC_LANG2:def 21 :: thesis: ( not F <> G '&' H or F is_subformula_of G or F is_subformula_of H )
assume F <> G '&' H ; :: thesis: ( F is_subformula_of G or F is_subformula_of H )
then 1 < n by A1, A3, A4, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A6: n = 2 + k by NAT_1:10;
reconsider k = k as Nat ;
(1 + 1) + k = (1 + k) + 1 ;
then 1 + k < n by A6, NAT_1:13;
then consider H1, G1 being Element of QC-WFF A such that
A7: L . (1 + k) = H1 and
A8: ( L . ((1 + k) + 1) = G1 & H1 is_immediate_constituent_of G1 ) by A5, NAT_1:11;
reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:15;
F is_subformula_of H1
proof
take m = 1 + k; :: according to QC_LANG2:def 20 :: thesis: ex L being FinSequence st
( 1 <= m & len L = m & L . 1 = F & L . m = H1 & ( for k being Nat st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
take L1 ; :: thesis: ( 1 <= m & len L1 = m & L1 . 1 = F & L1 . m = H1 & ( for k being Nat st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus A9: 1 <= m by NAT_1:11; :: thesis: ( len L1 = m & L1 . 1 = F & L1 . m = H1 & ( for k being Nat st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
1 + k <= (1 + k) + 1 by NAT_1:11;
hence len L1 = m by A2, A6, FINSEQ_1:17; :: thesis: ( L1 . 1 = F & L1 . m = H1 & ( for k being Nat st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
A10: for j being Nat st 1 <= j & j <= m holds
L1 . j = L . j by FUNCT_1:49, FINSEQ_1:1;
hence L1 . 1 = F by A3, A9; :: thesis: ( L1 . m = H1 & ( for k being Nat st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus L1 . m = H1 by A7, A9, A10; :: thesis: for k being Nat st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
let j be Nat; :: thesis: ( 1 <= j & j < m implies ex G1, H1 being Element of QC-WFF A st
( L1 . j = G1 & L1 . (j + 1) = H1 & G1 is_immediate_constituent_of H1 ) )
assume that
A11: 1 <= j and
A12: j < m ; :: thesis: ex G1, H1 being Element of QC-WFF A st
( L1 . j = G1 & L1 . (j + 1) = H1 & G1 is_immediate_constituent_of H1 )
m <= m + 1 by NAT_1:11;
then j < n by A6, A12, XXREAL_0:2;
then consider F1, G1 being Element of QC-WFF A such that
A13: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A5, A11;
take F1 ; :: thesis: ex H1 being Element of QC-WFF A st
( L1 . j = F1 & L1 . (j + 1) = H1 & F1 is_immediate_constituent_of H1 )
take G1 ; :: thesis: ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
( 1 <= 1 + j & j + 1 <= m ) by A11, A12, NAT_1:13;
hence ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A10, A11, A12, A13; :: thesis: verum
end;
hence ( F is_subformula_of G or F is_subformula_of H ) by A4, A6, A8, Th45; :: thesis: verum