let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |- A holds
F |= A
let F be Subset of LTLB_WFF; :: thesis: ( F |- A implies F |= A )
assume F |- A ; :: thesis: F |= 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,F,i by Def31;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len f implies F |= 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 |= f /. i
A8: prc f,F,i by A3, A6, A7;

per cases ( f . i in LTL_axioms or f . i in F 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 f . i in LTL_axioms ; :: thesis: F |= f /. i

then A9: f /. i in LTL_axioms by A6, A7, Th1;

per cases ( f /. i is LTL_TAUT_OF_PL or f /. i is axltl1 or f /. i is axltl1a or f /. i is axltl2 or f /. i is axltl3 or f /. i is axltl4 or f /. i is axltl5 or f /. i is axltl6 ) by A9, Th38;

suppose f /. i is LTL_TAUT_OF_PL ; :: thesis: F |= f /. i

hence F |= f /. i by Th34; :: thesis: verum

end;

suppose ( f /. i is axltl1 or f /. i is axltl1a or f /. i is axltl2 or f /. i is axltl3 or f /. i is axltl4 or f /. i is axltl5 or f /. i is axltl6 ) ; :: thesis: F |= f /. i

hence F |= f /. i by Th39; :: thesis: verum

end;

end;

end;

suppose f . i in F ; :: thesis: F |= f /. i

then A10: f /. i in F by A6, A7, Th1;
thus F |= f /. i :: thesis: verum

proof

let M be LTLModel; :: according to LTLAXIO1:def 14 :: thesis: ( M |= F implies M |= f /. i )
assume M |= F ; :: thesis: M |= f /. i
hence M |= f /. i by A10, Def14; :: thesis: verum

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 |= f /. i

then consider j, k being Nat such that
A11: 1 <= j and
A12: j < i and
A13: 1 <= k and
A14: k < i and
A15: ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ;
k <= len f by A7, A14, XXREAL_0:2;
then A16: F |= f /. k by A5, A13, A14;
A17: j <= len f by A7, A12, XXREAL_0:2;

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

suppose f /. j,f /. k MP_rule f /. i ; :: thesis: F |= f /. i

then F |= (f /. j) => (f /. i) by A16, Def21;
hence F |= f /. i by A5, A11, A12, A17, Th25; :: thesis: verum

end;

suppose f /. j,f /. k IND_rule f /. i ; :: thesis: F |= f /. i

then consider A, B being Element of LTLB_WFF such that
A18: f /. j = A => B and
A19: ( f /. k = A => ('X' A) & f /. i = A => ('G' B) ) by Def22;
F |= A => B by A5, A11, A12, A17, A18;
hence F |= f /. i by A16, A19, Th28; :: thesis: verum

end;

end;

end;

suppose ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ; :: thesis: F |= f /. i

then consider j being Nat such that
A20: 1 <= j and
A21: j < i and
A22: f /. j NEX_rule f /. i ;
S₁[j] by A5, A21;
then F |= 'X' (f /. j) by A7, A20, A21, Th26, XXREAL_0:2;
hence F |= f /. i by A22, Def20; :: thesis: verum

end;

end;

end;

end;

end;

A23: for i being Nat holds S₁[i] from NAT_1:sch 4(A4);
f /. (len f) = A by A1, A2, Th1;
hence F |= A by A2, A23; :: thesis: verum