proposition: Lemma classes_union_strict: forall `{DS.WF} size (x y: state), x < size -> y < size -> StateSetSet.Equal (classes size (DS.union t x y)) (StateSetSet.add (StateSet.union (DS.class_of t x) (DS.class_of t y)) (StateSetSet.remove (DS.class_of t x) (StateSetSet.remove (DS.class_of t y) (classes size t)))).
proof: Proof. intros t Ht size x y Hx Hy s. rewrite in_classes. StateSetSetProps.set_iff. rewrite in_classes. split. intros [z Hz H]. destruct (@DSUtils.sameclass_spec t Ht x (state_of_nat z)) as [Hxz|Hxz]. rewrite DSUtils.class_of_union_1 in H by auto. symmetry in H. auto. destruct (@DSUtils.sameclass_spec t Ht y (state_of_nat z)) as [Hyz|Hyz]. rewrite DSUtils.class_of_union_1 in H by auto. symmetry in H. auto. rewrite DSUtils.class_of_union_2 in H by auto. right. repeat split. eauto. rewrite H. intro F. apply DSUtils.class_of_injective in F; auto. rewrite H. intro F. apply DSUtils.class_of_injective in F; auto. intros [H|[[[z Hz H] Hys]Hxs]]. exists x; trivial. symmetry in H. rewrite DSUtils.class_of_union_1; auto. left. bool_simpl. reflexivity. exists z; trivial. rewrite DSUtils.class_of_union_2; auto. intro F. apply Hxs. rewrite F, H. reflexivity. intro F. apply Hys. rewrite F, H. reflexivity. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)