let A be Element of LTLB_WFF ; :: thesis: {A} |= 'G' ('X' A)

assume not {A} |= 'G' ('X' A) ; :: thesis: contradiction

then consider M being LTLModel such that

A1: ( M |= {A} & not M |= 'G' ('X' A) ) ;

consider i being Element of NAT such that

A2: not (SAT M) . [i,('G' ('X' A))] = 1 by A1;

consider j being Element of NAT such that

A3: not (SAT M) . [(i + j),('X' A)] = 1 by A2, LTLAXIO1:10;

A4: not (SAT M) . [((i + j) + 1),A] = 1 by A3, LTLAXIO1:9;

A in {A} by TARSKI:def 1;

then M |= A by A1;

hence contradiction by A4; :: thesis: verum

assume not {A} |= 'G' ('X' A) ; :: thesis: contradiction

then consider M being LTLModel such that

A1: ( M |= {A} & not M |= 'G' ('X' A) ) ;

consider i being Element of NAT such that

A2: not (SAT M) . [i,('G' ('X' A))] = 1 by A1;

consider j being Element of NAT such that

A3: not (SAT M) . [(i + j),('X' A)] = 1 by A2, LTLAXIO1:10;

A4: not (SAT M) . [((i + j) + 1),A] = 1 by A3, LTLAXIO1:9;

A in {A} by TARSKI:def 1;

then M |= A by A1;

hence contradiction by A4; :: thesis: verum