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 ;

defpred S_{1}[ 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_{1}[j] ) holds

S_{1}[i]
_{1}[i]
from NAT_1:sch 4(A4);

q = f /. (len f) by A1, A2, Lm1;

hence F |- ('G' p) => q by A2, A37; :: thesis: verum

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 ;

defpred S

A4: for i being Nat st ( for j being Nat st j < i holds

S

S

proof

A37:
for i being Nat holds S
let i be Nat; :: thesis: ( ( for j being Nat st j < i holds

S_{1}[j] ) implies S_{1}[i] )

assume A5: for j being Nat st j < i holds

S_{1}[j]
; :: thesis: S_{1}[i]

end;S

assume A5: for j being Nat st j < i holds

S

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

end;

suppose
not i < 1
; :: thesis: S_{1}[i]

assume that

A6: 1 <= i and

A7: i <= len f ; :: thesis: F |- ('G' p) => (f /. i)

end;A6: 1 <= i and

A7: i <= len f ; :: thesis: 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;

end;

( 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 A8:
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 Th34;

then A9: F |- (f /. i) => (('G' p) => (f /. i)) by Th42;

f /. i in LTL_axioms by A6, A7, A8, Lm1;

then F |- f /. i by Th42;

hence F |- ('G' p) => (f /. i) by A9, Th43; :: thesis: verum

end;(f /. i) => (('G' p) => (f /. i)) in LTL_axioms by Th34;

then A9: F |- (f /. i) => (('G' p) => (f /. i)) by Th42;

f /. i in LTL_axioms by A6, A7, A8, Lm1;

then F |- f /. i by Th42;

hence F |- ('G' p) => (f /. i) by A9, Th43; :: thesis: verum

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

end;

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

end;

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

set t = f /. i;

(f /. i) => (('G' p) => (f /. i)) in LTL_axioms by Th34;

then A12: F |- (f /. i) => (('G' p) => (f /. i)) by Th42;

f /. i in F by A6, A7, A11, Lm1;

then F |- f /. i by Th42;

hence F |- ('G' p) => (f /. i) by A12, Th43; :: thesis: verum

end;(f /. i) => (('G' p) => (f /. i)) in LTL_axioms by Th34;

then A12: F |- (f /. i) => (('G' p) => (f /. i)) by Th42;

f /. i in F by A6, A7, A11, Lm1;

then F |- f /. i by Th42;

hence F |- ('G' p) => (f /. i) by A12, Th43; :: thesis: verum

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

('G' p) => (p '&&' ('X' ('G' p))) in LTL_axioms
by Def17;

then A14: F |- ('G' p) => (p '&&' ('X' ('G' p))) by Th42;

f . i = p by A13, TARSKI:def 1;

then f /. i = p by A6, A7, Lm1;

hence F |- ('G' p) => (f /. i) by A14, Th46; :: thesis: verum

end;then A14: F |- ('G' p) => (p '&&' ('X' ('G' p))) by Th42;

f . i = p by A13, TARSKI:def 1;

then f /. i = p by A6, A7, Lm1;

hence F |- ('G' p) => (f /. i) by A14, Th46; :: thesis: verum

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)

( 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

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;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;

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

end;

suppose A22:
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 Th35;

then A23: F |- (('G' p) => ((f /. j) => (f /. i))) => ((('G' p) => (f /. j)) => (('G' p) => (f /. i))) by Th42;

F |- ('G' p) => ((f /. j) => (f /. i)) by A21, A22;

then F |- (('G' p) => (f /. j)) => (('G' p) => (f /. i)) by A23, Th43;

hence F |- ('G' p) => (f /. i) by A20, Th43; :: thesis: verum

end;(('G' p) => ((f /. j) => (f /. i))) => ((('G' p) => (f /. j)) => (('G' p) => (f /. i))) in LTL_axioms by Th35;

then A23: F |- (('G' p) => ((f /. j) => (f /. i))) => ((('G' p) => (f /. j)) => (('G' p) => (f /. i))) by Th42;

F |- ('G' p) => ((f /. j) => (f /. i)) by A21, A22;

then F |- (('G' p) => (f /. j)) => (('G' p) => (f /. i)) by A23, Th43;

hence F |- ('G' p) => (f /. i) by A20, Th43; :: thesis: verum

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

A24: f /. j = A => B and

A25: f /. k = A => ('X' A) and

A26: f /. i = A => ('G' B) ;

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 Def17;

then F |- ('G' p) => (p '&&' ('X' ('G' p))) by Th42;

then A27: F |- ('G' p) => ('X' ('G' p)) by Th46;

F |- (('G' p) '&&' A) => ('X' A) by A21, A25, Th48;

then A28: F |- (('G' p) '&&' A) => (('X' ('G' p)) '&&' ('X' A)) by A27, Th50;

F |- (('X' ('G' p)) '&&' ('X' A)) => ('X' (('G' p) '&&' A)) by Th53;

then A29: F |- (('G' p) '&&' A) => ('X' (('G' p) '&&' A)) by A28, Th47;

F |- (('G' p) '&&' A) => B by A20, A24, Th48;

then F |- (('G' p) '&&' A) => ('G' B) by A29, Th45;

hence F |- ('G' p) => (f /. i) by A26, Th49; :: thesis: verum

end;A24: f /. j = A => B and

A25: f /. k = A => ('X' A) and

A26: f /. i = A => ('G' B) ;

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 Def17;

then F |- ('G' p) => (p '&&' ('X' ('G' p))) by Th42;

then A27: F |- ('G' p) => ('X' ('G' p)) by Th46;

F |- (('G' p) '&&' A) => ('X' A) by A21, A25, Th48;

then A28: F |- (('G' p) '&&' A) => (('X' ('G' p)) '&&' ('X' A)) by A27, Th50;

F |- (('X' ('G' p)) '&&' ('X' A)) => ('X' (('G' p) '&&' A)) by Th53;

then A29: F |- (('G' p) '&&' A) => ('X' (('G' p) '&&' A)) by A28, Th47;

F |- (('G' p) '&&' A) => B by A20, A24, Th48;

then F |- (('G' p) '&&' A) => ('G' B) by A29, Th45;

hence F |- ('G' p) => (f /. i) by A26, Th49; :: thesis: verum

suppose A30:
ex j being Nat st

( 1 <= j & j < i & f /. j NEX_rule f /. i ) ; :: thesis: F |- ('G' p) => (f /. i)

( 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 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; :: thesis: verum

end;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; :: thesis: verum

q = f /. (len f) by A1, A2, Lm1;

hence F |- ('G' p) => q by A2, A37; :: thesis: verum