let H1, H2 be LTL-formula; :: thesis: for r being Element of Inf_seq AtomicFamily holds
( r |= H1 'U' H2 iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift r,j |= H1 ) & Shift r,m |= H2 ) )
let r be Element of Inf_seq AtomicFamily ; :: thesis: ( r |= H1 'U' H2 iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift r,j |= H1 ) & Shift r,m |= H2 ) )
A1: ( ex m being Nat st
( ( for j being Nat st j < m holds
Shift r,j |= Evaluate H1,AtomicKai ) & Shift r,m |= Evaluate H2,AtomicKai ) implies ex m being Nat st
( ( for j being Nat st j < m holds
Shift r,j |= H1 ) & Shift r,m |= H2 ) )

proof

assume ex m being Nat st
( ( for j being Nat st j < m holds
Shift r,j |= Evaluate H1,AtomicKai ) & Shift r,m |= Evaluate H2,AtomicKai ) ; :: thesis: ex m being Nat st
( ( for j being Nat st j < m holds
Shift r,j |= H1 ) & Shift r,m |= H2 )
then consider m being Nat such that
A2: for j being Nat st j < m holds
Shift r,j |= Evaluate H1,AtomicKai and
A3: Shift r,m |= Evaluate H2,AtomicKai ;
take m ; :: thesis: ( ( for j being Nat st j < m holds
Shift r,j |= H1 ) & Shift r,m |= H2 )
for j being Nat st j < m holds
Shift r,j |= H1

proof

let j be Nat; :: thesis: ( j < m implies Shift r,j |= H1 )
assume j < m ; :: thesis: Shift r,j |= H1
then Shift r,j |= Evaluate H1,AtomicKai by A2;
hence Shift r,j |= H1 by Def65; :: thesis: verum

end;

hence ( ( for j being Nat st j < m holds
Shift r,j |= H1 ) & Shift r,m |= H2 ) by A3, Def65; :: thesis: verum

end;

A4: ( ex m being Nat st
( ( for j being Nat st j < m holds
Shift r,j |= H1 ) & Shift r,m |= H2 ) implies ex m being Nat st
( ( for j being Nat st j < m holds
Shift r,j |= Evaluate H1,AtomicKai ) & Shift r,m |= Evaluate H2,AtomicKai ) )

proof

assume ex m being Nat st
( ( for j being Nat st j < m holds
Shift r,j |= H1 ) & Shift r,m |= H2 ) ; :: thesis: ex m being Nat st
( ( for j being Nat st j < m holds
Shift r,j |= Evaluate H1,AtomicKai ) & Shift r,m |= Evaluate H2,AtomicKai )
then consider m being Nat such that
A5: for j being Nat st j < m holds
Shift r,j |= H1 and
A6: Shift r,m |= H2 ;
take m ; :: thesis: ( ( for j being Nat st j < m holds
Shift r,j |= Evaluate H1,AtomicKai ) & Shift r,m |= Evaluate H2,AtomicKai )
for j being Nat st j < m holds
Shift r,j |= Evaluate H1,AtomicKai

proof

let j be Nat; :: thesis: ( j < m implies Shift r,j |= Evaluate H1,AtomicKai )
assume j < m ; :: thesis: Shift r,j |= Evaluate H1,AtomicKai
then Shift r,j |= H1 by A5;
hence Shift r,j |= Evaluate H1,AtomicKai by Def65; :: thesis: verum

end;

hence ( ( for j being Nat st j < m holds
Shift r,j |= Evaluate H1,AtomicKai ) & Shift r,m |= Evaluate H2,AtomicKai ) by A6, Def65; :: thesis: verum

end;

( r |= H1 'U' H2 iff r |= Evaluate (H1 'U' H2),AtomicKai ) by Def65;
then ( r |= H1 'U' H2 iff r |= (Evaluate H1,AtomicKai ) 'U' (Evaluate H2,AtomicKai ) ) by Th54;
hence ( r |= H1 'U' H2 iff ex m being Nat st
( ( for j being Nat st j < m holds
Shift r,j |= H1 ) & Shift r,m |= H2 ) ) by A1, A4, Th60; :: thesis: verum