proposition: Lemma equiv_eval_is_sound : forall rpo_infos n t1 t2, size t1 + size t2 <= n -> match equiv_eval rpo_infos n t1 t2 with | Some true => equiv t1 t2 | Some false => ~equiv t1 t2 | None => False end.
proof: Proof. intros rpo_infos n t1 t2 St; assert (H := equiv_eval_is_sound_weak rpo_infos n t1 t2); assert (T := @equiv_eval_terminates rpo_infos n t1 t2 St); assert (H' := @equiv_eval_is_complete_true rpo_infos n t1 t2 St); destruct (equiv_eval rpo_infos n t1 t2) as [ [ | ] | ]. apply H; trivial. intro t1_eq_t2; assert (H'' := H' t1_eq_t2); discriminate. apply T; 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)