let A be Element of LTLB_WFF ; :: thesis: for n being Element of NAT

for M being LTLModel holds

( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 )

let n be Element of NAT ; :: thesis: for M being LTLModel holds

( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 )

let M be LTLModel; :: thesis: ( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 )

thus (SAT M) . [n,('not' A)] = ((SAT M) . [n,A]) => ((SAT M) . [n,TFALSUM]) by Def11

.= 1 by A2 ; :: thesis: verum

for M being LTLModel holds

( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 )

let n be Element of NAT ; :: thesis: for M being LTLModel holds

( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 )

let M be LTLModel; :: thesis: ( (SAT M) . [n,('not' A)] = 1 iff (SAT M) . [n,A] = 0 )

hereby :: thesis: ( (SAT M) . [n,A] = 0 implies (SAT M) . [n,('not' A)] = 1 )

assume A2:
(SAT M) . [n,A] = 0
; :: thesis: (SAT M) . [n,('not' A)] = 1assume
(SAT M) . [n,('not' A)] = 1
; :: thesis: (SAT M) . [n,A] = 0

then A1: ((SAT M) . [n,A]) => ((SAT M) . [n,TFALSUM]) = 1 by Def11;

( (SAT M) . [n,A] = 1 or (SAT M) . [n,A] = 0 ) by XBOOLEAN:def 3;

hence (SAT M) . [n,A] = 0 by A1, Def11; :: thesis: verum

end;then A1: ((SAT M) . [n,A]) => ((SAT M) . [n,TFALSUM]) = 1 by Def11;

( (SAT M) . [n,A] = 1 or (SAT M) . [n,A] = 0 ) by XBOOLEAN:def 3;

hence (SAT M) . [n,A] = 0 by A1, Def11; :: thesis: verum

thus (SAT M) . [n,('not' A)] = ((SAT M) . [n,A]) => ((SAT M) . [n,TFALSUM]) by Def11

.= 1 by A2 ; :: thesis: verum