let p be Element of LTLB_WFF ; for X being Subset of LTLB_WFF st X |- p holds
X |- 'X' p
let X be Subset of LTLB_WFF; ( X |- p implies X |- 'X' p )
assume
X |- p
; X |- 'X' p
then consider f being FinSequence of LTLB_WFF such that
A1:
f . (len f) = p
and
A2:
1 <= len f
and
A3:
for i being Nat st 1 <= i & i <= len f holds
prc f,X,i
;
set g = f ^ <*('X' p)*>;
A4: len (f ^ <*('X' p)*>) =
(len f) + (len <*('X' p)*>)
by FINSEQ_1:22
.=
(len f) + 1
by FINSEQ_1:39
;
then A5:
len f < len (f ^ <*('X' p)*>)
by NAT_1:16;
then A6: (f ^ <*('X' p)*>) /. (len f) =
(f ^ <*('X' p)*>) . (len f)
by A2, Lm1
.=
p
by A1, A2, FINSEQ_1:64
;
1 <= len (f ^ <*('X' p)*>)
by A2, A4, NAT_1:16;
then (f ^ <*('X' p)*>) /. (len (f ^ <*('X' p)*>)) =
(f ^ <*('X' p)*>) . (len (f ^ <*('X' p)*>))
by Lm1
.=
'X' ((f ^ <*('X' p)*>) /. (len f))
by A4, A6, FINSEQ_1:42
;
then
(f ^ <*('X' p)*>) /. (len f) NEX_rule (f ^ <*('X' p)*>) /. (len (f ^ <*('X' p)*>))
;
then
prc f ^ <*('X' p)*>,X, len (f ^ <*('X' p)*>)
by A2, A5;
hence
X |- 'X' p
by A2, A3, Th40; verum