proposition: Lemma epsilon_rt_build: forall a i j A s t, bounded A -> belong i A -> belong j A -> belong s A -> belong t A -> epsilon_rt (build a i j A) s t -> epsilon_rt A s t \/ (epsilon_rt A s i /\ epsilon_rt A j t /\ non_strict a).
proof: Proof. induction a; simpl; intros u v A s t HA Hu Hv Hs Ht H; auto. apply epsilon_rt_add_one in H. intuition auto. apply IHa1 in H; auto. destruct H as [H|[H1 [H2 ?]]]. apply IHa2 in H; auto. destruct H as [H|[H1 [? ?]]]. auto using epsilon_rt_incr. not_epsilon. apply IHa2 in H1; auto. destruct H1 as [H1|[H3 [? ?]]]. apply IHa2 in H2; auto. destruct H2 as [H2|[? [? ?]]]. not_epsilon. auto using epsilon_rt_incr. not_epsilon. apply IHa1 in H; auto. destruct H as [H|[H1 [H2 ?]]]. apply IHa2 in H; intuition auto. apply IHa2 in H1; auto. apply IHa2 in H2; auto. intuition. apply epsilon_rt_add_one in H as [H|[H1 H2]]. apply IHa in H; auto. destruct H as [H|[H1 [H2 ?]]]. apply epsilon_rt_add_one in H as [H|[H1 H2]]. auto using epsilon_rt_incr. not_epsilon. apply epsilon_rt_add_one in H1. intuition (idtac; not_epsilon). apply IHa in H1; auto. apply IHa in H2; auto. destruct H1 as [H1|[H3 [H4 ?]]]. apply epsilon_rt_add_one in H1 as [H1|[H3 H4]]. 2: not_epsilon. destruct H2 as [H2|[H3 [H4 ?]]]. apply epsilon_rt_add_one in H2 as [H2|[H3 H4]]. not_epsilon. destruct A. auto. apply epsilon_rt_add_one in H4 as [H4|[H5 H6]]. not_epsilon. destruct A. auto. apply epsilon_rt_add_one in H3. intuition (idtac; not_epsilon). destruct A. auto. 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)