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;

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

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 )

( (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))))] = 1 and

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

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

end;

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;(SAT M) . [(n + j),B] = 1 ;

(SAT M) . [(n + 1),C] = 1 by A4, Th9;

hence contradiction by A3, A5, Def11; :: thesis: verum

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;

hence contradiction by A3, A9, Def11; :: thesis: verum

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

(SAT M) . [(n + (1 + i)),C] = 1
by A7;(SAT M) . [(n + j),B] = 1

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

assume A10: ( 1 <= j & j < 1 + i ) ; :: thesis: (SAT M) . [(n + b_{1}),B] = 1

end;assume A10: ( 1 <= j & j < 1 + i ) ; :: thesis: (SAT M) . [(n + b

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

end;

suppose A11:
( 1 < j & j < i + 1 )
; :: thesis: (SAT M) . [(n + b_{1}),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;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

hence contradiction by A3, A9, Def11; :: thesis: verum

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