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 (Inf_seqModel (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 (Inf_seqModel (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 (Inf_seqModel (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 (Inf_seqModel (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 ) by Th57;
( t |= f 'R' g iff t |= 'not' (('not' f) 'U' ('not' g)) ) by Def55;
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