let p, q be Element of LTLB_WFF ; for F being Subset of LTLB_WFF st F \/ {p} |- q holds
F |- ('G' p) => q
let F be Subset of LTLB_WFF; ( F \/ {p} |- q implies F |- ('G' p) => q )
set G = F \/ {p};
assume
F \/ {p} |- q
; F |- ('G' p) => q
then consider f being FinSequence of LTLB_WFF such that
A1:
f . (len f) = q
and
A2:
1 <= len f
and
A3:
for i being Nat st 1 <= i & i <= len f holds
prc f,F \/ {p},i
;
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len f implies F |- ('G' p) => (f /. $1) );
A4:
for i being Nat st ( for j being Nat st j < i holds
S1[j] ) holds
S1[i]
proof
let i be
Nat;
( ( for j being Nat st j < i holds
S1[j] ) implies S1[i] )
assume A5:
for
j being
Nat st
j < i holds
S1[
j]
;
S1[i]
per cases
( i = 0 or not i < 1 )
by NAT_1:14;
suppose
not
i < 1
;
S1[i]assume that A6:
1
<= i
and A7:
i <= len f
;
F |- ('G' p) => (f /. i)per cases
( f . i in LTL_axioms or f . i in F \/ {p} or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) )
by A3, A6, A7, Def29;
suppose
ex
j,
k being
Nat st
( 1
<= j &
j < i & 1
<= k &
k < i & (
f /. j,
f /. k MP_rule f /. i or
f /. j,
f /. k IND_rule f /. i ) )
;
F |- ('G' p) => (f /. i)then consider j,
k being
Nat such that A15:
1
<= j
and A16:
j < i
and A17:
1
<= k
and A18:
k < i
and A19:
(
f /. j,
f /. k MP_rule f /. i or
f /. j,
f /. k IND_rule f /. i )
;
j <= len f
by A7, A16, XXREAL_0:2;
then A20:
F |- ('G' p) => (f /. j)
by A5, A15, A16;
k <= len f
by A7, A18, XXREAL_0:2;
then A21:
F |- ('G' p) => (f /. k)
by A5, A17, A18;
end; suppose A30:
ex
j being
Nat st
( 1
<= j &
j < i &
f /. j NEX_rule f /. i )
;
F |- ('G' p) => (f /. i)
('G' p) => (p '&&' ('X' ('G' p))) in LTL_axioms
by Def17;
then
F |- ('G' p) => (p '&&' ('X' ('G' p)))
by Th42;
then A31:
F |- ('G' p) => ('X' ('G' p))
by Th46;
consider j being
Nat,
q,
r being
Element of
LTLB_WFF such that A32:
1
<= j
and A33:
j < i
and A34:
f /. j NEX_rule f /. i
by A30;
('X' (('G' p) => (f /. j))) => (('X' ('G' p)) => ('X' (f /. j))) in LTL_axioms
by Def17;
then A35:
F |- ('X' (('G' p) => (f /. j))) => (('X' ('G' p)) => ('X' (f /. j)))
by Th42;
j <= len f
by A7, A33, XXREAL_0:2;
then
F |- 'X' (('G' p) => (f /. j))
by A5, A32, A33, Th44;
then A36:
F |- ('X' ('G' p)) => ('X' (f /. j))
by A35, Th43;
f /. i = 'X' (f /. j)
by A34;
hence
F |- ('G' p) => (f /. i)
by A36, A31, Th47;
verum end; end; end; end;
end;
A37:
for i being Nat holds S1[i]
from NAT_1:sch 4(A4);
q = f /. (len f)
by A1, A2, Lm1;
hence
F |- ('G' p) => q
by A2, A37; verum