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 S_{1}[ 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

S_{1}[j] ) holds

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

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

hence F |=0 A by A2, A22; :: thesis: verum

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 S

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

S

S

proof

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

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

end;

( 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

end;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;assume M |=0 F ; :: thesis: M |=0 f /. i

hence M |=0 f /. i by A9; :: 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 MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) ; :: thesis: F |=0 f /. i

( 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 A7, A13, XXREAL_0:2;

then A15a: F |=0 f /. k by A5, A12, A13;

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

B5: F |=0 f /. j by A5, A10, A11, A16;

end;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 A7, A13, XXREAL_0:2;

then A15a: F |=0 f /. k by A5, A12, A13;

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

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;

end;

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;hence F |=0 f /. i by A5, A10, A11, A16, Th3; :: thesis: verum

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

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 A15a, A18, Th7; :: thesis: verum

end;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 A15a, A18, Th7; :: thesis: verum

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

( 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 A7, A20, XXREAL_0:2;

end;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 A7, A20, XXREAL_0:2;

per cases
( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i )
by A21;

end;

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

hence F |=0 A by A2, A22; :: thesis: verum