let A be Element of LTLB_WFF ; for F being finite Subset of LTLB_WFF st F |= A holds
F |- A
let F be finite Subset of LTLB_WFF; ( F |= A implies F |- A )
assume A3:
F |= A
; F |- A
now ( not F is empty implies F |- A )consider f being
FinSequence such that A4:
rng f = F
and
f is
one-to-one
by FINSEQ_4:58;
reconsider f =
f as
FinSequence of
LTLB_WFF by A4, FINSEQ_1:def 4;
assume A5:
not
F is
empty
;
F |- Athen A6:
1
<= len f
by RELAT_1:38, A4, FINSEQ_1:20;
then
1
<= len (impg (f,A))
by LTLAXIO2:def 3;
then A7:
(impg (f,A)) /. 1
= (impg (f,A)) . 1
by FINSEQ_4:15;
defpred S1[
Nat]
means ( 1
<= $1 & $1
<= len f implies
rng (f /^ $1) |= (impg (f,A)) /. $1 );
a8:
1
in dom f
by A6, FINSEQ_3:25;
rng (f | 1) =
rng <*(f . 1)*>
by FINSEQ_5:20, RELAT_1:38, A4, A5
.=
rng <*(f /. 1)*>
by a8, PARTFUN1:def 6
;
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 (impg (f,A)) = len f
by A6, LTLAXIO2:def 3;
A10:
now for i being Nat st S1[i] holds
S1[i + 1]let i be
Nat;
( S1[i] implies S1[i + 1] )A11:
i in NAT
by ORDINAL1:def 12;
assume A12:
S1[
i]
;
S1[i + 1]thus
S1[
i + 1]
verumproof
assume that A13:
1
<= i + 1
and A14:
i + 1
<= len f
;
rng (f /^ (i + 1)) |= (impg (f,A)) /. (i + 1)
per cases
( i = 0 or 1 <= i )
by NAT_1:25;
suppose A15:
i = 0
;
rng (f /^ (i + 1)) |= (impg (f,A)) /. (i + 1)('G' (f /. 1)) => A =
(impg (f,A)) . 1
by LTLAXIO2:def 3, A6
.=
(impg (f,A)) /. 1
by FINSEQ_4:15, A9, A6
;
hence
rng (f /^ (i + 1)) |= (impg (f,A)) /. (i + 1)
by A8, A4, A3, LTLAXIO1:30, A15;
verum end; suppose A16:
1
<= i
;
rng (f /^ (i + 1)) |= (impg (f,A)) /. (i + 1)
i + 1
in dom f
by FINSEQ_3:25, A13, A14;
then
rng (<*(f /. (i + 1))*> ^ (f /^ (i + 1))) |= (impg (f,A)) /. i
by A12, A16, NAT_1:13, A14, FINSEQ_5:31;
then
(rng <*(f /. (i + 1))*>) \/ (rng (f /^ (i + 1))) |= (impg (f,A)) /. i
by FINSEQ_1:31;
then A17:
(rng (f /^ (i + 1))) \/ {(f /. (i + 1))} |= (impg (f,A)) /. i
by FINSEQ_1:38;
A18:
i < len f
by NAT_1:13, A14;
(impg (f,A)) /. (i + 1) =
(impg (f,A)) . (i + 1)
by FINSEQ_4:15, A13, A14, A9
.=
('G' (f /. (i + 1))) => ((impg (f,A)) /. i)
by LTLAXIO2:def 3, A16, A18, A11
;
hence
rng (f /^ (i + 1)) |= (impg (f,A)) /. (i + 1)
by A17, LTLAXIO1:30;
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)) |= (impg (f,A)) /. (len f)
by A6;
then
{} LTLB_WFF |= (impg (f,A)) /. (len f)
by RFINSEQ:27, RELAT_1:38;
then A20:
{} LTLB_WFF |- (impg (f,A)) /. (len f)
by A1;
defpred S2[
Nat]
means ( $1
< len f implies
rng (f /^ ((len f) -' $1)) |- (impg (f,A)) /. ((len f) -' $1) );
A21:
now for i being Nat st S2[i] holds
S2[i + 1]let i be
Nat;
( S2[i] implies S2[i + 1] )assume A22:
S2[
i]
;
S2[i + 1]thus
S2[
i + 1]
verumproof
set j =
(len f) -' (i + 1);
assume A23:
i + 1
< len f
;
rng (f /^ ((len f) -' (i + 1))) |- (impg (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 (impg (f,A))
by A29, A25, LTLAXIO2:def 3;
then (impg (f,A)) /. ((len f) -' i) =
(impg (f,A)) . (((len f) -' (i + 1)) + 1)
by A28, FINSEQ_4:15, NAT_1:11
.=
('G' (f /. (((len f) -' (i + 1)) + 1))) => ((impg (f,A)) /. ((len f) -' (i + 1)))
by LTLAXIO2:def 3, A26, A30
;
then
(rng (f /^ ((len f) -' i))) \/ {(f /. (((len f) -' (i + 1)) + 1))} |- (impg (f,A)) /. ((len f) -' (i + 1))
by LTLAXIO1:59, A22, NAT_1:12, A23;
then
(rng <*(f /. (((len f) -' (i + 1)) + 1))*>) \/ (rng (f /^ ((len f) -' i))) |- (impg (f,A)) /. ((len f) -' (i + 1))
by FINSEQ_1:38;
then A31:
rng (<*(f /. (((len f) -' (i + 1)) + 1))*> ^ (f /^ ((len f) -' i))) |- (impg (f,A)) /. ((len f) -' (i + 1))
by FINSEQ_1:31;
((len f) -' (i + 1)) + 1
in dom f
by FINSEQ_3:25, NAT_1:11, A29, A25;
hence
rng (f /^ ((len f) -' (i + 1))) |- (impg (f,A)) /. ((len f) -' (i + 1))
by A31, FINSEQ_5:31, A28;
verum
end; end;
1
+ (- 1) <= (len f) + (- 1)
by XREAL_1:6, FINSEQ_1:20, RELAT_1:38, A4, A5;
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) - 0 >= 1
by RELAT_1:38, A4, A5, FINSEQ_1:20;
then
(len f) -' 0 = len f
by XREAL_0:def 2;
then A33:
S2[
0 ]
by A20, RELAT_1:38, RFINSEQ:27;
A34:
for
i being
Nat holds
S2[
i]
from NAT_1:sch 2(A33, A21);
(len f) -' i =
(len f) - i
by XREAL_0:def 2
.=
1
;
then
rng (f /^ 1) |- (impg (f,A)) /. 1
by A34, A32;
then
rng (f /^ 1) |- ('G' (f /. 1)) => A
by LTLAXIO2:def 3, A7, A6;
hence
F |- A
by A4, A8, LTLAXIO1:59;
verum end;
hence
F |- A
by A1, A3; verum