proposition: Lemma solved_var : forall sigma l x, is_a_solved_var x (mk_pb sigma l) = true <-> (match find X.eq_bool x sigma with | None => False | Some _ => ~ (VSet.mem x (set_of_variables_in_unsolved_part l)) /\ ~ (VSet.mem x (set_of_variables_in_range_of_subst sigma)) end).
proof: Proof. intros sigma l x; unfold is_a_solved_var; unfold VSet.mem; unfold DecVar.eq_A. simpl solved_part; simpl unsolved_part. destruct (find X.eq_bool x sigma) as [x_val | ]; split. generalize (mem_bool_ok _ _ X.eq_bool_ok x (VSet.support (set_of_variables_in_unsolved_part l))). case (mem_bool eq_var_bool x (VSet.support (set_of_variables_in_unsolved_part l))); intro H. intros; discriminate. generalize (mem_bool_ok _ _ X.eq_bool_ok x (VSet.support (set_of_variables_in_range_of_subst sigma))). case (mem_bool eq_var_bool x (VSet.support (set_of_variables_in_range_of_subst sigma))); intro H'. intros; discriminate. intros; split; assumption. intros [H G]; generalize (mem_bool_ok _ _ X.eq_bool_ok x (VSet.support (set_of_variables_in_unsolved_part l))). case (mem_bool eq_var_bool x (VSet.support (set_of_variables_in_unsolved_part l))); intro H'. apply False_rect; apply H; assumption. generalize (mem_bool_ok _ _ X.eq_bool_ok x (VSet.support (set_of_variables_in_range_of_subst sigma))). case (mem_bool eq_var_bool x (VSet.support (set_of_variables_in_range_of_subst sigma))); intro G'. apply False_rect; apply G; assumption. reflexivity. discriminate. contradiction. Qed.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)