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' C) 'or' ('X' (B '&&' (B 'U' C)))))] = 1

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

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

set sm = SAT M;

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

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

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

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

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

set sm = SAT M;

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

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

A2: (SAT M) . [n,(('X' C) 'or' ('X' (B '&&' (B 'U' C))))] = 0 and

A3: (SAT M) . [n,(B 'U' C)] = 1 ; :: thesis: contradiction

consider i being Element of NAT such that

A4: 0 < i and

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

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

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

A7: not (SAT M) . [n,('X' C)] = 1 by A2, Th8;

not (SAT M) . [n,('X' (B '&&' (B 'U' C)))] = 1 by A2, Th8;

then (SAT M) . [n,('X' (B '&&' (B 'U' C)))] = 0 by XBOOLEAN:def 3;

then A8: (SAT M) . [(n + 1),(B '&&' (B 'U' C))] = 0 by Th9;

end;A2: (SAT M) . [n,(('X' C) 'or' ('X' (B '&&' (B 'U' C))))] = 0 and

A3: (SAT M) . [n,(B 'U' C)] = 1 ; :: thesis: contradiction

consider i being Element of NAT such that

A4: 0 < i and

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

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

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

A7: not (SAT M) . [n,('X' C)] = 1 by A2, Th8;

not (SAT M) . [n,('X' (B '&&' (B 'U' C)))] = 1 by A2, Th8;

then (SAT M) . [n,('X' (B '&&' (B 'U' C)))] = 0 by XBOOLEAN:def 3;

then A8: (SAT M) . [(n + 1),(B '&&' (B 'U' C))] = 0 by Th9;

per cases
( i = 1 or i > 1 )
by A4, NAT_1:25;

end;

suppose A9:
i > 1
; :: thesis: contradiction

A15: i + (- 1) > 1 + (- 1) by A9, XREAL_1:8;

n + i = (n + 1) + (i - 1)

.= (n + 1) + (i -' 1) by A15, XREAL_0:def 2 ;

hence contradiction by A5, A6, A9, A15, A10, A14, Def11; :: thesis: verum

end;

A10: now :: thesis: for j being Element of NAT st 1 <= j & j < i -' 1 holds

(SAT M) . [((n + 1) + j),B] = 1

A14:
( not (SAT M) . [(n + 1),B] = 1 or not (SAT M) . [(n + 1),(B 'U' C)] = 1 )
by A8, Th7;(SAT M) . [((n + 1) + j),B] = 1

let j be Element of NAT ; :: thesis: ( 1 <= j & j < i -' 1 implies (SAT M) . [((n + 1) + j),B] = 1 )

assume that

A11: 1 <= j and

A12: j < i -' 1 ; :: thesis: (SAT M) . [((n + 1) + j),B] = 1

j + 1 < (i -' 1) + 1 by A12, XREAL_1:8;

then A13: j + 1 < (i - 1) + 1 by A12, XREAL_0:def 2;

1 <= j + 1 by A11, NAT_1:19;

then (SAT M) . [(n + (j + 1)),B] = 1 by A6, A13;

hence (SAT M) . [((n + 1) + j),B] = 1 ; :: thesis: verum

end;assume that

A11: 1 <= j and

A12: j < i -' 1 ; :: thesis: (SAT M) . [((n + 1) + j),B] = 1

j + 1 < (i -' 1) + 1 by A12, XREAL_1:8;

then A13: j + 1 < (i - 1) + 1 by A12, XREAL_0:def 2;

1 <= j + 1 by A11, NAT_1:19;

then (SAT M) . [(n + (j + 1)),B] = 1 by A6, A13;

hence (SAT M) . [((n + 1) + j),B] = 1 ; :: thesis: verum

A15: i + (- 1) > 1 + (- 1) by A9, XREAL_1:8;

n + i = (n + 1) + (i - 1)

.= (n + 1) + (i -' 1) by A15, XREAL_0:def 2 ;

hence contradiction by A5, A6, A9, A15, A10, A14, Def11; :: thesis: verum

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

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