let A be Element of LTLB_WFF ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( (SAT M) . [n,('F' A)] = 1 iff ex i being Element of NAT st (SAT M) . [(n + i),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; :: thesis: verum

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 ; :: thesis: 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; :: thesis: ( (SAT M) . [n,('F' A)] = 1 iff ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 )

hereby :: thesis: ( ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 implies (SAT M) . [n,('F' A)] = 1 )

assume
ex i being Element of NAT st (SAT M) . [(n + i),A] = 1
; :: thesis: (SAT M) . [n,('F' A)] = 1assume
(SAT M) . [n,('F' A)] = 1
; :: thesis: ex i being Element of NAT st (SAT M) . [(n + i),A] = 1

then (SAT M) . [n,('G' ('not' A))] = 0 by Th5;

then consider i being Element of NAT such that

A1: not (SAT M) . [(n + i),('not' A)] = 1 by Th10;

not (SAT M) . [(n + i),A] = 0 by A1, Th5;

hence ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 by XBOOLEAN:def 3; :: thesis: verum

end;then (SAT M) . [n,('G' ('not' A))] = 0 by Th5;

then consider i being Element of NAT such that

A1: not (SAT M) . [(n + i),('not' A)] = 1 by Th10;

not (SAT M) . [(n + i),A] = 0 by A1, Th5;

hence ex i being Element of NAT st (SAT M) . [(n + i),A] = 1 by XBOOLEAN:def 3; :: thesis: verum

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