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 ;
hence F |-0 A by ; :: 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 ;
A6: 1 <= len f by ;
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 ;
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
.= rng <*(f /. 1)*> by ;
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 ;
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
.= (implications (f,A)) /. 1 by ;
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 ;
then rng (<*(f /. (i + 1))*> ^ (f /^ (i + 1))) |=0 (implications (f,A)) /. i by ;
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 ;
(implications (f,A)) /. (i + 1) = (implications (f,A)) . (i + 1) by
.= (f /. (i + 1)) => ((implications (f,A)) /. i) by ;
hence rng (f /^ (i + 1)) |=0 (implications (f,A)) /. (i + 1) by ; :: thesis: verum
end;
end;
end;
end;
A19: S1[ 0 ] ;
for i being Nat holds S1[i] from then rng (f /^ (len f)) |=0 (implications (f,A)) /. (len f) by A6;
then {} LTLB_WFF |=0 (implications (f,A)) /. (len f) by ;
then D2: {} LTLB_WFF |- (implications (f,A)) /. (len f) by ;
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 ;
i < len f by ;
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
.= (len f) -' i by ;
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 ;
((len f) -' (i + 1)) + 1 <= len (implications (f,A)) by ;
then E5: (implications (f,A)) /. ((len f) -' i) = (implications (f,A)) . (((len f) -' (i + 1)) + 1) by
.= (f /. (((len f) -' (i + 1)) + 1)) => ((implications (f,A)) /. ((len f) -' (i + 1))) by ;
E9: ((len f) -' (i + 1)) + 1 in dom f by ;
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 ;
then rng f |-0 f /. (((len f) -' (i + 1)) + 1) by th10;
hence rng f |-0 (implications (f,A)) /. ((len f) -' (i + 1)) by ; :: thesis: verum
end;
end;
{} LTLB_WFF c= rng f ;
then D3: rng f |-0 (implications (f,A)) /. (len f) by ;
(len f) - 0 >= 1 by ;
then A33: S2[ 0 ] by ;
A34: for i being Nat holds S2[i] from 1 + (- 1) <= (len f) + (- 1) by ;
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 ;
then C2: F |-0 (f /. 1) => A by A4, imps, A7, A6;
C3: 1 in dom f by ;
then f . 1 in rng f by FUNCT_1:3;
then f /. 1 in rng f by ;
then F |-0 f /. 1 by ;
hence F |-0 A by ; :: thesis: verum
end;
end;