proposition: Lemma beta_algebraic_preserving : forall M N, algebraic M -> M -b-> N -> algebraic N.
proof: Proof. intro M. apply well_founded_ind with (R := subterm) (P := fun M => forall N, algebraic M -> M -b-> N -> algebraic N). apply subterm_wf. clear M; intros M IH N Malg MN. inversion MN. apply betaStep_algebraic_preserving with M; trivial. destruct (isFunApp_dec M) as [Mfa | Mnfa]. apply AlgFunApp; trivial. unfold isFunApp in * . term_inv N. apply app_beta_funS with M; trivial. rewrite <- (subject_reduction MN). apply algebraic_funApp_datatype; trivial. intros N' N'N. destruct (funS_fun (appHead M) Mfa) as [f Mf]. destruct (app_beta_args_eq N' Mapp MN Mf) as [M'M | [M' M'N' M'M]]; trivial. apply algebraic_arg with M; trivial. apply IH with M'; trivial. apply arg_subterm; trivial. apply algebraic_arg with M; trivial. apply algebraic_app with Napp. apply IH with (appBodyL Mapp); trivial. apply appBodyL_subterm. apply algebraic_appBodyL; trivial. rewrite <- H0. apply algebraic_appBodyR; trivial. destruct (isFunApp_dec M) as [Mfa | Mnfa]; inversion Malg; try solve [term_inv M]. apply AlgFunApp. unfold isFunApp in * . rewrite appHead_app with N Napp. rewrite <- H0. rewrite <- appHead_app; trivial. rewrite <- (subject_reduction MN); trivial. unfold isArg; rewrite (appArgs_app N Napp); intros. destruct (in_app_or H7). apply H5. apply appArg_left with Mapp. simpl; rewrite H0; trivial. inversion H8; try_solve. rewrite <- H9. apply IH with (appBodyR Mapp); trivial. apply appBodyR_subterm. apply algebraic_appBodyR; trivial. apply AlgApp; trivial. apply (notFunApp_left_eq M Mapp N Napp); trivial. unfold isAppUnit; rewrite (appUnits_app N Napp); intros. destruct (in_app_or H7). apply H5. apply appUnit_left with Mapp. simpl; rewrite H0; trivial. inversion H8; try_solve. rewrite <- H9. apply IH with (appBodyR Mapp); trivial. apply appBodyR_subterm. apply algebraic_appBodyR; trivial. apply AlgAbs with Nabs. apply IH with (absBody Mabs); trivial. apply absBody_subterm. inversion Malg; term_inv M. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)