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