let w be Element of Inf_seq AtomicFamily; :: thesis: for v being neg-inner-most LTL-formula st w |= 'X' v holds
w |= * (init v)
let v be neg-inner-most LTL-formula; :: thesis: ( w |= 'X' v implies w |= * (init v) )
assume A1: w |= 'X' v ; :: thesis: w |= * (init v)
for H being LTL-formula st H in 'X' (CastLTL (Seed v)) holds
w |= H
proof
let H be LTL-formula; :: thesis: ( H in 'X' (CastLTL (Seed v)) implies w |= H )
assume H in 'X' (CastLTL (Seed v)) ; :: thesis: w |= H
then ex x being LTL-formula st
( H = x & ex u being LTL-formula st
( u in CastLTL (Seed v) & x = 'X' u ) ) ;
hence w |= H by A1, TARSKI:def 1; :: thesis: verum
end;
hence w |= * (init v) ; :: thesis: verum