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;

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

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;

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

suppose i = 1 ; :: thesis: contradiction

hence contradiction by A5, A7, Th9; :: thesis: verum

end;

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

A10: now :: thesis: for j being Element of NAT st 1 <= j & j < i -' 1 holds
(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;

A14: ( not (SAT M) . [(n + 1),B] = 1 or not (SAT M) . [(n + 1),(B 'U' C)] = 1 ) by A8, Th7;
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;

end;

end;

( (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;
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