proposition: Lemma rpo_eval_equation : forall rpo_infos n t1 t2, rpo_eval rpo_infos n t1 t2 = if mem_bool eq_tt_bool (t1, t2) (rpo_l rpo_infos) then Some Less_than else if mem_bool eq_tt_bool (t2, t1) (rpo_l rpo_infos) then Some Greater_than else if mem_bool eq_tt_bool (t1, t2) (equiv_l rpo_infos) then Some Equivalent else if mem_bool eq_tt_bool (t2, t1) (equiv_l rpo_infos) then Some Equivalent else (match equiv_eval rpo_infos n t1 t2 with | None => None | Some true => Some Equivalent | Some false => (match t1, t2 with | Var _, Var _ => Some Uncomparable | Var x, (Term _ l) => if var_in_term_list x l then Some Less_than else Some Uncomparable | (Term _ l), Var x => if var_in_term_list x l then Some Greater_than else Some Uncomparable | (Term f1 l1), (Term f2 l2) => (match n with | 0 => None | S m => let check_l1_gt_t2 := list_exists_option (fun t => match rpo_eval rpo_infos m t t2 with | Some Equivalent | Some Greater_than => Some true | Some _ => Some false | None => None end) l1 in (match check_l1_gt_t2 with | None => None | Some true => Some Greater_than | Some false => let check_l2_gt_t1 := list_exists_option (fun t => match rpo_eval rpo_infos m t1 t with | Some Equivalent | Some Less_than => Some true | Some _ => Some false | None => None end) l2 in (match check_l2_gt_t1 with | None => None | Some true => Some Less_than | Some false => (match prec_eval f1 f2 with | Uncomparable => Some Uncomparable | Greater_than => let check_l2_lt_t1 := list_forall_option (fun t => match rpo_eval rpo_infos m t1 t with | Some Greater_than => Some true | Some _ => Some false | None => None end) l2 in (match check_l2_lt_t1 with | None => None | Some true => Some Greater_than | Some false => Some Uncomparable end) | Less_than => let check_l1_lt_t2 := list_forall_option (fun t => match rpo_eval rpo_infos m t t2 with | Some Less_than => Some true | Some _ => Some false | None => None end) l1 in (match check_l1_lt_t2 with | None => None | Some true => Some Less_than | Some false => Some Uncomparable end) | Equivalent => (match status Prec f1 with | Mul => match remove_equiv_eval_list (equiv_eval rpo_infos m) l1 l2 with | None => None | Some (nil, nil) => Some Equivalent | Some (nil, _ :: _) => Some Less_than | Some (_ :: _,nil) => Some Greater_than | Some (l1, l2) => mult_eval (rpo_eval rpo_infos m) l1 l2 end | Lex => if (Nat.eqb (length l1) (length l2)) || (leb (length l1) rpo_infos.(bb) && leb (length l2) rpo_infos.(bb)) then lexico_eval (rpo_eval rpo_infos m) t1 t2 l1 l2 else Some Uncomparable end) end) end) end) end) end) end).
proof: Proof. intros rpo_infos [ | n] [v1 | f1 l1] [v2 | f2 l2]; unfold rpo_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)