proposition: Lemma rpo_eval_is_complete : forall rpo_infos n t1 t2, size t1 + size t2 <= n -> match rpo_eval rpo_infos n t1 t2 with | Some Equivalent => equiv t1 t2 | Some Less_than => rpo rpo_infos.(bb) t1 t2 | Some Greater_than => rpo rpo_infos.(bb) t2 t1 | Some Uncomparable => ~equiv t1 t2 /\ ~ rpo rpo_infos.(bb) t1 t2 /\ ~rpo rpo_infos.(bb) t2 t1 | None => False end.
proof: Proof. intros rpo_infos n t1 t2 St; generalize (rpo_eval_is_sound_weak rpo_infos n t1 t2) (@rpo_eval_is_complete_equivalent rpo_infos n t1 t2 St) (@rpo_eval_is_complete_less_greater rpo_infos n t1 t2 St) (@rpo_eval_terminates rpo_infos n t1 t2 St); rewrite Nat.add_comm in St; generalize (@rpo_eval_is_complete_less_greater rpo_infos n t2 t1 St). destruct (rpo_eval rpo_infos n t1 t2) as [ [ | | | ] | ]; trivial. intros not_t2_lt_t1 _ t1_diff_t2 not_t1_lt_t2 T; repeat split; intro H. generalize (t1_diff_t2 H); discriminate. destruct (not_t1_lt_t2 H); discriminate. destruct (not_t2_lt_t1 H); discriminate. intros _ _ _ _ H; apply H; trivial. 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)