proposition: Lemma evalDet_repeat_steps_app_nil_h : forall (A : Set) P (x y : comp_state A), evalDet_repeat_steps P x y -> forall c ls1 ls2 b a, x = (cs_more c ls1) -> y = (cs_eof A) -> evalDet_repeat_steps P (cs_more c (ls1 ++ b :: nil)) (cs_done a ls2)-> (forall s s' b a, evalDet_steps (cs_more c s) (cs_eof A) -> evalDet_steps (cs_more c (s ++ b :: nil)) (cs_done a s') -> s' = nil) -> ls2 = nil.
proof: Proof. induction 1; intuition; subst. discriminate. inversion H0; clear H0; subst. inversion H2; clear H2; subst. eapply H3; eauto. assert (s' = nil). eapply H3; eauto. subst. eapply evalDet_repeat_steps_nil_inv. eauto. inversion H2; clear H2; subst. inversion H4; clear H4; subst. assert (evalDet_steps (cs_more c0 (ls1 ++ b :: nil)) (cs_done a (s' ++ b :: nil))). eapply evalDet_steps_app_eq. trivial. specialize (evalDet_steps_done_func H7 H2); intuition; subst. congruence. assert (evalDet_steps (cs_more c0 (ls1 ++ b :: nil)) (cs_done a (s' ++ b :: nil))). eapply evalDet_steps_app_eq. trivial. specialize (evalDet_steps_done_func H6 H2); intuition; subst. clear H6. eapply IHevalDet_repeat_steps. eauto. eauto. eauto. trivial. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia