[STATEMENT]
lemma 
  iNext_iff: "(\<circle> t t0 I. P t) = (\<box> t [\<dots>0] \<oplus> (inext t0 I). P t)" and
  iLast_iff: "(\<ominus> t t0 I. P t) = (\<box> t [\<dots>0] \<oplus> (iprev t0 I). P t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iNext t0 I P = (\<box> t [\<dots>0] \<oplus> inext t0 I. P t) &&& iLast t0 I P = (\<box> t [\<dots>0] \<oplus> iprev t0 I. P t)
[PROOF STEP]
by (fastforce simp: iTL_Next_defs iT_add iIN_0)+