proposition: Lemma exec_equiv `{M : @EMonoid A op one equ} : forall c x s y s' , config_equiv (x, s) (y, s') -> result_equiv (exec A op c x s) (exec A op c y s').
proof: Proof. induction c. - simpl; now constructor. - destruct a. + destruct s. * inversion 1. inversion H1. cbn in *; subst;simpl; constructor. * inversion 1; cbn in *; inversion H1; subst; simpl; apply IHc. constructor; trivial. cbn. now apply Monoid_def.Eop_proper. + intros;simpl; apply IHc. destruct H; split; auto. cbn;apply Monoid_def.Eop_proper; auto. + intros; simpl; apply IHc. destruct H; split; auto. right; auto. + destruct s; simpl. * destruct s'. -- constructor. -- inversion 1. inversion H1. * destruct s'. inversion 1. inversion H1. destruct s, s'. -- constructor. -- inversion 1; inversion H1. inversion H1. inversion H7. -- inversion 1. inversion H1. inversion H7. -- intros; apply IHc; auto. inversion H. inversion H1; subst. inversion H7; subst. constructor; auto; right; auto. right; auto. Qed.
imports: Coq(List PArith Relations Lia) additions(Monoid_def Monoid_instances Strategies) Coq(Recdef Wf_nat) additions(More_on_positive Pow Euclidean_Chains Dichotomy BinaryStrat) Coq(NArith)