let A be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |-0 A holds
F |=0 A

let F be Subset of LTLB_WFF; :: thesis: ( F |-0 A implies F |=0 A )
assume F |-0 A ; :: thesis: F |=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
prc0 f,F,i ;
defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= len f implies F |=0 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: F |=0 f /. i
per cases ( f . i in LTL0_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 MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) )
by A3, A6, A7, Def29;
suppose f . i in F ; :: thesis: F |=0 f /. i
then A9: f /. i in F by A6, A7, Lm1;
thus F |=0 f /. i :: thesis: verum
proof
let M be LTLModel; :: according to LTLAXIO5:def 3 :: thesis: ( M |=0 F implies M |=0 f /. i )
assume M |=0 F ; :: thesis: M |=0 f /. i
hence M |=0 f /. i by A9; :: 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 MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) ; :: thesis: F |=0 f /. i
then consider j, k being Nat such that
A10: 1 <= j and
A11: j < i and
A12: 1 <= k and
A13: k < i and
A14: ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ;
A15: k <= len f by ;
then A15a: F |=0 f /. k by A5, A12, A13;
A16: j <= len f by ;
B5: F |=0 f /. j by A5, A10, A11, A16;
per cases ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) by A14;
suppose f /. j,f /. k MP_rule f /. i ; :: thesis: F |=0 f /. i
then F |=0 (f /. j) => (f /. i) by A15, A5, A12, A13;
hence F |=0 f /. i by A5, A10, A11, A16, Th3; :: thesis: verum
end;
suppose f /. j,f /. k MP0_rule f /. i ; :: thesis: F |=0 f /. i
then consider A, B being Element of LTLB_WFF such that
B7: f /. j = 'G' A and
B8: f /. k = 'G' (A => B) and
B9: f /. i = 'G' B ;
thus F |=0 f /. i by Th4, B7, B8, B9, A15a, B5; :: thesis: verum
end;
suppose f /. j,f /. k IND0_rule f /. i ; :: thesis: F |=0 f /. i
then consider A, B being Element of LTLB_WFF such that
A17: f /. j = 'G' (A => B) and
A18: ( f /. k = 'G' (A => ('X' A)) & f /. i = 'G' (A => ('G' B)) ) ;
F |=0 'G' (A => B) by A5, A10, A11, A16, A17;
hence F |=0 f /. i by ; :: thesis: verum
end;
end;
end;
suppose ex j being Nat st
( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) ; :: thesis: F |=0 f /. i
then consider j being Nat such that
A19: 1 <= j and
A20: j < i and
A21: ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ;
B11: j <= len f by ;
per cases ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) by A21;
suppose f /. j NEX0_rule f /. i ; :: thesis: F |=0 f /. i
then consider A, B being Element of LTLB_WFF such that
B7: f /. j = 'G' A and
B9: f /. i = 'G' ('X' A) ;
thus F |=0 f /. i by Th5, B7, B9, B11, A5, A20, A19; :: thesis: verum
end;
suppose f /. j REFL0_rule f /. i ; :: thesis: F |=0 f /. i
hence F |=0 f /. i by Th6, B11, A5, A20, A19; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
A22: for i being Nat holds S1[i] from f /. (len f) = A by A1, A2, Lm1;
hence F |=0 A by ; :: thesis: verum