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, g being Assign of (LTLModel S,BASSIGN) holds
( t |= f 'U' g iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift t,j |= f ) & Shift t,m |= g ) )
let BASSIGN be non empty Subset of (ModelSP (Inf_seq S)); :: thesis: for t being Element of Inf_seq S
for f, g being Assign of (LTLModel S,BASSIGN) holds
( t |= f 'U' g iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift t,j |= f ) & Shift t,m |= g ) )
let t be Element of Inf_seq S; :: thesis: for f, g being Assign of (LTLModel S,BASSIGN) holds
( t |= f 'U' g iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift t,j |= f ) & Shift t,m |= g ) )
let f, g be Assign of (LTLModel S,BASSIGN); :: thesis: ( t |= f 'U' g iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift t,j |= f ) & Shift t,m |= g ) )
set V = LTLModel S,BASSIGN;
set S1 = Inf_seq S;
A1: f 'U' g = Until_0 f,g,S by Def55;
A2: ( ex m being Nat st
( ( for j being Nat st j < m holds
Shift t,j |= f ) & Shift t,m |= g ) implies t |= f 'U' g )

proof

assume A3: ex m being Nat st
( ( for j being Nat st j < m holds
Shift t,j |= f ) & Shift t,m |= g ) ; :: thesis: t |= f 'U' g
ex m being Nat st
( ( for j being Nat st j < m holds
(Fid f,(Inf_seq S)) . (Shift t,j,S) = TRUE ) & (Fid g,(Inf_seq S)) . (Shift t,m,S) = TRUE )

proof

consider m being Nat such that
A4: for j being Nat st j < m holds
Shift t,j |= f and
A5: Shift t,m |= g by A3;
take m ; :: thesis: ( ( for j being Nat st j < m holds
(Fid f,(Inf_seq S)) . (Shift t,j,S) = TRUE ) & (Fid g,(Inf_seq S)) . (Shift t,m,S) = TRUE )
for j being Nat st j < m holds
(Fid f,(Inf_seq S)) . (Shift t,j,S) = TRUE

proof

let j be Nat; :: thesis: ( j < m implies (Fid f,(Inf_seq S)) . (Shift t,j,S) = TRUE )
assume j < m ; :: thesis: (Fid f,(Inf_seq S)) . (Shift t,j,S) = TRUE
then Shift t,j |= f by A4;
hence (Fid f,(Inf_seq S)) . (Shift t,j,S) = TRUE by Def59; :: thesis: verum
set t1 = Shift t,j,S;

end;

hence ( ( for j being Nat st j < m holds
(Fid f,(Inf_seq S)) . (Shift t,j,S) = TRUE ) & (Fid g,(Inf_seq S)) . (Shift t,m,S) = TRUE ) by A5, Def59; :: thesis: verum

end;

then Until_univ t,(Fid f,(Inf_seq S)),(Fid g,(Inf_seq S)),S = TRUE by Def53;
then (Fid (f 'U' g),(Inf_seq S)) . t = TRUE by A1, Def54;
hence t |= f 'U' g by Def59; :: thesis: verum

end;

( t |= f 'U' g implies ex m being Nat st
( ( for j being Nat st j < m holds
Shift t,j |= f ) & Shift t,m |= g ) )

proof

assume t |= f 'U' g ; :: thesis: ex m being Nat st
( ( for j being Nat st j < m holds
Shift t,j |= f ) & Shift t,m |= g )
then (Fid (Until_0 f,g,S),(Inf_seq S)) . t = TRUE by A1, Def59;
then Until_univ t,(Fid f,(Inf_seq S)),(Fid g,(Inf_seq S)),S = TRUE by Def54;
then consider m being Nat such that
A6: for j being Nat st j < m holds
(Fid f,(Inf_seq S)) . (Shift t,j,S) = TRUE and
A7: (Fid g,(Inf_seq S)) . (Shift t,m,S) = TRUE by Def53;
take m ; :: thesis: ( ( for j being Nat st j < m holds
Shift t,j |= f ) & Shift t,m |= g )
for j being Nat st j < m holds
Shift t,j |= f

proof

let j be Nat; :: thesis: ( j < m implies Shift t,j |= f )
assume A8: j < m ; :: thesis: Shift t,j |= f
set t1 = Shift t,j;
(Fid f,(Inf_seq S)) . (Shift t,j) = TRUE by A6, A8;
hence Shift t,j |= f by Def59; :: thesis: verum

end;

hence ( ( for j being Nat st j < m holds
Shift t,j |= f ) & Shift t,m |= g ) by A7, Def59; :: thesis: verum

end;

hence ( t |= f 'U' g iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift t,j |= f ) & Shift t,m |= g ) ) by A2; :: thesis: verum