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