proposition: Lemma equiv_eval_terminates : forall rpo_infos n t1 t2, size t1 + size t2 <= n -> equiv_eval rpo_infos n t1 t2 <> None.
proof: Proof. intros rpo_infos n; induction n as [ | n]. intros t1 t2 St1; absurd (1 <= 0); auto with arith; apply Nat.le_trans with (size t1 + size t2); trivial; apply Nat.le_trans with (1 + size t2); [apply Nat.le_add_r | apply Nat.add_le_mono_r; apply size_ge_one]. intros t1 t2 St; rewrite equiv_eval_equation. destruct t1 as [ v1 | f1 l1]; destruct t2 as [ v2 | f2 l2]. discriminate. intros; discriminate. intros; discriminate. case (mem_bool eq_tt_bool ((Term f1 l1), (Term f2 l2)) (equiv_l rpo_infos));simpl. discriminate. case_eq (prec_eq_bool Prec f1 f2). intro f1_eq_f2. assert (H : forall t1 t2 : term, In t1 l1 -> In t2 l2 -> equiv_eval rpo_infos n t1 t2 <> None). intros t1 t2 t1_in_l1 t2_in_l2; apply IHn. rewrite size_unfold in St; rewrite <- Nat.add_assoc in St. rewrite size_unfold in St; simpl in St. refine (Nat.le_trans _ _ _ _ (le_S_n _ _ St)); apply Nat.add_le_mono. generalize (size_direct_subterm t1 (Term f1 l1) t1_in_l1); rewrite (size_unfold (Term f1 l1)); simpl; auto with arith. generalize (size_direct_subterm t2 (Term f1 l2) t2_in_l2); rewrite (size_unfold (Term f1 l2)); simpl; auto with arith. case (status Prec f1). apply equiv_eval_list_fully_evaluates; trivial. assert (H':= remove_equiv_eval_list_fully_evaluates (equiv_eval rpo_infos n) l1 l2 H); destruct (remove_equiv_eval_list (equiv_eval rpo_infos n) l1 l2) as [ [[ | t1' l1'] [ | t2' l2']] | ]; try discriminate. apply False_rect; apply H'; trivial. intros. discriminate. 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)