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
per cases ( F is empty or not F is empty ) ;
suppose S1: F is empty ; :: thesis: F |-0 A
then F |= A by th262b, th264p, Z1;
hence F |-0 A by th267, S1, LTLAXIO4:33; :: thesis: verum
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 S1[ 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;
A10: now :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
A11: i in NAT by ORDINAL1:def 12;
assume A12: S1[i] ; :: thesis: S1[i + 1]
thus S1[i + 1] :: thesis: verum
proof
assume that
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;
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;
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;
end;
end;
end;
A19: S1[ 0 ] ;
for i being Nat holds S1[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 S2[ Nat] means ( $1 < len f implies rng f |-0 (implications (f,A)) /. ((len f) -' $1) );
A21: now :: thesis: for i being Nat st S2[i] holds
S2[i + 1]
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume A22: S2[i] ; :: thesis: S2[i + 1]
thus S2[i + 1] :: thesis: verum
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;
end;
{} LTLB_WFF c= rng f ;
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: S2[ 0 ] by D3, XREAL_0:def 2;
A34: for i being Nat holds S2[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;
end;