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;

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

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

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

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;

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

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;

now :: thesis: for j being Element of NAT st j < i holds
(SAT M) . [(n + j),p] = 1

let j be Element of NAT ; :: thesis: ( j < i implies (SAT M) . [(n + b₁),p] = 1 )
assume A7: j < i ; :: thesis: (SAT M) . [(n + b₁),p] = 1

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

suppose j = 0 ; :: thesis: (SAT M) . [(n + b₁),p] = 1

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

end;

suppose not j = 0 ; :: thesis: (SAT M) . [(n + b₁),p] = 1

then 1 <= j by NAT_1:25;
hence (SAT M) . [(n + j),p] = 1 by A6, A7; :: thesis: verum

end;

end;

end;

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 A5; :: thesis: verum

end;

end;

end;

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

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

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

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;

end;