let B, C be Element of LTLB_WFF ; :: thesis: for n being Element of NAT
for M being LTLModel holds (SAT M) . [n,(('X' (B => C)) => (('X' B) => ('X' C)))] = 1
let n be Element of NAT ; :: thesis: for M being LTLModel holds (SAT M) . [n,(('X' (B => C)) => (('X' B) => ('X' C)))] = 1
let M be LTLModel; :: thesis: (SAT M) . [n,(('X' (B => C)) => (('X' B) => ('X' C)))] = 1
A1: ( (SAT M) . [(n + 1),B] = 0 or (SAT M) . [(n + 1),B] = 1 ) by XBOOLEAN:def 3;
A2: ( (SAT M) . [(n + 1),C] = 0 or (SAT M) . [(n + 1),C] = 1 ) by XBOOLEAN:def 3;
thus (SAT M) . [n,(('X' (B => C)) => (('X' B) => ('X' C)))] = ((SAT M) . [n,('X' (B => C))]) => ((SAT M) . [n,(('X' B) => ('X' C))]) by Def11
.= ((SAT M) . [(n + 1),(B => C)]) => ((SAT M) . [n,(('X' B) => ('X' C))]) by Th9
.= ((SAT M) . [(n + 1),(B => C)]) => (((SAT M) . [n,('X' B)]) => ((SAT M) . [n,('X' C)])) by Def11
.= ((SAT M) . [(n + 1),(B => C)]) => (((SAT M) . [(n + 1),B]) => ((SAT M) . [n,('X' C)])) by Th9
.= ((SAT M) . [(n + 1),(B => C)]) => (((SAT M) . [(n + 1),B]) => ((SAT M) . [(n + 1),C])) by Th9
.= 1 by A1, A2, Def11 ; :: thesis: verum