let w be Element of Inf_seq AtomicFamily; :: thesis: for v being neg-inner-most LTL-formula holds
( w |= v iff w |= * ('X' (init v)) )
let v be neg-inner-most LTL-formula; :: thesis: ( w |= v iff w |= * ('X' (init v)) )
set N = init v;
set M = 'X' (init v);
A1: * ('X' (init v)) = {v} by Lm33;
A2: ( w |= * ('X' (init v)) implies w |= v )
proof
assume A3: w |= * ('X' (init v)) ; :: thesis: w |= v
v in * ('X' (init v)) by A1, TARSKI:def 1;
hence w |= v by A3; :: thesis: verum
end;
( w |= v implies w |= * ('X' (init v)) ) by A1, TARSKI:def 1;
hence ( w |= v iff w |= * ('X' (init v)) ) by A2; :: thesis: verum