let H1, H2 be LTL-formula; :: thesis: for r being Element of Inf_seq AtomicFamily holds
( r |= H1 'R' H2 iff for m being Nat st ( for j being Nat st j < m holds
Shift r,j |= 'not' H1 ) holds
Shift r,m |= H2 )
let r be Element of Inf_seq AtomicFamily ; :: thesis: ( r |= H1 'R' H2 iff for m being Nat st ( for j being Nat st j < m holds
Shift r,j |= 'not' H1 ) holds
Shift r,m |= H2 )
( r |= H1 'R' H2 iff r |= Evaluate (H1 'R' H2),AtomicKai ) by Def65;
then A1: ( r |= H1 'R' H2 iff r |= (Evaluate H1,AtomicKai ) 'R' (Evaluate H2,AtomicKai ) ) by Th10;
A2: ( ( for m being Nat st ( for j being Nat st j < m holds
Shift r,j |= 'not' (Evaluate H1,AtomicKai ) ) holds
Shift r,m |= Evaluate H2,AtomicKai ) implies for m being Nat st ( for j being Nat st j < m holds
Shift r,j |= 'not' H1 ) holds
Shift r,m |= H2 )

proof

assume B1: for m being Nat st ( for j being Nat st j < m holds
Shift r,j |= 'not' (Evaluate H1,AtomicKai ) ) holds
Shift r,m |= Evaluate H2,AtomicKai ; :: thesis: for m being Nat st ( for j being Nat st j < m holds
Shift r,j |= 'not' H1 ) holds
Shift r,m |= H2
for m being Nat st ( for j being Nat st j < m holds
Shift r,j |= 'not' H1 ) holds
Shift r,m |= H2

proof

let m be Nat; :: thesis: ( ( for j being Nat st j < m holds
Shift r,j |= 'not' H1 ) implies Shift r,m |= H2 )
( ( for j being Nat st j < m holds
Shift r,j |= 'not' H1 ) implies Shift r,m |= H2 )

proof

assume D1: for j being Nat st j < m holds
Shift r,j |= 'not' H1 ; :: thesis: Shift r,m |= H2
for j being Nat st j < m holds
Shift r,j |= 'not' (Evaluate H1,AtomicKai )

proof

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

end;

then Shift r,m |= Evaluate H2,AtomicKai by B1;
hence Shift r,m |= H2 by Def65; :: thesis: verum

end;

hence ( ( for j being Nat st j < m holds
Shift r,j |= 'not' H1 ) implies Shift r,m |= H2 ) ; :: thesis: verum

end;

hence for m being Nat st ( for j being Nat st j < m holds
Shift r,j |= 'not' H1 ) holds
Shift r,m |= H2 ; :: thesis: verum

end;

( ( for m being Nat st ( for j being Nat st j < m holds
Shift r,j |= 'not' H1 ) holds
Shift r,m |= H2 ) implies for m being Nat st ( for j being Nat st j < m holds
Shift r,j |= 'not' (Evaluate H1,AtomicKai ) ) holds
Shift r,m |= Evaluate H2,AtomicKai )

proof

assume B1: for m being Nat st ( for j being Nat st j < m holds
Shift r,j |= 'not' H1 ) holds
Shift r,m |= H2 ; :: thesis: for m being Nat st ( for j being Nat st j < m holds
Shift r,j |= 'not' (Evaluate H1,AtomicKai ) ) holds
Shift r,m |= Evaluate H2,AtomicKai
for m being Nat st ( for j being Nat st j < m holds
Shift r,j |= 'not' (Evaluate H1,AtomicKai ) ) holds
Shift r,m |= Evaluate H2,AtomicKai

proof

let m be Nat; :: thesis: ( ( for j being Nat st j < m holds
Shift r,j |= 'not' (Evaluate H1,AtomicKai ) ) implies Shift r,m |= Evaluate H2,AtomicKai )
( ( for j being Nat st j < m holds
Shift r,j |= 'not' (Evaluate H1,AtomicKai ) ) implies Shift r,m |= Evaluate H2,AtomicKai )

proof

assume D1: for j being Nat st j < m holds
Shift r,j |= 'not' (Evaluate H1,AtomicKai ) ; :: thesis: Shift r,m |= Evaluate H2,AtomicKai
for j being Nat st j < m holds
Shift r,j |= 'not' H1

proof

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

end;

then Shift r,m |= H2 by B1;
hence Shift r,m |= Evaluate H2,AtomicKai by Def65; :: thesis: verum

end;

hence ( ( for j being Nat st j < m holds
Shift r,j |= 'not' (Evaluate H1,AtomicKai ) ) implies Shift r,m |= Evaluate H2,AtomicKai ) ; :: thesis: verum

end;

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

end;

hence ( r |= H1 'R' H2 iff for m being Nat st ( for j being Nat st j < m holds
Shift r,j |= 'not' H1 ) holds
Shift r,m |= H2 ) by A1, Th17, A2; :: thesis: verum