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) 'Uw' ('not' q))] = 0 by Th5;

A2: now :: thesis: for i being Nat holds
( not (SAT M) . [(n + i),('not' q)] = 1 or ex j being Nat st
( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) )

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, Th12;

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 :: thesis: for i being Nat holds
( not (SAT M) . [(n + i),p] = 1 or ex j being Nat st
( j <= i & not (SAT M) . [(n + j),q] = 1 ) )

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]
reconsider nk = n + k as Element of NAT by ORDINAL1:def 12;

now :: thesis: for j being Nat holds
( not j < k or (SAT M) . [(n + j),('not' p)] = 1 )

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 ;
reconsider nj = n + j as Element of NAT by ORDINAL1:def 12;
not (SAT M) . [nj,p] = 0 by A9, Th5;
hence contradiction by A7, A8; :: thesis: verum

end;

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

now :: thesis: for j being Nat holds
( not j <= k or (SAT M) . [(n + j),q] = 1 )

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

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

suppose j < k ; :: thesis: contradiction

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

end;

suppose not j < k ; :: thesis: contradiction

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

end;

end;

end;

hence S₁[k] by XBOOLEAN:def 3, A5; :: 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 A13: ( 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 A14: (SAT M) . [n,(('not' p) 'Uw' ('not' q))] = 1 by XBOOLEAN:def 3, Th5;

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

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
A15: (SAT M) . [(n + i),p] = 1 and
A16: for j being Element of NAT st j <= i holds
(SAT M) . [(n + j),q] = 1 ;
consider k being Element of NAT such that
A17: (SAT M) . [(n + k),('not' q)] = 1 and
A18: for j being Element of NAT st j < k holds
(SAT M) . [(n + j),('not' p)] = 1 by A14, Th12;

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

suppose k <= i ; :: thesis: contradiction

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

end;

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

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

end;

end;

end;

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

consider i being Element of NAT such that
A20: (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 A14, Th12;
(SAT M) . [(n + i),q] = 0 by A20, Th5;
hence contradiction by A19; :: thesis: verum

end;

end;

end;