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 )
A1: ( ( 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 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) ; :: 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 A3: 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 j < m ; :: thesis: Shift (r,j) |= 'not' (Evaluate (H1,AtomicKai))
then Shift (r,j) |= 'not' H1 by A3;
then Shift (r,j) |= Evaluate (('not' H1),AtomicKai) ;
hence Shift (r,j) |= 'not' (Evaluate (H1,AtomicKai)) by Th50; :: thesis: verum

end;

then Shift (r,m) |= Evaluate (H2,AtomicKai) by A2;
hence Shift (r,m) |= H2 ; :: 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;

A4: ( ( 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 A5: 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 A6: 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 j < m ; :: thesis: Shift (r,j) |= 'not' H1
then Shift (r,j) |= 'not' (Evaluate (H1,AtomicKai)) by A6;
then Shift (r,j) |= Evaluate (('not' H1),AtomicKai) by Th50;
hence Shift (r,j) |= 'not' H1 ; :: thesis: verum

end;

then Shift (r,m) |= H2 by A5;
hence Shift (r,m) |= Evaluate (H2,AtomicKai) ; :: 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;

( r |= H1 'R' H2 iff r |= (Evaluate (H1,AtomicKai)) 'R' (Evaluate (H2,AtomicKai)) ) by Th55;
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, A4, Th62; :: thesis: verum