let p, q be Element of LTLB_WFF ; 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; 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 ; ( (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;
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
; (SAT M) . [i,(p 'U' q)] = 1
reconsider n = j - i as Element of NAT by A6, NAT_1:21;
( 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; verum