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

for M being LTLModel holds (SAT M) . [n,((B 'U' C) => ('X' ('F' C)))] = 1

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

let M be LTLModel; :: thesis: (SAT M) . [n,((B 'U' C) => ('X' ('F' C)))] = 1

set sm = SAT M;

then ((SAT M) . [n,(B 'U' C)]) => ((SAT M) . [n,('X' ('F' C))]) = 1 by A1, XBOOLEAN:def 3;

hence (SAT M) . [n,((B 'U' C) => ('X' ('F' C)))] = 1 by Def11; :: thesis: verum

for M being LTLModel holds (SAT M) . [n,((B 'U' C) => ('X' ('F' C)))] = 1

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

let M be LTLModel; :: thesis: (SAT M) . [n,((B 'U' C) => ('X' ('F' C)))] = 1

set sm = SAT M;

A1: now :: thesis: ( (SAT M) . [n,(B 'U' C)] = 1 implies not (SAT M) . [n,('X' ('F' C))] = 0 )

( (SAT M) . [n,(B 'U' C)] = 0 or (SAT M) . [n,(B 'U' C)] = 1 )
by XBOOLEAN:def 3;assume that

A2: (SAT M) . [n,(B 'U' C)] = 1 and

A3: (SAT M) . [n,('X' ('F' C))] = 0 ; :: thesis: contradiction

consider i being Element of NAT such that

A4: 0 < i and

A5: (SAT M) . [(n + i),C] = 1 and

for j being Element of NAT st 1 <= j & j < i holds

(SAT M) . [(n + j),B] = 1 by A2, Def11;

i + (- 1) >= 1 + (- 1) by A4, NAT_1:25, XREAL_1:6;

then A6: (n + 1) + (i -' 1) = (n + 1) + (i - 1) by XREAL_0:def 2

.= n + i ;

(SAT M) . [(n + 1),('F' C)] = 0 by A3, Th9;

hence contradiction by A5, A6, Th11; :: thesis: verum

end;A2: (SAT M) . [n,(B 'U' C)] = 1 and

A3: (SAT M) . [n,('X' ('F' C))] = 0 ; :: thesis: contradiction

consider i being Element of NAT such that

A4: 0 < i and

A5: (SAT M) . [(n + i),C] = 1 and

for j being Element of NAT st 1 <= j & j < i holds

(SAT M) . [(n + j),B] = 1 by A2, Def11;

i + (- 1) >= 1 + (- 1) by A4, NAT_1:25, XREAL_1:6;

then A6: (n + 1) + (i -' 1) = (n + 1) + (i - 1) by XREAL_0:def 2

.= n + i ;

(SAT M) . [(n + 1),('F' C)] = 0 by A3, Th9;

hence contradiction by A5, A6, Th11; :: thesis: verum

then ((SAT M) . [n,(B 'U' C)]) => ((SAT M) . [n,('X' ('F' C))]) = 1 by A1, XBOOLEAN:def 3;

hence (SAT M) . [n,((B 'U' C) => ('X' ('F' C)))] = 1 by Def11; :: thesis: verum