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 |= 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
B1: for j being Nat st j < m holds
Shift r,j |= H1 and
B2: Shift r,m |= H2 by Th23;

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

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

then r |= H2 by LemShift03, B2;
hence r |= H2 'or' (H1 '&' ('X' (H1 'U' H2))) by Th21; :: thesis: verum

end;

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

set G = H1 'U' H2;
set k = m - 1;
set r1 = Shift r,1;
reconsider k = m - 1 as Nat by B3, NAT_1:20;
B301: Shift r,0 = r by LemShift03;
B302: Shift r,(k + 1) = Shift (Shift r,1),k by LemShift04;
B4: r |= H1 by B1, B3, B301;
B5: 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 C1: j < k ; :: thesis: Shift (Shift r,1),j |= H1
C2: Shift r,(j + 1) = Shift (Shift r,1),j by LemShift04;
j + 1 < k + 1 by C1, XREAL_1:10;
hence Shift (Shift r,1),j |= H1 by B1, C2; :: thesis: verum

end;

Shift r,1 |= H1 'U' H2 by B302, B2, B5, Th23;
then r |= 'X' (H1 'U' H2) by Th22;
then r |= H1 '&' ('X' (H1 'U' H2)) by B4, Th20;
hence r |= H2 'or' (H1 '&' ('X' (H1 'U' H2))) by Th21; :: thesis: verum

end;

end;

end;

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

proof

assume A1: 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 A1, Th21;

suppose B1: 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 B1, LemShift03; :: thesis: verum

end;

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

end;

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

then B1: ( r |= H1 & r |= 'X' (H1 'U' H2) ) by Th20;
then B2: Shift r,1 |= H1 'U' H2 by Th22;
set r1 = Shift r,1;
consider m being Nat such that
B3: for j being Nat st j < m holds
Shift (Shift r,1),j |= H1 and
B4: Shift (Shift r,1),m |= H2 by B2, Th23;
set m1 = m + 1;
B5: 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 C1: 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 LemShift03, B1; :: thesis: verum

end;

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

set j1 = j - 1;
reconsider j1 = j - 1 as Nat by C3, NAT_1:20;
j - 1 < (m + 1) - 1 by C1, XREAL_1:16;
then Shift (Shift r,1),j1 |= H1 by B3;
then Shift r,(j1 + 1) |= H1 by LemShift04;
hence Shift r,j |= H1 ; :: thesis: verum

end;

end;

end;

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

end;

Shift r,(m + 1) |= H2 by B4, LemShift04;
hence r |= H1 'U' H2 by Th23, B5; :: thesis: verum

end;

end;

end;

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

end;

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