proposition: Lemma exists_rpo_eval_less_greater: forall rpo_infos n a l2, (forall a'', In a'' l2 -> size a + size a'' <= n) -> (exists a' : term, mem equiv a' l2 /\ rpo_eval rpo_infos n a a' = Some Less_than) -> exists a'', In a'' l2 /\ rpo_eval rpo_infos n a'' a = Some Greater_than.
proof: Proof. intros rpo_infos n a l2 size_a H. destruct H. destruct H. destruct (mem_split_set _ _ equiv_bool_ok _ _ H) as [s'' [lc' [lc'' [s_eq_s'' [H5 _]]]]]. exists s''. assert (H2:=@rpo_eval_is_sound_weak rpo_infos n a x). rewrite H0 in H2. rewrite (equiv_rpo_equiv_1 (bb rpo_infos) s_eq_s'') in H2. split. rewrite H5. apply in_or_app. right. simpl. left. trivial. assert (size_a_s'':= size_a s''). assert (size a + size s'' <= n). apply size_a_s''. rewrite H5. apply in_or_app. right. simpl. left. trivial. assert (H3:= rpo_eval_is_complete_less_greater rpo_infos H1). apply H3. 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)