proposition: Theorem wf_build: forall a, strict_star_form a -> forall i j A, bounded A -> belong i A -> belong j A -> wf A -> (epsilon_rt A j i -> strict a) -> wf (build a i j A).
proof: Proof. intros a' a. induction a; simpl; intros u v A HAb Hu Hv HA Ha; auto. apply wf_add_one; auto. intro F. apply Ha in F. inversion F. destruct A. auto. apply wf_add_one; auto. apply IHa; auto. apply wf_add_one; auto. destruct A. auto. intro. not_epsilon. intro Hnu. apply epsilon_rt_build in Hnu; auto. assert (Hnu': epsilon_rt (add_one (size A) v (incr A)) (size A) u). intuition. clear Hnu. apply epsilon_rt_add_one in Hnu' as [Hnu|[_ Hvu]]. not_epsilon. apply epsilon_rt_incr in Hvu. apply Ha in Hvu. inversion Hvu. apply IHa1; auto. apply IHa2; auto. intro F. apply Ha in F. inversion_clear F. assumption. intro Hvu. apply epsilon_rt_build in Hvu; auto. apply Common.apply in Ha. inversion_clear Ha; auto. intuition. apply IHa1; auto. apply IHa2; auto. destruct A. auto. intro F. not_epsilon. intro Hnu. apply epsilon_rt_build in Hnu; auto. intuition. not_epsilon. apply non_strict_not_strict in H2. destruct A. apply Ha in H. inversion_clear H; tauto. 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)