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 by Def65;
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 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;

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 by Def65; :: thesis: verum

end;

then Shift r,m |= H2 by A5;
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;

( 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;
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