let A be Element of LTLB_WFF ; :: thesis: ( {} LTLB_WFF |- A implies {} LTLB_WFF |-0 A )

assume {} LTLB_WFF |- A ; :: thesis: {} LTLB_WFF |-0 A

then consider f being FinSequence of LTLB_WFF such that

A1: f . (len f) = A and

A2: 1 <= len f and

A3: for i being Nat st 1 <= i & i <= len f holds

prc f, {} LTLB_WFF,i ;

defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= len f implies {} LTLB_WFF |-0 'G' (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);

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

then {} LTLB_WFF |-0 'G' A by A37, A2;

hence {} LTLB_WFF |-0 A by th9; :: thesis: verum

assume {} LTLB_WFF |- A ; :: thesis: {} LTLB_WFF |-0 A

then consider f being FinSequence of LTLB_WFF such that

A1: f . (len f) = A and

A2: 1 <= len f and

A3: for i being Nat st 1 <= i & i <= len f holds

prc f, {} LTLB_WFF,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: {} LTLB_WFF |-0 'G' (f /. i)

end;A6: 1 <= i and

A7: i <= len f ; :: thesis: {} LTLB_WFF |-0 'G' (f /. i)

per cases
( f . i in LTL_axioms or f . i in {} LTLB_WFF 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, LTLAXIO1:def 29;

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, LTLAXIO1:def 29;

suppose
f . i in LTL_axioms
; :: thesis: {} LTLB_WFF |-0 'G' (f /. i)

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

then 'G' (f /. i) in LTL0_axioms ;

hence {} LTLB_WFF |-0 'G' (f /. i) by th10; :: thesis: verum

end;then 'G' (f /. i) in LTL0_axioms ;

hence {} LTLB_WFF |-0 'G' (f /. i) by th10; :: 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: {} LTLB_WFF |-0 'G' (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: {} LTLB_WFF |-0 'G' (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: {} LTLB_WFF |-0 'G' (f /. j) by A5, A15, A16;

k <= len f by A7, A18, XXREAL_0:2;

then A21: {} LTLB_WFF |-0 'G' (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: {} LTLB_WFF |-0 'G' (f /. j) by A5, A15, A16;

k <= len f by A7, A18, XXREAL_0:2;

then A21: {} LTLB_WFF |-0 'G' (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
f /. j,f /. k IND_rule f /. i
; :: thesis: {} LTLB_WFF |-0 'G' (f /. i)

then consider B, C being Element of LTLB_WFF such that

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

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

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

thus {} LTLB_WFF |-0 'G' (f /. i) by A24, A25, A26, th13, A20, A21; :: thesis: verum

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

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

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

thus {} LTLB_WFF |-0 'G' (f /. i) by A24, A25, A26, th13, A20, A21; :: thesis: verum

suppose
ex j being Nat st

( 1 <= j & j < i & f /. j NEX_rule f /. i ) ; :: thesis: {} LTLB_WFF |-0 'G' (f /. i)

( 1 <= j & j < i & f /. j NEX_rule f /. i ) ; :: thesis: {} LTLB_WFF |-0 'G' (f /. i)

then consider j being Nat such that

A15: 1 <= j and

A16: j < i and

A19: f /. j NEX_rule f /. i ;

j <= len f by A7, A16, XXREAL_0:2;

then {} LTLB_WFF |-0 'G' (f /. j) by A5, A15, A16;

hence {} LTLB_WFF |-0 'G' (f /. i) by A19, th12; :: thesis: verum

end;A15: 1 <= j and

A16: j < i and

A19: f /. j NEX_rule f /. i ;

j <= len f by A7, A16, XXREAL_0:2;

then {} LTLB_WFF |-0 'G' (f /. j) by A5, A15, A16;

hence {} LTLB_WFF |-0 'G' (f /. i) by A19, th12; :: thesis: verum

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

then {} LTLB_WFF |-0 'G' A by A37, A2;

hence {} LTLB_WFF |-0 A by th9; :: thesis: verum