let H1, H2 be LTL-formula; :: thesis: for r being Element of Inf_seq AtomicFamily holds
( r |= H1 'R' H2 iff r |= 'not' (('not' H1) 'U' ('not' H2)) )
let r be Element of Inf_seq AtomicFamily ; :: thesis: ( r |= H1 'R' H2 iff r |= 'not' (('not' H1) 'U' ('not' H2)) )
set H01 = Evaluate H1,AtomicKai ;
set H02 = Evaluate H2,AtomicKai ;
set nH1 = 'not' H1;
set nH2 = 'not' H2;
A1: 'not' (Evaluate H1,AtomicKai ) = Evaluate ('not' H1),AtomicKai by Th5;
A2: 'not' (Evaluate H2,AtomicKai ) = Evaluate ('not' H2),AtomicKai by Th5;
( r |= ('not' H1) 'U' ('not' H2) iff r |= Evaluate (('not' H1) 'U' ('not' H2)),AtomicKai ) by Def65;
then A3: ( r |= ('not' H1) 'U' ('not' H2) iff r |= ('not' (Evaluate H1,AtomicKai )) 'U' ('not' (Evaluate H2,AtomicKai )) ) by Th9, A1, A2;
( r |= H1 'R' H2 iff r |= Evaluate (H1 'R' H2),AtomicKai ) by Def65;
then ( r |= H1 'R' H2 iff r |= (Evaluate H1,AtomicKai ) 'R' (Evaluate H2,AtomicKai ) ) by Th10;
then ( r |= H1 'R' H2 iff r |= 'not' (('not' (Evaluate H1,AtomicKai )) 'U' ('not' (Evaluate H2,AtomicKai ))) ) by Def5402;
hence ( r |= H1 'R' H2 iff r |= 'not' (('not' H1) 'U' ('not' H2)) ) by Th12, Th19, A3; :: thesis: verum