proposition: Lemma ValidDGTree_EqualSets: forall p bl ep n f tree s1 s2 , s1 [=] s2 -> n = LocSet.cardinal s1 -> ValidDGTree p bl ep f s1 tree -> ValidDGTree p bl ep f s2 tree.
proof: Proof. intros p bl ep. induction n. intros. inversion H1. symmetry in H0. apply LocSetProp.cardinal_Empty in H0. assert (f'list = []). clear H4 H7 H6. generalize f'list, H5. clear f'list H5. induction f'list'. intros. simpl in H5. auto. intros. simpl in H5. assert (LocSet.mem a s1 = false). unfold LocSet.Empty in H0. specialize H0 with a. apply LocSetPropEq.mem_3; trivial. rewrite H4 in H5. intros. apply IHf'list'. trivial. rewrite H9 in H5. rewrite H9 in H7. apply ValidDGTree_def with dgs ad [] f'list'; trivial. assert (LocSet.Empty s2). unfold LocSet.Empty. intros. unfold LocSet.Empty in H0. unfold LocSet.Equal in H. intro. apply H in H10. elim H0 with a; trivial. clear H4 H5 H6 H7 H9. induction f'list'. simpl; trivial. assert (LocSet.mem a s2 = false). apply LocSetPropEq.mem_3; trivial. simpl. rewrite H4. trivial. rewrite H6. rewrite H9. trivial. intros. rewrite H6 in H10. rewrite H9 in H10. simpl in H10; inversion H10. intros. inversion H1. apply ValidDGTree_def with dgs ad f'list f'list'; trivial. generalize f'list, H5. clear f'list H4 H5 H6 H7. induction f'list'. simpl. trivial. simpl. intros. case_eq (LocSet.mem a s1); intros. rewrite H4 in H5. rewrite H in H4. rewrite H4. destruct f'list. inversion H5. specialize IHf'list' with f'list. rewrite IHf'list'. inversion H5. trivial. inversion H5; trivial. rewrite H4 in H5. rewrite H in H4. rewrite H4. rewrite IHf'list' with f'list; trivial. intros. specialize IHn with f' dgs' (LocSet.remove f' s1) (LocSet.remove f' s2). case_eq (LocSet.mem f' s1); intros. apply IHn. apply LocSetProp.Equal_remove; trivial. apply eq_add_S. rewrite H0. symmetry . apply LocSetPropEq.remove_cardinal_1; trivial. apply H7 with n0 f''; trivial. assert (LocSet.mem f' s1 = true). generalize nth_In. intros. assert (In f' f'list). rewrite <- H10. apply H13. rewrite <- H6. trivial. rewrite <- H5 in H14. clear H4. generalize f'list, H5. clear f'list H5 H10 H6 H7. induction f'list'. intros. simpl in *. inversion H14. intros. simpl in H5. case_eq (LocSet.mem a s1); intros. rewrite H4 in H5. simpl in H14. rewrite H4 in H14. case_eq (LocDec.eq_dec a f'). intros. unfold LocDec.eq in e. rewrite <- e. trivial. intros. simpl in H14. destruct H14. elim n1. unfold LocDec.eq. trivial. destruct f'list. inversion H5. apply IHf'list' with f'list in H7; trivial. inversion H5. trivial. rewrite H4 in H5. simpl in H14. rewrite H4 in H14. apply IHf'list' with f'list in H14; trivial. rewrite H12 in H13. inversion H13. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical) Coq(DecidableType) Coq(FSetInterface) Coq(FSetProperties) Coq(FSetEqProperties) Coq(FSetFacts) Coq(Sumbool) Coq(Lia)