proposition: Lemma equiv_eval_equation : forall rpo_infos n t1 t2, equiv_eval rpo_infos n t1 t2 = match n with | 0 => None | S m => match t1, t2 with | Var v1, Var v2 => Some (X.eq_bool v1 v2) | Term f1 l1, Term f2 l2 => if mem_bool eq_tt_bool (t1,t2) rpo_infos.(equiv_l) then Some true else if prec_eq_bool Prec f1 f2 then match status Prec f1 with | Lex => equiv_eval_list (equiv_eval rpo_infos m) l1 l2 | Mul => match remove_equiv_eval_list (equiv_eval rpo_infos m) l1 l2 with | Some (nil,nil) => Some true | Some _ => Some false | None => None end end else Some false | _, _ => Some false end end.
proof: Proof. intros rpo_infos [ | n] [v1 | f1 l1] [v2 | f2 l2]; unfold equiv_eval; simpl; 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)