let A be QC-alphabet ; :: thesis: for F, G, H being Element of QC-WFF A st F is_proper_subformula_of G & G is_proper_subformula_of H holds
F is_proper_subformula_of H
let F, G, H be Element of QC-WFF A; :: thesis: ( F is_proper_subformula_of G & G is_proper_subformula_of H implies F is_proper_subformula_of H )
assume that
A1: F is_proper_subformula_of G and
A2: G is_proper_subformula_of H ; :: thesis: F is_proper_subformula_of H
F is_subformula_of G by A1;
then consider n being Nat, L being FinSequence such that
A3: 1 <= n and
A4: len L = n and
A5: L . 1 = F and
A6: L . n = G and
A7: 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 ) ;
1 < n by A1, A3, A5, A6, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A8: n = 2 + k by NAT_1:10;
G is_subformula_of H by A2;
then consider m being Nat, L9 being FinSequence such that
A9: 1 <= m and
A10: len L9 = m and
A11: L9 . 1 = G and
A12: L9 . m = H and
A13: for k being Nat st 1 <= k & k < m holds
ex H1, F1 being Element of QC-WFF A st
( L9 . k = H1 & L9 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ;
reconsider k = k as Nat ;
reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:15;
thus F is_subformula_of H :: according to QC_LANG2:def 21 :: thesis: F <> H
proof
take l = (1 + k) + m; :: according to QC_LANG2:def 20 :: thesis: ex L being FinSequence st
( 1 <= l & len L = l & L . 1 = F & L . l = H & ( for k being Nat st 1 <= k & k < l 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 K = L1 ^ L9; :: thesis: ( 1 <= l & len K = l & K . 1 = F & K . l = H & ( for k being Nat st 1 <= k & k < l holds
ex G1, H1 being Element of QC-WFF A st
( K . k = G1 & K . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
A14: ((1 + k) + m) - (1 + k) = m ;
m <= m + (1 + k) by NAT_1:11;
hence 1 <= l by A9, XXREAL_0:2; :: thesis: ( len K = l & K . 1 = F & K . l = H & ( for k being Nat st 1 <= k & k < l holds
ex G1, H1 being Element of QC-WFF A st
( K . k = G1 & K . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
(1 + 1) + k = (1 + k) + 1 ;
then A15: 1 + k <= n by A8, NAT_1:11;
then A16: len L1 = 1 + k by A4, FINSEQ_1:17;
hence A17: len K = l by A10, FINSEQ_1:22; :: thesis: ( K . 1 = F & K . l = H & ( for k being Nat st 1 <= k & k < l holds
ex G1, H1 being Element of QC-WFF A st
( K . k = G1 & K . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
A18: now :: thesis: for j being Nat st 1 <= j & j <= 1 + k holds
K . j = L . j
let j be Nat; :: thesis: ( 1 <= j & j <= 1 + k implies K . j = L . j )
assume ( 1 <= j & j <= 1 + k ) ; :: thesis: K . j = L . j
then A19: j in Seg (1 + k) by FINSEQ_1:1;
then j in dom L1 by A4, A15, FINSEQ_1:17;
then K . j = L1 . j by FINSEQ_1:def 7;
hence K . j = L . j by A19, FUNCT_1:49; :: thesis: verum
end;
1 <= 1 + k by NAT_1:11;
hence K . 1 = F by A5, A18; :: thesis: ( K . l = H & ( for k being Nat st 1 <= k & k < l holds
ex G1, H1 being Element of QC-WFF A st
( K . k = G1 & K . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
(len L1) + 1 <= (len L1) + m by A9, XREAL_1:7;
then len L1 < l by A16, NAT_1:13;
then K . l = L9 . (l - (len L1)) by A17, FINSEQ_1:24;
hence K . l = H by A4, A12, A15, A14, FINSEQ_1:17; :: thesis: for k being Nat st 1 <= k & k < l holds
ex G1, H1 being Element of QC-WFF A st
( K . k = G1 & K . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
let j be Nat; :: thesis: ( 1 <= j & j < l implies ex G1, H1 being Element of QC-WFF A st
( K . j = G1 & K . (j + 1) = H1 & G1 is_immediate_constituent_of H1 ) )
assume that
A20: 1 <= j and
A21: j < l ; :: thesis: ex G1, H1 being Element of QC-WFF A st
( K . j = G1 & K . (j + 1) = H1 & G1 is_immediate_constituent_of H1 )
j + 0 <= j + 1 by XREAL_1:7;
then A22: 1 <= j + 1 by A20, XXREAL_0:2;
A23: now :: thesis: ( j < 1 + k implies ex F1, G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) )
assume A24: j < 1 + k ; :: thesis: ex F1, G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
then A25: j + 1 <= 1 + k by NAT_1:13;
then j + 1 <= n by A15, XXREAL_0:2;
then j < n by NAT_1:13;
then consider F1, G1 being Element of QC-WFF A such that
A26: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A7, A20;
take F1 = F1; :: thesis: ex G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
take G1 = G1; :: thesis: ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
thus ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A18, A20, A22, A24, A25, A26; :: thesis: verum
end;
A27: now :: thesis: ( 1 + k < j implies ex F1, G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) )
A28: j + 1 <= l by A21, NAT_1:13;
assume A29: 1 + k < j ; :: thesis: ex F1, G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
then A30: 1 + k < j + 1 by NAT_1:13;
(1 + k) + 1 <= j by A29, NAT_1:13;
then consider j1 being Nat such that
A31: j = ((1 + k) + 1) + j1 by NAT_1:10;
reconsider j1 = j1 as Nat ;
j - (1 + k) < l - (1 + k) by A21, XREAL_1:9;
then consider F1, G1 being Element of QC-WFF A such that
A32: ( L9 . (1 + j1) = F1 & L9 . ((1 + j1) + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A13, A31, NAT_1:11;
take F1 = F1; :: thesis: ex G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
take G1 = G1; :: thesis: ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
A33: ((1 + j1) + (1 + k)) - (1 + k) = ((1 + j1) + (1 + k)) + (- (1 + k)) ;
(j + 1) - (len L1) = 1 + (j + (- (len L1)))
.= (1 + j1) + 1 by A4, A15, A31, A33, FINSEQ_1:17 ;
hence ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A16, A17, A21, A29, A30, A28, A33, A32, FINSEQ_1:24; :: thesis: verum
end;
now :: thesis: ( j = 1 + k implies ex F1, G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) )
A34: ( j + 1 <= l & (j + 1) - j = (j + 1) + (- j) ) by A21, NAT_1:13;
assume A35: j = 1 + k ; :: thesis: ex F1, G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
then j < (1 + k) + 1 by NAT_1:13;
then consider F1, G1 being Element of QC-WFF A such that
A36: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A7, A8, A20;
take F1 = F1; :: thesis: ex G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
take G1 = G1; :: thesis: ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
1 + k < j + 1 by A35, NAT_1:13;
hence ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A6, A11, A8, A16, A17, A18, A20, A35, A34, A36, FINSEQ_1:24; :: thesis: verum
end;
hence ex G1, H1 being Element of QC-WFF A st
( K . j = G1 & K . (j + 1) = H1 & G1 is_immediate_constituent_of H1 ) by A23, A27, XXREAL_0:1; :: thesis: verum
end;
len (@ F) < len (@ G) by A1, Th54;
hence F <> H by A2, Th54; :: thesis: verum