proposition: Lemma evalDet_repeat_steps_dec : forall (s : Blist)(A : Set)(c : Comp A)(P : A -> bool), (exists a, In a (getSupport c) /\ P a = true) -> (forall s', (exists a s'', evalDet_steps (cs_more c s') (cs_done a s'')) \/ evalDet_steps (cs_more c s') (@cs_eof A)) -> exists y, evalDet_repeat_steps P (cs_more c s) y.
proof: Proof. intro. eapply (list_skipn_strong_ind s); intuition. destruct (H0 nil). destruct H1. destruct H1. destruct H. intuition. exists (cs_done x x0). econstructor. trivial. assert (x1 = x). eapply evalDet_steps_nil_eq; eauto. subst. trivial. exists (@cs_eof A). econstructor. trivial. destruct (H1 x). destruct H2. destruct H2. destruct H0; intuition. destruct (evalDet_steps_skipn _ H2 H3); subst. econstructor. econstructor; eauto. destruct H0; intuition; subst. case_eq (P x0); intuition. econstructor. econstructor; eauto. edestruct H; eauto. econstructor. eapply evalDet_repeat_steps_step. eapply H2. trivial. eauto. econstructor. eapply evalDet_repeat_steps_eof; eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia