let A be QC-alphabet ; 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; ( 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
; 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
QC_LANG2:def 21 F <> Hproof
take l =
(1 + k) + m;
QC_LANG2:def 20 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;
( 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;
( 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;
( 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 for j being Nat st 1 <= j & j <= 1 + k holds
K . j = L . jend;
1
<= 1
+ k
by NAT_1:11;
hence
K . 1
= F
by A5, A18;
( 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;
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;
( 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
;
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;
A27:
now ( 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
;
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;
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;
( 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;
verum end;
now ( 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
;
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;
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;
( 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;
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;
verum
end;
len (@ F) < len (@ G)
by A1, Th54;
hence
F <> H
by A2, Th54; verum