let H1, H2 be LTL-formula; :: thesis: for r being Element of Inf_seq AtomicFamily holds
( r |= H1 'R' H2 iff r |= (H1 '&' H2) 'or' (H2 '&' ('X' (H1 'R' H2))) )
let r be Element of Inf_seq AtomicFamily; :: thesis: ( r |= H1 'R' H2 iff r |= (H1 '&' H2) 'or' (H2 '&' ('X' (H1 'R' H2))) )
set nH1 = 'not' H1;
set nH2 = 'not' H2;
( r |= H1 'R' H2 iff r |= 'not' (('not' H1) 'U' ('not' H2)) ) by Th72;
then ( r |= H1 'R' H2 iff r |/= ('not' H1) 'U' ('not' H2) ) by Th64;
then ( r |= H1 'R' H2 iff r |/= ('not' H2) 'or' (('not' H1) '&' ('X' (('not' H1) 'U' ('not' H2)))) ) by Th75;
then ( r |= H1 'R' H2 iff r |= 'not' (('not' H2) 'or' (('not' H1) '&' ('X' (('not' H1) 'U' ('not' H2))))) ) by Th64;
then ( r |= H1 'R' H2 iff r |= ('not' ('not' H2)) '&' ('not' (('not' H1) '&' ('X' (('not' H1) 'U' ('not' H2))))) ) by Th70;
then ( r |= H1 'R' H2 iff ( r |= 'not' ('not' H2) & r |= 'not' (('not' H1) '&' ('X' (('not' H1) 'U' ('not' H2)))) ) ) by Th65;
then ( r |= H1 'R' H2 iff ( r |/= 'not' H2 & r |= ('not' ('not' H1)) 'or' ('not' ('X' (('not' H1) 'U' ('not' H2)))) ) ) by Th64, Th71;
then ( r |= H1 'R' H2 iff ( r |= H2 & ( r |= 'not' ('not' H1) or r |= 'not' ('X' (('not' H1) 'U' ('not' H2))) ) ) ) by Th64, Th66;
then ( r |= H1 'R' H2 iff ( r |= H2 & ( r |/= 'not' H1 or r |= 'X' ('not' (('not' H1) 'U' ('not' H2))) ) ) ) by Th64, Th74;
then ( r |= H1 'R' H2 iff ( r |= H2 & ( r |/= 'not' H1 or Shift (r,1) |= 'not' (('not' H1) 'U' ('not' H2)) ) ) ) by Th67;
then ( r |= H1 'R' H2 iff ( r |= H2 & ( r |= H1 or Shift (r,1) |= H1 'R' H2 ) ) ) by Th64, Th72;
then ( r |= H1 'R' H2 iff ( r |= H2 & ( r |= H1 or r |= 'X' (H1 'R' H2) ) ) ) by Th67;
then ( r |= H1 'R' H2 iff ( r |= H1 '&' H2 or r |= H2 '&' ('X' (H1 'R' H2)) ) ) by Th65;
hence ( r |= H1 'R' H2 iff r |= (H1 '&' H2) 'or' (H2 '&' ('X' (H1 'R' H2))) ) by Th66; :: thesis: verum