proposition: Lemma comp_pflat : forall N Ns, isPartialFlattening Ns N -> AllComputable Ns -> Computable N.
proof: Proof. intro N. case (isApp_dec N). destruct N as [E Pt T TypN]; induction TypN; try contr. intros Napp Ns Ns_pflat Ns_comp. unfold isPartialFlattening in Ns_pflat. repeat (destruct Ns; [contr | idtac]). rewrite (appUnits_app (buildT (TApp TypN1 TypN2)) I) in Ns_pflat. simpl in Ns_pflat. destruct Ns. destruct (app_inj_tail (appUnits t) (appUnits (buildT TypN1)) t0 (buildT TypN2)) as [t_L t0_R]; trivial. apply comp_app with I; simpl. rewrite <- (eq_units_eq_terms t (buildT TypN1) t_L). apply Ns_comp; auto with datatypes. rewrite <- t0_R. apply Ns_comp; auto with datatypes. destruct (@list_drop_last Term ((appUnits t) ++ t0::nil) (t1::Ns) (appUnits (buildT TypN1)) (buildT TypN2)) as [x xIn leq]. rewrite list_app_first_last; trivial. auto with datatypes. apply comp_app with I; simpl. set (pf := t::t0::x). case (isApp_dec (buildT TypN1)). intro N1app; apply IHTypN1 with pf; trivial. unfold isPartialFlattening; simpl. rewrite <- list_app_first_last; trivial. unfold pf; intros p pIn. apply Ns_comp. assert (inc: incl (t::t0::x) (t::t0::t1::Ns)). repeat (apply incl_cons; auto with datatypes). apply inc; trivial. intro N1napp. rewrite (appUnits_notApp (buildT TypN1)) in Ns_pflat; trivial. simpl in Ns_pflat. assert (N1_in: In (buildT TypN1) (t0::x)). rewrite (appUnits_notApp (buildT TypN1)) in leq; trivial. apply list_app_last with (appUnits t) (nil (A:=Term)). rewrite <- list_app_first_last; trivial. auto with datatypes. apply Ns_comp. destruct (in_inv N1_in). rewrite H; auto with datatypes. auto with datatypes. assert (N2_in: In (buildT TypN2) (t1::Ns)). apply list_app_last with (appUnits t ++ t0::nil) (appUnits (buildT TypN1)). rewrite list_app_first_last; trivial. auto with datatypes. apply Ns_comp; auto with datatypes. intros N_nApp Ns Ns_pflat Ns_comp. absurd (isApp N); trivial. apply partialFlattening_app with Ns; trivial. Qed.
imports: CoLoR(RelExtras ListExtras PairLex Horpo LogicUtil AccUtil) Coq(Setoid Morphisms Basics)