proposition: Lemma evalDet_steps_dec : forall (A : Set)(c : Comp A), well_formed_comp c -> forall s, (exists a s', evalDet_steps (cs_more c s) (cs_done a s')) \/ (evalDet_steps (cs_more c s) (@cs_eof A)).
proof: Proof. induction 1; intros. left. exists a. exists s. econstructor. simpl. eauto. econstructor. destruct (IHwell_formed_comp s). destruct H2. destruct H2. edestruct (H1 x). eapply getSupport_In_evalDet_steps. eauto. destruct H3. destruct H3. left. exists x1. exists x2. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done; eauto. eauto. right. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done; eauto. trivial. right. eapply evalDet_bind_eof; eauto. case_eq (shiftOut s n); intuition. left. destruct p. exists b. exists b0. econstructor. simpl. rewrite H. eauto. econstructor. simpl. eauto. econstructor. right. econstructor. simpl. rewrite H. eauto. econstructor. edestruct (evalDet_repeat_steps_dec). exists b. eapply filter_In; eauto. eauto. destruct x. left. econstructor. econstructor. eapply evalDet_repeat_steps_done_inv. eauto. right. eapply evalDet_repeat_steps_done_inv. eauto. exfalso. eauto using evalDet_repeat_steps_more_inv. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia