let p, q be Element of LTLB_WFF ; :: thesis: for n being Element of NAT

for M being LTLModel holds

( (SAT M) . [n,(p 'Uw' q)] = 1 iff ex i being Element of NAT st

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) ) )

let n be Element of NAT ; :: thesis: for M being LTLModel holds

( (SAT M) . [n,(p 'Uw' q)] = 1 iff ex i being Element of NAT st

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) ) )

let M be LTLModel; :: thesis: ( (SAT M) . [n,(p 'Uw' q)] = 1 iff ex i being Element of NAT st

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) ) )

set sm = SAT M;

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) ) ; :: thesis: (SAT M) . [n,(p 'Uw' q)] = 1

then consider i being Element of NAT such that

A8: (SAT M) . [(n + i),q] = 1 and

A9: for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ;

for M being LTLModel holds

( (SAT M) . [n,(p 'Uw' q)] = 1 iff ex i being Element of NAT st

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) ) )

let n be Element of NAT ; :: thesis: for M being LTLModel holds

( (SAT M) . [n,(p 'Uw' q)] = 1 iff ex i being Element of NAT st

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) ) )

let M be LTLModel; :: thesis: ( (SAT M) . [n,(p 'Uw' q)] = 1 iff ex i being Element of NAT st

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) ) )

set sm = SAT M;

hereby :: thesis: ( ex i being Element of NAT st

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) ) implies (SAT M) . [n,(p 'Uw' q)] = 1 )

assume
ex i being Element of NAT st ( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) ) implies (SAT M) . [n,(p 'Uw' q)] = 1 )

assume A1:
(SAT M) . [n,(p 'Uw' q)] = 1
; :: thesis: ex i being Element of NAT st

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) )

end;( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) )

per cases
( (SAT M) . [n,q] = 1 or (SAT M) . [n,(p '&&' (p 'U' q))] = 1 )
by A1, Th8;

end;

suppose A2:
(SAT M) . [n,q] = 1
; :: thesis: ex i being Element of NAT st

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) )

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) )

A3:
for j being Element of NAT st j < 0 holds

(SAT M) . [(n + j),p] = 1 ;

(SAT M) . [(n + 0),q] = 1 by A2;

hence ex i being Element of NAT st

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) ) by A3; :: thesis: verum

end;(SAT M) . [(n + j),p] = 1 ;

(SAT M) . [(n + 0),q] = 1 by A2;

hence ex i being Element of NAT st

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) ) by A3; :: thesis: verum

suppose A4:
(SAT M) . [n,(p '&&' (p 'U' q))] = 1
; :: thesis: ex i being Element of NAT st

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) )

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) )

then
(SAT M) . [n,(p 'U' q)] = 1
by Th7;

then consider i being Element of NAT such that

0 < i and

A5: (SAT M) . [(n + i),q] = 1 and

A6: for j being Element of NAT st 1 <= j & j < i holds

(SAT M) . [(n + j),p] = 1 by Def11;

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) ) by A5; :: thesis: verum

end;then consider i being Element of NAT such that

0 < i and

A5: (SAT M) . [(n + i),q] = 1 and

A6: for j being Element of NAT st 1 <= j & j < i holds

(SAT M) . [(n + j),p] = 1 by Def11;

now :: thesis: for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1

hence
ex i being Element of NAT st (SAT M) . [(n + j),p] = 1

let j be Element of NAT ; :: thesis: ( j < i implies (SAT M) . [(n + b_{1}),p] = 1 )

assume A7: j < i ; :: thesis: (SAT M) . [(n + b_{1}),p] = 1

end;assume A7: j < i ; :: thesis: (SAT M) . [(n + b

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) ) by A5; :: thesis: verum

( (SAT M) . [(n + i),q] = 1 & ( for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ) ) ; :: thesis: (SAT M) . [n,(p 'Uw' q)] = 1

then consider i being Element of NAT such that

A8: (SAT M) . [(n + i),q] = 1 and

A9: for j being Element of NAT st j < i holds

(SAT M) . [(n + j),p] = 1 ;

per cases
( i = 0 or not i = 0 )
;

end;

suppose A10:
not i = 0
; :: thesis: (SAT M) . [n,(p 'Uw' q)] = 1

for j being Element of NAT st 1 <= j & j < i holds

(SAT M) . [(n + j),p] = 1 by A9;

then A11: (SAT M) . [n,(p 'U' q)] = 1 by A8, A10, Def11;

(SAT M) . [(n + 0),p] = 1 by A9, A10;

then (SAT M) . [n,(p '&&' (p 'U' q))] = 1 by A11, Th7;

hence (SAT M) . [n,(p 'Uw' q)] = 1 by Th8; :: thesis: verum

end;(SAT M) . [(n + j),p] = 1 by A9;

then A11: (SAT M) . [n,(p 'U' q)] = 1 by A8, A10, Def11;

(SAT M) . [(n + 0),p] = 1 by A9, A10;

then (SAT M) . [n,(p '&&' (p 'U' q))] = 1 by A11, Th7;

hence (SAT M) . [n,(p 'Uw' q)] = 1 by Th8; :: thesis: verum