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

for M being LTLModel holds (SAT M) . [n,('not' ('X' B))] = (SAT M) . [n,('X' ('not' B))]

let n be Element of NAT ; :: thesis: for M being LTLModel holds (SAT M) . [n,('not' ('X' B))] = (SAT M) . [n,('X' ('not' B))]

let M be LTLModel; :: thesis: (SAT M) . [n,('not' ('X' B))] = (SAT M) . [n,('X' ('not' B))]

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

.= ((SAT M) . [(n + 1),B]) => ((SAT M) . [n,TFALSUM]) by Th9

.= ((SAT M) . [(n + 1),B]) => FALSE by Def11

.= ((SAT M) . [(n + 1),B]) => ((SAT M) . [(n + 1),TFALSUM]) by Def11

.= (SAT M) . [(n + 1),(B => TFALSUM)] by Def11

.= (SAT M) . [n,('X' ('not' B))] by Th9 ; :: thesis: verum

for M being LTLModel holds (SAT M) . [n,('not' ('X' B))] = (SAT M) . [n,('X' ('not' B))]

let n be Element of NAT ; :: thesis: for M being LTLModel holds (SAT M) . [n,('not' ('X' B))] = (SAT M) . [n,('X' ('not' B))]

let M be LTLModel; :: thesis: (SAT M) . [n,('not' ('X' B))] = (SAT M) . [n,('X' ('not' B))]

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

.= ((SAT M) . [(n + 1),B]) => ((SAT M) . [n,TFALSUM]) by Th9

.= ((SAT M) . [(n + 1),B]) => FALSE by Def11

.= ((SAT M) . [(n + 1),B]) => ((SAT M) . [(n + 1),TFALSUM]) by Def11

.= (SAT M) . [(n + 1),(B => TFALSUM)] by Def11

.= (SAT M) . [n,('X' ('not' B))] by Th9 ; :: thesis: verum