proposition: Lemma evalDet_app_nil : forall (A : Set)(c : Comp A), well_formed_comp c -> forall ls1 ls2 b a, evalDet c ls1 (ca_eof A) -> evalDet_steps (cs_more c (ls1 ++ b :: nil)) (cs_done a ls2) -> ls2 = nil.
proof: Proof. induction 1; intuition; simpl in *. exfalso. eapply evalDet_done_eof_func; eauto. econstructor. econstructor. eauto. simpl. econstructor. apply evalDet_steps_bind_done_inv in H3. destruct H3. destruct H3. intuition. edestruct (@evalDet_dec _ c1 ls1). trivial. destruct H3. inversion H3; clear H3; subst. assert (evalDet_steps (cs_more c1 (ls1 ++ b :: nil)) (cs_done x1 (s' ++ b :: nil))). eapply evalDet_steps_app_eq. eauto. specialize (evalDet_steps_done_func H4 H3); intuition. subst. clear H3. edestruct (@evalDet_dec _ (c2 x1) s'). eapply H0. eapply getSupport_In_evalDet_steps. eauto. destruct H3; inversion H3; clear H3; subst. exfalso. eapply evalDet_done_eof_func; [idtac | eapply H2]. econstructor. eapply evalDet_steps_trans. eapply evalDet_steps_bind_done; eauto. eauto. eapply H1; eauto. eapply getSupport_In_evalDet_steps. eauto. assert (x0 = nil). eapply IHwell_formed_comp. eauto. eauto. subst. eapply evalDet_steps_done_nil_inv; eauto. case_eq (shiftOut ls1 n); intuition. destruct p. exfalso. eapply evalDet_done_eof_func; [idtac | eapply H]. econstructor. econstructor. eauto. simpl. rewrite H1. econstructor. eauto. simpl. econstructor. inversion H0; clear H0; subst. simpl in *. apply shiftOut_None_inv in H1. case_eq (shiftOut (ls1 ++ b :: nil) n); intuition. destruct p. rewrite H0 in H6. inversion H6; clear H6; subst. simpl in *. inversion H7; clear H7; subst. specialize (shiftOut_Some_inv _ H0); intuition. apply shiftOut_correct_inv in H0. eapply app_eq_nil_inv. eapply H0. rewrite to_list_length. rewrite app_length in *; simpl in *. lia. rewrite H0 in H6. inversion H6. inversion H1; clear H1; subst. eapply evalDet_repeat_steps_app_nil. eapply evalDet_steps_repeat_eof_inv. eauto. eapply evalDet_steps_repeat_done_inv; eauto. intuition. eapply IHwell_formed_comp. econstructor. eauto. eauto. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia