let F, G, H be LTL-formula; ( F is_proper_subformula_of G & G is_proper_subformula_of H implies F is_proper_subformula_of H )
assume that
A1:
F is_subformula_of G
and
A2:
F <> G
and
A3:
G is_subformula_of H
and
A4:
G <> H
; MODELC_2:def 23 F is_proper_subformula_of H
consider m being Nat, L9 being FinSequence such that
A5:
1 <= m
and
A6:
len L9 = m
and
A7:
L9 . 1 = G
and
A8:
L9 . m = H
and
A9:
for k being Nat st 1 <= k & k < m holds
ex H1, F1 being LTL-formula st
( L9 . k = H1 & L9 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
by A3;
consider n being Nat, L being FinSequence such that
A10:
1 <= n
and
A11:
len L = n
and
A12:
L . 1 = F
and
A13:
L . n = G
and
A14:
for k being Nat st 1 <= k & k < n holds
ex H1, F1 being LTL-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
by A1;
1 < n
by A2, A10, A12, A13, XXREAL_0:1;
then
1 + 1 <= n
by NAT_1:13;
then consider k being Nat such that
A15:
n = 2 + k
by NAT_1:10;
reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:15;
thus
F is_subformula_of H
MODELC_2:def 23 F <> Hproof
take l =
(1 + k) + m;
MODELC_2:def 22 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 H1, F1 being LTL-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
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 H1, F1 being LTL-formula st
( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
A16:
((1 + k) + m) - (1 + k) = m
;
m <= m + (1 + k)
by NAT_1:11;
hence
1
<= l
by A5, XXREAL_0:2;
( len K = l & K . 1 = F & K . l = H & ( for k being Nat st 1 <= k & k < l holds
ex H1, F1 being LTL-formula st
( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
(1 + 1) + k = (1 + k) + 1
;
then A17:
1
+ k <= n
by A15, NAT_1:11;
then A18:
len L1 = 1
+ k
by A11, FINSEQ_1:17;
hence A19:
len K = l
by A6, FINSEQ_1:22;
( K . 1 = F & K . l = H & ( for k being Nat st 1 <= k & k < l holds
ex H1, F1 being LTL-formula st
( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
A20:
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 A12, A20;
( K . l = H & ( for k being Nat st 1 <= k & k < l holds
ex H1, F1 being LTL-formula st
( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
(len L1) + 1
<= (len L1) + m
by A5, XREAL_1:7;
then
len L1 < l
by A18, NAT_1:13;
then
K . l = L9 . (l - (len L1))
by A19, FINSEQ_1:24;
hence
K . l = H
by A11, A8, A17, A16, FINSEQ_1:17;
for k being Nat st 1 <= k & k < l holds
ex H1, F1 being LTL-formula st
( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
let j be
Nat;
( 1 <= j & j < l implies ex H1, F1 being LTL-formula st
( K . j = H1 & K . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) )
assume that A22:
1
<= j
and A23:
j < l
;
ex H1, F1 being LTL-formula st
( K . j = H1 & K . (j + 1) = F1 & H1 is_immediate_constituent_of F1 )
j + 0 <= j + 1
by XREAL_1:7;
then A24:
1
<= j + 1
by A22, XXREAL_0:2;
A29:
now ( 1 + k < j implies ex F1, G1 being LTL-formula st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) )A30:
j + 1
<= l
by A23, NAT_1:13;
assume A31:
1
+ k < j
;
ex F1, G1 being LTL-formula st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )then A32:
1
+ k < j + 1
by NAT_1:13;
(1 + k) + 1
<= j
by A31, NAT_1:13;
then consider j1 being
Nat such that A33:
j = ((1 + k) + 1) + j1
by NAT_1:10;
j - (1 + k) < l - (1 + k)
by A23, XREAL_1:9;
then consider F1,
G1 being
LTL-formula such that A34:
(
L9 . (1 + j1) = F1 &
L9 . ((1 + j1) + 1) = G1 &
F1 is_immediate_constituent_of G1 )
by A9, A33, NAT_1:11;
take F1 =
F1;
ex G1 being LTL-formula 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 )A35:
((1 + j1) + (1 + k)) - (1 + k) = ((1 + j1) + (1 + k)) + (- (1 + k))
;
(j + 1) - (len L1) =
1
+ (j + (- (len L1)))
.=
(1 + j1) + 1
by A11, A17, A33, A35, FINSEQ_1:17
;
hence
(
K . j = F1 &
K . (j + 1) = G1 &
F1 is_immediate_constituent_of G1 )
by A18, A19, A23, A31, A32, A30, A35, A34, FINSEQ_1:24;
verum end;
now ( j = 1 + k implies ex F1, G1 being LTL-formula st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) )A36:
(
j + 1
<= l &
(j + 1) - j = (j + 1) + (- j) )
by A23, NAT_1:13;
assume A37:
j = 1
+ k
;
ex F1, G1 being LTL-formula 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
LTL-formula such that A38:
(
L . j = F1 &
L . (j + 1) = G1 &
F1 is_immediate_constituent_of G1 )
by A14, A15, A22;
take F1 =
F1;
ex G1 being LTL-formula 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 A37, NAT_1:13;
hence
(
K . j = F1 &
K . (j + 1) = G1 &
F1 is_immediate_constituent_of G1 )
by A13, A7, A15, A18, A19, A20, A22, A37, A36, A38, FINSEQ_1:24;
verum end;
hence
ex
H1,
F1 being
LTL-formula st
(
K . j = H1 &
K . (j + 1) = F1 &
H1 is_immediate_constituent_of F1 )
by A25, A29, XXREAL_0:1;
verum
end;
assume A39:
F = H
; contradiction
F is_proper_subformula_of G
by A1, A2;
then A40:
len F < len G
by Th32;
G is_proper_subformula_of H
by A3, A4;
hence
contradiction
by A39, A40, Th32; verum