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

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