proposition: Lemma ValidDGTree_func: forall p bl ep tree f m, ValidDGTree p bl ep f m tree -> forall tree', ValidDGTree p bl ep f m tree' -> tree = tree'.
proof: Proof. intros p bl ep tree. elim tree using DGTree_ind2 with (Q := fun kids => forall k f m, In k kids -> ValidDGTree p bl ep f (LocSet.remove f m) k -> forall k', ValidDGTree p bl ep f (LocSet.remove f m) k' -> eq k k'). intros. inversion H0. inversion H1. rewrite H9. inversion H2. rewrite H18 in H. assert (eq dgs dgs0). rewrite H3 in H10. rewrite <- H10 in H11. rewrite H4 in H11. rewrite <- H11 in H12. rewrite H5 in H12. rewrite <- H12 in H13. rewrite <- H12 in H14. rewrite <- H6 in H13. clear a l H0 tree' H1 dg ad f'list' H2 H3 H4 H5 H8 dg0 ad0 f'list0 f'list'0 H9 H10 H11 H12 H15 H17 H18. assert (forall n f'', (nth n dgs (DGNode f'' nil)) = (nth n dgs0 (DGNode f'' nil))). intros. case_eq (Nat.compare n (length dgs)); intros. assert (le (length dgs) n). rewrite nat_compare_Eq in H0. lia. generalize H1; intro. apply nth_overflow with (d := DGNode f'' nil) in H1. rewrite <- H13 in H2. apply nth_overflow with (d := DGNode f'' nil) in H2. rewrite H1; rewrite H2; trivial. rewrite <- nat_compare_lt in H0. apply H with (nth n f'list f'') m. apply nth_In; trivial. apply H7 with n f''; trivial. apply H14 with n f''; trivial. rewrite H13; trivial. assert (le (length dgs) n). rewrite <- nat_compare_gt in H0. lia. generalize H1; intro. apply nth_overflow with (d := DGNode f'' nil) in H1. rewrite <- H13 in H2. apply nth_overflow with (d := DGNode f'' nil) in H2. rewrite H1; rewrite H2; trivial. clear p bl ep tree H f m f'list H6 H7 H14. symmetry in H13. generalize dgs0, H13, H0. clear dgs0 H13 H0. induction dgs. intros. destruct dgs0; trivial. inversion H13. intros. destruct dgs0. inversion H13. assert (eq a d). destruct a. specialize H0 with O am. simpl in H0; trivial. assert (eq dgs dgs0). apply IHdgs. auto. intros. specialize H0 with (S n) f''. simpl in H0; trivial. rewrite H; rewrite H1; trivial. rewrite H16; trivial. intros. inversion H. intros. simpl in H1. destruct H1. rewrite <- H1. rewrite <- H1 in H2. apply H with f (LocSet.remove f m); trivial. apply H0 with f m; trivial. 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)