let A be Element of LTLB_WFF ; for n being Element of NAT
for M being LTLModel holds
( (SAT M) . [n,('F' A)] = 1 iff ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 )
let n be Element of NAT ; for M being LTLModel holds
( (SAT M) . [n,('F' A)] = 1 iff ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 )
let M be LTLModel; ( (SAT M) . [n,('F' A)] = 1 iff ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 )
assume
ex i being Element of NAT st (SAT M) . [(n + i),A] = 1
; (SAT M) . [n,('F' A)] = 1
then consider i being Element of NAT such that
A2:
(SAT M) . [(n + i),A] = 1
;
not (SAT M) . [(n + i),('not' A)] = 1
by A2, Th5;
then
not (SAT M) . [n,('G' ('not' A))] = 1
by Th10;
hence
(SAT M) . [n,('F' A)] = 1
by Th5, XBOOLEAN:def 3; verum