let S be non empty set ; :: thesis: for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))
for t being Element of Inf_seq S
for f being Assign of (LTLModel S,BASSIGN) holds
( t |= 'X' f iff Shift t,1 |= f )
let BASSIGN be non empty Subset of (ModelSP (Inf_seq S)); :: thesis: for t being Element of Inf_seq S
for f being Assign of (LTLModel S,BASSIGN) holds
( t |= 'X' f iff Shift t,1 |= f )
let t be Element of Inf_seq S; :: thesis: for f being Assign of (LTLModel S,BASSIGN) holds
( t |= 'X' f iff Shift t,1 |= f )
let f be Assign of (LTLModel S,BASSIGN); :: thesis: ( t |= 'X' f iff Shift t,1 |= f )
set V = LTLModel S,BASSIGN;
set S1 = Inf_seq S;
set t1 = Shift t,1;
set t1p = Shift t,1,S;
A1: 'X' f = Next_0 f,S by Def46;
thus ( t |= 'X' f implies Shift t,1 |= f ) :: thesis: ( Shift t,1 |= f implies t |= 'X' f )

proof

assume t |= 'X' f ; :: thesis: Shift t,1 |= f
then (Fid (Next_0 f,S),(Inf_seq S)) . t = TRUE by A1, Def59;
then Next_univ t,(Fid f,(Inf_seq S)) = TRUE by Def45;
then (Fid f,(Inf_seq S)) . (Shift t,1,S) = TRUE by Def44;
hence Shift t,1 |= f by Def59; :: thesis: verum

end;

assume Shift t,1 |= f ; :: thesis: t |= 'X' f
then (Fid f,(Inf_seq S)) . (Shift t,1) = TRUE by Def59;
then Next_univ t,(Fid f,(Inf_seq S)) = TRUE by Def44;
then (Fid ('X' f),(Inf_seq S)) . t = TRUE by A1, Def45;
hence t |= 'X' f by Def59; :: thesis: verum