let F, G be LTL-formula; ( ( G is conjunctive or G is disjunctive or G is Until or G is Release ) & F is_proper_subformula_of G & not F is_subformula_of the_left_argument_of G implies F is_subformula_of the_right_argument_of G )
assume that
A1:
( G is conjunctive or G is disjunctive or G is Until or G is Release )
and
A2:
F is_subformula_of G
and
A3:
F <> G
; MODELC_2:def 23 ( F is_subformula_of the_left_argument_of G or F is_subformula_of the_right_argument_of G )
consider n being Nat, L being FinSequence such that
A4:
1 <= n
and
A5:
len L = n
and
A6:
L . 1 = F
and
A7:
L . n = G
and
A8:
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 A2;
1 < n
by A3, A4, A6, A7, XXREAL_0:1;
then
1 + 1 <= n
by NAT_1:13;
then consider k being Nat such that
A9:
n = 2 + k
by NAT_1:10;
reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:15;
(1 + 1) + k = (1 + k) + 1
;
then
1 + k < n
by A9, NAT_1:13;
then consider H1, G1 being LTL-formula such that
A10:
L . (1 + k) = H1
and
A11:
( L . ((1 + k) + 1) = G1 & H1 is_immediate_constituent_of G1 )
by A8, NAT_1:11;
F is_subformula_of H1
proof
take m = 1
+ k;
MODELC_2:def 22 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 H1, F1 being LTL-formula st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
take
L1
;
( 1 <= m & len L1 = m & L1 . 1 = F & L1 . m = H1 & ( for k being Nat st 1 <= k & k < m holds
ex H1, F1 being LTL-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus A12:
1
<= m
by NAT_1:11;
( len L1 = m & L1 . 1 = F & L1 . m = H1 & ( for k being Nat st 1 <= k & k < m holds
ex H1, F1 being LTL-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
1
+ k <= (1 + k) + 1
by NAT_1:11;
hence
len L1 = m
by A5, A9, FINSEQ_1:17;
( L1 . 1 = F & L1 . m = H1 & ( for k being Nat st 1 <= k & k < m holds
ex H1, F1 being LTL-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
A13:
now for j being Nat st 1 <= j & j <= m holds
L1 . j = L . jend;
hence
L1 . 1
= F
by A6, A12;
( L1 . m = H1 & ( for k being Nat st 1 <= k & k < m holds
ex H1, F1 being LTL-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) )
thus
L1 . m = H1
by A10, A12, A13;
for k being Nat st 1 <= k & k < m holds
ex H1, F1 being LTL-formula st
( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 )
let j be
Nat;
( 1 <= j & j < m implies ex H1, F1 being LTL-formula st
( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) )
assume that A14:
1
<= j
and A15:
j < m
;
ex H1, F1 being LTL-formula st
( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 )
m <= m + 1
by NAT_1:11;
then
j < n
by A9, A15, XXREAL_0:2;
then consider F1,
G1 being
LTL-formula such that A16:
(
L . j = F1 &
L . (j + 1) = G1 &
F1 is_immediate_constituent_of G1 )
by A8, A14;
take
F1
;
ex F1 being LTL-formula st
( L1 . j = F1 & L1 . (j + 1) = F1 & F1 is_immediate_constituent_of F1 )
take
G1
;
( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
( 1
<= 1
+ j &
j + 1
<= m )
by A14, A15, NAT_1:13;
hence
(
L1 . j = F1 &
L1 . (j + 1) = G1 &
F1 is_immediate_constituent_of G1 )
by A13, A14, A15, A16;
verum
end;
hence
( F is_subformula_of the_left_argument_of G or F is_subformula_of the_right_argument_of G )
by A1, A7, A9, A11, Th22, Th23, Th24, Th25; verum