let p, q be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F \/ {p} |- q holds
F |- ('G' p) => q
let F be Subset of LTLB_WFF; :: thesis: ( F \/ {p} |- q implies F |- ('G' p) => q )
set G = F \/ {p};
assume F \/ {p} |- q ; :: thesis: 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 by Def31;
defpred S₁[ 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
S₁[j] ) holds
S₁[i]

proof

let i be Nat; :: thesis: ( ( for j being Nat st j < i holds
S₁[j] ) implies S₁[i] )
assume A5: for j being Nat st j < i holds
S₁[j] ; :: thesis: S₁[i]

per cases ( i = 0 or not i < 1 ) by NAT_1:14;

suppose i = 0 ; :: thesis: S₁[i]

hence S₁[i] ; :: thesis: verum

end;

suppose not i < 1 ; :: thesis: S₁[i]

assume that
A6: 1 <= i and
A7: i <= len f ; :: thesis: F |- ('G' p) => (f /. i)
A8: prc f,F \/ {p},i by A3, A6, A7;

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 A8, Def30;

suppose A9: f . i in LTL_axioms ; :: thesis: F |- ('G' p) => (f /. i)

set t = f /. i;
(f /. i) => (('G' p) => (f /. i)) in LTL_axioms by Th36;
then A10: F |- (f /. i) => (('G' p) => (f /. i)) by Th44;
f /. i in LTL_axioms by A6, A7, A9, Th1;
then F |- f /. i by Th44;
hence F |- ('G' p) => (f /. i) by A10, Th45; :: thesis: verum

end;

suppose A11: f . i in F \/ {p} ; :: thesis: F |- ('G' p) => (f /. i)

per cases ( f . i in F or f . i in {p} ) by A11, XBOOLE_0:def 3;

suppose A12: f . i in F ; :: thesis: F |- ('G' p) => (f /. i)

set t = f /. i;
(f /. i) => (('G' p) => (f /. i)) in LTL_axioms by Th36;
then A13: F |- (f /. i) => (('G' p) => (f /. i)) by Th44;
f /. i in F by A6, A7, A12, Th1;
then F |- f /. i by Th44;
hence F |- ('G' p) => (f /. i) by A13, Th45; :: thesis: verum

end;

suppose A14: f . i in {p} ; :: thesis: F |- ('G' p) => (f /. i)

('G' p) => (p '&&' ('X' ('G' p))) in LTL_axioms by Def18;
then A15: F |- ('G' p) => (p '&&' ('X' ('G' p))) by Th44;
f . i = p by A14, TARSKI:def 1;
then f /. i = p by A6, A7, Th1;
hence F |- ('G' p) => (f /. i) by A15, Th48; :: thesis: verum

end;

end;

end;

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 ) ) ; :: thesis: F |- ('G' p) => (f /. i)

then consider j, k being Nat such that
A16: 1 <= j and
A17: j < i and
A18: 1 <= k and
A19: k < i and
A20: ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ;
j <= len f by A7, A17, XXREAL_0:2;
then A21: F |- ('G' p) => (f /. j) by A5, A16, A17;
k <= len f by A7, A19, XXREAL_0:2;
then A22: F |- ('G' p) => (f /. k) by A5, A18, A19;

per cases ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) by A20;

suppose A23: f /. j,f /. k MP_rule f /. i ; :: thesis: F |- ('G' p) => (f /. i)

set t3 = (('G' p) => ((f /. j) => (f /. i))) => ((('G' p) => (f /. j)) => (('G' p) => (f /. i)));
(('G' p) => ((f /. j) => (f /. i))) => ((('G' p) => (f /. j)) => (('G' p) => (f /. i))) in LTL_axioms by Th37;
then A24: F |- (('G' p) => ((f /. j) => (f /. i))) => ((('G' p) => (f /. j)) => (('G' p) => (f /. i))) by Th44;
F |- ('G' p) => ((f /. j) => (f /. i)) by A22, A23, Def21;
then F |- (('G' p) => (f /. j)) => (('G' p) => (f /. i)) by A24, Th45;
hence F |- ('G' p) => (f /. i) by A21, Th45; :: thesis: verum

end;

suppose f /. j,f /. k IND_rule f /. i ; :: thesis: F |- ('G' p) => (f /. i)

then consider A, B being Element of LTLB_WFF such that
A25: f /. j = A => B and
A26: f /. k = A => ('X' A) and
A27: f /. i = A => ('G' B) by Def22;
set Gp = 'G' p;
set XGp = 'X' ('G' p);
set XA = 'X' A;
set Xq = 'X' q;
set GB = 'G' B;
('G' p) => (p '&&' ('X' ('G' p))) in LTL_axioms by Def18;
then F |- ('G' p) => (p '&&' ('X' ('G' p))) by Th44;
then A28: F |- ('G' p) => ('X' ('G' p)) by Th48;
F |- (('G' p) '&&' A) => ('X' A) by A22, A26, Th50;
then A29: F |- (('G' p) '&&' A) => (('X' ('G' p)) '&&' ('X' A)) by A28, Th52;
F |- (('X' ('G' p)) '&&' ('X' A)) => ('X' (('G' p) '&&' A)) by Th55;
then A30: F |- (('G' p) '&&' A) => ('X' (('G' p) '&&' A)) by A29, Th49;
F |- (('G' p) '&&' A) => B by A21, A25, Th50;
then F |- (('G' p) '&&' A) => ('G' B) by A30, Th47;
hence F |- ('G' p) => (f /. i) by A27, Th51; :: thesis: verum

end;

end;

end;

suppose A31: ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ; :: thesis: F |- ('G' p) => (f /. i)

('G' p) => (p '&&' ('X' ('G' p))) in LTL_axioms by Def18;
then F |- ('G' p) => (p '&&' ('X' ('G' p))) by Th44;
then A33: F |- ('G' p) => ('X' ('G' p)) by Th48;
consider j being Nat, q, r being Element of LTLB_WFF such that
A34: 1 <= j and
A35: j < i and
A36: f /. j NEX_rule f /. i by A31;
('X' (('G' p) => (f /. j))) => (('X' ('G' p)) => ('X' (f /. j))) in LTL_axioms by Def18;
then A37: F |- ('X' (('G' p) => (f /. j))) => (('X' ('G' p)) => ('X' (f /. j))) by Th44;
j <= len f by A7, A35, XXREAL_0:2;
then F |- 'X' (('G' p) => (f /. j)) by A5, A34, A35, Th46;
then A38: F |- ('X' ('G' p)) => ('X' (f /. j)) by A37, Th45;
f /. i = 'X' (f /. j) by A36, Def20;
hence F |- ('G' p) => (f /. i) by A38, A33, Th49; :: thesis: verum

end;

end;

end;

end;

end;

A39: for i being Nat holds S₁[i] from NAT_1:sch 4(A4);
q = f /. (len f) by A1, A2, Th1;
hence F |- ('G' p) => q by A2, A39; :: thesis: verum