proposition: Lemma bisim_inv: forall n x y, bisim n x y -> (exists v, terminates x v /\ terminates y v) \/ (exists n' x' y', x = later x' /\ y = later y' /\ bisim n' x' y').
proof: Proof. induction n using lt_wf_ind. intros x y B; inversion B; subst. - left; exists v; split; constructor. - right; exists m, x0, y0; auto. - edestruct (H n0) as [(v & T1 & T2) | (n' & x' & y' & E1 & E2 & B')]. lia. eauto. + left; exists v; auto using terminates_later. + right. exists (S n'), (later x'), y'; intuition auto. congruence. apply bisim_left; auto. - edestruct (H n0) as [(v & T1 & T2) | (n' & x' & y' & E1 & E2 & B')]. lia. eauto. + left; exists v; auto using terminates_later. + right. exists (S n'), x', (later y'); intuition auto. congruence. apply bisim_right; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)