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

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, Lm29; :: 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

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

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

hence Shift r,j |= H1 by A7, Lm29; :: 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:16;
then Shift (Shift r,1),j1 |= H1 by A5;
then Shift r,(j1 + 1) |= H1 by Lm30;
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, Lm30;
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, Lm29;
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:10;
Shift r,(j + 1) = Shift (Shift r,1),j by Lm30;
hence Shift (Shift r,1),j |= H1 by A11, A15; :: thesis: verum

end;

Shift r,(k + 1) = Shift (Shift r,1),k by Lm30;
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 Lm29;
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
set G = H1 'U' H2;

end;

end;

end;

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