let p, q be Element of LTLB_WFF ; :: thesis: for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,(p 'R' q)] = 1 iff ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) )
let n be Element of NAT ; :: thesis: for M being LTLModel holds
( (SAT M) . [n,(p 'R' q)] = 1 iff ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) )
let M be LTLModel; :: thesis: ( (SAT M) . [n,(p 'R' q)] = 1 iff ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) )
set sm = SAT M;
set notp = 'not' p;
set notq = 'not' q;
thus ( not (SAT M) . [n,(p 'R' q)] = 1 or ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) :: thesis: ( ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) implies (SAT M) . [n,(p 'R' q)] = 1 )

proof

defpred S₁[ Nat] means ( (SAT M) . [(n + $1),q] = 1 & (SAT M) . [(n + $1),p] = 0 );
assume (SAT M) . [n,(p 'R' q)] = 1 ; :: thesis: ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 )
then A1: (SAT M) . [n,(('not' p) 'U' ('not' q))] = 0 by Th6;

A2: now

let i be Nat; :: thesis: ( not (SAT M) . [(n + b₁),('not' q)] = 1 or ex j being Nat st
( b₂ < j & not (SAT M) . [(n + b₂),('not' p)] = 1 ) )
reconsider ii = i as Element of NAT by ORDINAL1:def 12;

per cases ( not (SAT M) . [(n + ii),('not' q)] = 1 or ex j being Element of NAT st
( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ) by A1, Th13;

suppose not (SAT M) . [(n + ii),('not' q)] = 1 ; :: thesis: ( not (SAT M) . [(n + b₁),('not' q)] = 1 or ex j being Nat st
( b₂ < j & not (SAT M) . [(n + b₂),('not' p)] = 1 ) )

hence ( not (SAT M) . [(n + i),('not' q)] = 1 or ex j being Nat st
( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ) ; :: thesis: verum

end;

suppose ex j being Element of NAT st
( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ; :: thesis: ( not (SAT M) . [(n + b₁),('not' q)] = 1 or ex j being Nat st
( b₂ < j & not (SAT M) . [(n + b₂),('not' p)] = 1 ) )

hence ( not (SAT M) . [(n + i),('not' q)] = 1 or ex j being Nat st
( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ) ; :: thesis: verum

end;

end;

end;

assume that
A3: for i being Element of NAT holds
( not (SAT M) . [(n + i),p] = 1 or ex j being Element of NAT st
( j <= i & not (SAT M) . [(n + j),q] = 1 ) ) and
A4: not for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ; :: thesis: contradiction

A5: now

let i be Nat; :: thesis: ( not (SAT M) . [(n + i),p] = 1 or ex j being Nat st
( j <= i & not (SAT M) . [(n + j),q] = 1 ) )
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
( not (SAT M) . [(n + ii),p] = 1 or ex j being Element of NAT st
( j <= ii & not (SAT M) . [(n + j),q] = 1 ) ) by A3;
hence ( not (SAT M) . [(n + i),p] = 1 or ex j being Nat st
( j <= i & not (SAT M) . [(n + j),q] = 1 ) ) ; :: thesis: verum

end;

A6: for k being Nat st ( for m being Nat st m < k holds
S₁[m] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for m being Nat st m < k holds
S₁[m] ) implies S₁[k] )
assume A7: for m being Nat st m < k holds
S₁[m] ; :: thesis: S₁[k]

now

assume ex j being Nat st
( j < k & not (SAT M) . [(n + j),('not' p)] = 1 ) ; :: thesis: contradiction
then consider j being Nat such that
A8: j < k and
A9: not (SAT M) . [(n + j),('not' p)] = 1 ;
not (SAT M) . [(n + j),p] = 0 by A9, Th6;
hence contradiction by A7, A8; :: thesis: verum

end;

then not (SAT M) . [(n + k),('not' q)] = 1 by A2;
then A10: not (SAT M) . [(n + k),q] = 0 by Th6;
then A11: (SAT M) . [(n + k),q] = 1 by XBOOLEAN:def 3;

now

assume ex j being Nat st
( j <= k & not (SAT M) . [(n + j),q] = 1 ) ; :: thesis: contradiction
then consider j being Nat such that
A12: j <= k and
A13: not (SAT M) . [(n + j),q] = 1 ;

per cases ( j < k or not j < k ) ;

suppose j < k ; :: thesis: contradiction

hence contradiction by A7, A13; :: thesis: verum

end;

suppose not j < k ; :: thesis: contradiction

hence contradiction by A11, A12, A13, XXREAL_0:1; :: thesis: verum

end;

end;

end;

then not (SAT M) . [(n + k),p] = 1 by A5;
hence S₁[k] by A10, XBOOLEAN:def 3; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 4(A6);
hence contradiction by A4; :: thesis: verum

end;

thus ( ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) implies (SAT M) . [n,(p 'R' q)] = 1 ) :: thesis: verum

proof

assume A14: ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) ; :: thesis: (SAT M) . [n,(p 'R' q)] = 1
assume not (SAT M) . [n,(p 'R' q)] = 1 ; :: thesis: contradiction
then not (SAT M) . [n,(('not' p) 'U' ('not' q))] = 0 by Th6;
then A15: (SAT M) . [n,(('not' p) 'U' ('not' q))] = 1 by XBOOLEAN:def 3;

per cases ( ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) or for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ) by A14;

suppose ex i being Element of NAT st
( (SAT M) . [(n + i),p] = 1 & ( for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ) ) ; :: thesis: contradiction

then consider i being Element of NAT such that
A16: (SAT M) . [(n + i),p] = 1 and
A17: for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ;
consider k being Element of NAT such that
A18: (SAT M) . [(n + k),('not' q)] = 1 and
A19: for j being Element of NAT st j < k holds
(SAT M) . [(n + j),('not' p)] = 1 by A15, Th13;

per cases ( k <= i or not k <= i ) ;

suppose k <= i ; :: thesis: contradiction

then (SAT M) . [(n + k),q] = 1 by A17;
hence contradiction by A18, Th6; :: thesis: verum

end;

suppose not k <= i ; :: thesis: contradiction

then (SAT M) . [(n + i),('not' p)] = 1 by A19;
hence contradiction by A16, Th6; :: thesis: verum

end;

end;

end;

suppose A20: for i being Element of NAT holds (SAT M) . [(n + i),q] = 1 ; :: thesis: contradiction

consider i being Element of NAT such that
A21: (SAT M) . [(n + i),('not' q)] = 1 and
for j being Element of NAT st j < i holds
(SAT M) . [(n + j),('not' p)] = 1 by A15, Th13;
(SAT M) . [(n + i),q] = 0 by A21, Th6;
hence contradiction by A20; :: thesis: verum

end;

end;

end;