let A, B be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F \/ {A} |-0 B holds

F |-0 A => B

let F be Subset of LTLB_WFF; :: thesis: ( F \/ {A} |-0 B implies F |-0 A => B )

assume F \/ {A} |-0 B ; :: thesis: F |-0 A => B

then consider f being FinSequence of LTLB_WFF such that

A1: f . (len f) = B and

A2: 1 <= len f and

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

prc0 f,F \/ {A},i ;

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

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

hence F |-0 A => B by A2, A37; :: thesis: verum

F |-0 A => B

let F be Subset of LTLB_WFF; :: thesis: ( F \/ {A} |-0 B implies F |-0 A => B )

assume F \/ {A} |-0 B ; :: thesis: F |-0 A => B

then consider f being FinSequence of LTLB_WFF such that

A1: f . (len f) = B and

A2: 1 <= len f and

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

prc0 f,F \/ {A},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: F |-0 A => (f /. i)

end;A6: 1 <= i and

A7: i <= len f ; :: thesis: F |-0 A => (f /. i)

per cases
( f . i in LTL0_axioms or f . i in F \/ {A} 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 A8:
f . i in LTL0_axioms
; :: thesis: F |-0 A => (f /. i)

A9:
F |-0 (f /. i) => (A => (f /. i))
by th15, LTLAXIO1:34;

f /. i in LTL0_axioms by A6, A7, A8, Lm1;

then F |-0 f /. i by th10;

hence F |-0 A => (f /. i) by A9, th11a; :: thesis: verum

end;f /. i in LTL0_axioms by A6, A7, A8, Lm1;

then F |-0 f /. i by th10;

hence F |-0 A => (f /. i) by A9, th11a; :: thesis: verum

suppose A10:
f . i in F \/ {A}
; :: thesis: F |-0 A => (f /. i)

end;

per cases
( f . i in F or f . i in {A} )
by A10, XBOOLE_0:def 3;

end;

suppose A11:
f . i in F
; :: thesis: F |-0 A => (f /. i)

A12:
F |-0 (f /. i) => (A => (f /. i))
by th15, LTLAXIO1:34;

f /. i in F by A6, A7, A11, Lm1;

then F |-0 f /. i by th10;

hence F |-0 A => (f /. i) by A12, th11a; :: thesis: verum

end;f /. i in F by A6, A7, A11, Lm1;

then F |-0 f /. i by th10;

hence F |-0 A => (f /. i) by A12, th11a; :: thesis: verum

suppose
f . i in {A}
; :: thesis: F |-0 A => (f /. i)

then
f . i = A
by TARSKI:def 1;

then B1: f /. i = A by A6, A7, Lm1;

A => A is LTL_TAUT_OF_PL by LTLAXIO2:24;

then A => A in LTL_axioms by LTLAXIO1:def 17;

hence F |-0 A => (f /. i) by B1, th15; :: thesis: verum

end;then B1: f /. i = A by A6, A7, Lm1;

A => A is LTL_TAUT_OF_PL by LTLAXIO2:24;

then A => A in LTL_axioms by LTLAXIO1:def 17;

hence F |-0 A => (f /. i) by B1, th15; :: 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 A => (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 A => (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 MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ;

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

then A20: F |-0 A => (f /. j) by A5, A15, A16;

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

then A21: F |-0 A => (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 MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ;

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

then A20: F |-0 A => (f /. j) by A5, A15, A16;

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

then A21: F |-0 A => (f /. k) by A5, A17, A18;

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

end;

suppose A22:
f /. j,f /. k MP_rule f /. i
; :: thesis: F |-0 A => (f /. i)

A23:
F |-0 (A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i)))
by th15, LTLAXIO1:35;

F |-0 (A => (f /. j)) => (A => (f /. i)) by A23, th11a, A21, A22;

hence F |-0 A => (f /. i) by A20, th11a; :: thesis: verum

end;F |-0 (A => (f /. j)) => (A => (f /. i)) by A23, th11a, A21, A22;

hence F |-0 A => (f /. i) by A20, th11a; :: thesis: verum

suppose
f /. j,f /. k MP0_rule f /. i
; :: thesis: F |-0 A => (f /. i)

then consider C, D being Element of LTLB_WFF such that

A24: f /. j = 'G' C and

A25: f /. k = 'G' (C => D) and

A26: f /. i = 'G' D ;

B1: {} LTLB_WFF c= F ;

{} LTLB_WFF |-0 (f /. k) => ((f /. j) => (f /. i)) by th267, LTLAXIO1:60, A24, A25, A26;

then B2: F |-0 (f /. k) => ((f /. j) => (f /. i)) by mon, B1;

(A => (f /. k)) => (((f /. k) => ((f /. j) => (f /. i))) => (A => ((f /. j) => (f /. i)))) is LTL_TAUT_OF_PL by th16;

then (A => (f /. k)) => (((f /. k) => ((f /. j) => (f /. i))) => (A => ((f /. j) => (f /. i)))) in LTL_axioms by LTLAXIO1:def 17;

then F |-0 (A => (f /. k)) => (((f /. k) => ((f /. j) => (f /. i))) => (A => ((f /. j) => (f /. i)))) by th15;

then F |-0 ((f /. k) => ((f /. j) => (f /. i))) => (A => ((f /. j) => (f /. i))) by th11a, A21;

then B3: F |-0 A => ((f /. j) => (f /. i)) by B2, th11a;

(A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i))) is LTL_TAUT_OF_PL by th17;

then (A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i))) in LTL_axioms by LTLAXIO1:def 17;

then F |-0 (A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i))) by th15;

then F |-0 (A => (f /. j)) => (A => (f /. i)) by th11a, B3;

hence F |-0 A => (f /. i) by th11a, A20; :: thesis: verum

end;A24: f /. j = 'G' C and

A25: f /. k = 'G' (C => D) and

A26: f /. i = 'G' D ;

B1: {} LTLB_WFF c= F ;

{} LTLB_WFF |-0 (f /. k) => ((f /. j) => (f /. i)) by th267, LTLAXIO1:60, A24, A25, A26;

then B2: F |-0 (f /. k) => ((f /. j) => (f /. i)) by mon, B1;

(A => (f /. k)) => (((f /. k) => ((f /. j) => (f /. i))) => (A => ((f /. j) => (f /. i)))) is LTL_TAUT_OF_PL by th16;

then (A => (f /. k)) => (((f /. k) => ((f /. j) => (f /. i))) => (A => ((f /. j) => (f /. i)))) in LTL_axioms by LTLAXIO1:def 17;

then F |-0 (A => (f /. k)) => (((f /. k) => ((f /. j) => (f /. i))) => (A => ((f /. j) => (f /. i)))) by th15;

then F |-0 ((f /. k) => ((f /. j) => (f /. i))) => (A => ((f /. j) => (f /. i))) by th11a, A21;

then B3: F |-0 A => ((f /. j) => (f /. i)) by B2, th11a;

(A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i))) is LTL_TAUT_OF_PL by th17;

then (A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i))) in LTL_axioms by LTLAXIO1:def 17;

then F |-0 (A => ((f /. j) => (f /. i))) => ((A => (f /. j)) => (A => (f /. i))) by th15;

then F |-0 (A => (f /. j)) => (A => (f /. i)) by th11a, B3;

hence F |-0 A => (f /. i) by th11a, A20; :: thesis: verum

suppose
f /. j,f /. k IND0_rule f /. i
; :: thesis: F |-0 A => (f /. i)

then consider C, D being Element of LTLB_WFF such that

A24: f /. j = 'G' (C => D) and

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

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

(A => (f /. j)) => ((A => (f /. k)) => (A => ((f /. j) '&&' (f /. k)))) is LTL_TAUT_OF_PL by LTLAXIO2:40;

then (A => (f /. j)) => ((A => (f /. k)) => (A => ((f /. j) '&&' (f /. k)))) in LTL_axioms by LTLAXIO1:def 17;

then F |-0 (A => (f /. j)) => ((A => (f /. k)) => (A => ((f /. j) '&&' (f /. k)))) by th15;

then F |-0 (A => (f /. k)) => (A => ((f /. j) '&&' (f /. k))) by th11a, A20;

then B10: F |-0 A => ((f /. j) '&&' (f /. k)) by th11a, A21;

B12: {} LTLB_WFF c= F ;

{} LTLB_WFF |- (f /. j) => ((f /. k) => (f /. i)) by th20, A24, A25, A26;

then {} LTLB_WFF |- ((f /. j) '&&' (f /. k)) => (f /. i) by LTLAXIO1:48;

then B11: F |-0 ((f /. j) '&&' (f /. k)) => (f /. i) by mon, B12, th267;

(A => ((f /. j) '&&' (f /. k))) => ((((f /. j) '&&' (f /. k)) => (f /. i)) => (A => (f /. i))) is LTL_TAUT_OF_PL by th16;

then (A => ((f /. j) '&&' (f /. k))) => ((((f /. j) '&&' (f /. k)) => (f /. i)) => (A => (f /. i))) in LTL_axioms by LTLAXIO1:def 17;

then F |-0 (A => ((f /. j) '&&' (f /. k))) => ((((f /. j) '&&' (f /. k)) => (f /. i)) => (A => (f /. i))) by th15;

then F |-0 (((f /. j) '&&' (f /. k)) => (f /. i)) => (A => (f /. i)) by th11a, B10;

hence F |-0 A => (f /. i) by th11a, B11; :: thesis: verum

end;A24: f /. j = 'G' (C => D) and

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

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

(A => (f /. j)) => ((A => (f /. k)) => (A => ((f /. j) '&&' (f /. k)))) is LTL_TAUT_OF_PL by LTLAXIO2:40;

then (A => (f /. j)) => ((A => (f /. k)) => (A => ((f /. j) '&&' (f /. k)))) in LTL_axioms by LTLAXIO1:def 17;

then F |-0 (A => (f /. j)) => ((A => (f /. k)) => (A => ((f /. j) '&&' (f /. k)))) by th15;

then F |-0 (A => (f /. k)) => (A => ((f /. j) '&&' (f /. k))) by th11a, A20;

then B10: F |-0 A => ((f /. j) '&&' (f /. k)) by th11a, A21;

B12: {} LTLB_WFF c= F ;

{} LTLB_WFF |- (f /. j) => ((f /. k) => (f /. i)) by th20, A24, A25, A26;

then {} LTLB_WFF |- ((f /. j) '&&' (f /. k)) => (f /. i) by LTLAXIO1:48;

then B11: F |-0 ((f /. j) '&&' (f /. k)) => (f /. i) by mon, B12, th267;

(A => ((f /. j) '&&' (f /. k))) => ((((f /. j) '&&' (f /. k)) => (f /. i)) => (A => (f /. i))) is LTL_TAUT_OF_PL by th16;

then (A => ((f /. j) '&&' (f /. k))) => ((((f /. j) '&&' (f /. k)) => (f /. i)) => (A => (f /. i))) in LTL_axioms by LTLAXIO1:def 17;

then F |-0 (A => ((f /. j) '&&' (f /. k))) => ((((f /. j) '&&' (f /. k)) => (f /. i)) => (A => (f /. i))) by th15;

then F |-0 (((f /. j) '&&' (f /. k)) => (f /. i)) => (A => (f /. i)) by th11a, B10;

hence F |-0 A => (f /. i) by th11a, B11; :: 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 A => (f /. i)

( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) ; :: thesis: F |-0 A => (f /. i)

then consider j being Nat, q, r being Element of LTLB_WFF such that

A32: 1 <= j and

A33: j < i and

A34: ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ;

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

then B4a: F |-0 A => (f /. j) by A5, A32, A33;

end;A32: 1 <= j and

A33: j < i and

A34: ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ;

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

then B4a: F |-0 A => (f /. j) by A5, A32, A33;

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

end;

suppose
f /. j NEX0_rule f /. i
; :: thesis: F |-0 A => (f /. i)

then consider C being Element of LTLB_WFF such that

A24: f /. j = 'G' C and

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

B8: {} LTLB_WFF c= F ;

{} LTLB_WFF |-0 (f /. j) => (f /. i) by th19, th267, A24, A26;

then B9: F |-0 (f /. j) => (f /. i) by mon, B8;

(A => (f /. j)) => (((f /. j) => (f /. i)) => (A => (f /. i))) is LTL_TAUT_OF_PL by th16;

then (A => (f /. j)) => (((f /. j) => (f /. i)) => (A => (f /. i))) in LTL_axioms by LTLAXIO1:def 17;

then F |-0 (A => (f /. j)) => (((f /. j) => (f /. i)) => (A => (f /. i))) by th15;

then F |-0 ((f /. j) => (f /. i)) => (A => (f /. i)) by th11a, B4a;

hence F |-0 A => (f /. i) by B9, th11a; :: thesis: verum

end;A24: f /. j = 'G' C and

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

B8: {} LTLB_WFF c= F ;

{} LTLB_WFF |-0 (f /. j) => (f /. i) by th19, th267, A24, A26;

then B9: F |-0 (f /. j) => (f /. i) by mon, B8;

(A => (f /. j)) => (((f /. j) => (f /. i)) => (A => (f /. i))) is LTL_TAUT_OF_PL by th16;

then (A => (f /. j)) => (((f /. j) => (f /. i)) => (A => (f /. i))) in LTL_axioms by LTLAXIO1:def 17;

then F |-0 (A => (f /. j)) => (((f /. j) => (f /. i)) => (A => (f /. i))) by th15;

then F |-0 ((f /. j) => (f /. i)) => (A => (f /. i)) by th11a, B4a;

hence F |-0 A => (f /. i) by B9, th11a; :: thesis: verum

suppose
f /. j REFL0_rule f /. i
; :: thesis: F |-0 A => (f /. i)

then B6:
F |-0 A => ('G' (f /. i))
by B4, A5, A32, A33;

B5: {} LTLB_WFF c= F ;

{} LTLB_WFF |-0 ('G' (f /. i)) => (f /. i) by th267, th18;

then B7: F |-0 ('G' (f /. i)) => (f /. i) by mon, B5;

(A => ('G' (f /. i))) => ((('G' (f /. i)) => (f /. i)) => (A => (f /. i))) is LTL_TAUT_OF_PL by th16;

then (A => ('G' (f /. i))) => ((('G' (f /. i)) => (f /. i)) => (A => (f /. i))) in LTL_axioms by LTLAXIO1:def 17;

then F |-0 (A => ('G' (f /. i))) => ((('G' (f /. i)) => (f /. i)) => (A => (f /. i))) by th15;

then F |-0 (('G' (f /. i)) => (f /. i)) => (A => (f /. i)) by B6, th11a;

hence F |-0 A => (f /. i) by th11a, B7; :: thesis: verum

end;B5: {} LTLB_WFF c= F ;

{} LTLB_WFF |-0 ('G' (f /. i)) => (f /. i) by th267, th18;

then B7: F |-0 ('G' (f /. i)) => (f /. i) by mon, B5;

(A => ('G' (f /. i))) => ((('G' (f /. i)) => (f /. i)) => (A => (f /. i))) is LTL_TAUT_OF_PL by th16;

then (A => ('G' (f /. i))) => ((('G' (f /. i)) => (f /. i)) => (A => (f /. i))) in LTL_axioms by LTLAXIO1:def 17;

then F |-0 (A => ('G' (f /. i))) => ((('G' (f /. i)) => (f /. i)) => (A => (f /. i))) by th15;

then F |-0 (('G' (f /. i)) => (f /. i)) => (A => (f /. i)) by B6, th11a;

hence F |-0 A => (f /. i) by th11a, B7; :: thesis: verum

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

hence F |-0 A => B by A2, A37; :: thesis: verum