let A be Element of LTLB_WFF ; for F being finite Subset of LTLB_WFF st F |=0 A holds
F |-0 A
let F be finite Subset of LTLB_WFF; ( F |=0 A implies F |-0 A )
assume Z1:
F |=0 A
; F |-0 A
per cases
( F is empty or not F is empty )
;
suppose S2:
not
F is
empty
;
F |-0 Aconsider 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 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)) |=0 (implications (f,A)) /. (i + 1)
per cases
( i = 0 or 1 <= i )
by NAT_1:25;
suppose A15:
i = 0
;
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;
verum end; suppose A16:
1
<= i
;
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;
verum 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 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 |-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;
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;
verum end;