proposition: Lemma wf_add_one: forall A i j, wf A -> ~ epsilon_rt A j i -> wf (add_one i j A).
proof: Proof. intros A i j HA Hij. assert (Hj: forall v, epsilon_rt A j v -> Acc (transp _ (epsilon (add_one i j A))) v). induction v as [v IH] using (well_founded_induction HA); intros Hiv. constructor. intros u Hvu. apply epsilon_add_one in Hvu as [Hvu|[-> ->]]. apply IH. assumption. eauto using rt_trans, rt_step. elim Hij. assumption. intro v. induction v as [v IH] using (well_founded_induction HA). constructor. intros u Hvu. apply epsilon_add_one in Hvu as [Hvu|[-> ->]]. apply IH. assumption. apply Hj. constructor 2. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(DKA_CheckLabels) ATBR(StrictStarForm) ATBR(Utils_WF) Coq(Relations)