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: ( r |= ('not' H1) 'U' ('not' H2) iff r |= Evaluate (('not' H1) 'U' ('not' H2)),AtomicKai ) by Def65;
( 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 Th55;
then A2: ( r |= H1 'R' H2 iff r |= 'not' (('not' (Evaluate H1,AtomicKai )) 'U' ('not' (Evaluate H2,AtomicKai ))) ) by Def57;
( 'not' (Evaluate H1,AtomicKai ) = Evaluate ('not' H1),AtomicKai & 'not' (Evaluate H2,AtomicKai ) = Evaluate ('not' H2),AtomicKai ) by Th50;
then ( r |= ('not' H1) 'U' ('not' H2) iff r |= ('not' (Evaluate H1,AtomicKai )) 'U' ('not' (Evaluate H2,AtomicKai )) ) by A1, Th54;
hence ( r |= H1 'R' H2 iff r |= 'not' (('not' H1) 'U' ('not' H2)) ) by A2, Th57, Th64; :: thesis: verum