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

F |-0 A

let F be finite Subset of LTLB_WFF; :: thesis: ( F |=0 A implies F |-0 A )

assume Z1: F |=0 A ; :: thesis: F |-0 A

F |-0 A

let F be finite Subset of LTLB_WFF; :: thesis: ( F |=0 A implies F |-0 A )

assume Z1: F |=0 A ; :: thesis: F |-0 A

per cases
( F is empty or not F is empty )
;

end;

suppose S2:
not F is empty
; :: thesis: F |-0 A

consider f being FinSequence such that

A4: ( rng f = F & f is one-to-one ) by FINSEQ_4:58;

reconsider f = f as FinSequence of LTLB_WFF by A4, FINSEQ_1:def 4;

A6: 1 <= len f by RELAT_1:38, A4, FINSEQ_1:20, S2;

then 1 <= len (implications (f,A)) by imps;

then A7: (implications (f,A)) /. 1 = (implications (f,A)) . 1 by FINSEQ_4:15;

AA: 1 in dom f by A6, FINSEQ_3:25;

defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= len f implies rng (f /^ $1) |=0 (implications (f,A)) /. $1 );

rng (f | 1) = rng <*(f . 1)*> by FINSEQ_5:20, RELAT_1:38, A4, S2

.= rng <*(f /. 1)*> by PARTFUN1:def 6, AA ;

then A8: (rng (f /^ 1)) \/ {(f /. 1)} = (rng (f | 1)) \/ (rng (f /^ 1)) by FINSEQ_1:38

.= rng ((f | 1) ^ (f /^ 1)) by FINSEQ_1:31

.= rng f by RFINSEQ:8 ;

A9: len (implications (f,A)) = len f by A6, imps;

_{1}[ 0 ]
;

for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A19, A10);

then rng (f /^ (len f)) |=0 (implications (f,A)) /. (len f) by A6;

then {} LTLB_WFF |=0 (implications (f,A)) /. (len f) by RFINSEQ:27, RELAT_1:38;

then D2: {} LTLB_WFF |- (implications (f,A)) /. (len f) by LTLAXIO4:33, th262b, th264p;

defpred S_{2}[ Nat] means ( $1 < len f implies rng f |-0 (implications (f,A)) /. ((len f) -' $1) );

then D3: rng f |-0 (implications (f,A)) /. (len f) by mon, D2, th267;

(len f) - 0 >= 1 by RELAT_1:38, A4, S2, FINSEQ_1:20;

then A33: S_{2}[ 0 ]
by D3, XREAL_0:def 2;

A34: for i being Nat holds S_{2}[i]
from NAT_1:sch 2(A33, A21);

1 + (- 1) <= (len f) + (- 1) by XREAL_1:6, FINSEQ_1:20, RELAT_1:38, A4, S2;

then (len f) -' 1 = (len f) - 1 by XREAL_0:def 2;

then reconsider i = (len f) - 1 as Element of NAT ;

A32: (len f) + (- 1) < len f by XREAL_1:37;

(len f) -' i = (len f) - i by XREAL_0:def 2

.= 1 ;

then rng f |-0 (implications (f,A)) /. 1 by A34, A32;

then C2: F |-0 (f /. 1) => A by A4, imps, A7, A6;

C3: 1 in dom f by A6, FINSEQ_3:25;

then f . 1 in rng f by FUNCT_1:3;

then f /. 1 in rng f by PARTFUN1:def 6, C3;

then F |-0 f /. 1 by A4, th10;

hence F |-0 A by C2, th11a; :: thesis: verum

end;A4: ( rng f = F & f is one-to-one ) by FINSEQ_4:58;

reconsider f = f as FinSequence of LTLB_WFF by A4, FINSEQ_1:def 4;

A6: 1 <= len f by RELAT_1:38, A4, FINSEQ_1:20, S2;

then 1 <= len (implications (f,A)) by imps;

then A7: (implications (f,A)) /. 1 = (implications (f,A)) . 1 by FINSEQ_4:15;

AA: 1 in dom f by A6, FINSEQ_3:25;

defpred S

rng (f | 1) = rng <*(f . 1)*> by FINSEQ_5:20, RELAT_1:38, A4, S2

.= rng <*(f /. 1)*> by PARTFUN1:def 6, AA ;

then A8: (rng (f /^ 1)) \/ {(f /. 1)} = (rng (f | 1)) \/ (rng (f /^ 1)) by FINSEQ_1:38

.= rng ((f | 1) ^ (f /^ 1)) by FINSEQ_1:31

.= rng f by RFINSEQ:8 ;

A9: len (implications (f,A)) = len f by A6, imps;

A10: now :: thesis: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]

A19:
SS

let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

A11: i in NAT by ORDINAL1:def 12;

assume A12: S_{1}[i]
; :: thesis: S_{1}[i + 1]

thus S_{1}[i + 1]
:: thesis: verum

end;A11: i in NAT by ORDINAL1:def 12;

assume A12: S

thus S

proof

assume that

A13: 1 <= i + 1 and

A14: i + 1 <= len f ; :: thesis: rng (f /^ (i + 1)) |=0 (implications (f,A)) /. (i + 1)

end;A13: 1 <= i + 1 and

A14: i + 1 <= len f ; :: thesis: rng (f /^ (i + 1)) |=0 (implications (f,A)) /. (i + 1)

per cases
( i = 0 or 1 <= i )
by NAT_1:25;

end;

suppose A15:
i = 0
; :: thesis: rng (f /^ (i + 1)) |=0 (implications (f,A)) /. (i + 1)

(f /. 1) => A =
(implications (f,A)) . 1
by imps, A6

.= (implications (f,A)) /. 1 by FINSEQ_4:15, A9, A6 ;

hence rng (f /^ (i + 1)) |=0 (implications (f,A)) /. (i + 1) by A8, A4, Z1, th263, A15; :: thesis: verum

end;.= (implications (f,A)) /. 1 by FINSEQ_4:15, A9, A6 ;

hence rng (f /^ (i + 1)) |=0 (implications (f,A)) /. (i + 1) by A8, A4, Z1, th263, A15; :: thesis: verum

suppose A16:
1 <= i
; :: thesis: rng (f /^ (i + 1)) |=0 (implications (f,A)) /. (i + 1)

i + 1 in dom f
by FINSEQ_3:25, A13, A14;

then rng (<*(f /. (i + 1))*> ^ (f /^ (i + 1))) |=0 (implications (f,A)) /. i by A12, A16, NAT_1:13, A14, FINSEQ_5:31;

then (rng <*(f /. (i + 1))*>) \/ (rng (f /^ (i + 1))) |=0 (implications (f,A)) /. i by FINSEQ_1:31;

then A17: (rng (f /^ (i + 1))) \/ {(f /. (i + 1))} |=0 (implications (f,A)) /. i by FINSEQ_1:38;

A18: i < len f by NAT_1:13, A14;

(implications (f,A)) /. (i + 1) = (implications (f,A)) . (i + 1) by FINSEQ_4:15, A13, A14, A9

.= (f /. (i + 1)) => ((implications (f,A)) /. i) by imps, A16, A18, A11 ;

hence rng (f /^ (i + 1)) |=0 (implications (f,A)) /. (i + 1) by A17, th263; :: thesis: verum

end;then rng (<*(f /. (i + 1))*> ^ (f /^ (i + 1))) |=0 (implications (f,A)) /. i by A12, A16, NAT_1:13, A14, FINSEQ_5:31;

then (rng <*(f /. (i + 1))*>) \/ (rng (f /^ (i + 1))) |=0 (implications (f,A)) /. i by FINSEQ_1:31;

then A17: (rng (f /^ (i + 1))) \/ {(f /. (i + 1))} |=0 (implications (f,A)) /. i by FINSEQ_1:38;

A18: i < len f by NAT_1:13, A14;

(implications (f,A)) /. (i + 1) = (implications (f,A)) . (i + 1) by FINSEQ_4:15, A13, A14, A9

.= (f /. (i + 1)) => ((implications (f,A)) /. i) by imps, A16, A18, A11 ;

hence rng (f /^ (i + 1)) |=0 (implications (f,A)) /. (i + 1) by A17, th263; :: thesis: verum

for i being Nat holds S

then rng (f /^ (len f)) |=0 (implications (f,A)) /. (len f) by A6;

then {} LTLB_WFF |=0 (implications (f,A)) /. (len f) by RFINSEQ:27, RELAT_1:38;

then D2: {} LTLB_WFF |- (implications (f,A)) /. (len f) by LTLAXIO4:33, th262b, th264p;

defpred S

A21: now :: thesis: for i being Nat st S_{2}[i] holds

S_{2}[i + 1]

{} LTLB_WFF c= rng f
;S

let i be Nat; :: thesis: ( S_{2}[i] implies S_{2}[i + 1] )

assume A22: S_{2}[i]
; :: thesis: S_{2}[i + 1]

thus S_{2}[i + 1]
:: thesis: verum

end;assume A22: S

thus S

proof

set j = (len f) -' (i + 1);

assume A23: i + 1 < len f ; :: thesis: rng f |-0 (implications (f,A)) /. ((len f) -' (i + 1))

then A24: (i + 1) + (- (i + 1)) < (len f) + (- (i + 1)) by XREAL_1:8;

then A25: (len f) -' (i + 1) = (len f) - (i + 1) by XREAL_0:def 2;

then A26: 1 <= (len f) -' (i + 1) by NAT_1:25, A24;

i < len f by A23, NAT_1:12;

then (len f) + (- i) > i + (- i) by XREAL_1:8;

then A27: (len f) - i > 0 ;

A28: ((len f) -' (i + 1)) + 1 = ((len f) - (i + 1)) + 1 by XREAL_0:def 2, A24

.= (len f) -' i by XREAL_0:def 2, A27 ;

A29: (len f) + (- i) <= len f by XREAL_1:32;

then ((len f) -' (i + 1)) + 1 <= len f by A25;

then A30: (len f) -' (i + 1) < len f by NAT_1:16, XXREAL_0:2;

((len f) -' (i + 1)) + 1 <= len (implications (f,A)) by A29, A25, imps;

then E5: (implications (f,A)) /. ((len f) -' i) = (implications (f,A)) . (((len f) -' (i + 1)) + 1) by A28, FINSEQ_4:15, NAT_1:11

.= (f /. (((len f) -' (i + 1)) + 1)) => ((implications (f,A)) /. ((len f) -' (i + 1))) by imps, A26, A30 ;

E9: ((len f) -' (i + 1)) + 1 in dom f by FINSEQ_3:25, NAT_1:11, A29, A25;

then f . (((len f) -' (i + 1)) + 1) in rng f by FUNCT_1:3;

then f /. (((len f) -' (i + 1)) + 1) in rng f by PARTFUN1:def 6, E9;

then rng f |-0 f /. (((len f) -' (i + 1)) + 1) by th10;

hence rng f |-0 (implications (f,A)) /. ((len f) -' (i + 1)) by th11a, E5, A22, A23, NAT_1:12; :: thesis: verum

end;assume A23: i + 1 < len f ; :: thesis: rng f |-0 (implications (f,A)) /. ((len f) -' (i + 1))

then A24: (i + 1) + (- (i + 1)) < (len f) + (- (i + 1)) by XREAL_1:8;

then A25: (len f) -' (i + 1) = (len f) - (i + 1) by XREAL_0:def 2;

then A26: 1 <= (len f) -' (i + 1) by NAT_1:25, A24;

i < len f by A23, NAT_1:12;

then (len f) + (- i) > i + (- i) by XREAL_1:8;

then A27: (len f) - i > 0 ;

A28: ((len f) -' (i + 1)) + 1 = ((len f) - (i + 1)) + 1 by XREAL_0:def 2, A24

.= (len f) -' i by XREAL_0:def 2, A27 ;

A29: (len f) + (- i) <= len f by XREAL_1:32;

then ((len f) -' (i + 1)) + 1 <= len f by A25;

then A30: (len f) -' (i + 1) < len f by NAT_1:16, XXREAL_0:2;

((len f) -' (i + 1)) + 1 <= len (implications (f,A)) by A29, A25, imps;

then E5: (implications (f,A)) /. ((len f) -' i) = (implications (f,A)) . (((len f) -' (i + 1)) + 1) by A28, FINSEQ_4:15, NAT_1:11

.= (f /. (((len f) -' (i + 1)) + 1)) => ((implications (f,A)) /. ((len f) -' (i + 1))) by imps, A26, A30 ;

E9: ((len f) -' (i + 1)) + 1 in dom f by FINSEQ_3:25, NAT_1:11, A29, A25;

then f . (((len f) -' (i + 1)) + 1) in rng f by FUNCT_1:3;

then f /. (((len f) -' (i + 1)) + 1) in rng f by PARTFUN1:def 6, E9;

then rng f |-0 f /. (((len f) -' (i + 1)) + 1) by th10;

hence rng f |-0 (implications (f,A)) /. ((len f) -' (i + 1)) by th11a, E5, A22, A23, NAT_1:12; :: thesis: verum

then D3: rng f |-0 (implications (f,A)) /. (len f) by mon, D2, th267;

(len f) - 0 >= 1 by RELAT_1:38, A4, S2, FINSEQ_1:20;

then A33: S

A34: for i being Nat holds S

1 + (- 1) <= (len f) + (- 1) by XREAL_1:6, FINSEQ_1:20, RELAT_1:38, A4, S2;

then (len f) -' 1 = (len f) - 1 by XREAL_0:def 2;

then reconsider i = (len f) - 1 as Element of NAT ;

A32: (len f) + (- 1) < len f by XREAL_1:37;

(len f) -' i = (len f) - i by XREAL_0:def 2

.= 1 ;

then rng f |-0 (implications (f,A)) /. 1 by A34, A32;

then C2: F |-0 (f /. 1) => A by A4, imps, A7, A6;

C3: 1 in dom f by A6, FINSEQ_3:25;

then f . 1 in rng f by FUNCT_1:3;

then f /. 1 in rng f by PARTFUN1:def 6, C3;

then F |-0 f /. 1 by A4, th10;

hence F |-0 A by C2, th11a; :: thesis: verum