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

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

assume that
A2: (SAT M) . [n,(('X' C) 'or' ('X' (B '&&' (B 'U' C))))] = 1 and
A3: (SAT M) . [n,(B 'U' C)] = 0 ; :: thesis: contradiction

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

suppose A4: (SAT M) . [n,('X' C)] = 1 ; :: thesis: contradiction

A5: for j being Element of NAT st 1 <= j & j < 1 holds
(SAT M) . [(n + j),B] = 1 ;
(SAT M) . [(n + 1),C] = 1 by A4, Th9;
hence contradiction by A3, A5, Def11; :: thesis: verum

end;

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

then A6: (SAT M) . [(n + 1),(B '&&' (B 'U' C))] = 1 by Th9;
then (SAT M) . [(n + 1),(B 'U' C)] = 1 by Th7;
then consider i being Element of NAT such that
i > 0 and
A7: (SAT M) . [((n + 1) + i),C] = 1 and
A8: for j being Element of NAT st 1 <= j & j < i holds
(SAT M) . [((n + 1) + j),B] = 1 by Def11;

A9: now :: thesis: for j being Element of NAT st 1 <= j & j < 1 + i holds
(SAT M) . [(n + j),B] = 1

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

per cases ( 1 = j or ( 1 < j & j < i + 1 ) ) by A10, NAT_1:25;

suppose 1 = j ; :: thesis: (SAT M) . [(n + b₁),B] = 1

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

end;

suppose A11: ( 1 < j & j < i + 1 ) ; :: thesis: (SAT M) . [(n + b₁),B] = 1

then A12: 1 + (- 1) < j + (- 1) by XREAL_1:8;
then j - 1 > 0 ;
then j -' 1 > 0 by XREAL_0:def 2;
then A13: 1 <= j -' 1 by NAT_1:25;
A14: ((n + j) + 1) - 1 = (n + 1) + (j - 1)
.= (n + 1) + (j -' 1) by A12, XREAL_0:def 2 ;
j + (- 1) < (i + 1) + (- 1) by A11, XREAL_1:8;
hence (SAT M) . [(n + j),B] = 1 by A8, A14, A13; :: thesis: verum

end;

end;

end;

(SAT M) . [(n + (1 + i)),C] = 1 by A7;
hence contradiction by A3, A9, 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,(('X' C) 'or' ('X' (B '&&' (B 'U' C))))]) => ((SAT M) . [n,(B 'U' C)]) = 1 by A1, XBOOLEAN:def 3;
hence (SAT M) . [n,((('X' C) 'or' ('X' (B '&&' (B 'U' C)))) => (B 'U' C))] = 1 by Def11; :: thesis: verum