proposition: Lemma measure_for_unif_pb_swapp_eq : forall s t l sigma, measure_for_unif_pb (mk_pb sigma ((s,t) :: l)) = measure_for_unif_pb (mk_pb sigma ((t,s) :: l)).
proof: Proof. intros s t l sigma. assert (Phi1 : phi1 (mk_pb sigma ((s,t) :: l)) = phi1 (mk_pb sigma ((t,s) :: l))). unfold phi1; apply VSet.cardinal_eq_set; intro v; split; apply VSet.subset_filter; clear v; intro v. simpl; intro v_in_s_t_l_sigma; destruct_set v_in_s_t_l_sigma v_in_s_t_l v_in_sigma. destruct_set v_in_s_t_l v_in_s_t v_in_l. destruct_set v_in_s_t v_in_s v_in_t. do 2 apply VSet.union_1; apply VSet.union_2; trivial. do 3 apply VSet.union_1; trivial. apply VSet.union_1; apply VSet.union_2; trivial. apply VSet.union_2; trivial. intro H; rewrite solved_var_swapp_eq; trivial. simpl; intro v_in_s_t_l_sigma; destruct_set v_in_s_t_l_sigma v_in_s_t_l v_in_sigma. destruct_set v_in_s_t_l v_in_s_t v_in_l. destruct_set v_in_s_t v_in_s v_in_t. do 2 apply VSet.union_1; apply VSet.union_2; trivial. do 3 apply VSet.union_1; trivial. apply VSet.union_1; apply VSet.union_2; trivial. apply VSet.union_2; trivial. intro H; rewrite solved_var_swapp_eq; trivial. assert (Phi2 : phi2 (mk_pb sigma ((s,t) :: l)) = phi2 (mk_pb sigma ((t,s) :: l))). unfold phi2, size_of_solved_part, size_of_unsolved_part; simpl; rewrite Nat.max_comm; trivial. assert (Phi3 : phi3 (mk_pb sigma ((s,t) :: l)) = phi3 (mk_pb sigma ((t,s) :: l))). unfold phi3, nb_var_eq_of_unsolved_part; simpl; destruct s; destruct t; trivial. unfold measure_for_unif_pb; rewrite Phi1; rewrite Phi2; rewrite Phi3; trivial. Defined.
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)