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 )

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

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

thus
( ( ex i being Element of NAT st
defpred S_{1}[ 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;

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

S_{1}[m] ) holds

S_{1}[k]
_{1}[i]
from NAT_1:sch 4(A6);

hence contradiction by A4; :: thesis: verum

end;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 ) )

assume that ( 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_{1}),('not' q)] = 1 or ex j being Nat st

( b_{2} < j & not (SAT M) . [(n + b_{2}),('not' p)] = 1 ) )

reconsider ii = i as Element of NAT by ORDINAL1:def 12;

end;( b

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;

end;

( 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_{1}),('not' q)] = 1 or ex j being Nat st

( b_{2} < j & not (SAT M) . [(n + b_{2}),('not' p)] = 1 ) )

( b

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;( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ) ; :: thesis: verum

suppose
ex j being Element of NAT st

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

( b_{2} < j & not (SAT M) . [(n + b_{2}),('not' p)] = 1 ) )

( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ; :: thesis: ( not (SAT M) . [(n + b

( b

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;( j < i & not (SAT M) . [(n + j),('not' p)] = 1 ) ) ; :: thesis: verum

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 ) )

A6:
for k being Nat st ( for m being Nat st m < k 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;( 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

S

S

proof

for i being Nat holds S
let k be Nat; :: thesis: ( ( for m being Nat st m < k holds

S_{1}[m] ) implies S_{1}[k] )

assume A7: for m being Nat st m < k holds

S_{1}[m]
; :: thesis: S_{1}[k]

reconsider nk = n + k as Element of NAT by ORDINAL1:def 12;

then not (SAT M) . [nk,q] = 0 by Th5;

then A10: (SAT M) . [(n + k),q] = 1 by XBOOLEAN:def 3;

_{1}[k]
by XBOOLEAN:def 3, A5; :: thesis: verum

end;S

assume A7: for m being Nat st m < k holds

S

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 )

then
not (SAT M) . [(n + k),('not' q)] = 1
by A2;( 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;( 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

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 )

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

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

hence contradiction by A4; :: thesis: verum

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

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

end;

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

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

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

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