let S be non empty set ; :: thesis: for BASSIGN being non empty Subset of (ModelSP (Inf_seq S))
for t being Element of Inf_seq S
for f, g being Assign of (LTLModel S,BASSIGN) holds
( t |= f 'R' g iff for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |= g )
let BASSIGN be non empty Subset of (ModelSP (Inf_seq S)); :: thesis: for t being Element of Inf_seq S
for f, g being Assign of (LTLModel S,BASSIGN) holds
( t |= f 'R' g iff for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |= g )
let t be Element of Inf_seq S; :: thesis: for f, g being Assign of (LTLModel S,BASSIGN) holds
( t |= f 'R' g iff for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |= g )
let f, g be Assign of (LTLModel S,BASSIGN); :: thesis: ( t |= f 'R' g iff for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |= g )
A1: ( ( for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |/= 'not' g ) implies for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |= g )

proof

assume A2: for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |/= 'not' g ; :: thesis: for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |= g
for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |= g

proof

let m be Nat; :: thesis: ( ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) implies Shift t,m |= g )
( ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) implies Shift t,m |/= 'not' g ) by A2;
hence ( ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) implies Shift t,m |= g ) by Th57; :: thesis: verum

end;

hence for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |= g ; :: thesis: verum

end;

A3: ( ( for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |= g ) implies for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |/= 'not' g )

proof

assume A4: for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |= g ; :: thesis: for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |/= 'not' g
for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |/= 'not' g

proof

let m be Nat; :: thesis: ( ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) implies Shift t,m |/= 'not' g )
( ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) implies Shift t,m |= g ) by A4;
hence ( ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) implies Shift t,m |/= 'not' g ) by Th57; :: thesis: verum

end;

hence for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |/= 'not' g ; :: thesis: verum

end;

( t |= f 'R' g iff t |= 'not' (('not' f) 'U' ('not' g)) ) by Def57;
then ( t |= f 'R' g iff not t |= ('not' f) 'U' ('not' g) ) by Th57;
hence ( t |= f 'R' g iff for m being Nat st ( for j being Nat st j < m holds
Shift t,j |= 'not' f ) holds
Shift t,m |= g ) by A1, A3, Th60; :: thesis: verum