let A be Element of LTLB_WFF ; :: thesis: ( {} LTLB_WFF |- A implies {} LTLB_WFF |-0 A )
assume {} LTLB_WFF |- A ; :: thesis:
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 S1[ 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
S1[j] ) holds
S1[i]
proof
let i be Nat; :: thesis: ( ( 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] ; :: thesis: S1[i]
per cases ( i = 0 or not i < 1 ) by NAT_1:14;
suppose not i < 1 ; :: thesis: S1[i]
assume that
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 ;
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)
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 ;
then A20: {} LTLB_WFF |-0 'G' (f /. j) by A5, A15, A16;
k <= len f by ;
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;
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;
end;
end;
suppose ex j being Nat st
( 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 ;
then {} LTLB_WFF |-0 'G' (f /. j) by A5, A15, A16;
hence {} LTLB_WFF |-0 'G' (f /. i) by ; :: thesis: verum
end;
end;
end;
end;
end;
A37: for i being Nat holds S1[i] from A = f /. (len f) by A1, A2, Lm1;
then {} LTLB_WFF |-0 'G' A by ;
hence {} LTLB_WFF |-0 A by th9; :: thesis: verum