proposition: Lemma rpo_eval_is_complete_equivalent : forall rpo_infos n t1 t2, size t1 + size t2 <= n -> equiv t1 t2 -> rpo_eval rpo_infos n t1 t2 = Some Equivalent.
proof: Proof. intros rpo_infos n t1 t2 St t1_eq_t2; rewrite rpo_eval_equation. case_eq (mem_bool eq_tt_bool (t1, t2) (rpo_l rpo_infos)). intro abs. generalize (find_is_sound (rpo rpo_infos.(bb)) _ (rpo_l_valid rpo_infos) _ _ abs). intro h;absurd (rpo rpo_infos.(bb) t1 t1). intro;apply rpo_antirefl with (1:=H). rewrite <- (equiv_rpo_equiv_1 _ t1_eq_t2) in h. assumption. intro h1. case_eq (mem_bool eq_tt_bool (t2, t1) (rpo_l rpo_infos)). intro abs. generalize (find_is_sound (rpo rpo_infos.(bb)) _ (rpo_l_valid rpo_infos) _ _ abs). intro h;absurd (rpo rpo_infos.(bb) t2 t2). intro;apply rpo_antirefl with (1:=H). rewrite (equiv_rpo_equiv_1 _ t1_eq_t2) in h. assumption. intro h2. case_eq (mem_bool eq_tt_bool (t1, t2) (equiv_l rpo_infos)). trivial. intro h3. case_eq (mem_bool eq_tt_bool (t2, t1) (equiv_l rpo_infos)). trivial. intro h4. assert (H := @equiv_eval_is_sound rpo_infos _ _ _ St). destruct (equiv_eval rpo_infos n t1 t2) as [ [ | ] | ]. trivial. absurd (equiv t1 t2); trivial. contradiction. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)