let p, q be Element of LTLB_WFF ; :: thesis: for M being LTLModel
for i being Element of NAT holds
( (SAT M) . [i,(p 'U' q)] = 1 iff ex j being Element of NAT st
( j > i & (SAT M) . [j,q] = 1 & ( for k being Element of NAT st i < k & k < j holds
(SAT M) . [k,p] = 1 ) ) )
let M be LTLModel; :: thesis: for i being Element of NAT holds
( (SAT M) . [i,(p 'U' q)] = 1 iff ex j being Element of NAT st
( j > i & (SAT M) . [j,q] = 1 & ( for k being Element of NAT st i < k & k < j holds
(SAT M) . [k,p] = 1 ) ) )
let i be Element of NAT ; :: thesis: ( (SAT M) . [i,(p 'U' q)] = 1 iff ex j being Element of NAT st
( j > i & (SAT M) . [j,q] = 1 & ( for k being Element of NAT st i < k & k < j holds
(SAT M) . [k,p] = 1 ) ) )
set s = SAT M;

hereby :: thesis: ( ex j being Element of NAT st
( j > i & (SAT M) . [j,q] = 1 & ( for k being Element of NAT st i < k & k < j holds
(SAT M) . [k,p] = 1 ) ) implies (SAT M) . [i,(p 'U' q)] = 1 )

assume (SAT M) . [i,(p 'U' q)] = 1 ; :: thesis: ex j being Element of NAT st
( j > i & (SAT M) . [j,q] = 1 & ( for k being Element of NAT st i < k & k < j holds
(SAT M) . [k,p] = 1 ) )
then consider j being Element of NAT such that
A1: ( 0 < j & (SAT M) . [(i + j),q] = 1 ) and
A2: for k being Element of NAT st 1 <= k & k < j holds
(SAT M) . [(i + k),p] = 1 by LTLAXIO1:def 11;
set m = i + j;

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

let k be Element of NAT ; :: thesis: ( i < k & k < i + j implies (SAT M) . [k,p] = 1 )
assume that
A3: i < k and
A4: k < i + j ; :: thesis: (SAT M) . [k,p] = 1
reconsider k1 = k - i as Element of NAT by A3, NAT_1:21;
i + (- i) < k + (- i) by A3, XREAL_1:8;
then A5: 1 <= k1 by NAT_1:25;
k + (- i) < (i + j) + (- i) by A4, XREAL_1:8;
then (SAT M) . [(i + k1),p] = 1 by A5, A2;
hence (SAT M) . [k,p] = 1 ; :: thesis: verum

end;

hence ex j being Element of NAT st
( j > i & (SAT M) . [j,q] = 1 & ( for k being Element of NAT st i < k & k < j holds
(SAT M) . [k,p] = 1 ) ) by A1, NAT_1:16; :: thesis: verum

end;

given j being Element of NAT such that A6: j > i and
A7: (SAT M) . [j,q] = 1 and
A8: for k being Element of NAT st i < k & k < j holds
(SAT M) . [k,p] = 1 ; :: thesis: (SAT M) . [i,(p 'U' q)] = 1
reconsider n = j - i as Element of NAT by A6, NAT_1:21;

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

let k be Element of NAT ; :: thesis: ( 1 <= k & k < n implies (SAT M) . [(i + k),p] = 1 )
assume ( 1 <= k & k < n ) ; :: thesis: (SAT M) . [(i + k),p] = 1
then ( k + i < n + i & i < i + k ) by XREAL_1:8, NAT_1:16;
hence (SAT M) . [(i + k),p] = 1 by A8; :: thesis: verum

end;

( j + (- i) > i + (- i) & (SAT M) . [(i + n),q] = 1 ) by A6, XREAL_1:8, A7;
hence (SAT M) . [i,(p 'U' q)] = 1 by A9, LTLAXIO1:def 11; :: thesis: verum