let H1, H2 be LTL-formula; :: thesis: for r being Element of Inf_seq AtomicFamily holds
( r |= H1 'U' H2 iff r |= H2 'or' (H1 '&' ('X' (H1 'U' H2))) )
let r be Element of Inf_seq AtomicFamily; :: thesis: ( r |= H1 'U' H2 iff r |= H2 'or' (H1 '&' ('X' (H1 'U' H2))) )
A1: ( r |= H2 'or' (H1 '&' ('X' (H1 'U' H2))) implies r |= H1 'U' H2 )

proof

assume A2: r |= H2 'or' (H1 '&' ('X' (H1 'U' H2))) ; :: thesis: r |= H1 'U' H2

now :: thesis: r |= H1 'U' H2

per cases ( r |= H2 or r |= H1 '&' ('X' (H1 'U' H2)) ) by A2, Th66;

suppose A3: r |= H2 ; :: thesis: r |= H1 'U' H2

ex m being Nat st
( ( for j being Nat st j < m holds
Shift (r,j) |= H1 ) & Shift (r,m) |= H2 )

proof

take 0 ; :: thesis: ( ( for j being Nat st j < 0 holds
Shift (r,j) |= H1 ) & Shift (r,0) |= H2 )
thus ( ( for j being Nat st j < 0 holds
Shift (r,j) |= H1 ) & Shift (r,0) |= H2 ) by A3, Lm28; :: thesis: verum

end;

hence r |= H1 'U' H2 by Th68; :: thesis: verum

end;

suppose A4: r |= H1 '&' ('X' (H1 'U' H2)) ; :: thesis: r |= H1 'U' H2

set r1 = Shift (r,1);
r |= 'X' (H1 'U' H2) by A4, Th65;
then Shift (r,1) |= H1 'U' H2 by Th67;
then consider m being Nat such that
A5: for j being Nat st j < m holds
Shift ((Shift (r,1)),j) |= H1 and
A6: Shift ((Shift (r,1)),m) |= H2 by Th68;
set m1 = m + 1;
A7: r |= H1 by A4, Th65;
A8: for j being Nat st j < m + 1 holds
Shift (r,j) |= H1

proof

let j be Nat; :: thesis: ( j < m + 1 implies Shift (r,j) |= H1 )
assume A9: j < m + 1 ; :: thesis: Shift (r,j) |= H1

now :: thesis: Shift (r,j) |= H1

per cases ( j = 0 or j > 0 ) ;

suppose j = 0 ; :: thesis: Shift (r,j) |= H1

hence Shift (r,j) |= H1 by A7, Lm28; :: thesis: verum

end;

suppose A10: j > 0 ; :: thesis: Shift (r,j) |= H1

set j1 = j - 1;
reconsider j1 = j - 1 as Nat by A10, NAT_1:20;
j - 1 < (m + 1) - 1 by A9, XREAL_1:14;
then Shift ((Shift (r,1)),j1) |= H1 by A5;
then Shift (r,(j1 + 1)) |= H1 by Lm29;
hence Shift (r,j) |= H1 ; :: thesis: verum

end;

end;

end;

hence Shift (r,j) |= H1 ; :: thesis: verum

end;

Shift (r,(m + 1)) |= H2 by A6, Lm29;
hence r |= H1 'U' H2 by A8, Th68; :: thesis: verum

end;

end;

end;

hence r |= H1 'U' H2 ; :: thesis: verum

end;

( r |= H1 'U' H2 implies r |= H2 'or' (H1 '&' ('X' (H1 'U' H2))) )

proof

assume r |= H1 'U' H2 ; :: thesis: r |= H2 'or' (H1 '&' ('X' (H1 'U' H2)))
then consider m being Nat such that
A11: for j being Nat st j < m holds
Shift (r,j) |= H1 and
A12: Shift (r,m) |= H2 by Th68;

per cases ( m = 0 or m > 0 ) ;

suppose m = 0 ; :: thesis: r |= H2 'or' (H1 '&' ('X' (H1 'U' H2)))

then r |= H2 by A12, Lm28;
hence r |= H2 'or' (H1 '&' ('X' (H1 'U' H2))) by Th66; :: thesis: verum

end;

suppose A13: m > 0 ; :: thesis: r |= H2 'or' (H1 '&' ('X' (H1 'U' H2)))

set k = m - 1;
reconsider k = m - 1 as Nat by A13, NAT_1:20;
set r1 = Shift (r,1);
A14: for j being Nat st j < k holds
Shift ((Shift (r,1)),j) |= H1

proof

let j be Nat; :: thesis: ( j < k implies Shift ((Shift (r,1)),j) |= H1 )
assume j < k ; :: thesis: Shift ((Shift (r,1)),j) |= H1
then A15: j + 1 < k + 1 by XREAL_1:8;
Shift (r,(j + 1)) = Shift ((Shift (r,1)),j) by Lm29;
hence Shift ((Shift (r,1)),j) |= H1 by A11, A15; :: thesis: verum

end;

Shift (r,(k + 1)) = Shift ((Shift (r,1)),k) by Lm29;
then Shift (r,1) |= H1 'U' H2 by A12, A14, Th68;
then A16: r |= 'X' (H1 'U' H2) by Th67;
Shift (r,0) = r by Lm28;
then r |= H1 by A11, A13;
then r |= H1 '&' ('X' (H1 'U' H2)) by A16, Th65;
hence r |= H2 'or' (H1 '&' ('X' (H1 'U' H2))) by Th66; :: thesis: verum

end;

end;

end;

hence ( r |= H1 'U' H2 iff r |= H2 'or' (H1 '&' ('X' (H1 'U' H2))) ) by A1; :: thesis: verum