diff --git a/Makefile.in b/Makefile.in index 6957c6d94..ab04084a3 100644 --- a/Makefile.in +++ b/Makefile.in @@ -171,16 +171,16 @@ test-suite: rm tests.ok $(TESTDIR)/%.dpdusage.log: $(TESTDIR)/%.dpd $(DPDUSAGE) - $(DPDUSAGE) $< > $@ + $(DPDUSAGE) $< | sort > $@ $(TESTDIR)/file_not_found.err.log: $(DPD2DOT) - $(DPD2DOT) file_not_found.err.dpd > $@ 2>&1 + $(DPD2DOT) file_not_found.err.dpd | sort > $@ 2>&1 $(TESTDIR)/%.err.log: $(TESTDIR)/%.err.dpd $(DPD2DOT) - $(DPD2DOT) $< > $@ 2>&1 + $(DPD2DOT) $< | sort > $@ 2>&1 %.log : % - cp $< $@ + sort $< > $@ %.vo : %.v coqc -q -R . dpdgraph $< @@ -215,7 +215,7 @@ $(TESTDIR)/PrimitiveProjections.dpd $(TESTDIR)/PrimitiveProjections2.dpd: \ $(TESTDIR)/search.log : $(TESTDIR)/Test.vo $(TESTDIR)/search.cmd $(DPDPLUGIN) cat $(TESTDIR)/search.cmd | coqtop -R . dpdgraph 2> /dev/null \ - | sed -e 's/Welcome to Coq.*/Welcome to Coq/' > $@ + | sed -e 's/Welcome to Coq.*/Welcome to Coq/' | sort > $@ %.dot : %.dpd $(DPD2DOT) $(DPD2DOT) $< > /dev/null diff --git a/tests/Morph.dot.oracle b/tests/Morph.dot.oracle index 21776ee5e..520f5bb53 100644 --- a/tests/Morph.dot.oracle +++ b/tests/Morph.dot.oracle @@ -1,37 +1,37 @@ digraph tests/Morph { +} /* END */ graph [ratio=0.5] - node [style=filled] -Morph_rw [label="rw", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Morph_FsmpM [label="FsmpM", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Morph_FsmpM_Proper [label="FsmpM_Proper", URL=, fillcolor="#FFB57F"] ; -Morph_Fsmp [label="Fsmp", URL=, fillcolor="#FACDEF"] ; +Morph_Fequiv [label="Fequiv", URL=, fillcolor="#FACDEF"] ; + Morph_Fequiv -> Morph_F [] ; +Morph_Fequiv_refl [label="Fequiv_refl", URL=, fillcolor="#FFB57F"] ; + Morph_Fequiv_refl -> Morph_Fequiv [] ; Morph_FequivR [label="FequivR", URL=, fillcolor="#7FFFD4"] ; -Morph_FequivR_Transitive [label="FequivR_Transitive", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Morph_FequivR_Symmetric [label="FequivR_Symmetric", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Morph_FequivR -> Morph_Fequiv_refl [] ; + Morph_FequivR -> Morph_Fequiv_sym [] ; + Morph_FequivR -> Morph_Fequiv_trans [] ; Morph_FequivR_Reflexive [label="FequivR_Reflexive", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Morph_FequivR_Reflexive -> Morph_Fequiv_refl [] ; Morph_FequivR_relation [label="FequivR_relation", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Morph_Fequiv_trans [label="Fequiv_trans", URL=, fillcolor="#FFB57F"] ; + Morph_FequivR_relation -> Morph_Fequiv [] ; +Morph_FequivR_Symmetric [label="FequivR_Symmetric", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Morph_FequivR_Symmetric -> Morph_Fequiv_sym [] ; +Morph_FequivR_Transitive [label="FequivR_Transitive", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Morph_FequivR_Transitive -> Morph_Fequiv_trans [] ; Morph_Fequiv_sym [label="Fequiv_sym", URL=, fillcolor="#FFB57F"] ; -Morph_Fequiv_refl [label="Fequiv_refl", URL=, fillcolor="#FFB57F"] ; -Morph_Fequiv [label="Fequiv", URL=, fillcolor="#FACDEF"] ; + Morph_Fequiv_sym -> Morph_Fequiv [] ; +Morph_Fequiv_trans [label="Fequiv_trans", URL=, fillcolor="#FFB57F"] ; + Morph_Fequiv_trans -> Morph_Fequiv [] ; Morph_F [label="F", URL=, fillcolor="#FACDEF"] ; - Morph_rw -> Morph_FsmpM_Proper [] ; - Morph_rw -> Morph_FequivR [] ; +Morph_F; Morph_Fequiv; Morph_Fequiv_refl; Morph_Fequiv_sym; Morph_Fequiv_trans; Morph_FequivR_relation; Morph_FequivR_Reflexive; Morph_FequivR_Symmetric; Morph_FequivR_Transitive; Morph_FequivR; Morph_Fsmp; Morph_FsmpM_Proper; Morph_FsmpM; Morph_rw; }; +Morph_Fsmp [label="Fsmp", URL=, fillcolor="#FACDEF"] ; +Morph_FsmpM [label="FsmpM", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Morph_FsmpM -> Morph_FsmpM_Proper [] ; - Morph_FsmpM_Proper -> Morph_Fsmp [] ; - Morph_FsmpM_Proper -> Morph_Fequiv [] ; Morph_Fsmp -> Morph_F [] ; - Morph_FequivR -> Morph_Fequiv_trans [] ; - Morph_FequivR -> Morph_Fequiv_sym [] ; - Morph_FequivR -> Morph_Fequiv_refl [] ; - Morph_FequivR_Transitive -> Morph_Fequiv_trans [] ; - Morph_FequivR_Symmetric -> Morph_Fequiv_sym [] ; - Morph_FequivR_Reflexive -> Morph_Fequiv_refl [] ; - Morph_FequivR_relation -> Morph_Fequiv [] ; - Morph_Fequiv_trans -> Morph_Fequiv [] ; - Morph_Fequiv_sym -> Morph_Fequiv [] ; - Morph_Fequiv_refl -> Morph_Fequiv [] ; - Morph_Fequiv -> Morph_F [] ; +Morph_FsmpM_Proper [label="FsmpM_Proper", URL=, fillcolor="#FFB57F"] ; + Morph_FsmpM_Proper -> Morph_Fequiv [] ; + Morph_FsmpM_Proper -> Morph_Fsmp [] ; +Morph_rw [label="rw", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Morph_rw -> Morph_FequivR [] ; + Morph_rw -> Morph_FsmpM_Proper [] ; + node [style=filled] subgraph cluster_Morph { label="Morph"; fillcolor="#FFFFC3"; labeljust=l; style=filled -Morph_F; Morph_Fequiv; Morph_Fequiv_refl; Morph_Fequiv_sym; Morph_Fequiv_trans; Morph_FequivR_relation; Morph_FequivR_Reflexive; Morph_FequivR_Symmetric; Morph_FequivR_Transitive; Morph_FequivR; Morph_Fsmp; Morph_FsmpM_Proper; Morph_FsmpM; Morph_rw; }; -} /* END */ diff --git a/tests/Morph.dpd.oracle b/tests/Morph.dpd.oracle index 58813a56d..1fee52c7c 100644 --- a/tests/Morph.dpd.oracle +++ b/tests/Morph.dpd.oracle @@ -1,29 +1,22 @@ -N: 14 "F" [body=no, kind=cnst, prop=no, path="Morph", ]; -N: 13 "Fequiv" [body=no, kind=cnst, prop=no, path="Morph", ]; -N: 5 "FequivR" [body=yes, kind=cnst, prop=yes, path="Morph", ]; -N: 8 "FequivR_Reflexive" [body=yes, kind=cnst, prop=yes, path="Morph", ]; -N: 7 "FequivR_Symmetric" [body=yes, kind=cnst, prop=yes, path="Morph", ]; -N: 6 "FequivR_Transitive" [body=yes, kind=cnst, prop=yes, path="Morph", ]; -N: 9 "FequivR_relation" [body=yes, kind=cnst, prop=yes, path="Morph", ]; -N: 12 "Fequiv_refl" [body=no, kind=cnst, prop=yes, path="Morph", ]; -N: 11 "Fequiv_sym" [body=no, kind=cnst, prop=yes, path="Morph", ]; -N: 10 "Fequiv_trans" [body=no, kind=cnst, prop=yes, path="Morph", ]; -N: 4 "Fsmp" [body=no, kind=cnst, prop=no, path="Morph", ]; -N: 2 "FsmpM" [body=yes, kind=cnst, prop=yes, path="Morph", ]; -N: 3 "FsmpM_Proper" [body=no, kind=cnst, prop=yes, path="Morph", ]; -N: 1 "rw" [body=yes, kind=cnst, prop=yes, path="Morph", ]; +E: 10 13 [weight=3, ]; +E: 10 14 [weight=3, ]; +E: 11 13 [weight=2, ]; +E: 11 14 [weight=2, ]; +E: 1 13 [weight=8, ]; +E: 1 14 [weight=6, ]; +E: 12 13 [weight=1, ]; +E: 12 14 [weight=1, ]; +E: 13 14 [weight=2, ]; E: 1 3 [weight=1, ]; E: 1 4 [weight=5, ]; E: 1 5 [weight=1, ]; -E: 1 13 [weight=8, ]; -E: 1 14 [weight=6, ]; -E: 2 3 [weight=1, ]; -E: 2 4 [weight=3, ]; E: 2 13 [weight=4, ]; E: 2 14 [weight=6, ]; -E: 3 4 [weight=1, ]; +E: 2 3 [weight=1, ]; +E: 2 4 [weight=3, ]; E: 3 13 [weight=2, ]; E: 3 14 [weight=4, ]; +E: 3 4 [weight=1, ]; E: 4 14 [weight=2, ]; E: 5 10 [weight=1, ]; E: 5 11 [weight=1, ]; @@ -41,10 +34,17 @@ E: 8 13 [weight=1, ]; E: 8 14 [weight=1, ]; E: 9 13 [weight=2, ]; E: 9 14 [weight=2, ]; -E: 10 13 [weight=3, ]; -E: 10 14 [weight=3, ]; -E: 11 13 [weight=2, ]; -E: 11 14 [weight=2, ]; -E: 12 13 [weight=1, ]; -E: 12 14 [weight=1, ]; -E: 13 14 [weight=2, ]; +N: 10 "Fequiv_trans" [body=no, kind=cnst, prop=yes, path="Morph", ]; +N: 11 "Fequiv_sym" [body=no, kind=cnst, prop=yes, path="Morph", ]; +N: 12 "Fequiv_refl" [body=no, kind=cnst, prop=yes, path="Morph", ]; +N: 13 "Fequiv" [body=no, kind=cnst, prop=no, path="Morph", ]; +N: 14 "F" [body=no, kind=cnst, prop=no, path="Morph", ]; +N: 1 "rw" [body=yes, kind=cnst, prop=yes, path="Morph", ]; +N: 2 "FsmpM" [body=yes, kind=cnst, prop=yes, path="Morph", ]; +N: 3 "FsmpM_Proper" [body=no, kind=cnst, prop=yes, path="Morph", ]; +N: 4 "Fsmp" [body=no, kind=cnst, prop=no, path="Morph", ]; +N: 5 "FequivR" [body=yes, kind=cnst, prop=yes, path="Morph", ]; +N: 6 "FequivR_Transitive" [body=yes, kind=cnst, prop=yes, path="Morph", ]; +N: 7 "FequivR_Symmetric" [body=yes, kind=cnst, prop=yes, path="Morph", ]; +N: 8 "FequivR_Reflexive" [body=yes, kind=cnst, prop=yes, path="Morph", ]; +N: 9 "FequivR_relation" [body=yes, kind=cnst, prop=yes, path="Morph", ]; diff --git a/tests/Morph_rw.dot.oracle b/tests/Morph_rw.dot.oracle index 8bda340f5..ea160e05b 100644 --- a/tests/Morph_rw.dot.oracle +++ b/tests/Morph_rw.dot.oracle @@ -1,96 +1,96 @@ +Basics_flip [label="flip", URL=, fillcolor="#F070D1"] ; +Basics_impl; Basics_flip; }; +Basics_impl [label="impl", URL=, fillcolor="#F070D1"] ; digraph tests/Morph_rw { +} /* END */ graph [ratio=0.5] - node [style=filled] -Morph_rw [label="rw", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Morphisms_trans_sym_co_inv_impl_morphism [label="trans_sym_co_inv_impl_morphism", URL=, fillcolor="#7FFFD4"] ; -Morph_FsmpM_Proper [label="FsmpM_Proper", URL=, fillcolor="#FFB57F"] ; -Morph_F [label="F", URL=, fillcolor="#FACDEF"] ; -Morph_Fsmp [label="Fsmp", URL=, fillcolor="#FACDEF"] ; -RelationClasses_Equivalence_PER [label="Equivalence_PER", URL=, fillcolor="#7FFFD4"] ; Morph_Fequiv [label="Fequiv", URL=, fillcolor="#FACDEF"] ; -Morph_FequivR [label="FequivR", URL=, fillcolor="#7FFFD4"] ; -Morph_Fequiv_trans [label="Fequiv_trans", URL=, fillcolor="#FFB57F"] ; + Morph_Fequiv -> Morph_F [] ; Morph_Fequiv_refl [label="Fequiv_refl", URL=, fillcolor="#FFB57F"] ; + Morph_Fequiv_refl -> Morph_Fequiv [] ; +Morph_FequivR [label="FequivR", URL=, fillcolor="#7FFFD4"] ; + Morph_FequivR -> Morph_Fequiv_refl [] ; + Morph_FequivR -> Morph_Fequiv_sym [] ; + Morph_FequivR -> Morph_Fequiv_trans [] ; + Morph_FequivR -> RelationClasses_Build_Equivalence [] ; + Morph_FequivR -> RelationClasses_Equivalence [] ; Morph_Fequiv_sym [label="Fequiv_sym", URL=, fillcolor="#FFB57F"] ; -RelationClasses_Equivalence [label="Equivalence", URL=, fillcolor="#E2CDFA"] ; -RelationClasses_Build_Equivalence [label="Build_Equivalence", URL=, fillcolor="#7FAAFF"] ; -RelationClasses_Symmetric [label="Symmetric", URL=, fillcolor="#F070D1"] ; -RelationClasses_Reflexive [label="Reflexive", URL=, fillcolor="#F070D1"] ; -Relation_Definitions_relation [label="relation", URL=, fillcolor="#F070D1"] ; -RelationClasses_Transitive [label="Transitive", URL=, fillcolor="#F070D1"] ; -RelationClasses_Equivalence_Transitive [label="Equivalence_Transitive", URL=, fillcolor="#7FFFD4"] ; -RelationClasses_Equivalence_Symmetric [label="Equivalence_Symmetric", URL=, fillcolor="#7FFFD4"] ; -RelationClasses_PER [label="PER", URL=, fillcolor="#E2CDFA"] ; -RelationClasses_Build_PER [label="Build_PER", URL=, fillcolor="#7FAAFF"] ; + Morph_Fequiv_sym -> Morph_Fequiv [] ; +Morph_Fequiv_sym; Morph_Fequiv_refl; Morph_Fequiv_trans; Morph_FequivR; Morph_Fequiv; Morph_Fsmp; Morph_F; Morph_FsmpM_Proper; Morph_rw; }; +Morph_Fequiv_trans [label="Fequiv_trans", URL=, fillcolor="#FFB57F"] ; + Morph_Fequiv_trans -> Morph_Fequiv [] ; +Morph_F [label="F", URL=, fillcolor="#FACDEF"] ; +Morph_Fsmp [label="Fsmp", URL=, fillcolor="#FACDEF"] ; + Morph_Fsmp -> Morph_F [] ; +Morph_FsmpM_Proper [label="FsmpM_Proper", URL=, fillcolor="#FFB57F"] ; + Morph_FsmpM_Proper -> Morph_Fequiv [] ; + Morph_FsmpM_Proper -> Morph_Fsmp [] ; + Morph_FsmpM_Proper -> Morphisms_Proper [] ; + Morph_FsmpM_Proper -> Morphisms_respectful [] ; Morphisms_Proper [label="Proper", URL=, fillcolor="#F070D1"] ; + Morphisms_Proper -> Relation_Definitions_relation [] ; Morphisms_respectful [label="respectful", URL=, fillcolor="#F070D1"] ; -Basics_flip [label="flip", URL=, fillcolor="#F070D1"] ; -Basics_impl [label="impl", URL=, fillcolor="#F070D1"] ; + Morphisms_respectful -> Relation_Definitions_relation [] ; +Morphisms_trans_sym_co_inv_impl_morphism [label="trans_sym_co_inv_impl_morphism", URL=, fillcolor="#7FFFD4"] ; + Morphisms_trans_sym_co_inv_impl_morphism -> Morphisms_Proper [] ; + Morphisms_trans_sym_co_inv_impl_morphism -> Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 [] ; + Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> Basics_flip [] ; + Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> Basics_impl [] ; Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 [label="trans_sym_co_inv_impl_morphism_obligation_1", URL=, fillcolor="#7FFFD4"] ; -RelationClasses_PER_Symmetric [label="PER_Symmetric", URL=, fillcolor="#7FFFD4"] ; -RelationClasses_symmetry [label="symmetry", URL=, fillcolor="#7FFFD4"] ; -RelationClasses_PER_Transitive [label="PER_Transitive", URL=, fillcolor="#7FFFD4"] ; -RelationClasses_transitivity [label="transitivity", URL=, fillcolor="#7FFFD4"] ; - Morph_rw -> Morphisms_trans_sym_co_inv_impl_morphism [] ; + Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> Morphisms_respectful [] ; +Morphisms_trans_sym_co_inv_impl_morphism_obligation_1; Morphisms_respectful; Morphisms_Proper; Morphisms_trans_sym_co_inv_impl_morphism; }; + Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> RelationClasses_PER_Symmetric [] ; + Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> RelationClasses_PER_Transitive [] ; + Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> RelationClasses_symmetry [] ; + Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> RelationClasses_transitivity [] ; +Morph_rw [label="rw", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Morph_rw -> Morph_FequivR [] ; Morph_rw -> Morph_FsmpM_Proper [] ; + Morph_rw -> Morphisms_trans_sym_co_inv_impl_morphism [] ; Morph_rw -> RelationClasses_Equivalence_PER [] ; - Morph_rw -> Morph_FequivR [] ; - Morphisms_trans_sym_co_inv_impl_morphism -> Morphisms_Proper [] ; - Morphisms_trans_sym_co_inv_impl_morphism -> Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 [] ; - Morph_FsmpM_Proper -> Morph_Fsmp [] ; - Morph_FsmpM_Proper -> Morph_Fequiv [] ; - Morph_FsmpM_Proper -> Morphisms_Proper [] ; - Morph_FsmpM_Proper -> Morphisms_respectful [] ; - Morph_Fsmp -> Morph_F [] ; - RelationClasses_Equivalence_PER -> RelationClasses_Equivalence_Transitive [] ; + node [style=filled] +RelationClasses_Build_Equivalence [label="Build_Equivalence", URL=, fillcolor="#7FAAFF"] ; + RelationClasses_Build_Equivalence -> RelationClasses_Reflexive [] ; + RelationClasses_Build_Equivalence -> RelationClasses_Symmetric [] ; + RelationClasses_Build_Equivalence -> RelationClasses_Transitive [] ; +RelationClasses_Build_PER [label="Build_PER", URL=, fillcolor="#7FAAFF"] ; + RelationClasses_Build_PER -> RelationClasses_Symmetric [] ; + RelationClasses_Build_PER -> RelationClasses_Transitive [] ; +RelationClasses_Equivalence [label="Equivalence", URL=, fillcolor="#E2CDFA"] ; +RelationClasses_Equivalence_PER [label="Equivalence_PER", URL=, fillcolor="#7FFFD4"] ; + RelationClasses_Equivalence_PER -> RelationClasses_Build_PER [] ; RelationClasses_Equivalence_PER -> RelationClasses_Equivalence_Symmetric [] ; + RelationClasses_Equivalence_PER -> RelationClasses_Equivalence_Transitive [] ; RelationClasses_Equivalence_PER -> RelationClasses_PER [] ; - RelationClasses_Equivalence_PER -> RelationClasses_Build_PER [] ; - Morph_Fequiv -> Morph_F [] ; - Morph_FequivR -> Morph_Fequiv_trans [] ; - Morph_FequivR -> Morph_Fequiv_refl [] ; - Morph_FequivR -> Morph_Fequiv_sym [] ; - Morph_FequivR -> RelationClasses_Equivalence [] ; - Morph_FequivR -> RelationClasses_Build_Equivalence [] ; - Morph_Fequiv_trans -> Morph_Fequiv [] ; - Morph_Fequiv_refl -> Morph_Fequiv [] ; - Morph_Fequiv_sym -> Morph_Fequiv [] ; - RelationClasses_Equivalence -> RelationClasses_Symmetric [] ; RelationClasses_Equivalence -> RelationClasses_Reflexive [] ; + RelationClasses_Equivalence -> RelationClasses_Symmetric [] ; RelationClasses_Equivalence -> RelationClasses_Transitive [] ; - RelationClasses_Build_Equivalence -> RelationClasses_Symmetric [] ; - RelationClasses_Build_Equivalence -> RelationClasses_Reflexive [] ; - RelationClasses_Build_Equivalence -> RelationClasses_Transitive [] ; - RelationClasses_Symmetric -> Relation_Definitions_relation [] ; - RelationClasses_Reflexive -> Relation_Definitions_relation [] ; - RelationClasses_Transitive -> Relation_Definitions_relation [] ; - RelationClasses_Equivalence_Transitive -> RelationClasses_Equivalence [] ; +RelationClasses_Equivalence_Symmetric [label="Equivalence_Symmetric", URL=, fillcolor="#7FFFD4"] ; RelationClasses_Equivalence_Symmetric -> RelationClasses_Equivalence [] ; +RelationClasses_Equivalence_Transitive [label="Equivalence_Transitive", URL=, fillcolor="#7FFFD4"] ; + RelationClasses_Equivalence_Transitive -> RelationClasses_Equivalence [] ; +RelationClasses_PER [label="PER", URL=, fillcolor="#E2CDFA"] ; RelationClasses_PER -> RelationClasses_Symmetric [] ; RelationClasses_PER -> RelationClasses_Transitive [] ; - RelationClasses_Build_PER -> RelationClasses_Symmetric [] ; - RelationClasses_Build_PER -> RelationClasses_Transitive [] ; - Morphisms_Proper -> Relation_Definitions_relation [] ; - Morphisms_respectful -> Relation_Definitions_relation [] ; - Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> Morphisms_respectful [] ; - Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> Basics_flip [] ; - Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> Basics_impl [] ; - Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> RelationClasses_PER_Symmetric [] ; - Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> RelationClasses_symmetry [] ; - Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> RelationClasses_PER_Transitive [] ; - Morphisms_trans_sym_co_inv_impl_morphism_obligation_1 -> RelationClasses_transitivity [] ; +RelationClasses_PER_Symmetric [label="PER_Symmetric", URL=, fillcolor="#7FFFD4"] ; RelationClasses_PER_Symmetric -> RelationClasses_PER [] ; - RelationClasses_symmetry -> RelationClasses_Symmetric [] ; +RelationClasses_PER_Transitive [label="PER_Transitive", URL=, fillcolor="#7FFFD4"] ; RelationClasses_PER_Transitive -> RelationClasses_PER [] ; +RelationClasses_Reflexive [label="Reflexive", URL=, fillcolor="#F070D1"] ; + RelationClasses_Reflexive -> Relation_Definitions_relation [] ; +RelationClasses_Symmetric [label="Symmetric", URL=, fillcolor="#F070D1"] ; + RelationClasses_Symmetric -> Relation_Definitions_relation [] ; +RelationClasses_symmetry [label="symmetry", URL=, fillcolor="#7FFFD4"] ; + RelationClasses_symmetry -> RelationClasses_Symmetric [] ; +RelationClasses_Transitive [label="Transitive", URL=, fillcolor="#F070D1"] ; + RelationClasses_Transitive -> Relation_Definitions_relation [] ; +RelationClasses_transitivity [label="transitivity", URL=, fillcolor="#7FFFD4"] ; +RelationClasses_transitivity; RelationClasses_PER_Transitive; RelationClasses_symmetry; RelationClasses_PER_Symmetric; RelationClasses_Build_PER; RelationClasses_PER; RelationClasses_Equivalence_Symmetric; RelationClasses_Equivalence_Transitive; RelationClasses_Transitive; RelationClasses_Reflexive; RelationClasses_Symmetric; RelationClasses_Build_Equivalence; RelationClasses_Equivalence; RelationClasses_Equivalence_PER; }; RelationClasses_transitivity -> RelationClasses_Transitive [] ; +Relation_Definitions_relation; }; +Relation_Definitions_relation [label="relation", URL=, fillcolor="#F070D1"] ; subgraph cluster_Basics { label="Basics"; fillcolor="#FFFFC3"; labeljust=l; style=filled -Basics_impl; Basics_flip; }; -subgraph cluster_RelationClasses { label="RelationClasses"; fillcolor="#FFFFC3"; labeljust=l; style=filled -RelationClasses_transitivity; RelationClasses_PER_Transitive; RelationClasses_symmetry; RelationClasses_PER_Symmetric; RelationClasses_Build_PER; RelationClasses_PER; RelationClasses_Equivalence_Symmetric; RelationClasses_Equivalence_Transitive; RelationClasses_Transitive; RelationClasses_Reflexive; RelationClasses_Symmetric; RelationClasses_Build_Equivalence; RelationClasses_Equivalence; RelationClasses_Equivalence_PER; }; subgraph cluster_Morphisms { label="Morphisms"; fillcolor="#FFFFC3"; labeljust=l; style=filled -Morphisms_trans_sym_co_inv_impl_morphism_obligation_1; Morphisms_respectful; Morphisms_Proper; Morphisms_trans_sym_co_inv_impl_morphism; }; -subgraph cluster_Relation_Definitions { label="Relation_Definitions"; fillcolor="#FFFFC3"; labeljust=l; style=filled -Relation_Definitions_relation; }; subgraph cluster_Morph { label="Morph"; fillcolor="#FFFFC3"; labeljust=l; style=filled -Morph_Fequiv_sym; Morph_Fequiv_refl; Morph_Fequiv_trans; Morph_FequivR; Morph_Fequiv; Morph_Fsmp; Morph_F; Morph_FsmpM_Proper; Morph_rw; }; -} /* END */ +subgraph cluster_RelationClasses { label="RelationClasses"; fillcolor="#FFFFC3"; labeljust=l; style=filled +subgraph cluster_Relation_Definitions { label="Relation_Definitions"; fillcolor="#FFFFC3"; labeljust=l; style=filled diff --git a/tests/Morph_rw.dpd.oracle b/tests/Morph_rw.dpd.oracle index b899a01ec..9bb333274 100644 --- a/tests/Morph_rw.dpd.oracle +++ b/tests/Morph_rw.dpd.oracle @@ -1,33 +1,3 @@ -N: 20 "Equivalence_PER" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ]; -N: 33 "Equivalence_Symmetric" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ]; -N: 32 "Equivalence_Transitive" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ]; -N: 18 "F" [body=no, kind=cnst, prop=no, path="Morph", ]; -N: 21 "Fequiv" [body=no, kind=cnst, prop=no, path="Morph", ]; -N: 22 "FequivR" [body=yes, kind=cnst, prop=yes, path="Morph", ]; -N: 24 "Fequiv_refl" [body=no, kind=cnst, prop=yes, path="Morph", ]; -N: 25 "Fequiv_sym" [body=no, kind=cnst, prop=yes, path="Morph", ]; -N: 23 "Fequiv_trans" [body=no, kind=cnst, prop=yes, path="Morph", ]; -N: 19 "Fsmp" [body=no, kind=cnst, prop=no, path="Morph", ]; -N: 17 "FsmpM_Proper" [body=no, kind=cnst, prop=yes, path="Morph", ]; -N: 41 "PER_Symmetric" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ]; -N: 43 "PER_Transitive" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ]; -N: 36 "Proper" [body=yes, kind=cnst, prop=no, path="Morphisms", ]; -N: 29 "Reflexive" [body=yes, kind=cnst, prop=no, path="RelationClasses", ]; -N: 28 "Symmetric" [body=yes, kind=cnst, prop=no, path="RelationClasses", ]; -N: 31 "Transitive" [body=yes, kind=cnst, prop=no, path="RelationClasses", ]; -N: 38 "flip" [body=yes, kind=cnst, prop=no, path="Basics", ]; -N: 39 "impl" [body=yes, kind=cnst, prop=no, path="Basics", ]; -N: 30 "relation" [body=yes, kind=cnst, prop=no, path="Relation_Definitions", ]; -N: 37 "respectful" [body=yes, kind=cnst, prop=no, path="Morphisms", ]; -N: 15 "rw" [body=yes, kind=cnst, prop=yes, path="Morph", ]; -N: 42 "symmetry" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ]; -N: 16 "trans_sym_co_inv_impl_morphism" [body=yes, kind=cnst, prop=yes, path="Morphisms", ]; -N: 40 "trans_sym_co_inv_impl_morphism_obligation_1" [body=yes, kind=cnst, prop=yes, path="Morphisms", ]; -N: 44 "transitivity" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ]; -N: 26 "Equivalence" [kind=inductive, prop=no, path="RelationClasses", ]; -N: 34 "PER" [kind=inductive, prop=no, path="RelationClasses", ]; -N: 27 "Build_Equivalence" [kind=construct, prop=yes, path="RelationClasses", ]; -N: 35 "Build_PER" [kind=construct, prop=yes, path="RelationClasses", ]; E: 15 16 [weight=1, ]; E: 15 17 [weight=1, ]; E: 15 18 [weight=6, ]; @@ -118,3 +88,33 @@ E: 43 31 [weight=3, ]; E: 43 34 [weight=4, ]; E: 44 30 [weight=2, ]; E: 44 31 [weight=2, ]; +N: 15 "rw" [body=yes, kind=cnst, prop=yes, path="Morph", ]; +N: 16 "trans_sym_co_inv_impl_morphism" [body=yes, kind=cnst, prop=yes, path="Morphisms", ]; +N: 17 "FsmpM_Proper" [body=no, kind=cnst, prop=yes, path="Morph", ]; +N: 18 "F" [body=no, kind=cnst, prop=no, path="Morph", ]; +N: 19 "Fsmp" [body=no, kind=cnst, prop=no, path="Morph", ]; +N: 20 "Equivalence_PER" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ]; +N: 21 "Fequiv" [body=no, kind=cnst, prop=no, path="Morph", ]; +N: 22 "FequivR" [body=yes, kind=cnst, prop=yes, path="Morph", ]; +N: 23 "Fequiv_trans" [body=no, kind=cnst, prop=yes, path="Morph", ]; +N: 24 "Fequiv_refl" [body=no, kind=cnst, prop=yes, path="Morph", ]; +N: 25 "Fequiv_sym" [body=no, kind=cnst, prop=yes, path="Morph", ]; +N: 26 "Equivalence" [kind=inductive, prop=no, path="RelationClasses", ]; +N: 27 "Build_Equivalence" [kind=construct, prop=yes, path="RelationClasses", ]; +N: 28 "Symmetric" [body=yes, kind=cnst, prop=no, path="RelationClasses", ]; +N: 29 "Reflexive" [body=yes, kind=cnst, prop=no, path="RelationClasses", ]; +N: 30 "relation" [body=yes, kind=cnst, prop=no, path="Relation_Definitions", ]; +N: 31 "Transitive" [body=yes, kind=cnst, prop=no, path="RelationClasses", ]; +N: 32 "Equivalence_Transitive" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ]; +N: 33 "Equivalence_Symmetric" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ]; +N: 34 "PER" [kind=inductive, prop=no, path="RelationClasses", ]; +N: 35 "Build_PER" [kind=construct, prop=yes, path="RelationClasses", ]; +N: 36 "Proper" [body=yes, kind=cnst, prop=no, path="Morphisms", ]; +N: 37 "respectful" [body=yes, kind=cnst, prop=no, path="Morphisms", ]; +N: 38 "flip" [body=yes, kind=cnst, prop=no, path="Basics", ]; +N: 39 "impl" [body=yes, kind=cnst, prop=no, path="Basics", ]; +N: 40 "trans_sym_co_inv_impl_morphism_obligation_1" [body=yes, kind=cnst, prop=yes, path="Morphisms", ]; +N: 41 "PER_Symmetric" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ]; +N: 42 "symmetry" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ]; +N: 43 "PER_Transitive" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ]; +N: 44 "transitivity" [body=yes, kind=cnst, prop=yes, path="RelationClasses", ]; diff --git a/tests/Polymorph.dot.oracle b/tests/Polymorph.dot.oracle index 7a44d8df3..1ca554b32 100644 --- a/tests/Polymorph.dot.oracle +++ b/tests/Polymorph.dot.oracle @@ -1,11 +1,11 @@ digraph tests/Polymorph { +} /* END */ +_existT [label="existT", URL=<.html#existT>, fillcolor="#7FAAFF"] ; graph [ratio=0.5] node [style=filled] +Polymorph_foo; }; + Polymorph_foo -> _existT [] ; Polymorph_foo [label="foo", URL=, peripheries=3, fillcolor="#F070D1"] ; -_sigT [label="sigT", URL=<.html#sigT>, fillcolor="#E2CDFA"] ; -_existT [label="existT", URL=<.html#existT>, fillcolor="#7FAAFF"] ; Polymorph_foo -> _sigT [] ; - Polymorph_foo -> _existT [] ; +_sigT [label="sigT", URL=<.html#sigT>, fillcolor="#E2CDFA"] ; subgraph cluster_Polymorph { label="Polymorph"; fillcolor="#FFFFC3"; labeljust=l; style=filled -Polymorph_foo; }; -} /* END */ diff --git a/tests/Polymorph.dpd.oracle b/tests/Polymorph.dpd.oracle index 008e95623..6e9b17a7d 100644 --- a/tests/Polymorph.dpd.oracle +++ b/tests/Polymorph.dpd.oracle @@ -1,5 +1,5 @@ +E: 1 2 [weight=17, ]; +E: 1 3 [weight=2, ]; N: 1 "foo" [body=yes, kind=cnst, prop=no, path="Polymorph", ]; N: 2 "sigT" [kind=inductive, prop=no, ]; N: 3 "existT" [kind=construct, prop=no, ]; -E: 1 2 [weight=17, ]; -E: 1 3 [weight=2, ]; diff --git a/tests/PrimitiveProjections.dot.oracle b/tests/PrimitiveProjections.dot.oracle index ce81da97c..1f7102671 100644 --- a/tests/PrimitiveProjections.dot.oracle +++ b/tests/PrimitiveProjections.dot.oracle @@ -1,19 +1,19 @@ digraph tests/PrimitiveProjections { +} /* END */ graph [ratio=0.5] node [style=filled] -PrimitiveProjections_foo [label="foo", URL=, peripheries=3, fillcolor="#F070D1"] ; -PrimitiveProjections_baz [label="baz", URL=, peripheries=3, fillcolor="#F070D1"] ; PrimitiveProjections_bar [label="bar", URL=, peripheries=3, fillcolor="#F070D1"] ; -PrimitiveProjections_projT2 [label="projT2", URL=, peripheries=3, fillcolor="#F070D1"] ; -PrimitiveProjections_projT1 [label="projT1", URL=, fillcolor="#F070D1"] ; + PrimitiveProjections_bar -> PrimitiveProjections_projT1 [] ; +PrimitiveProjections_baz [label="baz", URL=, peripheries=3, fillcolor="#F070D1"] ; + PrimitiveProjections_baz -> PrimitiveProjections_sigT [] ; PrimitiveProjections_existT [label="existT", URL=, fillcolor="#7FAAFF"] ; -PrimitiveProjections_sigT [label="sigT", URL=, fillcolor="#E2CDFA"] ; +PrimitiveProjections_foo [label="foo", URL=, peripheries=3, fillcolor="#F070D1"] ; PrimitiveProjections_foo -> PrimitiveProjections_existT [] ; PrimitiveProjections_foo -> PrimitiveProjections_sigT [] ; - PrimitiveProjections_baz -> PrimitiveProjections_sigT [] ; - PrimitiveProjections_bar -> PrimitiveProjections_projT1 [] ; - PrimitiveProjections_projT2 -> PrimitiveProjections_sigT [] ; +PrimitiveProjections_projT1 [label="projT1", URL=, fillcolor="#F070D1"] ; PrimitiveProjections_projT1 -> PrimitiveProjections_sigT [] ; -subgraph cluster_PrimitiveProjections { label="PrimitiveProjections"; fillcolor="#FFFFC3"; labeljust=l; style=filled +PrimitiveProjections_projT2 [label="projT2", URL=, peripheries=3, fillcolor="#F070D1"] ; + PrimitiveProjections_projT2 -> PrimitiveProjections_sigT [] ; +PrimitiveProjections_sigT [label="sigT", URL=, fillcolor="#E2CDFA"] ; PrimitiveProjections_sigT; PrimitiveProjections_existT; PrimitiveProjections_projT1; PrimitiveProjections_projT2; PrimitiveProjections_bar; PrimitiveProjections_baz; PrimitiveProjections_foo; }; -} /* END */ +subgraph cluster_PrimitiveProjections { label="PrimitiveProjections"; fillcolor="#FFFFC3"; labeljust=l; style=filled diff --git a/tests/PrimitiveProjections.dpd.oracle b/tests/PrimitiveProjections.dpd.oracle index 3d9d3a8ec..8ffa4faa3 100644 --- a/tests/PrimitiveProjections.dpd.oracle +++ b/tests/PrimitiveProjections.dpd.oracle @@ -1,10 +1,3 @@ -N: 3 "bar" [body=yes, kind=cnst, prop=no, path="PrimitiveProjections", ]; -N: 2 "baz" [body=yes, kind=cnst, prop=no, path="PrimitiveProjections", ]; -N: 1 "foo" [body=yes, kind=cnst, prop=no, path="PrimitiveProjections", ]; -N: 5 "projT1" [body=yes, kind=cnst, prop=no, path="PrimitiveProjections", ]; -N: 4 "projT2" [body=yes, kind=cnst, prop=no, path="PrimitiveProjections", ]; -N: 7 "sigT" [kind=inductive, prop=no, path="PrimitiveProjections", ]; -N: 6 "existT" [kind=construct, prop=no, path="PrimitiveProjections", ]; E: 1 6 [weight=2, ]; E: 1 7 [weight=8, ]; E: 2 7 [weight=2, ]; @@ -12,3 +5,10 @@ E: 3 5 [weight=1, ]; E: 3 7 [weight=1, ]; E: 4 7 [weight=2, ]; E: 5 7 [weight=2, ]; +N: 1 "foo" [body=yes, kind=cnst, prop=no, path="PrimitiveProjections", ]; +N: 2 "baz" [body=yes, kind=cnst, prop=no, path="PrimitiveProjections", ]; +N: 3 "bar" [body=yes, kind=cnst, prop=no, path="PrimitiveProjections", ]; +N: 4 "projT2" [body=yes, kind=cnst, prop=no, path="PrimitiveProjections", ]; +N: 5 "projT1" [body=yes, kind=cnst, prop=no, path="PrimitiveProjections", ]; +N: 6 "existT" [kind=construct, prop=no, path="PrimitiveProjections", ]; +N: 7 "sigT" [kind=inductive, prop=no, path="PrimitiveProjections", ]; diff --git a/tests/PrimitiveProjections2.dot.oracle b/tests/PrimitiveProjections2.dot.oracle index 67253c13e..7b5c4b160 100644 --- a/tests/PrimitiveProjections2.dot.oracle +++ b/tests/PrimitiveProjections2.dot.oracle @@ -1,11 +1,11 @@ digraph tests/PrimitiveProjections2 { +} /* END */ graph [ratio=0.5] node [style=filled] -PrimitiveProjections_foo [label="foo", URL=, peripheries=3, fillcolor="#F070D1"] ; -PrimitiveProjections_sigT [label="sigT", URL=, fillcolor="#E2CDFA"] ; PrimitiveProjections_existT [label="existT", URL=, fillcolor="#7FAAFF"] ; - PrimitiveProjections_foo -> PrimitiveProjections_sigT [] ; +PrimitiveProjections_existT; PrimitiveProjections_sigT; PrimitiveProjections_foo; }; +PrimitiveProjections_foo [label="foo", URL=, peripheries=3, fillcolor="#F070D1"] ; PrimitiveProjections_foo -> PrimitiveProjections_existT [] ; + PrimitiveProjections_foo -> PrimitiveProjections_sigT [] ; +PrimitiveProjections_sigT [label="sigT", URL=, fillcolor="#E2CDFA"] ; subgraph cluster_PrimitiveProjections { label="PrimitiveProjections"; fillcolor="#FFFFC3"; labeljust=l; style=filled -PrimitiveProjections_existT; PrimitiveProjections_sigT; PrimitiveProjections_foo; }; -} /* END */ diff --git a/tests/PrimitiveProjections2.dpd.oracle b/tests/PrimitiveProjections2.dpd.oracle index 904cee2a9..f91962851 100644 --- a/tests/PrimitiveProjections2.dpd.oracle +++ b/tests/PrimitiveProjections2.dpd.oracle @@ -1,5 +1,5 @@ +E: 8 10 [weight=2, ]; +E: 8 9 [weight=8, ]; +N: 10 "existT" [kind=construct, prop=no, path="PrimitiveProjections", ]; N: 8 "foo" [body=yes, kind=cnst, prop=no, path="PrimitiveProjections", ]; N: 9 "sigT" [kind=inductive, prop=no, path="PrimitiveProjections", ]; -N: 10 "existT" [kind=construct, prop=no, path="PrimitiveProjections", ]; -E: 8 9 [weight=8, ]; -E: 8 10 [weight=2, ]; diff --git a/tests/attributes.err.oracle b/tests/attributes.err.oracle index 56e514604..1faa95b48 100644 --- a/tests/attributes.err.oracle +++ b/tests/attributes.err.oracle @@ -1,2 +1,2 @@ -Info: read file tests/attributes.err.dpd Error: no node with number 10: cannot build edge. +Info: read file tests/attributes.err.dpd diff --git a/tests/double_node.err.oracle b/tests/double_node.err.oracle index 6596f15db..802b5d708 100644 --- a/tests/double_node.err.oracle +++ b/tests/double_node.err.oracle @@ -1,2 +1,2 @@ -Info: read file tests/double_node.err.dpd Error: a node named 'two' already has the number 2. Cannot create new node named 'another two' with the same number. +Info: read file tests/double_node.err.dpd diff --git a/tests/file_not_found.err.oracle b/tests/file_not_found.err.oracle index 0c185d6d9..7444b9d75 100644 --- a/tests/file_not_found.err.oracle +++ b/tests/file_not_found.err.oracle @@ -1,2 +1,2 @@ -Info: read file file_not_found.err.dpd Error: file_not_found.err.dpd: No such file or directory. +Info: read file file_not_found.err.dpd diff --git a/tests/graph.dot.oracle b/tests/graph.dot.oracle index 87aad5c44..37fb5d216 100644 --- a/tests/graph.dot.oracle +++ b/tests/graph.dot.oracle @@ -1,623 +1,623 @@ digraph tests/graph { +} /* END */ graph [ratio=0.5] node [style=filled] -Test_removelast_app [label="removelast_app", URL=, fillcolor="#7FFFD4"] ; -Test_exists_last [label="exists_last", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_ReDun_NoDup_Permutation [label="NoDup_Permutation", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_removelast_last [label="app_removelast_last", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_ReDun_NoDup_remove_2 [label="NoDup_remove_2", URL=, fillcolor="#7FFFD4"] ; -Test_removelast [label="removelast", URL=, fillcolor="#F070D1"] ; -Test_ReDun_NoDup_remove_1 [label="NoDup_remove_1", URL=, fillcolor="#7FFFD4"] ; -Test_last [label="last", URL=, fillcolor="#F070D1"] ; -Test_ReDun_NoDup_sind [label="NoDup_sind", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_remove_In [label="remove_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_ReDun_NoDup_ind [label="NoDup_ind", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_ReDun_NoDup_cons [label="NoDup_cons", URL=, fillcolor="#7FAAFF"] ; -Test_remove [label="remove", URL=, fillcolor="#F070D1"] ; -Test_ReDun_NoDup_nil [label="NoDup_nil", URL=, peripheries=3, fillcolor="#7FAAFF"] ; -Test_app_nth2 [label="app_nth2", URL=, fillcolor="#7FFFD4"] ; -Test_ReDun_NoDup [label="NoDup", URL=, fillcolor="#E2CDFA"] ; -Test_app_nth1 [label="app_nth1", URL=, fillcolor="#7FFFD4"] ; -Test_nth_indep [label="nth_indep", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_ReDun_A [label="A", URL=, fillcolor="#FACDEF"] ; -Test_seq_shift [label="seq_shift", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_nth_overflow [label="nth_overflow", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_seq_nth [label="seq_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_nth_In [label="nth_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_seq_length [label="seq_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_nth_default [label="nth_default", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_seq [label="seq", URL=, fillcolor="#F070D1"] ; -Test_nth_error [label="nth_error", URL=, fillcolor="#F070D1"] ; -Test_nth_S_cons [label="nth_S_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_firstn_removelast [label="firstn_removelast", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_removelast_firstn [label="removelast_firstn", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_nth_in_or_default [label="nth_in_or_default", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_nth_ok [label="nth_ok", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_firstn_length [label="firstn_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_nth [label="nth", URL=, fillcolor="#F070D1"] ; -Test_firstn_skipn [label="firstn_skipn", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_skipn [label="skipn", URL=, fillcolor="#F070D1"] ; -Test_app_inv_tail [label="app_inv_tail", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_firstn [label="firstn", URL=, fillcolor="#F070D1"] ; +subgraph cluster_Test { label="Test"; fillcolor="#FFFFC3"; labeljust=l; style=filled +subgraph cluster_Test_ReDun { label="ReDun"; fillcolor="#FFFFA3"; labeljust=l; style=filled +Test_app_ass [label="app_ass", URL=, fillcolor="#7FFFD4"] ; + Test_app_ass -> Test_app [] ; + Test_app_ass -> Test_list_ind [] ; +Test_app_comm_cons [label="app_comm_cons", URL=, fillcolor="#7FFFD4"] ; + Test_app_comm_cons -> Test_app [] ; +Test_app_cons_not_nil [label="app_cons_not_nil", URL=, fillcolor="#7FFFD4"] ; + Test_app_cons_not_nil -> Test_app [] ; + Test_app_cons_not_nil -> Test_nil [] ; +Test_app_eq_nil [label="app_eq_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_eq_nil -> Test_app [] ; + Test_app_eq_nil -> Test_nil [] ; +Test_app_eq_unit [label="app_eq_unit", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_eq_unit -> Test_app_cons_not_nil [] ; + Test_app_eq_unit -> Test_app_nil_end [] ; +Test_app_inj_tail [label="app_inj_tail", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_inj_tail -> Test_app_cons_not_nil [] ; + Test_app_inj_tail -> Test_list_ind [] ; Test_app_inv_head [label="app_inv_head", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_incl_app [label="incl_app", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_or_app [label="in_or_app", URL=, fillcolor="#7FFFD4"] ; -Test_incl_cons [label="incl_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_app_or [label="in_app_or", URL=, fillcolor="#7FFFD4"] ; -Test_incl_appr [label="incl_appr", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_inv_head -> Test_app [] ; + Test_app_inv_head -> Test_list_ind [] ; +Test_app_inv_tail [label="app_inv_tail", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_inv_tail -> Test_app_length [] ; +Test_app [label="app", URL=, fillcolor="#F070D1"] ; Test_app_length [label="app_length", URL=, fillcolor="#7FFFD4"] ; -Test_incl_appl [label="incl_appl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_inj_tail [label="app_inj_tail", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_incl_tran [label="incl_tran", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_eq_unit [label="app_eq_unit", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_incl_tl [label="incl_tl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_eq_nil [label="app_eq_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_incl_refl [label="incl_refl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_comm_cons [label="app_comm_cons", URL=, fillcolor="#7FFFD4"] ; -Test_incl [label="incl", URL=, fillcolor="#F070D1"] ; -Test_ass_app [label="ass_app", URL=, fillcolor="#7FFFD4"] ; -Test_lel_nil [label="lel_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_ass [label="app_ass", URL=, fillcolor="#7FFFD4"] ; -Test_lel_tail [label="lel_tail", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_length -> Test_app [] ; + Test_app_length -> Test_length [] ; + Test_app_length -> Test_list_ind [] ; Test_app_nil_end [label="app_nil_end", URL=, fillcolor="#7FFFD4"] ; -Test_lel_cons [label="lel_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_cons_not_nil [label="app_cons_not_nil", URL=, fillcolor="#7FFFD4"] ; -Test_lel_cons_cons [label="lel_cons_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_In_dec [label="In_dec", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_lel_trans [label="lel_trans", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_inv [label="in_inv", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_lel_refl [label="lel_refl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_In_split [label="In_split", URL=, fillcolor="#7FFFD4"] ; -Test_lel [label="lel", URL=, fillcolor="#F070D1"] ; -Test_in_nil [label="in_nil", URL=, fillcolor="#7FFFD4"] ; -Test_prod_length [label="prod_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_cons [label="in_cons", URL=, fillcolor="#7FFFD4"] ; -Test_in_prod_iff [label="in_prod_iff", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_eq [label="in_eq", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_prod [label="in_prod", URL=, fillcolor="#7FFFD4"] ; -Test_head_cons [label="head_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_prod_aux [label="in_prod_aux", URL=, fillcolor="#7FFFD4"] ; -Test_head_nil [label="head_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_list_prod [label="list_prod", URL=, fillcolor="#F070D1"] ; -Test_destruct_list [label="destruct_list", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_nil_cons [label="nil_cons", URL=, fillcolor="#7FFFD4"] ; -Test_combine_nth [label="combine_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_nil_end -> Test_app [] ; + Test_app_nil_end -> Test_list_ind [] ; +Test_app_nth1 [label="app_nth1", URL=, fillcolor="#7FFFD4"] ; + Test_app_nth1 -> Test_app [] ; + Test_app_nth1 -> Test_length [] ; + Test_app_nth1 -> Test_list_ind [] ; + Test_app_nth1 -> Test_nth [] ; +Test_app_nth2 [label="app_nth2", URL=, fillcolor="#7FFFD4"] ; + Test_app_nth2 -> Test_app [] ; + Test_app_nth2 -> Test_length [] ; + Test_app_nth2 -> Test_list_ind [] ; + Test_app_nth2 -> Test_nth [] ; +Test_app_removelast_last [label="app_removelast_last", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_removelast_last -> Test_app [] ; + Test_app_removelast_last -> Test_last [] ; + Test_app_removelast_last -> Test_list_ind [] ; + Test_app_removelast_last -> Test_removelast [] ; + Test_app -> Test_cons [] ; + Test_app -> Test_list [] ; +Test_ass_app [label="ass_app", URL=, fillcolor="#7FFFD4"] ; + Test_ass_app -> Test_app_ass [] ; +Test_combine [label="combine", URL=, fillcolor="#F070D1"] ; Test_combine_length [label="combine_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app [label="app", URL=, fillcolor="#F070D1"] ; -Test_in_combine_r [label="in_combine_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_In [label="In", URL=, fillcolor="#F070D1"] ; -Test_size_nil [label="size_nil", URL=, peripheries=3, fillcolor="#FFB57F"] ; -Test_in_combine_l [label="in_combine_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_size [label="size", URL=, fillcolor="#FACDEF"] ; + Test_combine_length -> Test_combine [] ; + Test_combine_length -> Test_length [] ; + Test_combine_length -> Test_list_ind [] ; +Test_combine_nth [label="combine_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_combine_nth -> Test_combine [] ; + Test_combine_nth -> Test_length [] ; + Test_combine_nth -> Test_list_ind [] ; + Test_combine_nth -> Test_nth [] ; Test_combine_split [label="combine_split", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_split_combine [label="split_combine", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_length [label="length", URL=, fillcolor="#F070D1"] ; -Test_tail [label="tail", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_combine [label="combine", URL=, fillcolor="#F070D1"] ; -Test_split_length_r [label="split_length_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_hd [label="hd", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_split_length_l [label="split_length_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_head [label="head", URL=, fillcolor="#F070D1"] ; -Test_split_nth [label="split_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_list_sind [label="list_sind", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_list_rec [label="list_rec", URL=, fillcolor="#F070D1"] ; -Test_in_split_r [label="in_split_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_list_ind [label="list_ind", URL=, fillcolor="#7FFFD4"] ; -Test_in_split_l [label="in_split_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_split [label="split", URL=, fillcolor="#F070D1"] ; -Test_list_rect [label="list_rect", URL=, fillcolor="#F070D1"] ; + Test_combine_split -> Test_combine [] ; + Test_combine_split -> Test_length [] ; + Test_combine_split -> Test_list_ind [] ; + Test_combine_split -> Test_split [] ; + Test_combine -> Test_cons [] ; + Test_combine -> Test_list [] ; + Test_combine -> Test_nil [] ; Test_cons [label="cons", URL=, fillcolor="#7FAAFF"] ; -Test_partition [label="partition", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_nil [label="nil", URL=, fillcolor="#7FAAFF"] ; -Test_find [label="find", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_list [label="list", URL=, fillcolor="#E2CDFA"] ; -Test_filter_In [label="filter_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_filter [label="filter", URL=, fillcolor="#F070D1"] ; -Test_forallb_forall [label="forallb_forall", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_forallb [label="forallb", URL=, fillcolor="#F070D1"] ; -Test_existsb_nth [label="existsb_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_existsb_exists [label="existsb_exists", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_existsb [label="existsb", URL=, fillcolor="#F070D1"] ; -Test_list_power [label="list_power", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_fold_symmetric [label="fold_symmetric", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_fold_left_rev_right [label="fold_left_rev_right", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_fold_right_app [label="fold_right_app", URL=, fillcolor="#7FFFD4"] ; -Test_fold_right [label="fold_right", URL=, fillcolor="#F070D1"] ; -Test_fold_left_length [label="fold_left_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_fold_left_app [label="fold_left_app", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_fold_left [label="fold_left", URL=, fillcolor="#F070D1"] ; -Test_map_ext [label="map_ext", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_map_map [label="map_map", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_flat_map [label="in_flat_map", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_flat_map [label="flat_map", URL=, fillcolor="#F070D1"] ; -Test_Permutation_map [label="Permutation_map", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_map_rev [label="map_rev", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_map_app [label="map_app", URL=, fillcolor="#7FFFD4"] ; -Test_map_nth [label="map_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_map_length [label="map_length", URL=, fillcolor="#7FFFD4"] ; -Test_in_map_iff [label="in_map_iff", URL=, fillcolor="#7FFFD4"] ; -Test_in_map [label="in_map", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_map [label="map", URL=, fillcolor="#F070D1"] ; -Test_list_eq_dec [label="list_eq_dec", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_Permutation_app_inv_r [label="Permutation_app_inv_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_app_inv_l [label="Permutation_app_inv_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_cons_app_inv [label="Permutation_cons_app_inv", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_cons_inv [label="Permutation_cons_inv", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_app_inv [label="Permutation_app_inv", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_ind_bis [label="Permutation_ind_bis", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_rev [label="Permutation_rev", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_length [label="Permutation_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_cons_app [label="Permutation_cons_app", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_app_swap [label="Permutation_app_swap", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_app [label="Permutation_app", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_app_head [label="Permutation_app_head", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_app_tail [label="Permutation_app_tail", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_in [label="Permutation_in", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_trans [label="Permutation_trans", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_sym [label="Permutation_sym", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_refl [label="Permutation_refl", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_nil_cons [label="Permutation_nil_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_nil [label="Permutation_nil", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_sind [label="Permutation_sind", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_Permutation_ind [label="Permutation_ind", URL=, fillcolor="#7FFFD4"] ; -Test_perm_trans [label="perm_trans", URL=, fillcolor="#7FAAFF"] ; -Test_perm_swap [label="perm_swap", URL=, fillcolor="#7FAAFF"] ; -Test_perm_skip [label="perm_skip", URL=, fillcolor="#7FAAFF"] ; -Test_perm_nil [label="perm_nil", URL=, fillcolor="#7FAAFF"] ; -Test_Permutation [label="Permutation", URL=, fillcolor="#E2CDFA"] ; -Test_rev_ind [label="rev_ind", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_rev_list_ind [label="rev_list_ind", URL=, fillcolor="#7FFFD4"] ; -Test_rev_alt [label="rev_alt", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_rev_append_rev [label="rev_append_rev", URL=, fillcolor="#7FFFD4"] ; -Test_rev_ [label="rev'", URL=, peripheries=3, fillcolor="#F070D1"] ; -Test_rev_append [label="rev_append", URL=, fillcolor="#F070D1"] ; -Test_rev_nth [label="rev_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_rev_length [label="rev_length", URL=, fillcolor="#7FFFD4"] ; -Test_In_rev [label="In_rev", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_rev_involutive [label="rev_involutive", URL=, fillcolor="#7FFFD4"] ; -Test_rev_unit [label="rev_unit", URL=, fillcolor="#7FFFD4"] ; -Test_distr_rev [label="distr_rev", URL=, fillcolor="#7FFFD4"] ; -Test_rev [label="rev", URL=, fillcolor="#F070D1"] ; -Test_count_occ_cons_neq [label="count_occ_cons_neq", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_count_occ_cons_eq [label="count_occ_cons_eq", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_count_occ_nil [label="count_occ_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_count_occ_inv_nil [label="count_occ_inv_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_count_occ_cons_eq -> Test_cons [] ; + Test_count_occ_cons_eq -> Test_count_occ [] ; +Test_count_occ_cons_neq [label="count_occ_cons_neq", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_count_occ_cons_neq -> Test_cons [] ; + Test_count_occ_cons_neq -> Test_count_occ [] ; Test_count_occ_In [label="count_occ_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_count_occ_In -> Test_count_occ [] ; + Test_count_occ_In -> Test_In [] ; + Test_count_occ_In -> Test_list_ind [] ; +Test_count_occ_inv_nil [label="count_occ_inv_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_count_occ_inv_nil -> Test_count_occ [] ; + Test_count_occ_inv_nil -> Test_list_ind [] ; Test_count_occ [label="count_occ", URL=, fillcolor="#F070D1"] ; - Test_removelast_app -> Test_removelast [] ; - Test_removelast_app -> Test_app [] ; - Test_removelast_app -> Test_list_ind [] ; - Test_exists_last -> Test_app [] ; - Test_exists_last -> Test_list_rect [] ; - Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_2 [] ; - Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_1 [] ; - Test_ReDun_NoDup_Permutation -> Test_Permutation_cons_app [] ; - Test_ReDun_NoDup_Permutation -> Test_In_split [] ; - Test_app_removelast_last -> Test_removelast [] ; - Test_app_removelast_last -> Test_last [] ; - Test_app_removelast_last -> Test_app [] ; - Test_app_removelast_last -> Test_list_ind [] ; - Test_ReDun_NoDup_remove_2 -> Test_ReDun_NoDup [] ; - Test_ReDun_NoDup_remove_2 -> Test_in_or_app [] ; - Test_removelast -> Test_cons [] ; - Test_removelast -> Test_nil [] ; - Test_removelast -> Test_list [] ; - Test_ReDun_NoDup_remove_1 -> Test_ReDun_NoDup_cons [] ; - Test_ReDun_NoDup_remove_1 -> Test_ReDun_NoDup [] ; - Test_ReDun_NoDup_remove_1 -> Test_in_or_app [] ; - Test_ReDun_NoDup_remove_1 -> Test_in_app_or [] ; - Test_last -> Test_list [] ; - Test_ReDun_NoDup_sind -> Test_ReDun_NoDup [] ; - Test_remove_In -> Test_remove [] ; - Test_remove_In -> Test_In [] ; - Test_remove_In -> Test_list_ind [] ; - Test_ReDun_NoDup_ind -> Test_ReDun_NoDup [] ; - Test_ReDun_NoDup_cons -> Test_ReDun_A [] ; - Test_ReDun_NoDup_cons -> Test_In [] ; - Test_ReDun_NoDup_cons -> Test_cons [] ; - Test_ReDun_NoDup_cons -> Test_nil [] ; - Test_remove -> Test_cons [] ; - Test_remove -> Test_nil [] ; - Test_remove -> Test_list [] ; - Test_ReDun_NoDup_nil -> Test_ReDun_A [] ; - Test_ReDun_NoDup_nil -> Test_In [] ; - Test_ReDun_NoDup_nil -> Test_cons [] ; - Test_ReDun_NoDup_nil -> Test_nil [] ; - Test_app_nth2 -> Test_nth [] ; - Test_app_nth2 -> Test_app [] ; - Test_app_nth2 -> Test_length [] ; - Test_app_nth2 -> Test_list_ind [] ; - Test_ReDun_NoDup -> Test_ReDun_A [] ; - Test_ReDun_NoDup -> Test_In [] ; - Test_ReDun_NoDup -> Test_cons [] ; - Test_ReDun_NoDup -> Test_nil [] ; - Test_app_nth1 -> Test_nth [] ; - Test_app_nth1 -> Test_app [] ; - Test_app_nth1 -> Test_length [] ; - Test_app_nth1 -> Test_list_ind [] ; - Test_nth_indep -> Test_nth [] ; - Test_nth_indep -> Test_length [] ; - Test_nth_indep -> Test_list_ind [] ; - Test_seq_shift -> Test_seq [] ; - Test_seq_shift -> Test_map [] ; - Test_nth_overflow -> Test_nth [] ; - Test_nth_overflow -> Test_length [] ; - Test_nth_overflow -> Test_list_ind [] ; - Test_seq_nth -> Test_seq [] ; - Test_seq_nth -> Test_nth [] ; - Test_nth_In -> Test_nth [] ; - Test_nth_In -> Test_In [] ; - Test_nth_In -> Test_length [] ; - Test_nth_In -> Test_cons [] ; - Test_nth_In -> Test_nil [] ; - Test_seq_length -> Test_seq [] ; - Test_seq_length -> Test_length [] ; - Test_nth_default -> Test_nth_error [] ; - Test_seq -> Test_cons [] ; - Test_seq -> Test_nil [] ; - Test_seq -> Test_list [] ; - Test_nth_error -> Test_list [] ; - Test_nth_S_cons -> Test_nth [] ; - Test_nth_S_cons -> Test_In [] ; - Test_nth_S_cons -> Test_cons [] ; - Test_firstn_removelast -> Test_firstn [] ; - Test_firstn_removelast -> Test_removelast_app [] ; - Test_firstn_removelast -> Test_length [] ; - Test_removelast_firstn -> Test_firstn [] ; - Test_removelast_firstn -> Test_removelast_app [] ; - Test_removelast_firstn -> Test_length [] ; - Test_nth_in_or_default -> Test_nth [] ; - Test_nth_in_or_default -> Test_In [] ; - Test_nth_in_or_default -> Test_list_rec [] ; - Test_nth_ok -> Test_list [] ; +Test_count_occ_nil [label="count_occ_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_count_occ_nil -> Test_count_occ [] ; + Test_count_occ_nil -> Test_nil [] ; +Test_count_occ; Test_count_occ_In; Test_count_occ_inv_nil; Test_count_occ_nil; Test_count_occ_cons_eq; Test_count_occ_cons_neq; Test_rev; Test_distr_rev; Test_rev_unit; Test_rev_involutive; Test_In_rev; Test_rev_length; Test_rev_nth; Test_rev_append; Test_rev_; Test_rev_append_rev; Test_rev_alt; Test_rev_list_ind; Test_rev_ind; Test_Permutation; Test_perm_nil; Test_perm_skip; Test_perm_swap; Test_perm_trans; Test_Permutation_ind; Test_Permutation_sind; Test_Permutation_nil; Test_Permutation_nil_cons; Test_Permutation_refl; Test_Permutation_sym; Test_Permutation_trans; Test_Permutation_in; Test_Permutation_app_tail; Test_Permutation_app_head; Test_Permutation_app; Test_Permutation_app_swap; Test_Permutation_cons_app; Test_Permutation_length; Test_Permutation_rev; Test_Permutation_ind_bis; Test_Permutation_app_inv; Test_Permutation_cons_inv; Test_Permutation_cons_app_inv; Test_Permutation_app_inv_l; Test_Permutation_app_inv_r; Test_list_eq_dec; Test_map; Test_in_map; Test_in_map_iff; Test_map_length; Test_map_nth; Test_map_app; Test_map_rev; Test_Permutation_map; Test_flat_map; Test_in_flat_map; Test_map_map; Test_map_ext; Test_fold_left; Test_fold_left_app; Test_fold_left_length; Test_fold_right; Test_fold_right_app; Test_fold_left_rev_right; Test_fold_symmetric; Test_list_power; Test_existsb; Test_existsb_exists; Test_existsb_nth; Test_forallb; Test_forallb_forall; Test_filter; Test_filter_In; Test_list; Test_find; Test_nil; Test_partition; Test_cons; Test_list_rect; Test_split; Test_in_split_l; Test_list_ind; Test_in_split_r; Test_list_rec; Test_list_sind; Test_split_nth; Test_head; Test_split_length_l; Test_hd; Test_split_length_r; Test_combine; Test_tail; Test_split_combine; Test_length; Test_size; Test_combine_split; Test_size_nil; Test_in_combine_l; Test_In; Test_in_combine_r; Test_app; Test_combine_length; Test_nil_cons; Test_combine_nth; Test_destruct_list; Test_list_prod; Test_in_prod_aux; Test_head_nil; Test_head_cons; Test_in_prod; Test_in_eq; Test_in_prod_iff; Test_prod_length; Test_in_cons; Test_lel; Test_in_nil; Test_lel_refl; Test_In_split; Test_lel_trans; Test_in_inv; Test_lel_cons_cons; Test_In_dec; Test_lel_cons; Test_app_cons_not_nil; Test_lel_tail; Test_app_nil_end; Test_app_ass; Test_lel_nil; Test_ass_app; Test_incl; Test_app_comm_cons; Test_incl_refl; Test_incl_tl; Test_app_eq_nil; Test_app_eq_unit; Test_incl_tran; Test_app_inj_tail; Test_incl_appl; Test_incl_appr; Test_app_length; Test_in_app_or; Test_incl_cons; Test_incl_app; Test_in_or_app; Test_app_inv_head; Test_firstn; Test_app_inv_tail; Test_skipn; Test_firstn_skipn; Test_nth; Test_firstn_length; Test_nth_ok; Test_removelast_firstn; Test_nth_in_or_default; Test_firstn_removelast; Test_nth_S_cons; Test_seq; Test_nth_error; Test_seq_length; Test_nth_default; Test_seq_nth; Test_nth_In; Test_nth_overflow; Test_seq_shift; Test_nth_indep; Test_app_nth1; Test_app_nth2; Test_remove; Test_remove_In; Test_last; Test_removelast; Test_app_removelast_last; Test_exists_last; Test_removelast_app; }; + Test_count_occ -> Test_list [] ; +Test_destruct_list [label="destruct_list", URL=, peripheries=3, fillcolor="#F070D1"] ; + Test_destruct_list -> Test_list_rect [] ; +Test_distr_rev [label="distr_rev", URL=, fillcolor="#7FFFD4"] ; + Test_distr_rev -> Test_app_ass [] ; + Test_distr_rev -> Test_app_nil_end [] ; + Test_distr_rev -> Test_rev [] ; +Test_existsb_exists [label="existsb_exists", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_existsb_exists -> Test_existsb [] ; + Test_existsb_exists -> Test_In [] ; + Test_existsb_exists -> Test_list_ind [] ; +Test_existsb [label="existsb", URL=, fillcolor="#F070D1"] ; +Test_existsb_nth [label="existsb_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_existsb_nth -> Test_existsb [] ; + Test_existsb_nth -> Test_length [] ; + Test_existsb_nth -> Test_list_ind [] ; + Test_existsb_nth -> Test_nth [] ; + Test_existsb -> Test_list [] ; +Test_exists_last [label="exists_last", URL=, peripheries=3, fillcolor="#F070D1"] ; + Test_exists_last -> Test_app [] ; + Test_exists_last -> Test_list_rect [] ; +Test_filter_In [label="filter_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_filter_In -> Test_filter [] ; + Test_filter_In -> Test_In [] ; + Test_filter_In -> Test_list_ind [] ; +Test_filter [label="filter", URL=, fillcolor="#F070D1"] ; + Test_filter -> Test_cons [] ; + Test_filter -> Test_list [] ; + Test_filter -> Test_nil [] ; +Test_find [label="find", URL=, peripheries=3, fillcolor="#F070D1"] ; + Test_find -> Test_list [] ; +Test_firstn [label="firstn", URL=, fillcolor="#F070D1"] ; +Test_firstn_length [label="firstn_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_firstn_length -> Test_firstn [] ; Test_firstn_length -> Test_length [] ; - Test_nth -> Test_list [] ; - Test_firstn_skipn -> Test_skipn [] ; - Test_firstn_skipn -> Test_firstn [] ; +Test_firstn_removelast [label="firstn_removelast", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_firstn_removelast -> Test_firstn [] ; + Test_firstn_removelast -> Test_length [] ; + Test_firstn_removelast -> Test_removelast_app [] ; +Test_firstn_skipn [label="firstn_skipn", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_firstn_skipn -> Test_app [] ; - Test_skipn -> Test_nil [] ; - Test_skipn -> Test_list [] ; - Test_app_inv_tail -> Test_app_length [] ; + Test_firstn_skipn -> Test_firstn [] ; + Test_firstn_skipn -> Test_skipn [] ; Test_firstn -> Test_cons [] ; - Test_firstn -> Test_nil [] ; Test_firstn -> Test_list [] ; - Test_app_inv_head -> Test_app [] ; - Test_app_inv_head -> Test_list_ind [] ; - Test_incl_app -> Test_incl [] ; - Test_incl_app -> Test_in_app_or [] ; - Test_in_or_app -> Test_app [] ; - Test_in_or_app -> Test_In [] ; - Test_in_or_app -> Test_list_ind [] ; - Test_incl_cons -> Test_incl [] ; - Test_incl_cons -> Test_cons [] ; + Test_firstn -> Test_nil [] ; +Test_flat_map [label="flat_map", URL=, fillcolor="#F070D1"] ; + Test_flat_map -> Test_app [] ; + Test_flat_map -> Test_nil [] ; +Test_fold_left_app [label="fold_left_app", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_fold_left_app -> Test_app [] ; + Test_fold_left_app -> Test_fold_left [] ; + Test_fold_left_app -> Test_list_ind [] ; +Test_fold_left [label="fold_left", URL=, fillcolor="#F070D1"] ; +Test_fold_left_length [label="fold_left_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_fold_left_length -> Test_fold_left [] ; + Test_fold_left_length -> Test_length [] ; + Test_fold_left_length -> Test_list_ind [] ; +Test_fold_left_rev_right [label="fold_left_rev_right", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_fold_left_rev_right -> Test_fold_left [] ; + Test_fold_left_rev_right -> Test_fold_right_app [] ; + Test_fold_left_rev_right -> Test_rev [] ; + Test_fold_left -> Test_list [] ; +Test_fold_right_app [label="fold_right_app", URL=, fillcolor="#7FFFD4"] ; + Test_fold_right_app -> Test_app [] ; + Test_fold_right_app -> Test_fold_right [] ; + Test_fold_right_app -> Test_list_ind [] ; +Test_fold_right [label="fold_right", URL=, fillcolor="#F070D1"] ; + Test_fold_right -> Test_list [] ; +Test_fold_symmetric [label="fold_symmetric", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_fold_symmetric -> Test_fold_left [] ; + Test_fold_symmetric -> Test_fold_right [] ; + Test_fold_symmetric -> Test_list_ind [] ; +Test_forallb_forall [label="forallb_forall", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_forallb_forall -> Test_forallb [] ; + Test_forallb_forall -> Test_In [] ; + Test_forallb_forall -> Test_list_ind [] ; +Test_forallb [label="forallb", URL=, fillcolor="#F070D1"] ; + Test_forallb -> Test_list [] ; +Test_hd [label="hd", URL=, peripheries=3, fillcolor="#F070D1"] ; + Test_hd -> Test_list [] ; +Test_head_cons [label="head_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_head_cons -> Test_cons [] ; + Test_head_cons -> Test_head [] ; +Test_head [label="head", URL=, fillcolor="#F070D1"] ; +Test_head_nil [label="head_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_head_nil -> Test_head [] ; + Test_head_nil -> Test_nil [] ; + Test_head -> Test_list [] ; +Test_in_app_or [label="in_app_or", URL=, fillcolor="#7FFFD4"] ; Test_in_app_or -> Test_app [] ; Test_in_app_or -> Test_In [] ; Test_in_app_or -> Test_list_ind [] ; - Test_incl_appr -> Test_incl [] ; - Test_incl_appr -> Test_in_or_app [] ; - Test_app_length -> Test_app [] ; - Test_app_length -> Test_length [] ; - Test_app_length -> Test_list_ind [] ; +Test_incl_app [label="incl_app", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_incl_appl [label="incl_appl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_incl_appl -> Test_incl [] ; Test_incl_appl -> Test_in_or_app [] ; - Test_app_inj_tail -> Test_app_cons_not_nil [] ; - Test_app_inj_tail -> Test_list_ind [] ; - Test_incl_tran -> Test_incl [] ; - Test_app_eq_unit -> Test_app_nil_end [] ; - Test_app_eq_unit -> Test_app_cons_not_nil [] ; - Test_incl_tl -> Test_incl [] ; - Test_incl_tl -> Test_in_cons [] ; - Test_app_eq_nil -> Test_app [] ; - Test_app_eq_nil -> Test_nil [] ; +Test_incl_appr [label="incl_appr", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_incl_appr -> Test_incl [] ; + Test_incl_appr -> Test_in_or_app [] ; + Test_incl_app -> Test_in_app_or [] ; + Test_incl_app -> Test_incl [] ; +Test_incl_cons [label="incl_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_incl_cons -> Test_cons [] ; + Test_incl_cons -> Test_incl [] ; +Test_incl [label="incl", URL=, fillcolor="#F070D1"] ; +Test_incl_refl [label="incl_refl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_incl_refl -> Test_incl [] ; - Test_app_comm_cons -> Test_app [] ; Test_incl -> Test_In [] ; - Test_ass_app -> Test_app_ass [] ; - Test_lel_nil -> Test_lel [] ; - Test_lel_nil -> Test_list_ind [] ; - Test_app_ass -> Test_app [] ; - Test_app_ass -> Test_list_ind [] ; - Test_lel_tail -> Test_lel [] ; - Test_lel_tail -> Test_cons [] ; - Test_app_nil_end -> Test_app [] ; - Test_app_nil_end -> Test_list_ind [] ; - Test_lel_cons -> Test_lel [] ; - Test_lel_cons -> Test_cons [] ; - Test_app_cons_not_nil -> Test_app [] ; - Test_app_cons_not_nil -> Test_nil [] ; - Test_lel_cons_cons -> Test_lel [] ; - Test_lel_cons_cons -> Test_cons [] ; +Test_incl_tl [label="incl_tl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_incl_tl -> Test_incl [] ; + Test_incl_tl -> Test_in_cons [] ; +Test_incl_tran [label="incl_tran", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_incl_tran -> Test_incl [] ; +Test_in_combine_l [label="in_combine_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_in_combine_l -> Test_combine [] ; + Test_in_combine_l -> Test_In [] ; + Test_in_combine_l -> Test_list_ind [] ; +Test_in_combine_r [label="in_combine_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_in_combine_r -> Test_combine [] ; + Test_in_combine_r -> Test_In [] ; + Test_in_combine_r -> Test_list_ind [] ; +Test_in_cons [label="in_cons", URL=, fillcolor="#7FFFD4"] ; + Test_in_cons -> Test_cons [] ; + Test_in_cons -> Test_In [] ; +Test_In_dec [label="In_dec", URL=, peripheries=3, fillcolor="#F070D1"] ; Test_In_dec -> Test_in_nil [] ; Test_In_dec -> Test_list_rec [] ; - Test_lel_trans -> Test_lel [] ; - Test_in_inv -> Test_In [] ; +Test_in_eq [label="in_eq", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_in_eq -> Test_cons [] ; + Test_in_eq -> Test_In [] ; +Test_in_flat_map [label="in_flat_map", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_in_flat_map -> Test_flat_map [] ; + Test_in_flat_map -> Test_in_app_or [] ; + Test_in_flat_map -> Test_in_or_app [] ; +Test_in_inv [label="in_inv", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_in_inv -> Test_cons [] ; - Test_lel_refl -> Test_lel [] ; - Test_In_split -> Test_app [] ; - Test_In_split -> Test_In [] ; - Test_In_split -> Test_list_ind [] ; - Test_lel -> Test_length [] ; + Test_in_inv -> Test_In [] ; +Test_In [label="In", URL=, fillcolor="#F070D1"] ; +Test_in_map_iff [label="in_map_iff", URL=, fillcolor="#7FFFD4"] ; + Test_in_map_iff -> Test_In [] ; + Test_in_map_iff -> Test_list_ind [] ; + Test_in_map_iff -> Test_map [] ; +Test_in_map [label="in_map", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_in_map -> Test_In [] ; + Test_in_map -> Test_list_ind [] ; + Test_in_map -> Test_map [] ; +Test_in_nil [label="in_nil", URL=, fillcolor="#7FFFD4"] ; Test_in_nil -> Test_In [] ; Test_in_nil -> Test_nil [] ; - Test_prod_length -> Test_list_prod [] ; - Test_prod_length -> Test_map_length [] ; - Test_prod_length -> Test_app_length [] ; - Test_in_cons -> Test_In [] ; - Test_in_cons -> Test_cons [] ; - Test_in_prod_iff -> Test_in_prod [] ; - Test_in_prod_iff -> Test_in_map_iff [] ; - Test_in_prod_iff -> Test_in_app_or [] ; - Test_in_eq -> Test_In [] ; - Test_in_eq -> Test_cons [] ; - Test_in_prod -> Test_in_prod_aux [] ; - Test_in_prod -> Test_list_prod [] ; - Test_in_prod -> Test_in_or_app [] ; - Test_head_cons -> Test_head [] ; - Test_head_cons -> Test_cons [] ; - Test_in_prod_aux -> Test_map [] ; +Test_in_or_app [label="in_or_app", URL=, fillcolor="#7FFFD4"] ; + Test_in_or_app -> Test_app [] ; + Test_in_or_app -> Test_In [] ; + Test_in_or_app -> Test_list_ind [] ; +Test_in_prod_aux [label="in_prod_aux", URL=, fillcolor="#7FFFD4"] ; Test_in_prod_aux -> Test_In [] ; Test_in_prod_aux -> Test_list_ind [] ; - Test_head_nil -> Test_head [] ; - Test_head_nil -> Test_nil [] ; - Test_list_prod -> Test_map [] ; - Test_list_prod -> Test_app [] ; - Test_destruct_list -> Test_list_rect [] ; - Test_nil_cons -> Test_cons [] ; - Test_nil_cons -> Test_nil [] ; - Test_nil_cons -> Test_list [] ; - Test_combine_nth -> Test_combine [] ; - Test_combine_nth -> Test_nth [] ; - Test_combine_nth -> Test_length [] ; - Test_combine_nth -> Test_list_ind [] ; - Test_combine_length -> Test_combine [] ; - Test_combine_length -> Test_length [] ; - Test_combine_length -> Test_list_ind [] ; - Test_app -> Test_cons [] ; - Test_app -> Test_list [] ; - Test_in_combine_r -> Test_combine [] ; - Test_in_combine_r -> Test_In [] ; - Test_in_combine_r -> Test_list_ind [] ; - Test_In -> Test_list [] ; - Test_size_nil -> Test_size [] ; - Test_size_nil -> Test_nil [] ; - Test_in_combine_l -> Test_combine [] ; - Test_in_combine_l -> Test_In [] ; - Test_in_combine_l -> Test_list_ind [] ; - Test_size -> Test_list [] ; - Test_combine_split -> Test_combine [] ; - Test_combine_split -> Test_split [] ; - Test_combine_split -> Test_length [] ; - Test_combine_split -> Test_list_ind [] ; - Test_split_combine -> Test_combine [] ; - Test_split_combine -> Test_split [] ; - Test_split_combine -> Test_list_ind [] ; - Test_length -> Test_list [] ; - Test_tail -> Test_nil [] ; - Test_tail -> Test_list [] ; - Test_combine -> Test_cons [] ; - Test_combine -> Test_nil [] ; - Test_combine -> Test_list [] ; - Test_split_length_r -> Test_split [] ; - Test_split_length_r -> Test_length [] ; - Test_split_length_r -> Test_list_ind [] ; - Test_hd -> Test_list [] ; - Test_split_length_l -> Test_split [] ; - Test_split_length_l -> Test_length [] ; - Test_split_length_l -> Test_list_ind [] ; - Test_head -> Test_list [] ; - Test_split_nth -> Test_split [] ; - Test_split_nth -> Test_nth [] ; - Test_split_nth -> Test_list_ind [] ; - Test_list_sind -> Test_cons [] ; - Test_list_sind -> Test_nil [] ; - Test_list_sind -> Test_list [] ; - Test_list_rec -> Test_list_rect [] ; - Test_in_split_r -> Test_split [] ; + Test_in_prod_aux -> Test_map [] ; +Test_in_prod_iff [label="in_prod_iff", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_in_prod_iff -> Test_in_app_or [] ; + Test_in_prod_iff -> Test_in_map_iff [] ; + Test_in_prod_iff -> Test_in_prod [] ; +Test_in_prod [label="in_prod", URL=, fillcolor="#7FFFD4"] ; + Test_in_prod -> Test_in_or_app [] ; + Test_in_prod -> Test_in_prod_aux [] ; + Test_in_prod -> Test_list_prod [] ; +Test_In_rev [label="In_rev", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_In_rev -> Test_in_app_or [] ; + Test_In_rev -> Test_in_or_app [] ; + Test_In_rev -> Test_rev [] ; +Test_In_split [label="In_split", URL=, fillcolor="#7FFFD4"] ; +Test_in_split_l [label="in_split_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_in_split_l -> Test_In [] ; + Test_in_split_l -> Test_list_ind [] ; + Test_in_split_l -> Test_split [] ; +Test_in_split_r [label="in_split_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_in_split_r -> Test_In [] ; Test_in_split_r -> Test_list_ind [] ; + Test_in_split_r -> Test_split [] ; + Test_In_split -> Test_app [] ; + Test_In_split -> Test_In [] ; + Test_In_split -> Test_list_ind [] ; + Test_In -> Test_list [] ; +Test_last [label="last", URL=, fillcolor="#F070D1"] ; + Test_last -> Test_list [] ; +Test_lel_cons_cons [label="lel_cons_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_lel_cons_cons -> Test_cons [] ; + Test_lel_cons_cons -> Test_lel [] ; +Test_lel_cons [label="lel_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_lel_cons -> Test_cons [] ; + Test_lel_cons -> Test_lel [] ; +Test_lel [label="lel", URL=, fillcolor="#F070D1"] ; +Test_lel_nil [label="lel_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_lel_nil -> Test_lel [] ; + Test_lel_nil -> Test_list_ind [] ; +Test_lel_refl [label="lel_refl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_lel_refl -> Test_lel [] ; +Test_lel_tail [label="lel_tail", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_lel_tail -> Test_cons [] ; + Test_lel_tail -> Test_lel [] ; + Test_lel -> Test_length [] ; +Test_lel_trans [label="lel_trans", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_lel_trans -> Test_lel [] ; +Test_length [label="length", URL=, fillcolor="#F070D1"] ; + Test_length -> Test_list [] ; +Test_list_eq_dec [label="list_eq_dec", URL=, peripheries=3, fillcolor="#F070D1"] ; + Test_list_eq_dec -> Test_list_rect [] ; + Test_list_eq_dec -> Test_nil_cons [] ; +Test_list_ind [label="list_ind", URL=, fillcolor="#7FFFD4"] ; Test_list_ind -> Test_cons [] ; - Test_list_ind -> Test_nil [] ; Test_list_ind -> Test_list [] ; - Test_in_split_l -> Test_split [] ; - Test_in_split_l -> Test_In [] ; - Test_in_split_l -> Test_list_ind [] ; - Test_split -> Test_cons [] ; - Test_split -> Test_nil [] ; - Test_split -> Test_list [] ; - Test_list_rect -> Test_cons [] ; - Test_list_rect -> Test_nil [] ; - Test_list_rect -> Test_list [] ; - Test_partition -> Test_cons [] ; - Test_partition -> Test_nil [] ; - Test_partition -> Test_list [] ; - Test_find -> Test_list [] ; - Test_filter_In -> Test_filter [] ; - Test_filter_In -> Test_In [] ; - Test_filter_In -> Test_list_ind [] ; - Test_filter -> Test_cons [] ; - Test_filter -> Test_nil [] ; - Test_filter -> Test_list [] ; - Test_forallb_forall -> Test_forallb [] ; - Test_forallb_forall -> Test_In [] ; - Test_forallb_forall -> Test_list_ind [] ; - Test_forallb -> Test_list [] ; - Test_existsb_nth -> Test_existsb [] ; - Test_existsb_nth -> Test_nth [] ; - Test_existsb_nth -> Test_length [] ; - Test_existsb_nth -> Test_list_ind [] ; - Test_existsb_exists -> Test_existsb [] ; - Test_existsb_exists -> Test_In [] ; - Test_existsb_exists -> Test_list_ind [] ; - Test_existsb -> Test_list [] ; + Test_list_ind -> Test_nil [] ; +Test_list [label="list", URL=, fillcolor="#E2CDFA"] ; +Test_list_power [label="list_power", URL=, peripheries=3, fillcolor="#F070D1"] ; Test_list_power -> Test_flat_map [] ; Test_list_power -> Test_map [] ; - Test_fold_symmetric -> Test_fold_right [] ; - Test_fold_symmetric -> Test_fold_left [] ; - Test_fold_symmetric -> Test_list_ind [] ; - Test_fold_left_rev_right -> Test_fold_right_app [] ; - Test_fold_left_rev_right -> Test_fold_left [] ; - Test_fold_left_rev_right -> Test_rev [] ; - Test_fold_right_app -> Test_fold_right [] ; - Test_fold_right_app -> Test_app [] ; - Test_fold_right_app -> Test_list_ind [] ; - Test_fold_right -> Test_list [] ; - Test_fold_left_length -> Test_fold_left [] ; - Test_fold_left_length -> Test_length [] ; - Test_fold_left_length -> Test_list_ind [] ; - Test_fold_left_app -> Test_fold_left [] ; - Test_fold_left_app -> Test_app [] ; - Test_fold_left_app -> Test_list_ind [] ; - Test_fold_left -> Test_list [] ; - Test_map_ext -> Test_map [] ; - Test_map_ext -> Test_list_ind [] ; - Test_map_map -> Test_map [] ; - Test_map_map -> Test_list_ind [] ; - Test_in_flat_map -> Test_flat_map [] ; - Test_in_flat_map -> Test_in_or_app [] ; - Test_in_flat_map -> Test_in_app_or [] ; - Test_flat_map -> Test_app [] ; - Test_flat_map -> Test_nil [] ; - Test_Permutation_map -> Test_map [] ; - Test_Permutation_map -> Test_Permutation_ind [] ; - Test_Permutation_map -> Test_perm_trans [] ; - Test_Permutation_map -> Test_perm_swap [] ; - Test_Permutation_map -> Test_perm_skip [] ; - Test_Permutation_map -> Test_perm_nil [] ; - Test_map_rev -> Test_map_app [] ; - Test_map_rev -> Test_rev [] ; - Test_map_app -> Test_map [] ; +Test_list_prod [label="list_prod", URL=, fillcolor="#F070D1"] ; + Test_list_prod -> Test_app [] ; + Test_list_prod -> Test_map [] ; +Test_list_rec [label="list_rec", URL=, fillcolor="#F070D1"] ; + Test_list_rec -> Test_list_rect [] ; +Test_list_rect [label="list_rect", URL=, fillcolor="#F070D1"] ; + Test_list_rect -> Test_cons [] ; + Test_list_rect -> Test_list [] ; + Test_list_rect -> Test_nil [] ; +Test_list_sind [label="list_sind", URL=, peripheries=3, fillcolor="#F070D1"] ; + Test_list_sind -> Test_cons [] ; + Test_list_sind -> Test_list [] ; + Test_list_sind -> Test_nil [] ; +Test_map_app [label="map_app", URL=, fillcolor="#7FFFD4"] ; Test_map_app -> Test_app [] ; Test_map_app -> Test_list_ind [] ; - Test_map_nth -> Test_map [] ; - Test_map_nth -> Test_nth [] ; - Test_map_nth -> Test_list_ind [] ; - Test_map_length -> Test_map [] ; + Test_map_app -> Test_map [] ; +Test_map_ext [label="map_ext", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_map_ext -> Test_list_ind [] ; + Test_map_ext -> Test_map [] ; +Test_map [label="map", URL=, fillcolor="#F070D1"] ; +Test_map_length [label="map_length", URL=, fillcolor="#7FFFD4"] ; Test_map_length -> Test_length [] ; Test_map_length -> Test_list_ind [] ; - Test_in_map_iff -> Test_map [] ; - Test_in_map_iff -> Test_In [] ; - Test_in_map_iff -> Test_list_ind [] ; - Test_in_map -> Test_map [] ; - Test_in_map -> Test_In [] ; - Test_in_map -> Test_list_ind [] ; + Test_map_length -> Test_map [] ; +Test_map_map [label="map_map", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_map_map -> Test_list_ind [] ; + Test_map_map -> Test_map [] ; +Test_map_nth [label="map_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_map_nth -> Test_list_ind [] ; + Test_map_nth -> Test_map [] ; + Test_map_nth -> Test_nth [] ; +Test_map_rev [label="map_rev", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_map_rev -> Test_map_app [] ; + Test_map_rev -> Test_rev [] ; Test_map -> Test_cons [] ; - Test_map -> Test_nil [] ; Test_map -> Test_list [] ; - Test_list_eq_dec -> Test_nil_cons [] ; - Test_list_eq_dec -> Test_list_rect [] ; - Test_Permutation_app_inv_r -> Test_Permutation_app_inv [] ; - Test_Permutation_app_inv_r -> Test_app_nil_end [] ; + Test_map -> Test_nil [] ; +Test_nil_cons [label="nil_cons", URL=, fillcolor="#7FFFD4"] ; + Test_nil_cons -> Test_cons [] ; + Test_nil_cons -> Test_list [] ; + Test_nil_cons -> Test_nil [] ; +Test_nil [label="nil", URL=, fillcolor="#7FAAFF"] ; +Test_nth_default [label="nth_default", URL=, peripheries=3, fillcolor="#F070D1"] ; + Test_nth_default -> Test_nth_error [] ; +Test_nth_error [label="nth_error", URL=, fillcolor="#F070D1"] ; + Test_nth_error -> Test_list [] ; +Test_nth_indep [label="nth_indep", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_nth_indep -> Test_length [] ; + Test_nth_indep -> Test_list_ind [] ; + Test_nth_indep -> Test_nth [] ; +Test_nth_In [label="nth_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_nth_in_or_default [label="nth_in_or_default", URL=, peripheries=3, fillcolor="#F070D1"] ; + Test_nth_in_or_default -> Test_In [] ; + Test_nth_in_or_default -> Test_list_rec [] ; + Test_nth_in_or_default -> Test_nth [] ; + Test_nth_In -> Test_cons [] ; + Test_nth_In -> Test_In [] ; + Test_nth_In -> Test_length [] ; + Test_nth_In -> Test_nil [] ; + Test_nth_In -> Test_nth [] ; +Test_nth [label="nth", URL=, fillcolor="#F070D1"] ; +Test_nth_ok [label="nth_ok", URL=, peripheries=3, fillcolor="#F070D1"] ; + Test_nth_ok -> Test_list [] ; +Test_nth_overflow [label="nth_overflow", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_nth_overflow -> Test_length [] ; + Test_nth_overflow -> Test_list_ind [] ; + Test_nth_overflow -> Test_nth [] ; +Test_nth_S_cons [label="nth_S_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_nth_S_cons -> Test_cons [] ; + Test_nth_S_cons -> Test_In [] ; + Test_nth_S_cons -> Test_nth [] ; + Test_nth -> Test_list [] ; +Test_partition [label="partition", URL=, peripheries=3, fillcolor="#F070D1"] ; + Test_partition -> Test_cons [] ; + Test_partition -> Test_list [] ; + Test_partition -> Test_nil [] ; +Test_perm_nil [label="perm_nil", URL=, fillcolor="#7FAAFF"] ; + Test_perm_nil -> Test_cons [] ; + Test_perm_nil -> Test_list [] ; + Test_perm_nil -> Test_nil [] ; +Test_perm_skip [label="perm_skip", URL=, fillcolor="#7FAAFF"] ; + Test_perm_skip -> Test_cons [] ; + Test_perm_skip -> Test_list [] ; + Test_perm_skip -> Test_nil [] ; +Test_perm_swap [label="perm_swap", URL=, fillcolor="#7FAAFF"] ; + Test_perm_swap -> Test_cons [] ; + Test_perm_swap -> Test_list [] ; + Test_perm_swap -> Test_nil [] ; +Test_perm_trans [label="perm_trans", URL=, fillcolor="#7FAAFF"] ; + Test_perm_trans -> Test_cons [] ; + Test_perm_trans -> Test_list [] ; + Test_perm_trans -> Test_nil [] ; +Test_Permutation_app_head [label="Permutation_app_head", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_app_head -> Test_app_comm_cons [] ; + Test_Permutation_app_head -> Test_list_ind [] ; + Test_Permutation_app_head -> Test_perm_skip [] ; + Test_Permutation_app_head -> Test_Permutation [] ; +Test_Permutation_app_inv [label="Permutation_app_inv", URL=, fillcolor="#7FFFD4"] ; +Test_Permutation_app_inv_l [label="Permutation_app_inv_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_Permutation_app_inv_l -> Test_Permutation_cons_inv [] ; - Test_Permutation_cons_app_inv -> Test_Permutation_app_inv [] ; - Test_Permutation_cons_inv -> Test_Permutation_app_inv [] ; - Test_Permutation_app_inv -> Test_Permutation_ind_bis [] ; +Test_Permutation_app_inv_r [label="Permutation_app_inv_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_Permutation_app_inv_r -> Test_app_nil_end [] ; + Test_Permutation_app_inv_r -> Test_Permutation_app_inv [] ; + Test_Permutation_app_inv -> Test_in_or_app [] ; + Test_Permutation_app_inv -> Test_In_split [] ; Test_Permutation_app_inv -> Test_Permutation_cons_app [] ; Test_Permutation_app_inv -> Test_Permutation_in [] ; + Test_Permutation_app_inv -> Test_Permutation_ind_bis [] ; Test_Permutation_app_inv -> Test_Permutation_sym [] ; - Test_Permutation_app_inv -> Test_in_or_app [] ; - Test_Permutation_app_inv -> Test_In_split [] ; - Test_Permutation_ind_bis -> Test_Permutation_refl [] ; - Test_Permutation_ind_bis -> Test_Permutation_ind [] ; - Test_Permutation_ind_bis -> Test_perm_swap [] ; - Test_Permutation_rev -> Test_Permutation_app_swap [] ; - Test_Permutation_rev -> Test_rev [] ; - Test_Permutation_length -> Test_Permutation_ind [] ; - Test_Permutation_length -> Test_length [] ; - Test_Permutation_cons_app -> Test_Permutation_refl [] ; - Test_Permutation_cons_app -> Test_perm_trans [] ; - Test_Permutation_cons_app -> Test_perm_swap [] ; - Test_Permutation_cons_app -> Test_app [] ; - Test_Permutation_app_swap -> Test_Permutation_trans [] ; - Test_Permutation_app_swap -> Test_Permutation_sym [] ; - Test_Permutation_app_swap -> Test_Permutation_refl [] ; +Test_Permutation_app [label="Permutation_app", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_Permutation_app_swap [label="Permutation_app_swap", URL=, fillcolor="#7FFFD4"] ; Test_Permutation_app_swap -> Test_app_comm_cons [] ; Test_Permutation_app_swap -> Test_app_nil_end [] ; + Test_Permutation_app_swap -> Test_Permutation_refl [] ; + Test_Permutation_app_swap -> Test_Permutation_sym [] ; + Test_Permutation_app_swap -> Test_Permutation_trans [] ; +Test_Permutation_app_tail [label="Permutation_app_tail", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_app_tail -> Test_app [] ; + Test_Permutation_app_tail -> Test_Permutation_refl [] ; + Test_Permutation_app_tail -> Test_Permutation_sym [] ; + Test_Permutation_app_tail -> Test_Permutation_trans [] ; Test_Permutation_app -> Test_Permutation_app_head [] ; Test_Permutation_app -> Test_Permutation_app_tail [] ; - Test_Permutation_app_head -> Test_perm_skip [] ; - Test_Permutation_app_head -> Test_Permutation [] ; - Test_Permutation_app_head -> Test_app_comm_cons [] ; - Test_Permutation_app_head -> Test_list_ind [] ; - Test_Permutation_app_tail -> Test_Permutation_trans [] ; - Test_Permutation_app_tail -> Test_Permutation_sym [] ; - Test_Permutation_app_tail -> Test_Permutation_refl [] ; - Test_Permutation_app_tail -> Test_app [] ; - Test_Permutation_in -> Test_Permutation_ind [] ; +Test_Permutation_cons_app_inv [label="Permutation_cons_app_inv", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_Permutation_cons_app_inv -> Test_Permutation_app_inv [] ; +Test_Permutation_cons_app [label="Permutation_cons_app", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_cons_app -> Test_app [] ; + Test_Permutation_cons_app -> Test_perm_swap [] ; + Test_Permutation_cons_app -> Test_perm_trans [] ; + Test_Permutation_cons_app -> Test_Permutation_refl [] ; +Test_Permutation_cons_inv [label="Permutation_cons_inv", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_cons_inv -> Test_Permutation_app_inv [] ; +Test_Permutation_ind_bis [label="Permutation_ind_bis", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_ind_bis -> Test_perm_swap [] ; + Test_Permutation_ind_bis -> Test_Permutation_ind [] ; + Test_Permutation_ind_bis -> Test_Permutation_refl [] ; +Test_Permutation_ind [label="Permutation_ind", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_ind -> Test_Permutation [] ; +Test_Permutation_in [label="Permutation_in", URL=, fillcolor="#7FFFD4"] ; Test_Permutation_in -> Test_In [] ; - Test_Permutation_trans -> Test_perm_trans [] ; - Test_Permutation_trans -> Test_Permutation [] ; - Test_Permutation_sym -> Test_Permutation_ind [] ; - Test_Permutation_sym -> Test_perm_trans [] ; - Test_Permutation_sym -> Test_perm_swap [] ; - Test_Permutation_sym -> Test_perm_skip [] ; - Test_Permutation_sym -> Test_perm_nil [] ; - Test_Permutation_refl -> Test_perm_skip [] ; - Test_Permutation_refl -> Test_perm_nil [] ; - Test_Permutation_refl -> Test_Permutation [] ; - Test_Permutation_refl -> Test_list_ind [] ; + Test_Permutation_in -> Test_Permutation_ind [] ; +Test_Permutation [label="Permutation", URL=, fillcolor="#E2CDFA"] ; +Test_Permutation_length [label="Permutation_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_Permutation_length -> Test_length [] ; + Test_Permutation_length -> Test_Permutation_ind [] ; +Test_Permutation_map [label="Permutation_map", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_Permutation_map -> Test_map [] ; + Test_Permutation_map -> Test_perm_nil [] ; + Test_Permutation_map -> Test_perm_skip [] ; + Test_Permutation_map -> Test_perm_swap [] ; + Test_Permutation_map -> Test_perm_trans [] ; + Test_Permutation_map -> Test_Permutation_ind [] ; +Test_Permutation_nil_cons [label="Permutation_nil_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_Permutation_nil_cons -> Test_Permutation_nil [] ; - Test_Permutation_nil -> Test_Permutation_ind [] ; +Test_Permutation_nil [label="Permutation_nil", URL=, fillcolor="#7FFFD4"] ; Test_Permutation_nil -> Test_nil_cons [] ; + Test_Permutation_nil -> Test_Permutation_ind [] ; +Test_Permutation_refl [label="Permutation_refl", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_refl -> Test_list_ind [] ; + Test_Permutation_refl -> Test_perm_nil [] ; + Test_Permutation_refl -> Test_perm_skip [] ; + Test_Permutation_refl -> Test_Permutation [] ; +Test_Permutation_rev [label="Permutation_rev", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_Permutation_rev -> Test_Permutation_app_swap [] ; + Test_Permutation_rev -> Test_rev [] ; +Test_Permutation_sind [label="Permutation_sind", URL=, peripheries=3, fillcolor="#F070D1"] ; Test_Permutation_sind -> Test_Permutation [] ; - Test_Permutation_ind -> Test_Permutation [] ; - Test_perm_trans -> Test_cons [] ; - Test_perm_trans -> Test_nil [] ; - Test_perm_trans -> Test_list [] ; - Test_perm_swap -> Test_cons [] ; - Test_perm_swap -> Test_nil [] ; - Test_perm_swap -> Test_list [] ; - Test_perm_skip -> Test_cons [] ; - Test_perm_skip -> Test_nil [] ; - Test_perm_skip -> Test_list [] ; - Test_perm_nil -> Test_cons [] ; - Test_perm_nil -> Test_nil [] ; - Test_perm_nil -> Test_list [] ; +Test_Permutation_sym [label="Permutation_sym", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_sym -> Test_perm_nil [] ; + Test_Permutation_sym -> Test_perm_skip [] ; + Test_Permutation_sym -> Test_perm_swap [] ; + Test_Permutation_sym -> Test_perm_trans [] ; + Test_Permutation_sym -> Test_Permutation_ind [] ; Test_Permutation -> Test_cons [] ; - Test_Permutation -> Test_nil [] ; Test_Permutation -> Test_list [] ; - Test_rev_ind -> Test_rev_list_ind [] ; - Test_rev_ind -> Test_rev_involutive [] ; - Test_rev_list_ind -> Test_rev [] ; - Test_rev_list_ind -> Test_list_ind [] ; - Test_rev_alt -> Test_rev_append_rev [] ; + Test_Permutation -> Test_nil [] ; +Test_Permutation_trans [label="Permutation_trans", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_trans -> Test_perm_trans [] ; + Test_Permutation_trans -> Test_Permutation [] ; +Test_prod_length [label="prod_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_prod_length -> Test_app_length [] ; + Test_prod_length -> Test_list_prod [] ; + Test_prod_length -> Test_map_length [] ; +Test_ReDun_A [label="A", URL=, fillcolor="#FACDEF"] ; +Test_ReDun_A; Test_ReDun_NoDup; Test_ReDun_NoDup_nil; Test_ReDun_NoDup_cons; Test_ReDun_NoDup_ind; Test_ReDun_NoDup_sind; Test_ReDun_NoDup_remove_1; Test_ReDun_NoDup_remove_2; Test_ReDun_NoDup_Permutation; }; +Test_ReDun_NoDup_cons [label="NoDup_cons", URL=, fillcolor="#7FAAFF"] ; + Test_ReDun_NoDup_cons -> Test_cons [] ; + Test_ReDun_NoDup_cons -> Test_In [] ; + Test_ReDun_NoDup_cons -> Test_nil [] ; + Test_ReDun_NoDup_cons -> Test_ReDun_A [] ; +Test_ReDun_NoDup_ind [label="NoDup_ind", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_ReDun_NoDup_ind -> Test_ReDun_NoDup [] ; +Test_ReDun_NoDup [label="NoDup", URL=, fillcolor="#E2CDFA"] ; +Test_ReDun_NoDup_nil [label="NoDup_nil", URL=, peripheries=3, fillcolor="#7FAAFF"] ; + Test_ReDun_NoDup_nil -> Test_cons [] ; + Test_ReDun_NoDup_nil -> Test_In [] ; + Test_ReDun_NoDup_nil -> Test_nil [] ; + Test_ReDun_NoDup_nil -> Test_ReDun_A [] ; +Test_ReDun_NoDup_Permutation [label="NoDup_Permutation", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_ReDun_NoDup_Permutation -> Test_In_split [] ; + Test_ReDun_NoDup_Permutation -> Test_Permutation_cons_app [] ; + Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_1 [] ; + Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_2 [] ; +Test_ReDun_NoDup_remove_1 [label="NoDup_remove_1", URL=, fillcolor="#7FFFD4"] ; + Test_ReDun_NoDup_remove_1 -> Test_in_app_or [] ; + Test_ReDun_NoDup_remove_1 -> Test_in_or_app [] ; + Test_ReDun_NoDup_remove_1 -> Test_ReDun_NoDup [] ; + Test_ReDun_NoDup_remove_1 -> Test_ReDun_NoDup_cons [] ; +Test_ReDun_NoDup_remove_2 [label="NoDup_remove_2", URL=, fillcolor="#7FFFD4"] ; + Test_ReDun_NoDup_remove_2 -> Test_in_or_app [] ; + Test_ReDun_NoDup_remove_2 -> Test_ReDun_NoDup [] ; +Test_ReDun_NoDup_sind [label="NoDup_sind", URL=, peripheries=3, fillcolor="#F070D1"] ; + Test_ReDun_NoDup_sind -> Test_ReDun_NoDup [] ; + Test_ReDun_NoDup -> Test_cons [] ; + Test_ReDun_NoDup -> Test_In [] ; + Test_ReDun_NoDup -> Test_nil [] ; + Test_ReDun_NoDup -> Test_ReDun_A [] ; +Test_remove_In [label="remove_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_remove_In -> Test_In [] ; + Test_remove_In -> Test_list_ind [] ; + Test_remove_In -> Test_remove [] ; +Test_remove [label="remove", URL=, fillcolor="#F070D1"] ; +Test_removelast_app [label="removelast_app", URL=, fillcolor="#7FFFD4"] ; + Test_removelast_app -> Test_app [] ; + Test_removelast_app -> Test_list_ind [] ; + Test_removelast_app -> Test_removelast [] ; +Test_removelast_firstn [label="removelast_firstn", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_removelast_firstn -> Test_firstn [] ; + Test_removelast_firstn -> Test_length [] ; + Test_removelast_firstn -> Test_removelast_app [] ; +Test_removelast [label="removelast", URL=, fillcolor="#F070D1"] ; + Test_removelast -> Test_cons [] ; + Test_removelast -> Test_list [] ; + Test_removelast -> Test_nil [] ; + Test_remove -> Test_cons [] ; + Test_remove -> Test_list [] ; + Test_remove -> Test_nil [] ; +Test_rev_alt [label="rev_alt", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_rev_alt -> Test_app_nil_end [] ; - Test_rev_append_rev -> Test_rev_append [] ; - Test_rev_append_rev -> Test_rev [] ; + Test_rev_alt -> Test_rev_append_rev [] ; +Test_rev_append [label="rev_append", URL=, fillcolor="#F070D1"] ; +Test_rev_append_rev [label="rev_append_rev", URL=, fillcolor="#7FFFD4"] ; Test_rev_append_rev -> Test_ass_app [] ; - Test_rev_ -> Test_rev_append [] ; - Test_rev_ -> Test_nil [] ; + Test_rev_append_rev -> Test_rev [] ; + Test_rev_append_rev -> Test_rev_append [] ; Test_rev_append -> Test_cons [] ; Test_rev_append -> Test_list [] ; - Test_rev_nth -> Test_rev_length [] ; - Test_rev_nth -> Test_app_nth2 [] ; - Test_rev_nth -> Test_app_nth1 [] ; - Test_rev_length -> Test_rev [] ; - Test_rev_length -> Test_app_length [] ; - Test_In_rev -> Test_rev [] ; - Test_In_rev -> Test_in_or_app [] ; - Test_In_rev -> Test_in_app_or [] ; +Test_rev_ind [label="rev_ind", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_rev_ind -> Test_rev_involutive [] ; + Test_rev_ind -> Test_rev_list_ind [] ; +Test_rev_involutive [label="rev_involutive", URL=, fillcolor="#7FFFD4"] ; Test_rev_involutive -> Test_rev_unit [] ; - Test_rev_unit -> Test_distr_rev [] ; - Test_distr_rev -> Test_rev [] ; - Test_distr_rev -> Test_app_ass [] ; - Test_distr_rev -> Test_app_nil_end [] ; +Test_rev [label="rev", URL=, fillcolor="#F070D1"] ; +Test_rev_ [label="rev'", URL=, peripheries=3, fillcolor="#F070D1"] ; +Test_rev_length [label="rev_length", URL=, fillcolor="#7FFFD4"] ; + Test_rev_length -> Test_app_length [] ; + Test_rev_length -> Test_rev [] ; +Test_rev_list_ind [label="rev_list_ind", URL=, fillcolor="#7FFFD4"] ; + Test_rev_list_ind -> Test_list_ind [] ; + Test_rev_list_ind -> Test_rev [] ; +Test_rev_nth [label="rev_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_rev_nth -> Test_app_nth1 [] ; + Test_rev_nth -> Test_app_nth2 [] ; + Test_rev_nth -> Test_rev_length [] ; Test_rev -> Test_app [] ; Test_rev -> Test_nil [] ; - Test_count_occ_cons_neq -> Test_count_occ [] ; - Test_count_occ_cons_neq -> Test_cons [] ; - Test_count_occ_cons_eq -> Test_count_occ [] ; - Test_count_occ_cons_eq -> Test_cons [] ; - Test_count_occ_nil -> Test_count_occ [] ; - Test_count_occ_nil -> Test_nil [] ; - Test_count_occ_inv_nil -> Test_count_occ [] ; - Test_count_occ_inv_nil -> Test_list_ind [] ; - Test_count_occ_In -> Test_count_occ [] ; - Test_count_occ_In -> Test_In [] ; - Test_count_occ_In -> Test_list_ind [] ; - Test_count_occ -> Test_list [] ; -subgraph cluster_Test { label="Test"; fillcolor="#FFFFC3"; labeljust=l; style=filled -subgraph cluster_Test_ReDun { label="ReDun"; fillcolor="#FFFFA3"; labeljust=l; style=filled -Test_ReDun_A; Test_ReDun_NoDup; Test_ReDun_NoDup_nil; Test_ReDun_NoDup_cons; Test_ReDun_NoDup_ind; Test_ReDun_NoDup_sind; Test_ReDun_NoDup_remove_1; Test_ReDun_NoDup_remove_2; Test_ReDun_NoDup_Permutation; }; -Test_count_occ; Test_count_occ_In; Test_count_occ_inv_nil; Test_count_occ_nil; Test_count_occ_cons_eq; Test_count_occ_cons_neq; Test_rev; Test_distr_rev; Test_rev_unit; Test_rev_involutive; Test_In_rev; Test_rev_length; Test_rev_nth; Test_rev_append; Test_rev_; Test_rev_append_rev; Test_rev_alt; Test_rev_list_ind; Test_rev_ind; Test_Permutation; Test_perm_nil; Test_perm_skip; Test_perm_swap; Test_perm_trans; Test_Permutation_ind; Test_Permutation_sind; Test_Permutation_nil; Test_Permutation_nil_cons; Test_Permutation_refl; Test_Permutation_sym; Test_Permutation_trans; Test_Permutation_in; Test_Permutation_app_tail; Test_Permutation_app_head; Test_Permutation_app; Test_Permutation_app_swap; Test_Permutation_cons_app; Test_Permutation_length; Test_Permutation_rev; Test_Permutation_ind_bis; Test_Permutation_app_inv; Test_Permutation_cons_inv; Test_Permutation_cons_app_inv; Test_Permutation_app_inv_l; Test_Permutation_app_inv_r; Test_list_eq_dec; Test_map; Test_in_map; Test_in_map_iff; Test_map_length; Test_map_nth; Test_map_app; Test_map_rev; Test_Permutation_map; Test_flat_map; Test_in_flat_map; Test_map_map; Test_map_ext; Test_fold_left; Test_fold_left_app; Test_fold_left_length; Test_fold_right; Test_fold_right_app; Test_fold_left_rev_right; Test_fold_symmetric; Test_list_power; Test_existsb; Test_existsb_exists; Test_existsb_nth; Test_forallb; Test_forallb_forall; Test_filter; Test_filter_In; Test_list; Test_find; Test_nil; Test_partition; Test_cons; Test_list_rect; Test_split; Test_in_split_l; Test_list_ind; Test_in_split_r; Test_list_rec; Test_list_sind; Test_split_nth; Test_head; Test_split_length_l; Test_hd; Test_split_length_r; Test_combine; Test_tail; Test_length; Test_split_combine; Test_combine_split; Test_size; Test_in_combine_l; Test_size_nil; Test_In; Test_in_combine_r; Test_app; Test_combine_length; Test_combine_nth; Test_nil_cons; Test_destruct_list; Test_list_prod; Test_head_nil; Test_in_prod_aux; Test_head_cons; Test_in_prod; Test_in_eq; Test_in_prod_iff; Test_in_cons; Test_prod_length; Test_in_nil; Test_lel; Test_In_split; Test_lel_refl; Test_in_inv; Test_lel_trans; Test_In_dec; Test_lel_cons_cons; Test_app_cons_not_nil; Test_lel_cons; Test_app_nil_end; Test_lel_tail; Test_app_ass; Test_lel_nil; Test_ass_app; Test_incl; Test_app_comm_cons; Test_incl_refl; Test_app_eq_nil; Test_incl_tl; Test_app_eq_unit; Test_incl_tran; Test_app_inj_tail; Test_incl_appl; Test_app_length; Test_incl_appr; Test_in_app_or; Test_incl_cons; Test_in_or_app; Test_incl_app; Test_app_inv_head; Test_firstn; Test_app_inv_tail; Test_skipn; Test_firstn_skipn; Test_nth; Test_firstn_length; Test_nth_ok; Test_nth_in_or_default; Test_removelast_firstn; Test_firstn_removelast; Test_nth_S_cons; Test_nth_error; Test_seq; Test_nth_default; Test_seq_length; Test_nth_In; Test_seq_nth; Test_nth_overflow; Test_seq_shift; Test_nth_indep; Test_app_nth1; Test_app_nth2; Test_remove; Test_remove_In; Test_last; Test_removelast; Test_app_removelast_last; Test_exists_last; Test_removelast_app; }; -} /* END */ + Test_rev_ -> Test_nil [] ; + Test_rev_ -> Test_rev_append [] ; +Test_rev_unit [label="rev_unit", URL=, fillcolor="#7FFFD4"] ; + Test_rev_unit -> Test_distr_rev [] ; +Test_seq [label="seq", URL=, fillcolor="#F070D1"] ; +Test_seq_length [label="seq_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_seq_length -> Test_length [] ; + Test_seq_length -> Test_seq [] ; +Test_seq_nth [label="seq_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_seq_nth -> Test_nth [] ; + Test_seq_nth -> Test_seq [] ; +Test_seq_shift [label="seq_shift", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_seq_shift -> Test_map [] ; + Test_seq_shift -> Test_seq [] ; + Test_seq -> Test_cons [] ; + Test_seq -> Test_list [] ; + Test_seq -> Test_nil [] ; +Test_size [label="size", URL=, fillcolor="#FACDEF"] ; +Test_size_nil [label="size_nil", URL=, peripheries=3, fillcolor="#FFB57F"] ; + Test_size_nil -> Test_nil [] ; + Test_size_nil -> Test_size [] ; + Test_size -> Test_list [] ; +Test_skipn [label="skipn", URL=, fillcolor="#F070D1"] ; + Test_skipn -> Test_list [] ; + Test_skipn -> Test_nil [] ; +Test_split_combine [label="split_combine", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_split_combine -> Test_combine [] ; + Test_split_combine -> Test_list_ind [] ; + Test_split_combine -> Test_split [] ; +Test_split [label="split", URL=, fillcolor="#F070D1"] ; +Test_split_length_l [label="split_length_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_split_length_l -> Test_length [] ; + Test_split_length_l -> Test_list_ind [] ; + Test_split_length_l -> Test_split [] ; +Test_split_length_r [label="split_length_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_split_length_r -> Test_length [] ; + Test_split_length_r -> Test_list_ind [] ; + Test_split_length_r -> Test_split [] ; +Test_split_nth [label="split_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_split_nth -> Test_list_ind [] ; + Test_split_nth -> Test_nth [] ; + Test_split_nth -> Test_split [] ; + Test_split -> Test_cons [] ; + Test_split -> Test_list [] ; + Test_split -> Test_nil [] ; +Test_tail [label="tail", URL=, peripheries=3, fillcolor="#F070D1"] ; + Test_tail -> Test_list [] ; + Test_tail -> Test_nil [] ; diff --git a/tests/graph.dpd.oracle b/tests/graph.dpd.oracle index 7164690c2..6545459c0 100644 --- a/tests/graph.dpd.oracle +++ b/tests/graph.dpd.oracle @@ -1,263 +1,235 @@ -N: 9 "A" [body=no, kind=cnst, prop=no, path="Test.ReDun", ]; -N: 170 "In" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 159 "In_dec" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 117 "In_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 161 "In_split" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 1 "NoDup_Permutation" [body=yes, kind=cnst, prop=yes, path="Test.ReDun", ]; -N: 5 "NoDup_ind" [body=yes, kind=cnst, prop=yes, path="Test.ReDun", ]; -N: 3 "NoDup_remove_1" [body=yes, kind=cnst, prop=yes, path="Test.ReDun", ]; -N: 2 "NoDup_remove_2" [body=yes, kind=cnst, prop=yes, path="Test.ReDun", ]; -N: 4 "NoDup_sind" [body=yes, kind=cnst, prop=no, path="Test.ReDun", ]; -N: 93 "Permutation_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 94 "Permutation_app_head" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 87 "Permutation_app_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 84 "Permutation_app_inv_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 83 "Permutation_app_inv_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 92 "Permutation_app_swap" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 95 "Permutation_app_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 91 "Permutation_cons_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 85 "Permutation_cons_app_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 86 "Permutation_cons_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 96 "Permutation_in" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 103 "Permutation_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 88 "Permutation_ind_bis" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 90 "Permutation_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 74 "Permutation_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 101 "Permutation_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 100 "Permutation_nil_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 99 "Permutation_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 89 "Permutation_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 102 "Permutation_sind" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 98 "Permutation_sym" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 97 "Permutation_trans" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 169 "app" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 156 "app_ass" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 154 "app_comm_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 158 "app_cons_not_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 153 "app_eq_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 152 "app_eq_unit" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 151 "app_inj_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 147 "app_inv_head" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 146 "app_inv_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 150 "app_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 157 "app_nil_end" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 136 "app_nth1" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 135 "app_nth2" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 130 "app_removelast_last" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 155 "ass_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 46 "combine" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 41 "combine_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 40 "combine_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 44 "combine_split" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 127 "count_occ" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 126 "count_occ_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 123 "count_occ_cons_eq" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 122 "count_occ_cons_neq" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 125 "count_occ_inv_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 124 "count_occ_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 167 "destruct_list" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 120 "distr_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 129 "exists_last" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 61 "existsb" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 60 "existsb_exists" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 59 "existsb_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 56 "filter" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 55 "filter_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 54 "find" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 19 "firstn" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 16 "firstn_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 14 "firstn_removelast" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 17 "firstn_skipn" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 73 "flat_map" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 69 "fold_left" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 68 "fold_left_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 67 "fold_left_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 64 "fold_left_rev_right" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 66 "fold_right" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 65 "fold_right_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 63 "fold_symmetric" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 58 "forallb" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 57 "forallb_forall" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 175 "hd" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 176 "head" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 165 "head_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 166 "head_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 149 "in_app_or" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 43 "in_combine_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 42 "in_combine_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 163 "in_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 164 "in_eq" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 72 "in_flat_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 160 "in_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 80 "in_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 79 "in_map_iff" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 162 "in_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 148 "in_or_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 37 "in_prod" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 38 "in_prod_aux" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 36 "in_prod_iff" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 51 "in_split_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 50 "in_split_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 27 "incl" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 20 "incl_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 23 "incl_appl" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 22 "incl_appr" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 21 "incl_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 26 "incl_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 25 "incl_tl" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 24 "incl_tran" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 132 "last" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 34 "lel" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 30 "lel_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 31 "lel_cons_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 28 "lel_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 33 "lel_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 29 "lel_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 32 "lel_trans" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 173 "length" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 82 "list_eq_dec" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 179 "list_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 62 "list_power" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 39 "list_prod" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 178 "list_rec" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 180 "list_rect" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 177 "list_sind" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 81 "map" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 76 "map_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 70 "map_ext" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 78 "map_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 71 "map_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 77 "map_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 75 "map_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 168 "nil_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 145 "nth" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 139 "nth_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 142 "nth_S_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 140 "nth_default" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 141 "nth_error" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 143 "nth_in_or_default" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 137 "nth_indep" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 144 "nth_ok" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 138 "nth_overflow" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 53 "partition" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 35 "prod_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 134 "remove" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 133 "remove_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 131 "removelast" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 128 "removelast_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 15 "removelast_firstn" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 121 "rev" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 113 "rev'" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 111 "rev_alt" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 114 "rev_append" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 112 "rev_append_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 109 "rev_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 118 "rev_involutive" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 116 "rev_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 110 "rev_list_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 115 "rev_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 119 "rev_unit" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 13 "seq" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 12 "seq_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 11 "seq_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 10 "seq_shift" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 172 "size" [body=no, kind=cnst, prop=no, path="Test", ]; -N: 171 "size_nil" [body=no, kind=cnst, prop=yes, path="Test", ]; -N: 18 "skipn" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 52 "split" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 45 "split_combine" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 48 "split_length_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 47 "split_length_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 49 "split_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 174 "tail" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 8 "NoDup" [kind=inductive, prop=no, path="Test.ReDun", ]; -N: 108 "Permutation" [kind=inductive, prop=no, path="Test", ]; -N: 183 "list" [kind=inductive, prop=no, path="Test", ]; -N: 7 "NoDup_nil" [kind=construct, prop=yes, path="Test.ReDun", ]; -N: 107 "perm_nil" [kind=construct, prop=yes, path="Test", ]; -N: 182 "nil" [kind=construct, prop=no, path="Test", ]; -N: 6 "NoDup_cons" [kind=construct, prop=yes, path="Test.ReDun", ]; -N: 106 "perm_skip" [kind=construct, prop=yes, path="Test", ]; -N: 181 "cons" [kind=construct, prop=no, path="Test", ]; -N: 105 "perm_swap" [kind=construct, prop=yes, path="Test", ]; -N: 104 "perm_trans" [kind=construct, prop=yes, path="Test", ]; -E: 1 2 [weight=1, ]; -E: 1 3 [weight=1, ]; -E: 1 8 [weight=26, ]; -E: 1 9 [weight=392, ]; -E: 1 91 [weight=1, ]; +E: 100 101 [weight=1, ]; +E: 100 108 [weight=3, ]; +E: 100 168 [weight=1, ]; +E: 100 181 [weight=5, ]; +E: 100 182 [weight=4, ]; +E: 100 183 [weight=4, ]; +E: 101 103 [weight=1, ]; +E: 101 108 [weight=5, ]; +E: 101 168 [weight=2, ]; +E: 101 181 [weight=10, ]; +E: 101 182 [weight=23, ]; +E: 101 183 [weight=30, ]; +E: 10 13 [weight=14, ]; +E: 10 181 [weight=3, ]; +E: 10 182 [weight=1, ]; +E: 10 183 [weight=10, ]; +E: 102 108 [weight=14, ]; +E: 102 181 [weight=12, ]; +E: 102 182 [weight=4, ]; +E: 102 183 [weight=30, ]; +E: 103 108 [weight=14, ]; +E: 103 181 [weight=12, ]; +E: 103 182 [weight=4, ]; +E: 103 183 [weight=30, ]; +E: 104 181 [weight=6, ]; +E: 104 182 [weight=2, ]; +E: 104 183 [weight=6, ]; +E: 105 181 [weight=6, ]; +E: 105 182 [weight=2, ]; +E: 105 183 [weight=6, ]; +E: 106 181 [weight=6, ]; +E: 106 182 [weight=2, ]; +E: 106 183 [weight=6, ]; +E: 107 181 [weight=6, ]; +E: 107 182 [weight=2, ]; +E: 107 183 [weight=6, ]; +E: 108 181 [weight=6, ]; +E: 108 182 [weight=2, ]; +E: 108 183 [weight=6, ]; +E: 10 81 [weight=6, ]; +E: 109 110 [weight=1, ]; +E: 109 118 [weight=1, ]; +E: 109 121 [weight=9, ]; +E: 109 169 [weight=2, ]; +E: 109 181 [weight=3, ]; +E: 109 182 [weight=4, ]; +E: 109 183 [weight=11, ]; +E: 110 121 [weight=7, ]; +E: 110 179 [weight=1, ]; +E: 110 181 [weight=2, ]; +E: 110 182 [weight=2, ]; +E: 110 183 [weight=8, ]; E: 1 107 [weight=1, ]; E: 1 108 [weight=16, ]; -E: 1 148 [weight=2, ]; -E: 1 149 [weight=2, ]; -E: 1 161 [weight=1, ]; -E: 1 169 [weight=37, ]; -E: 1 170 [weight=125, ]; -E: 1 179 [weight=1, ]; -E: 1 181 [weight=78, ]; -E: 1 182 [weight=20, ]; -E: 1 183 [weight=65, ]; -E: 2 8 [weight=21, ]; -E: 2 9 [weight=272, ]; -E: 2 148 [weight=1, ]; -E: 2 169 [weight=43, ]; -E: 2 170 [weight=33, ]; -E: 2 179 [weight=1, ]; -E: 2 181 [weight=66, ]; -E: 2 182 [weight=8, ]; -E: 2 183 [weight=80, ]; -E: 3 6 [weight=1, ]; -E: 3 8 [weight=34, ]; -E: 3 9 [weight=244, ]; -E: 3 148 [weight=1, ]; -E: 3 149 [weight=1, ]; -E: 3 169 [weight=37, ]; -E: 3 170 [weight=27, ]; -E: 3 179 [weight=1, ]; -E: 3 181 [weight=67, ]; -E: 3 182 [weight=8, ]; -E: 3 183 [weight=75, ]; -E: 4 8 [weight=8, ]; -E: 4 9 [weight=19, ]; -E: 4 170 [weight=3, ]; -E: 4 181 [weight=2, ]; -E: 4 182 [weight=2, ]; -E: 4 183 [weight=9, ]; -E: 5 8 [weight=8, ]; -E: 5 9 [weight=19, ]; -E: 5 170 [weight=3, ]; -E: 5 181 [weight=2, ]; -E: 5 182 [weight=2, ]; -E: 5 183 [weight=9, ]; -E: 6 9 [weight=5, ]; -E: 6 170 [weight=1, ]; -E: 6 181 [weight=1, ]; -E: 6 182 [weight=1, ]; -E: 6 183 [weight=1, ]; -E: 7 9 [weight=5, ]; -E: 7 170 [weight=1, ]; -E: 7 181 [weight=1, ]; -E: 7 182 [weight=1, ]; -E: 7 183 [weight=1, ]; -E: 8 9 [weight=5, ]; -E: 8 170 [weight=1, ]; -E: 8 181 [weight=1, ]; -E: 8 182 [weight=1, ]; -E: 8 183 [weight=1, ]; -E: 10 13 [weight=14, ]; -E: 10 81 [weight=6, ]; -E: 10 181 [weight=3, ]; -E: 10 182 [weight=1, ]; -E: 10 183 [weight=10, ]; +E: 111 112 [weight=1, ]; +E: 111 114 [weight=2, ]; +E: 111 121 [weight=4, ]; +E: 111 157 [weight=1, ]; +E: 111 169 [weight=1, ]; +E: 111 182 [weight=4, ]; +E: 111 183 [weight=6, ]; E: 11 13 [weight=12, ]; E: 11 145 [weight=12, ]; E: 11 181 [weight=3, ]; +E: 112 114 [weight=7, ]; +E: 112 121 [weight=9, ]; +E: 112 155 [weight=1, ]; +E: 112 169 [weight=10, ]; +E: 112 179 [weight=1, ]; +E: 112 181 [weight=9, ]; +E: 112 182 [weight=5, ]; +E: 112 183 [weight=21, ]; +E: 113 114 [weight=1, ]; +E: 113 182 [weight=1, ]; +E: 113 183 [weight=3, ]; +E: 114 181 [weight=1, ]; +E: 114 183 [weight=12, ]; +E: 1 148 [weight=2, ]; +E: 1 149 [weight=2, ]; +E: 115 116 [weight=2, ]; +E: 115 121 [weight=36, ]; +E: 115 135 [weight=1, ]; +E: 115 136 [weight=1, ]; +E: 115 145 [weight=43, ]; +E: 115 169 [weight=10, ]; +E: 115 173 [weight=78, ]; +E: 115 179 [weight=1, ]; +E: 115 181 [weight=30, ]; +E: 115 182 [weight=37, ]; +E: 115 183 [weight=4, ]; +E: 116 121 [weight=9, ]; +E: 116 150 [weight=1, ]; +E: 116 169 [weight=1, ]; +E: 116 173 [weight=22, ]; +E: 116 179 [weight=1, ]; +E: 116 181 [weight=7, ]; +E: 116 182 [weight=7, ]; +E: 116 183 [weight=4, ]; +E: 1 161 [weight=1, ]; +E: 1 169 [weight=37, ]; +E: 1 170 [weight=125, ]; +E: 117 121 [weight=30, ]; +E: 117 148 [weight=2, ]; +E: 117 149 [weight=1, ]; +E: 117 169 [weight=5, ]; +E: 117 170 [weight=62, ]; +E: 117 179 [weight=1, ]; +E: 117 181 [weight=16, ]; +E: 117 182 [weight=18, ]; +E: 117 183 [weight=4, ]; +E: 1 179 [weight=1, ]; +E: 118 119 [weight=1, ]; +E: 118 121 [weight=17, ]; +E: 118 169 [weight=1, ]; +E: 118 179 [weight=1, ]; +E: 118 181 [weight=8, ]; +E: 118 182 [weight=4, ]; +E: 118 183 [weight=17, ]; +E: 1 181 [weight=78, ]; +E: 1 182 [weight=20, ]; +E: 1 183 [weight=65, ]; +E: 119 120 [weight=1, ]; +E: 119 121 [weight=2, ]; +E: 119 169 [weight=1, ]; +E: 119 181 [weight=3, ]; +E: 119 182 [weight=2, ]; +E: 119 183 [weight=3, ]; +E: 120 121 [weight=29, ]; +E: 120 156 [weight=1, ]; +E: 120 157 [weight=1, ]; +E: 120 169 [weight=20, ]; +E: 120 179 [weight=1, ]; +E: 120 181 [weight=8, ]; +E: 120 182 [weight=13, ]; +E: 120 183 [weight=23, ]; +E: 121 169 [weight=1, ]; +E: 121 181 [weight=1, ]; +E: 121 182 [weight=2, ]; +E: 121 183 [weight=9, ]; E: 12 13 [weight=6, ]; E: 12 173 [weight=6, ]; +E: 122 127 [weight=10, ]; +E: 122 181 [weight=2, ]; +E: 122 183 [weight=2, ]; +E: 123 127 [weight=10, ]; +E: 123 181 [weight=2, ]; +E: 123 183 [weight=2, ]; +E: 124 127 [weight=2, ]; +E: 124 182 [weight=2, ]; +E: 125 127 [weight=19, ]; +E: 125 179 [weight=1, ]; +E: 125 181 [weight=3, ]; +E: 125 182 [weight=11, ]; +E: 125 183 [weight=14, ]; +E: 126 127 [weight=29, ]; +E: 126 170 [weight=27, ]; +E: 126 179 [weight=1, ]; +E: 126 181 [weight=2, ]; +E: 126 182 [weight=2, ]; +E: 126 183 [weight=4, ]; +E: 127 183 [weight=6, ]; +E: 128 131 [weight=38, ]; +E: 128 169 [weight=35, ]; +E: 128 179 [weight=1, ]; +E: 128 181 [weight=26, ]; +E: 128 182 [weight=30, ]; +E: 128 183 [weight=77, ]; +E: 129 169 [weight=25, ]; +E: 129 180 [weight=1, ]; +E: 129 181 [weight=50, ]; +E: 129 182 [weight=46, ]; +E: 129 183 [weight=78, ]; +E: 1 2 [weight=1, ]; +E: 130 131 [weight=13, ]; +E: 130 132 [weight=13, ]; +E: 130 169 [weight=13, ]; +E: 130 179 [weight=1, ]; +E: 130 181 [weight=44, ]; +E: 130 182 [weight=35, ]; +E: 130 183 [weight=37, ]; +E: 131 181 [weight=1, ]; +E: 131 182 [weight=2, ]; +E: 131 183 [weight=13, ]; E: 13 181 [weight=1, ]; E: 13 182 [weight=1, ]; E: 13 183 [weight=3, ]; -E: 14 19 [weight=30, ]; +E: 132 183 [weight=9, ]; +E: 133 134 [weight=12, ]; +E: 133 170 [weight=11, ]; +E: 133 179 [weight=1, ]; +E: 133 181 [weight=4, ]; +E: 133 182 [weight=2, ]; +E: 133 183 [weight=5, ]; +E: 134 181 [weight=1, ]; +E: 134 182 [weight=1, ]; +E: 134 183 [weight=10, ]; +E: 135 145 [weight=26, ]; +E: 135 169 [weight=8, ]; +E: 135 173 [weight=30, ]; +E: 135 179 [weight=1, ]; +E: 135 181 [weight=9, ]; +E: 135 182 [weight=6, ]; +E: 135 183 [weight=9, ]; +E: 136 145 [weight=24, ]; +E: 136 169 [weight=11, ]; +E: 136 173 [weight=24, ]; +E: 136 179 [weight=1, ]; +E: 136 181 [weight=9, ]; +E: 136 182 [weight=19, ]; +E: 136 183 [weight=9, ]; +E: 137 145 [weight=14, ]; +E: 137 173 [weight=13, ]; +E: 137 179 [weight=1, ]; +E: 137 181 [weight=3, ]; +E: 137 182 [weight=3, ]; +E: 137 183 [weight=4, ]; +E: 138 145 [weight=9, ]; +E: 138 173 [weight=18, ]; +E: 138 179 [weight=1, ]; +E: 138 181 [weight=6, ]; +E: 138 182 [weight=6, ]; +E: 138 183 [weight=4, ]; +E: 139 145 [weight=14, ]; +E: 139 170 [weight=14, ]; +E: 139 173 [weight=19, ]; +E: 139 181 [weight=6, ]; +E: 139 182 [weight=6, ]; +E: 139 183 [weight=14, ]; +E: 1 3 [weight=1, ]; +E: 140 141 [weight=1, ]; +E: 140 183 [weight=2, ]; +E: 141 183 [weight=9, ]; E: 14 128 [weight=1, ]; E: 14 131 [weight=17, ]; E: 14 169 [weight=3, ]; @@ -265,91 +237,246 @@ E: 14 173 [weight=26, ]; E: 14 181 [weight=17, ]; E: 14 182 [weight=27, ]; E: 14 183 [weight=42, ]; -E: 15 19 [weight=30, ]; -E: 15 128 [weight=1, ]; -E: 15 131 [weight=11, ]; -E: 15 169 [weight=3, ]; -E: 15 173 [weight=18, ]; -E: 15 181 [weight=16, ]; -E: 15 182 [weight=37, ]; -E: 15 183 [weight=50, ]; -E: 16 19 [weight=10, ]; -E: 16 173 [weight=20, ]; -E: 16 181 [weight=4, ]; -E: 16 182 [weight=4, ]; -E: 16 183 [weight=11, ]; -E: 17 18 [weight=13, ]; -E: 17 19 [weight=13, ]; -E: 17 169 [weight=13, ]; -E: 17 181 [weight=10, ]; -E: 17 182 [weight=4, ]; -E: 17 183 [weight=30, ]; -E: 18 182 [weight=1, ]; -E: 18 183 [weight=10, ]; -E: 19 181 [weight=1, ]; -E: 19 182 [weight=2, ]; -E: 19 183 [weight=10, ]; -E: 20 27 [weight=6, ]; -E: 20 149 [weight=1, ]; -E: 20 169 [weight=4, ]; -E: 20 170 [weight=16, ]; -E: 20 183 [weight=12, ]; -E: 21 27 [weight=4, ]; -E: 21 170 [weight=18, ]; -E: 21 181 [weight=3, ]; -E: 21 183 [weight=8, ]; -E: 22 27 [weight=4, ]; -E: 22 148 [weight=1, ]; -E: 22 169 [weight=2, ]; -E: 22 170 [weight=3, ]; -E: 22 183 [weight=6, ]; -E: 23 27 [weight=4, ]; -E: 23 148 [weight=1, ]; +E: 14 19 [weight=30, ]; +E: 142 145 [weight=7, ]; +E: 142 170 [weight=6, ]; +E: 142 181 [weight=4, ]; +E: 142 183 [weight=3, ]; +E: 143 145 [weight=32, ]; +E: 143 170 [weight=16, ]; +E: 143 178 [weight=1, ]; +E: 143 181 [weight=9, ]; +E: 143 182 [weight=4, ]; +E: 143 183 [weight=4, ]; +E: 144 183 [weight=9, ]; +E: 145 183 [weight=9, ]; +E: 146 150 [weight=2, ]; +E: 146 169 [weight=36, ]; +E: 146 173 [weight=46, ]; +E: 146 179 [weight=1, ]; +E: 146 181 [weight=38, ]; +E: 146 182 [weight=13, ]; +E: 146 183 [weight=105, ]; +E: 147 169 [weight=18, ]; +E: 147 179 [weight=1, ]; +E: 147 181 [weight=7, ]; +E: 147 182 [weight=2, ]; +E: 147 183 [weight=48, ]; +E: 148 169 [weight=11, ]; +E: 148 170 [weight=40, ]; +E: 148 179 [weight=1, ]; +E: 148 181 [weight=2, ]; +E: 148 182 [weight=2, ]; +E: 148 183 [weight=7, ]; +E: 149 169 [weight=9, ]; +E: 149 170 [weight=39, ]; +E: 149 179 [weight=1, ]; +E: 149 181 [weight=2, ]; +E: 149 182 [weight=2, ]; +E: 149 183 [weight=7, ]; +E: 150 169 [weight=6, ]; +E: 150 173 [weight=19, ]; +E: 150 179 [weight=1, ]; +E: 150 181 [weight=2, ]; +E: 150 182 [weight=2, ]; +E: 150 183 [weight=11, ]; +E: 151 158 [weight=2, ]; +E: 151 169 [weight=41, ]; +E: 151 179 [weight=1, ]; +E: 151 181 [weight=88, ]; +E: 151 182 [weight=78, ]; +E: 151 183 [weight=119, ]; +E: 15 128 [weight=1, ]; +E: 15 131 [weight=11, ]; +E: 15 169 [weight=3, ]; +E: 15 173 [weight=18, ]; +E: 15 181 [weight=16, ]; +E: 15 182 [weight=37, ]; +E: 15 183 [weight=50, ]; +E: 15 19 [weight=30, ]; +E: 152 157 [weight=1, ]; +E: 152 158 [weight=1, ]; +E: 152 169 [weight=19, ]; +E: 152 181 [weight=87, ]; +E: 152 182 [weight=107, ]; +E: 152 183 [weight=118, ]; +E: 153 169 [weight=12, ]; +E: 153 181 [weight=21, ]; +E: 153 182 [weight=56, ]; +E: 153 183 [weight=62, ]; +E: 154 169 [weight=3, ]; +E: 154 181 [weight=3, ]; +E: 154 183 [weight=6, ]; +E: 155 156 [weight=1, ]; +E: 155 169 [weight=8, ]; +E: 155 183 [weight=8, ]; +E: 156 169 [weight=29, ]; +E: 156 179 [weight=1, ]; +E: 156 181 [weight=5, ]; +E: 156 182 [weight=2, ]; +E: 156 183 [weight=18, ]; +E: 157 169 [weight=6, ]; +E: 157 179 [weight=1, ]; +E: 157 181 [weight=5, ]; +E: 157 182 [weight=9, ]; +E: 157 183 [weight=14, ]; +E: 158 169 [weight=7, ]; +E: 158 181 [weight=12, ]; +E: 158 182 [weight=10, ]; +E: 158 183 [weight=30, ]; +E: 159 162 [weight=1, ]; +E: 159 170 [weight=36, ]; +E: 159 178 [weight=1, ]; +E: 159 181 [weight=6, ]; +E: 159 182 [weight=2, ]; +E: 159 183 [weight=4, ]; +E: 160 170 [weight=10, ]; +E: 160 181 [weight=2, ]; +E: 160 183 [weight=2, ]; +E: 161 169 [weight=25, ]; +E: 161 170 [weight=8, ]; +E: 161 179 [weight=1, ]; +E: 161 181 [weight=46, ]; +E: 161 182 [weight=6, ]; +E: 161 183 [weight=103, ]; +E: 16 173 [weight=20, ]; +E: 16 181 [weight=4, ]; +E: 16 182 [weight=4, ]; +E: 16 183 [weight=11, ]; +E: 16 19 [weight=10, ]; +E: 162 170 [weight=3, ]; +E: 162 182 [weight=3, ]; +E: 163 170 [weight=6, ]; +E: 163 181 [weight=2, ]; +E: 163 183 [weight=3, ]; +E: 164 170 [weight=3, ]; +E: 164 181 [weight=2, ]; +E: 164 183 [weight=3, ]; +E: 165 176 [weight=2, ]; +E: 165 181 [weight=2, ]; +E: 165 183 [weight=2, ]; +E: 166 176 [weight=2, ]; +E: 166 182 [weight=2, ]; +E: 167 180 [weight=1, ]; +E: 167 181 [weight=12, ]; +E: 167 182 [weight=8, ]; +E: 167 183 [weight=32, ]; +E: 168 181 [weight=4, ]; +E: 168 182 [weight=4, ]; +E: 168 183 [weight=10, ]; +E: 169 181 [weight=1, ]; +E: 169 183 [weight=12, ]; +E: 170 183 [weight=6, ]; +E: 171 172 [weight=1, ]; +E: 171 182 [weight=1, ]; +E: 17 169 [weight=13, ]; +E: 17 181 [weight=10, ]; +E: 17 182 [weight=4, ]; +E: 17 183 [weight=30, ]; +E: 17 18 [weight=13, ]; +E: 17 19 [weight=13, ]; +E: 172 183 [weight=1, ]; +E: 173 183 [weight=6, ]; +E: 174 182 [weight=1, ]; +E: 174 183 [weight=7, ]; +E: 175 183 [weight=5, ]; +E: 176 183 [weight=5, ]; +E: 177 181 [weight=2, ]; +E: 177 182 [weight=2, ]; +E: 177 183 [weight=10, ]; +E: 178 180 [weight=1, ]; +E: 178 181 [weight=1, ]; +E: 178 182 [weight=1, ]; +E: 178 183 [weight=4, ]; +E: 179 181 [weight=2, ]; +E: 179 182 [weight=2, ]; +E: 179 183 [weight=10, ]; +E: 180 181 [weight=2, ]; +E: 180 182 [weight=2, ]; +E: 180 183 [weight=10, ]; +E: 18 182 [weight=1, ]; +E: 18 183 [weight=10, ]; +E: 1 8 [weight=26, ]; +E: 19 181 [weight=1, ]; +E: 19 182 [weight=2, ]; +E: 19 183 [weight=10, ]; +E: 1 91 [weight=1, ]; +E: 1 9 [weight=392, ]; +E: 20 149 [weight=1, ]; +E: 20 169 [weight=4, ]; +E: 20 170 [weight=16, ]; +E: 20 183 [weight=12, ]; +E: 20 27 [weight=6, ]; +E: 21 170 [weight=18, ]; +E: 21 181 [weight=3, ]; +E: 21 183 [weight=8, ]; +E: 21 27 [weight=4, ]; +E: 2 148 [weight=1, ]; +E: 2 169 [weight=43, ]; +E: 2 170 [weight=33, ]; +E: 2 179 [weight=1, ]; +E: 2 181 [weight=66, ]; +E: 2 182 [weight=8, ]; +E: 2 183 [weight=80, ]; +E: 22 148 [weight=1, ]; +E: 22 169 [weight=2, ]; +E: 22 170 [weight=3, ]; +E: 22 183 [weight=6, ]; +E: 22 27 [weight=4, ]; +E: 23 148 [weight=1, ]; E: 23 169 [weight=2, ]; E: 23 170 [weight=3, ]; E: 23 183 [weight=6, ]; -E: 24 27 [weight=6, ]; +E: 23 27 [weight=4, ]; E: 24 170 [weight=1, ]; E: 24 183 [weight=6, ]; -E: 25 27 [weight=4, ]; +E: 24 27 [weight=6, ]; E: 25 163 [weight=1, ]; E: 25 170 [weight=1, ]; E: 25 181 [weight=2, ]; E: 25 183 [weight=4, ]; -E: 26 27 [weight=2, ]; +E: 25 27 [weight=4, ]; E: 26 170 [weight=1, ]; E: 26 183 [weight=2, ]; +E: 26 27 [weight=2, ]; E: 27 170 [weight=2, ]; E: 27 183 [weight=4, ]; -E: 28 34 [weight=5, ]; E: 28 173 [weight=1, ]; E: 28 179 [weight=1, ]; E: 28 181 [weight=2, ]; E: 28 182 [weight=11, ]; E: 28 183 [weight=9, ]; -E: 29 34 [weight=4, ]; +E: 28 34 [weight=5, ]; +E: 2 8 [weight=21, ]; E: 29 173 [weight=8, ]; E: 29 181 [weight=6, ]; E: 29 183 [weight=4, ]; -E: 30 34 [weight=4, ]; +E: 29 34 [weight=4, ]; +E: 2 9 [weight=272, ]; E: 30 173 [weight=8, ]; E: 30 181 [weight=3, ]; E: 30 183 [weight=4, ]; -E: 31 34 [weight=4, ]; +E: 30 34 [weight=4, ]; E: 31 173 [weight=14, ]; E: 31 181 [weight=6, ]; E: 31 183 [weight=4, ]; -E: 32 34 [weight=6, ]; +E: 31 34 [weight=4, ]; +E: 3 148 [weight=1, ]; +E: 3 149 [weight=1, ]; +E: 3 169 [weight=37, ]; +E: 3 170 [weight=27, ]; +E: 3 179 [weight=1, ]; +E: 3 181 [weight=67, ]; +E: 3 182 [weight=8, ]; +E: 3 183 [weight=75, ]; E: 32 173 [weight=7, ]; E: 32 183 [weight=6, ]; -E: 33 34 [weight=2, ]; +E: 32 34 [weight=6, ]; E: 33 173 [weight=1, ]; E: 33 183 [weight=2, ]; +E: 33 34 [weight=2, ]; E: 34 173 [weight=2, ]; E: 34 183 [weight=4, ]; -E: 35 39 [weight=10, ]; -E: 35 78 [weight=1, ]; -E: 35 81 [weight=4, ]; E: 35 150 [weight=1, ]; E: 35 169 [weight=1, ]; E: 35 173 [weight=31, ]; @@ -357,10 +484,9 @@ E: 35 179 [weight=1, ]; E: 35 181 [weight=2, ]; E: 35 182 [weight=2, ]; E: 35 183 [weight=11, ]; -E: 36 37 [weight=1, ]; -E: 36 39 [weight=12, ]; -E: 36 79 [weight=1, ]; -E: 36 81 [weight=10, ]; +E: 35 39 [weight=10, ]; +E: 35 78 [weight=1, ]; +E: 35 81 [weight=4, ]; E: 36 149 [weight=1, ]; E: 36 169 [weight=1, ]; E: 36 170 [weight=85, ]; @@ -368,96 +494,113 @@ E: 36 179 [weight=1, ]; E: 36 181 [weight=2, ]; E: 36 182 [weight=2, ]; E: 36 183 [weight=6, ]; -E: 37 38 [weight=1, ]; -E: 37 39 [weight=9, ]; -E: 37 81 [weight=5, ]; +E: 36 37 [weight=1, ]; +E: 36 39 [weight=12, ]; +E: 36 79 [weight=1, ]; +E: 36 81 [weight=10, ]; +E: 3 6 [weight=1, ]; E: 37 148 [weight=1, ]; E: 37 170 [weight=27, ]; E: 37 179 [weight=1, ]; E: 37 181 [weight=2, ]; E: 37 182 [weight=2, ]; E: 37 183 [weight=11, ]; -E: 38 81 [weight=8, ]; +E: 37 38 [weight=1, ]; +E: 37 39 [weight=9, ]; +E: 37 81 [weight=5, ]; E: 38 170 [weight=16, ]; E: 38 179 [weight=1, ]; E: 38 181 [weight=2, ]; E: 38 182 [weight=2, ]; E: 38 183 [weight=4, ]; -E: 39 81 [weight=1, ]; +E: 38 81 [weight=8, ]; +E: 3 8 [weight=34, ]; E: 39 169 [weight=1, ]; E: 39 182 [weight=1, ]; E: 39 183 [weight=12, ]; -E: 40 46 [weight=13, ]; +E: 39 81 [weight=1, ]; +E: 3 9 [weight=244, ]; E: 40 145 [weight=39, ]; E: 40 173 [weight=24, ]; E: 40 179 [weight=1, ]; E: 40 181 [weight=25, ]; E: 40 182 [weight=25, ]; E: 40 183 [weight=15, ]; -E: 41 46 [weight=8, ]; +E: 40 46 [weight=13, ]; E: 41 173 [weight=24, ]; E: 41 179 [weight=1, ]; E: 41 181 [weight=8, ]; E: 41 182 [weight=4, ]; E: 41 183 [weight=13, ]; -E: 42 46 [weight=10, ]; +E: 41 46 [weight=8, ]; +E: 4 170 [weight=3, ]; +E: 4 181 [weight=2, ]; +E: 4 182 [weight=2, ]; +E: 4 183 [weight=9, ]; E: 42 170 [weight=21, ]; E: 42 179 [weight=1, ]; E: 42 181 [weight=5, ]; E: 42 182 [weight=3, ]; E: 42 183 [weight=13, ]; -E: 43 46 [weight=10, ]; +E: 42 46 [weight=10, ]; E: 43 170 [weight=21, ]; E: 43 179 [weight=1, ]; E: 43 181 [weight=7, ]; E: 43 182 [weight=3, ]; E: 43 183 [weight=13, ]; -E: 44 46 [weight=10, ]; -E: 44 52 [weight=10, ]; +E: 43 46 [weight=10, ]; E: 44 173 [weight=30, ]; E: 44 179 [weight=1, ]; E: 44 181 [weight=23, ]; E: 44 182 [weight=23, ]; E: 44 183 [weight=94, ]; -E: 45 46 [weight=16, ]; -E: 45 52 [weight=7, ]; +E: 44 46 [weight=10, ]; +E: 44 52 [weight=10, ]; E: 45 179 [weight=1, ]; E: 45 181 [weight=17, ]; E: 45 182 [weight=3, ]; E: 45 183 [weight=73, ]; +E: 45 46 [weight=16, ]; +E: 45 52 [weight=7, ]; E: 46 181 [weight=1, ]; E: 46 182 [weight=2, ]; E: 46 183 [weight=16, ]; -E: 47 52 [weight=7, ]; E: 47 173 [weight=22, ]; E: 47 179 [weight=1, ]; E: 47 181 [weight=8, ]; E: 47 182 [weight=2, ]; E: 47 183 [weight=52, ]; -E: 48 52 [weight=7, ]; +E: 47 52 [weight=7, ]; E: 48 173 [weight=22, ]; E: 48 179 [weight=1, ]; E: 48 181 [weight=8, ]; E: 48 182 [weight=2, ]; E: 48 183 [weight=52, ]; -E: 49 52 [weight=32, ]; +E: 48 52 [weight=7, ]; +E: 4 8 [weight=8, ]; E: 49 145 [weight=66, ]; E: 49 179 [weight=1, ]; E: 49 181 [weight=39, ]; E: 49 182 [weight=15, ]; E: 49 183 [weight=196, ]; -E: 50 52 [weight=8, ]; +E: 49 52 [weight=32, ]; +E: 4 9 [weight=19, ]; E: 50 170 [weight=28, ]; E: 50 179 [weight=1, ]; E: 50 181 [weight=10, ]; E: 50 182 [weight=2, ]; E: 50 183 [weight=64, ]; -E: 51 52 [weight=8, ]; +E: 50 52 [weight=8, ]; E: 51 170 [weight=28, ]; E: 51 179 [weight=1, ]; E: 51 181 [weight=10, ]; E: 51 182 [weight=2, ]; E: 51 183 [weight=64, ]; +E: 51 52 [weight=8, ]; +E: 5 170 [weight=3, ]; +E: 5 181 [weight=2, ]; +E: 5 182 [weight=2, ]; +E: 5 183 [weight=9, ]; E: 52 181 [weight=2, ]; E: 52 182 [weight=2, ]; E: 52 183 [weight=24, ]; @@ -465,87 +608,97 @@ E: 53 181 [weight=2, ]; E: 53 182 [weight=2, ]; E: 53 183 [weight=26, ]; E: 54 183 [weight=6, ]; -E: 55 56 [weight=49, ]; E: 55 170 [weight=107, ]; E: 55 179 [weight=1, ]; E: 55 181 [weight=5, ]; E: 55 182 [weight=2, ]; E: 55 183 [weight=6, ]; +E: 55 56 [weight=49, ]; E: 56 181 [weight=1, ]; E: 56 182 [weight=1, ]; E: 56 183 [weight=10, ]; -E: 57 58 [weight=25, ]; E: 57 170 [weight=19, ]; E: 57 179 [weight=1, ]; E: 57 181 [weight=2, ]; E: 57 182 [weight=2, ]; E: 57 183 [weight=4, ]; +E: 57 58 [weight=25, ]; E: 58 183 [weight=6, ]; -E: 59 61 [weight=13, ]; +E: 5 8 [weight=8, ]; E: 59 145 [weight=11, ]; E: 59 173 [weight=24, ]; E: 59 179 [weight=1, ]; E: 59 181 [weight=3, ]; E: 59 182 [weight=19, ]; E: 59 183 [weight=4, ]; -E: 60 61 [weight=37, ]; +E: 59 61 [weight=13, ]; +E: 5 9 [weight=19, ]; E: 60 170 [weight=55, ]; E: 60 179 [weight=1, ]; E: 60 181 [weight=2, ]; E: 60 182 [weight=2, ]; E: 60 183 [weight=4, ]; +E: 60 61 [weight=37, ]; E: 61 183 [weight=6, ]; -E: 62 73 [weight=1, ]; -E: 62 81 [weight=1, ]; +E: 6 170 [weight=1, ]; +E: 6 181 [weight=1, ]; +E: 6 182 [weight=1, ]; +E: 6 183 [weight=1, ]; E: 62 181 [weight=2, ]; E: 62 182 [weight=2, ]; E: 62 183 [weight=21, ]; -E: 63 66 [weight=18, ]; -E: 63 69 [weight=13, ]; +E: 62 73 [weight=1, ]; +E: 62 81 [weight=1, ]; E: 63 179 [weight=1, ]; E: 63 181 [weight=4, ]; E: 63 182 [weight=3, ]; E: 63 183 [weight=7, ]; -E: 64 65 [weight=1, ]; -E: 64 66 [weight=10, ]; -E: 64 69 [weight=7, ]; +E: 63 66 [weight=18, ]; +E: 63 69 [weight=13, ]; E: 64 121 [weight=9, ]; E: 64 169 [weight=1, ]; E: 64 179 [weight=1, ]; E: 64 181 [weight=6, ]; E: 64 182 [weight=6, ]; E: 64 183 [weight=4, ]; -E: 65 66 [weight=30, ]; +E: 64 65 [weight=1, ]; +E: 64 66 [weight=10, ]; +E: 64 69 [weight=7, ]; E: 65 169 [weight=11, ]; E: 65 179 [weight=1, ]; E: 65 181 [weight=2, ]; E: 65 182 [weight=2, ]; E: 65 183 [weight=11, ]; +E: 65 66 [weight=30, ]; E: 66 183 [weight=6, ]; -E: 67 69 [weight=8, ]; E: 67 173 [weight=12, ]; E: 67 179 [weight=1, ]; E: 67 181 [weight=2, ]; E: 67 182 [weight=2, ]; E: 67 183 [weight=7, ]; -E: 68 69 [weight=16, ]; +E: 67 69 [weight=8, ]; E: 68 169 [weight=5, ]; E: 68 179 [weight=1, ]; E: 68 181 [weight=2, ]; E: 68 182 [weight=2, ]; E: 68 183 [weight=10, ]; +E: 68 69 [weight=16, ]; E: 69 183 [weight=6, ]; -E: 70 81 [weight=16, ]; +E: 6 9 [weight=5, ]; E: 70 179 [weight=1, ]; E: 70 181 [weight=7, ]; E: 70 182 [weight=3, ]; E: 70 183 [weight=15, ]; -E: 71 81 [weight=20, ]; +E: 70 81 [weight=16, ]; E: 71 179 [weight=1, ]; E: 71 181 [weight=5, ]; E: 71 182 [weight=3, ]; E: 71 183 [weight=14, ]; -E: 72 73 [weight=30, ]; +E: 7 170 [weight=1, ]; +E: 7 181 [weight=1, ]; +E: 71 81 [weight=20, ]; +E: 7 182 [weight=1, ]; +E: 7 183 [weight=1, ]; E: 72 148 [weight=1, ]; E: 72 149 [weight=1, ]; E: 72 169 [weight=3, ]; @@ -554,10 +707,10 @@ E: 72 179 [weight=1, ]; E: 72 181 [weight=2, ]; E: 72 182 [weight=2, ]; E: 72 183 [weight=6, ]; +E: 72 73 [weight=30, ]; E: 73 169 [weight=1, ]; E: 73 182 [weight=1, ]; E: 73 183 [weight=12, ]; -E: 74 81 [weight=24, ]; E: 74 103 [weight=1, ]; E: 74 104 [weight=1, ]; E: 74 105 [weight=1, ]; @@ -567,53 +720,58 @@ E: 74 108 [weight=14, ]; E: 74 181 [weight=6, ]; E: 74 182 [weight=2, ]; E: 74 183 [weight=12, ]; -E: 75 76 [weight=1, ]; -E: 75 81 [weight=19, ]; +E: 74 81 [weight=24, ]; E: 75 121 [weight=18, ]; E: 75 169 [weight=6, ]; E: 75 179 [weight=1, ]; E: 75 181 [weight=9, ]; E: 75 182 [weight=10, ]; E: 75 183 [weight=17, ]; -E: 76 81 [weight=23, ]; +E: 75 76 [weight=1, ]; +E: 75 81 [weight=19, ]; E: 76 169 [weight=14, ]; E: 76 179 [weight=1, ]; E: 76 181 [weight=5, ]; E: 76 182 [weight=2, ]; E: 76 183 [weight=21, ]; -E: 77 81 [weight=8, ]; +E: 76 81 [weight=23, ]; E: 77 145 [weight=21, ]; E: 77 179 [weight=1, ]; E: 77 181 [weight=5, ]; E: 77 182 [weight=6, ]; E: 77 183 [weight=4, ]; -E: 78 81 [weight=6, ]; +E: 77 81 [weight=8, ]; E: 78 173 [weight=12, ]; E: 78 179 [weight=1, ]; E: 78 181 [weight=2, ]; E: 78 182 [weight=2, ]; E: 78 183 [weight=4, ]; -E: 79 81 [weight=50, ]; +E: 78 81 [weight=6, ]; E: 79 170 [weight=125, ]; E: 79 179 [weight=1, ]; E: 79 181 [weight=21, ]; E: 79 182 [weight=13, ]; E: 79 183 [weight=4, ]; -E: 80 81 [weight=8, ]; +E: 79 81 [weight=50, ]; +E: 7 9 [weight=5, ]; E: 80 170 [weight=16, ]; E: 80 179 [weight=1, ]; E: 80 181 [weight=2, ]; E: 80 182 [weight=2, ]; E: 80 183 [weight=4, ]; +E: 80 81 [weight=8, ]; E: 81 181 [weight=1, ]; E: 81 182 [weight=1, ]; E: 81 183 [weight=9, ]; +E: 8 170 [weight=1, ]; +E: 8 181 [weight=1, ]; +E: 8 182 [weight=1, ]; +E: 8 183 [weight=1, ]; E: 82 168 [weight=2, ]; E: 82 180 [weight=1, ]; E: 82 181 [weight=70, ]; E: 82 182 [weight=14, ]; E: 82 183 [weight=116, ]; -E: 83 87 [weight=1, ]; E: 83 108 [weight=12, ]; E: 83 157 [weight=2, ]; E: 83 169 [weight=11, ]; @@ -621,29 +779,25 @@ E: 83 179 [weight=1, ]; E: 83 181 [weight=2, ]; E: 83 182 [weight=3, ]; E: 83 183 [weight=18, ]; -E: 84 86 [weight=1, ]; +E: 83 87 [weight=1, ]; E: 84 108 [weight=12, ]; E: 84 169 [weight=14, ]; E: 84 179 [weight=1, ]; E: 84 181 [weight=4, ]; E: 84 182 [weight=2, ]; E: 84 183 [weight=18, ]; -E: 85 87 [weight=1, ]; +E: 84 86 [weight=1, ]; E: 85 108 [weight=3, ]; E: 85 169 [weight=3, ]; E: 85 181 [weight=4, ]; E: 85 182 [weight=1, ]; E: 85 183 [weight=6, ]; -E: 86 87 [weight=1, ]; +E: 85 87 [weight=1, ]; E: 86 108 [weight=3, ]; E: 86 181 [weight=4, ]; E: 86 182 [weight=2, ]; E: 86 183 [weight=4, ]; -E: 87 88 [weight=1, ]; -E: 87 91 [weight=6, ]; -E: 87 96 [weight=1, ]; -E: 87 98 [weight=23, ]; -E: 87 99 [weight=6, ]; +E: 86 87 [weight=1, ]; E: 87 104 [weight=10, ]; E: 87 105 [weight=3, ]; E: 87 106 [weight=15, ]; @@ -655,7 +809,11 @@ E: 87 170 [weight=4, ]; E: 87 181 [weight=975, ]; E: 87 182 [weight=35, ]; E: 87 183 [weight=914, ]; -E: 88 99 [weight=6, ]; +E: 87 88 [weight=1, ]; +E: 87 91 [weight=6, ]; +E: 87 96 [weight=1, ]; +E: 87 98 [weight=23, ]; +E: 87 99 [weight=6, ]; E: 88 103 [weight=1, ]; E: 88 105 [weight=1, ]; E: 88 108 [weight=13, ]; @@ -663,10 +821,7 @@ E: 88 179 [weight=2, ]; E: 88 181 [weight=23, ]; E: 88 182 [weight=4, ]; E: 88 183 [weight=34, ]; -E: 89 92 [weight=1, ]; -E: 89 97 [weight=1, ]; -E: 89 98 [weight=2, ]; -E: 89 99 [weight=1, ]; +E: 88 99 [weight=6, ]; E: 89 106 [weight=1, ]; E: 89 108 [weight=6, ]; E: 89 121 [weight=12, ]; @@ -675,13 +830,17 @@ E: 89 179 [weight=1, ]; E: 89 181 [weight=12, ]; E: 89 182 [weight=7, ]; E: 89 183 [weight=4, ]; +E: 89 92 [weight=1, ]; +E: 89 97 [weight=1, ]; +E: 89 98 [weight=2, ]; +E: 89 99 [weight=1, ]; +E: 8 9 [weight=5, ]; E: 90 103 [weight=1, ]; E: 90 108 [weight=5, ]; E: 90 173 [weight=24, ]; E: 90 181 [weight=6, ]; E: 90 182 [weight=2, ]; E: 90 183 [weight=12, ]; -E: 91 99 [weight=1, ]; E: 91 104 [weight=2, ]; E: 91 105 [weight=1, ]; E: 91 106 [weight=3, ]; @@ -691,9 +850,7 @@ E: 91 179 [weight=1, ]; E: 91 181 [weight=27, ]; E: 91 182 [weight=2, ]; E: 91 183 [weight=19, ]; -E: 92 97 [weight=3, ]; -E: 92 98 [weight=3, ]; -E: 92 99 [weight=2, ]; +E: 91 99 [weight=1, ]; E: 92 105 [weight=1, ]; E: 92 106 [weight=3, ]; E: 92 108 [weight=11, ]; @@ -704,10 +861,9 @@ E: 92 179 [weight=2, ]; E: 92 181 [weight=42, ]; E: 92 182 [weight=6, ]; E: 92 183 [weight=18, ]; -E: 93 94 [weight=1, ]; -E: 93 95 [weight=1, ]; -E: 93 97 [weight=2, ]; -E: 93 98 [weight=2, ]; +E: 92 97 [weight=3, ]; +E: 92 98 [weight=3, ]; +E: 92 99 [weight=2, ]; E: 93 103 [weight=1, ]; E: 93 105 [weight=1, ]; E: 93 106 [weight=1, ]; @@ -716,6 +872,10 @@ E: 93 154 [weight=10, ]; E: 93 169 [weight=53, ]; E: 93 181 [weight=66, ]; E: 93 183 [weight=36, ]; +E: 93 94 [weight=1, ]; +E: 93 95 [weight=1, ]; +E: 93 97 [weight=2, ]; +E: 93 98 [weight=2, ]; E: 94 106 [weight=1, ]; E: 94 108 [weight=7, ]; E: 94 154 [weight=2, ]; @@ -723,9 +883,6 @@ E: 94 169 [weight=14, ]; E: 94 179 [weight=1, ]; E: 94 181 [weight=6, ]; E: 94 183 [weight=12, ]; -E: 95 97 [weight=1, ]; -E: 95 98 [weight=2, ]; -E: 95 99 [weight=1, ]; E: 95 103 [weight=1, ]; E: 95 105 [weight=1, ]; E: 95 106 [weight=1, ]; @@ -734,6 +891,9 @@ E: 95 169 [weight=28, ]; E: 95 181 [weight=10, ]; E: 95 182 [weight=2, ]; E: 95 183 [weight=14, ]; +E: 95 97 [weight=1, ]; +E: 95 98 [weight=2, ]; +E: 95 99 [weight=1, ]; E: 96 103 [weight=1, ]; E: 96 108 [weight=5, ]; E: 96 170 [weight=40, ]; @@ -755,346 +915,186 @@ E: 99 107 [weight=1, ]; E: 99 108 [weight=3, ]; E: 99 179 [weight=1, ]; E: 99 183 [weight=4, ]; -E: 100 101 [weight=1, ]; -E: 100 108 [weight=3, ]; -E: 100 168 [weight=1, ]; -E: 100 181 [weight=5, ]; -E: 100 182 [weight=4, ]; -E: 100 183 [weight=4, ]; -E: 101 103 [weight=1, ]; -E: 101 108 [weight=5, ]; -E: 101 168 [weight=2, ]; -E: 101 181 [weight=10, ]; -E: 101 182 [weight=23, ]; -E: 101 183 [weight=30, ]; -E: 102 108 [weight=14, ]; -E: 102 181 [weight=12, ]; -E: 102 182 [weight=4, ]; -E: 102 183 [weight=30, ]; -E: 103 108 [weight=14, ]; -E: 103 181 [weight=12, ]; -E: 103 182 [weight=4, ]; -E: 103 183 [weight=30, ]; -E: 104 181 [weight=6, ]; -E: 104 182 [weight=2, ]; -E: 104 183 [weight=6, ]; -E: 105 181 [weight=6, ]; -E: 105 182 [weight=2, ]; -E: 105 183 [weight=6, ]; -E: 106 181 [weight=6, ]; -E: 106 182 [weight=2, ]; -E: 106 183 [weight=6, ]; -E: 107 181 [weight=6, ]; -E: 107 182 [weight=2, ]; -E: 107 183 [weight=6, ]; -E: 108 181 [weight=6, ]; -E: 108 182 [weight=2, ]; -E: 108 183 [weight=6, ]; -E: 109 110 [weight=1, ]; -E: 109 118 [weight=1, ]; -E: 109 121 [weight=9, ]; -E: 109 169 [weight=2, ]; -E: 109 181 [weight=3, ]; -E: 109 182 [weight=4, ]; -E: 109 183 [weight=11, ]; -E: 110 121 [weight=7, ]; -E: 110 179 [weight=1, ]; -E: 110 181 [weight=2, ]; -E: 110 182 [weight=2, ]; -E: 110 183 [weight=8, ]; -E: 111 112 [weight=1, ]; -E: 111 114 [weight=2, ]; -E: 111 121 [weight=4, ]; -E: 111 157 [weight=1, ]; -E: 111 169 [weight=1, ]; -E: 111 182 [weight=4, ]; -E: 111 183 [weight=6, ]; -E: 112 114 [weight=7, ]; -E: 112 121 [weight=9, ]; -E: 112 155 [weight=1, ]; -E: 112 169 [weight=10, ]; -E: 112 179 [weight=1, ]; -E: 112 181 [weight=9, ]; -E: 112 182 [weight=5, ]; -E: 112 183 [weight=21, ]; -E: 113 114 [weight=1, ]; -E: 113 182 [weight=1, ]; -E: 113 183 [weight=3, ]; -E: 114 181 [weight=1, ]; -E: 114 183 [weight=12, ]; -E: 115 116 [weight=2, ]; -E: 115 121 [weight=36, ]; -E: 115 135 [weight=1, ]; -E: 115 136 [weight=1, ]; -E: 115 145 [weight=43, ]; -E: 115 169 [weight=10, ]; -E: 115 173 [weight=78, ]; -E: 115 179 [weight=1, ]; -E: 115 181 [weight=30, ]; -E: 115 182 [weight=37, ]; -E: 115 183 [weight=4, ]; -E: 116 121 [weight=9, ]; -E: 116 150 [weight=1, ]; -E: 116 169 [weight=1, ]; -E: 116 173 [weight=22, ]; -E: 116 179 [weight=1, ]; -E: 116 181 [weight=7, ]; -E: 116 182 [weight=7, ]; -E: 116 183 [weight=4, ]; -E: 117 121 [weight=30, ]; -E: 117 148 [weight=2, ]; -E: 117 149 [weight=1, ]; -E: 117 169 [weight=5, ]; -E: 117 170 [weight=62, ]; -E: 117 179 [weight=1, ]; -E: 117 181 [weight=16, ]; -E: 117 182 [weight=18, ]; -E: 117 183 [weight=4, ]; -E: 118 119 [weight=1, ]; -E: 118 121 [weight=17, ]; -E: 118 169 [weight=1, ]; -E: 118 179 [weight=1, ]; -E: 118 181 [weight=8, ]; -E: 118 182 [weight=4, ]; -E: 118 183 [weight=17, ]; -E: 119 120 [weight=1, ]; -E: 119 121 [weight=2, ]; -E: 119 169 [weight=1, ]; -E: 119 181 [weight=3, ]; -E: 119 182 [weight=2, ]; -E: 119 183 [weight=3, ]; -E: 120 121 [weight=29, ]; -E: 120 156 [weight=1, ]; -E: 120 157 [weight=1, ]; -E: 120 169 [weight=20, ]; -E: 120 179 [weight=1, ]; -E: 120 181 [weight=8, ]; -E: 120 182 [weight=13, ]; -E: 120 183 [weight=23, ]; -E: 121 169 [weight=1, ]; -E: 121 181 [weight=1, ]; -E: 121 182 [weight=2, ]; -E: 121 183 [weight=9, ]; -E: 122 127 [weight=10, ]; -E: 122 181 [weight=2, ]; -E: 122 183 [weight=2, ]; -E: 123 127 [weight=10, ]; -E: 123 181 [weight=2, ]; -E: 123 183 [weight=2, ]; -E: 124 127 [weight=2, ]; -E: 124 182 [weight=2, ]; -E: 125 127 [weight=19, ]; -E: 125 179 [weight=1, ]; -E: 125 181 [weight=3, ]; -E: 125 182 [weight=11, ]; -E: 125 183 [weight=14, ]; -E: 126 127 [weight=29, ]; -E: 126 170 [weight=27, ]; -E: 126 179 [weight=1, ]; -E: 126 181 [weight=2, ]; -E: 126 182 [weight=2, ]; -E: 126 183 [weight=4, ]; -E: 127 183 [weight=6, ]; -E: 128 131 [weight=38, ]; -E: 128 169 [weight=35, ]; -E: 128 179 [weight=1, ]; -E: 128 181 [weight=26, ]; -E: 128 182 [weight=30, ]; -E: 128 183 [weight=77, ]; -E: 129 169 [weight=25, ]; -E: 129 180 [weight=1, ]; -E: 129 181 [weight=50, ]; -E: 129 182 [weight=46, ]; -E: 129 183 [weight=78, ]; -E: 130 131 [weight=13, ]; -E: 130 132 [weight=13, ]; -E: 130 169 [weight=13, ]; -E: 130 179 [weight=1, ]; -E: 130 181 [weight=44, ]; -E: 130 182 [weight=35, ]; -E: 130 183 [weight=37, ]; -E: 131 181 [weight=1, ]; -E: 131 182 [weight=2, ]; -E: 131 183 [weight=13, ]; -E: 132 183 [weight=9, ]; -E: 133 134 [weight=12, ]; -E: 133 170 [weight=11, ]; -E: 133 179 [weight=1, ]; -E: 133 181 [weight=4, ]; -E: 133 182 [weight=2, ]; -E: 133 183 [weight=5, ]; -E: 134 181 [weight=1, ]; -E: 134 182 [weight=1, ]; -E: 134 183 [weight=10, ]; -E: 135 145 [weight=26, ]; -E: 135 169 [weight=8, ]; -E: 135 173 [weight=30, ]; -E: 135 179 [weight=1, ]; -E: 135 181 [weight=9, ]; -E: 135 182 [weight=6, ]; -E: 135 183 [weight=9, ]; -E: 136 145 [weight=24, ]; -E: 136 169 [weight=11, ]; -E: 136 173 [weight=24, ]; -E: 136 179 [weight=1, ]; -E: 136 181 [weight=9, ]; -E: 136 182 [weight=19, ]; -E: 136 183 [weight=9, ]; -E: 137 145 [weight=14, ]; -E: 137 173 [weight=13, ]; -E: 137 179 [weight=1, ]; -E: 137 181 [weight=3, ]; -E: 137 182 [weight=3, ]; -E: 137 183 [weight=4, ]; -E: 138 145 [weight=9, ]; -E: 138 173 [weight=18, ]; -E: 138 179 [weight=1, ]; -E: 138 181 [weight=6, ]; -E: 138 182 [weight=6, ]; -E: 138 183 [weight=4, ]; -E: 139 145 [weight=14, ]; -E: 139 170 [weight=14, ]; -E: 139 173 [weight=19, ]; -E: 139 181 [weight=6, ]; -E: 139 182 [weight=6, ]; -E: 139 183 [weight=14, ]; -E: 140 141 [weight=1, ]; -E: 140 183 [weight=2, ]; -E: 141 183 [weight=9, ]; -E: 142 145 [weight=7, ]; -E: 142 170 [weight=6, ]; -E: 142 181 [weight=4, ]; -E: 142 183 [weight=3, ]; -E: 143 145 [weight=32, ]; -E: 143 170 [weight=16, ]; -E: 143 178 [weight=1, ]; -E: 143 181 [weight=9, ]; -E: 143 182 [weight=4, ]; -E: 143 183 [weight=4, ]; -E: 144 183 [weight=9, ]; -E: 145 183 [weight=9, ]; -E: 146 150 [weight=2, ]; -E: 146 169 [weight=36, ]; -E: 146 173 [weight=46, ]; -E: 146 179 [weight=1, ]; -E: 146 181 [weight=38, ]; -E: 146 182 [weight=13, ]; -E: 146 183 [weight=105, ]; -E: 147 169 [weight=18, ]; -E: 147 179 [weight=1, ]; -E: 147 181 [weight=7, ]; -E: 147 182 [weight=2, ]; -E: 147 183 [weight=48, ]; -E: 148 169 [weight=11, ]; -E: 148 170 [weight=40, ]; -E: 148 179 [weight=1, ]; -E: 148 181 [weight=2, ]; -E: 148 182 [weight=2, ]; -E: 148 183 [weight=7, ]; -E: 149 169 [weight=9, ]; -E: 149 170 [weight=39, ]; -E: 149 179 [weight=1, ]; -E: 149 181 [weight=2, ]; -E: 149 182 [weight=2, ]; -E: 149 183 [weight=7, ]; -E: 150 169 [weight=6, ]; -E: 150 173 [weight=19, ]; -E: 150 179 [weight=1, ]; -E: 150 181 [weight=2, ]; -E: 150 182 [weight=2, ]; -E: 150 183 [weight=11, ]; -E: 151 158 [weight=2, ]; -E: 151 169 [weight=41, ]; -E: 151 179 [weight=1, ]; -E: 151 181 [weight=88, ]; -E: 151 182 [weight=78, ]; -E: 151 183 [weight=119, ]; -E: 152 157 [weight=1, ]; -E: 152 158 [weight=1, ]; -E: 152 169 [weight=19, ]; -E: 152 181 [weight=87, ]; -E: 152 182 [weight=107, ]; -E: 152 183 [weight=118, ]; -E: 153 169 [weight=12, ]; -E: 153 181 [weight=21, ]; -E: 153 182 [weight=56, ]; -E: 153 183 [weight=62, ]; -E: 154 169 [weight=3, ]; -E: 154 181 [weight=3, ]; -E: 154 183 [weight=6, ]; -E: 155 156 [weight=1, ]; -E: 155 169 [weight=8, ]; -E: 155 183 [weight=8, ]; -E: 156 169 [weight=29, ]; -E: 156 179 [weight=1, ]; -E: 156 181 [weight=5, ]; -E: 156 182 [weight=2, ]; -E: 156 183 [weight=18, ]; -E: 157 169 [weight=6, ]; -E: 157 179 [weight=1, ]; -E: 157 181 [weight=5, ]; -E: 157 182 [weight=9, ]; -E: 157 183 [weight=14, ]; -E: 158 169 [weight=7, ]; -E: 158 181 [weight=12, ]; -E: 158 182 [weight=10, ]; -E: 158 183 [weight=30, ]; -E: 159 162 [weight=1, ]; -E: 159 170 [weight=36, ]; -E: 159 178 [weight=1, ]; -E: 159 181 [weight=6, ]; -E: 159 182 [weight=2, ]; -E: 159 183 [weight=4, ]; -E: 160 170 [weight=10, ]; -E: 160 181 [weight=2, ]; -E: 160 183 [weight=2, ]; -E: 161 169 [weight=25, ]; -E: 161 170 [weight=8, ]; -E: 161 179 [weight=1, ]; -E: 161 181 [weight=46, ]; -E: 161 182 [weight=6, ]; -E: 161 183 [weight=103, ]; -E: 162 170 [weight=3, ]; -E: 162 182 [weight=3, ]; -E: 163 170 [weight=6, ]; -E: 163 181 [weight=2, ]; -E: 163 183 [weight=3, ]; -E: 164 170 [weight=3, ]; -E: 164 181 [weight=2, ]; -E: 164 183 [weight=3, ]; -E: 165 176 [weight=2, ]; -E: 165 181 [weight=2, ]; -E: 165 183 [weight=2, ]; -E: 166 176 [weight=2, ]; -E: 166 182 [weight=2, ]; -E: 167 180 [weight=1, ]; -E: 167 181 [weight=12, ]; -E: 167 182 [weight=8, ]; -E: 167 183 [weight=32, ]; -E: 168 181 [weight=4, ]; -E: 168 182 [weight=4, ]; -E: 168 183 [weight=10, ]; -E: 169 181 [weight=1, ]; -E: 169 183 [weight=12, ]; -E: 170 183 [weight=6, ]; -E: 171 172 [weight=1, ]; -E: 171 182 [weight=1, ]; -E: 172 183 [weight=1, ]; -E: 173 183 [weight=6, ]; -E: 174 182 [weight=1, ]; -E: 174 183 [weight=7, ]; -E: 175 183 [weight=5, ]; -E: 176 183 [weight=5, ]; -E: 177 181 [weight=2, ]; -E: 177 182 [weight=2, ]; -E: 177 183 [weight=10, ]; -E: 178 180 [weight=1, ]; -E: 178 181 [weight=1, ]; -E: 178 182 [weight=1, ]; -E: 178 183 [weight=4, ]; -E: 179 181 [weight=2, ]; -E: 179 182 [weight=2, ]; -E: 179 183 [weight=10, ]; -E: 180 181 [weight=2, ]; -E: 180 182 [weight=2, ]; -E: 180 183 [weight=10, ]; +N: 100 "Permutation_nil_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 101 "Permutation_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 102 "Permutation_sind" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 103 "Permutation_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 104 "perm_trans" [kind=construct, prop=yes, path="Test", ]; +N: 105 "perm_swap" [kind=construct, prop=yes, path="Test", ]; +N: 106 "perm_skip" [kind=construct, prop=yes, path="Test", ]; +N: 107 "perm_nil" [kind=construct, prop=yes, path="Test", ]; +N: 108 "Permutation" [kind=inductive, prop=no, path="Test", ]; +N: 109 "rev_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 10 "seq_shift" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 110 "rev_list_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 111 "rev_alt" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 112 "rev_append_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 113 "rev'" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 114 "rev_append" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 115 "rev_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 116 "rev_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 117 "In_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 118 "rev_involutive" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 119 "rev_unit" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 11 "seq_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 120 "distr_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 121 "rev" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 122 "count_occ_cons_neq" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 123 "count_occ_cons_eq" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 124 "count_occ_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 125 "count_occ_inv_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 126 "count_occ_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 127 "count_occ" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 128 "removelast_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 129 "exists_last" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 12 "seq_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 130 "app_removelast_last" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 131 "removelast" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 132 "last" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 133 "remove_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 134 "remove" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 135 "app_nth2" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 136 "app_nth1" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 137 "nth_indep" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 138 "nth_overflow" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 139 "nth_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 13 "seq" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 140 "nth_default" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 141 "nth_error" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 142 "nth_S_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 143 "nth_in_or_default" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 144 "nth_ok" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 145 "nth" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 146 "app_inv_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 147 "app_inv_head" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 148 "in_or_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 149 "in_app_or" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 14 "firstn_removelast" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 150 "app_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 151 "app_inj_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 152 "app_eq_unit" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 153 "app_eq_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 154 "app_comm_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 155 "ass_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 156 "app_ass" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 157 "app_nil_end" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 158 "app_cons_not_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 159 "In_dec" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 15 "removelast_firstn" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 160 "in_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 161 "In_split" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 162 "in_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 163 "in_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 164 "in_eq" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 165 "head_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 166 "head_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 167 "destruct_list" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 168 "nil_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 169 "app" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 16 "firstn_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 170 "In" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 171 "size_nil" [body=no, kind=cnst, prop=yes, path="Test", ]; +N: 172 "size" [body=no, kind=cnst, prop=no, path="Test", ]; +N: 173 "length" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 174 "tail" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 175 "hd" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 176 "head" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 177 "list_sind" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 178 "list_rec" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 179 "list_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 17 "firstn_skipn" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 180 "list_rect" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 181 "cons" [kind=construct, prop=no, path="Test", ]; +N: 182 "nil" [kind=construct, prop=no, path="Test", ]; +N: 183 "list" [kind=inductive, prop=no, path="Test", ]; +N: 18 "skipn" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 19 "firstn" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 1 "NoDup_Permutation" [body=yes, kind=cnst, prop=yes, path="Test.ReDun", ]; +N: 20 "incl_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 21 "incl_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 22 "incl_appr" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 23 "incl_appl" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 24 "incl_tran" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 25 "incl_tl" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 26 "incl_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 27 "incl" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 28 "lel_nil" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 29 "lel_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 2 "NoDup_remove_2" [body=yes, kind=cnst, prop=yes, path="Test.ReDun", ]; +N: 30 "lel_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 31 "lel_cons_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 32 "lel_trans" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 33 "lel_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 34 "lel" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 35 "prod_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 36 "in_prod_iff" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 37 "in_prod" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 38 "in_prod_aux" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 39 "list_prod" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 3 "NoDup_remove_1" [body=yes, kind=cnst, prop=yes, path="Test.ReDun", ]; +N: 40 "combine_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 41 "combine_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 42 "in_combine_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 43 "in_combine_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 44 "combine_split" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 45 "split_combine" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 46 "combine" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 47 "split_length_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 48 "split_length_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 49 "split_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 4 "NoDup_sind" [body=yes, kind=cnst, prop=no, path="Test.ReDun", ]; +N: 50 "in_split_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 51 "in_split_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 52 "split" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 53 "partition" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 54 "find" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 55 "filter_In" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 56 "filter" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 57 "forallb_forall" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 58 "forallb" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 59 "existsb_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 5 "NoDup_ind" [body=yes, kind=cnst, prop=yes, path="Test.ReDun", ]; +N: 60 "existsb_exists" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 61 "existsb" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 62 "list_power" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 63 "fold_symmetric" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 64 "fold_left_rev_right" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 65 "fold_right_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 66 "fold_right" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 67 "fold_left_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 68 "fold_left_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 69 "fold_left" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 6 "NoDup_cons" [kind=construct, prop=yes, path="Test.ReDun", ]; +N: 70 "map_ext" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 71 "map_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 72 "in_flat_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 73 "flat_map" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 74 "Permutation_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 75 "map_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 76 "map_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 77 "map_nth" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 78 "map_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 79 "in_map_iff" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 7 "NoDup_nil" [kind=construct, prop=yes, path="Test.ReDun", ]; +N: 80 "in_map" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 81 "map" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 82 "list_eq_dec" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 83 "Permutation_app_inv_r" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 84 "Permutation_app_inv_l" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 85 "Permutation_cons_app_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 86 "Permutation_cons_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 87 "Permutation_app_inv" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 88 "Permutation_ind_bis" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 89 "Permutation_rev" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 8 "NoDup" [kind=inductive, prop=no, path="Test.ReDun", ]; +N: 90 "Permutation_length" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 91 "Permutation_cons_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 92 "Permutation_app_swap" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 93 "Permutation_app" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 94 "Permutation_app_head" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 95 "Permutation_app_tail" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 96 "Permutation_in" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 97 "Permutation_trans" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 98 "Permutation_sym" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 99 "Permutation_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 9 "A" [body=no, kind=cnst, prop=no, path="Test.ReDun", ]; diff --git a/tests/graph.without.dot.oracle b/tests/graph.without.dot.oracle index 632fd7594..11c3b3f47 100644 --- a/tests/graph.without.dot.oracle +++ b/tests/graph.without.dot.oracle @@ -1,280 +1,280 @@ digraph tests/graph { +} /* END */ graph [ratio=0.5] node [style=filled] -Test_removelast_app [label="removelast_app", URL=, fillcolor="#7FFFD4"] ; -Test_ReDun_NoDup_Permutation [label="NoDup_Permutation", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_removelast_last [label="app_removelast_last", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_ReDun_NoDup_remove_2 [label="NoDup_remove_2", URL=, fillcolor="#7FFFD4"] ; -Test_ReDun_NoDup_remove_1 [label="NoDup_remove_1", URL=, fillcolor="#7FFFD4"] ; -Test_remove_In [label="remove_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_ReDun_NoDup_ind [label="NoDup_ind", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_ReDun_NoDup_cons [label="NoDup_cons", URL=, fillcolor="#7FAAFF"] ; -Test_ReDun_NoDup_nil [label="NoDup_nil", URL=, peripheries=3, fillcolor="#7FAAFF"] ; -Test_app_nth2 [label="app_nth2", URL=, fillcolor="#7FFFD4"] ; -Test_app_nth1 [label="app_nth1", URL=, fillcolor="#7FFFD4"] ; -Test_nth_indep [label="nth_indep", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_seq_shift [label="seq_shift", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_nth_overflow [label="nth_overflow", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_seq_nth [label="seq_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_nth_In [label="nth_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_seq_length [label="seq_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_nth_S_cons [label="nth_S_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_firstn_removelast [label="firstn_removelast", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_removelast_firstn [label="removelast_firstn", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_firstn_length [label="firstn_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_firstn_skipn [label="firstn_skipn", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_inv_tail [label="app_inv_tail", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +subgraph cluster_Test { label="Test"; fillcolor="#FFFFC3"; labeljust=l; style=filled +subgraph cluster_Test_ReDun { label="ReDun"; fillcolor="#FFFFA3"; labeljust=l; style=filled +Test_app_ass [label="app_ass", URL=, fillcolor="#7FFFD4"] ; + Test_app_ass -> Test_list_ind [] ; +Test_app_comm_cons [label="app_comm_cons", URL=, fillcolor="#7FFFD4"] ; +Test_app_cons_not_nil [label="app_cons_not_nil", URL=, fillcolor="#7FFFD4"] ; +Test_app_eq_nil [label="app_eq_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_app_eq_unit [label="app_eq_unit", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_eq_unit -> Test_app_cons_not_nil [] ; + Test_app_eq_unit -> Test_app_nil_end [] ; +Test_app_inj_tail [label="app_inj_tail", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_inj_tail -> Test_app_cons_not_nil [] ; + Test_app_inj_tail -> Test_list_ind [] ; Test_app_inv_head [label="app_inv_head", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_incl_app [label="incl_app", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_or_app [label="in_or_app", URL=, fillcolor="#7FFFD4"] ; -Test_incl_cons [label="incl_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_app_or [label="in_app_or", URL=, fillcolor="#7FFFD4"] ; -Test_incl_appr [label="incl_appr", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_inv_head -> Test_list_ind [] ; +Test_app_inv_tail [label="app_inv_tail", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_inv_tail -> Test_app_length [] ; Test_app_length [label="app_length", URL=, fillcolor="#7FFFD4"] ; -Test_incl_appl [label="incl_appl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_inj_tail [label="app_inj_tail", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_incl_tran [label="incl_tran", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_eq_unit [label="app_eq_unit", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_incl_tl [label="incl_tl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_eq_nil [label="app_eq_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_incl_refl [label="incl_refl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_comm_cons [label="app_comm_cons", URL=, fillcolor="#7FFFD4"] ; -Test_ass_app [label="ass_app", URL=, fillcolor="#7FFFD4"] ; -Test_lel_nil [label="lel_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_ass [label="app_ass", URL=, fillcolor="#7FFFD4"] ; -Test_lel_tail [label="lel_tail", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_length -> Test_list_ind [] ; Test_app_nil_end [label="app_nil_end", URL=, fillcolor="#7FFFD4"] ; -Test_lel_cons [label="lel_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_app_cons_not_nil [label="app_cons_not_nil", URL=, fillcolor="#7FFFD4"] ; -Test_lel_cons_cons [label="lel_cons_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_lel_trans [label="lel_trans", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_inv [label="in_inv", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_lel_refl [label="lel_refl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_In_split [label="In_split", URL=, fillcolor="#7FFFD4"] ; -Test_in_nil [label="in_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_prod_length [label="prod_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_cons [label="in_cons", URL=, fillcolor="#7FFFD4"] ; -Test_in_prod_iff [label="in_prod_iff", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_eq [label="in_eq", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_prod [label="in_prod", URL=, fillcolor="#7FFFD4"] ; -Test_head_cons [label="head_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_prod_aux [label="in_prod_aux", URL=, fillcolor="#7FFFD4"] ; -Test_head_nil [label="head_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_nil_cons [label="nil_cons", URL=, fillcolor="#7FFFD4"] ; -Test_combine_nth [label="combine_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_nil_end -> Test_list_ind [] ; +Test_app_nth1 [label="app_nth1", URL=, fillcolor="#7FFFD4"] ; + Test_app_nth1 -> Test_list_ind [] ; +Test_app_nth2 [label="app_nth2", URL=, fillcolor="#7FFFD4"] ; + Test_app_nth2 -> Test_list_ind [] ; +Test_app_removelast_last [label="app_removelast_last", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_app_removelast_last -> Test_list_ind [] ; +Test_ass_app [label="ass_app", URL=, fillcolor="#7FFFD4"] ; + Test_ass_app -> Test_app_ass [] ; Test_combine_length [label="combine_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_combine_r [label="in_combine_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_size_nil [label="size_nil", URL=, peripheries=3, fillcolor="#FFB57F"] ; -Test_in_combine_l [label="in_combine_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_combine_length -> Test_list_ind [] ; +Test_combine_nth [label="combine_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_combine_nth -> Test_list_ind [] ; Test_combine_split [label="combine_split", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_split_combine [label="split_combine", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_split_length_r [label="split_length_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_split_length_l [label="split_length_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_split_nth [label="split_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_in_split_r [label="in_split_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_list_ind [label="list_ind", URL=, fillcolor="#7FFFD4"] ; -Test_in_split_l [label="in_split_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_filter_In [label="filter_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_forallb_forall [label="forallb_forall", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_existsb_nth [label="existsb_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_combine_split -> Test_list_ind [] ; +Test_count_occ_cons_eq [label="count_occ_cons_eq", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_count_occ_cons_neq [label="count_occ_cons_neq", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_count_occ_In [label="count_occ_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_count_occ_In; Test_count_occ_inv_nil; Test_count_occ_nil; Test_count_occ_cons_eq; Test_count_occ_cons_neq; Test_distr_rev; Test_rev_unit; Test_rev_involutive; Test_In_rev; Test_rev_length; Test_rev_nth; Test_rev_append_rev; Test_rev_alt; Test_rev_list_ind; Test_rev_ind; Test_perm_nil; Test_perm_skip; Test_perm_swap; Test_perm_trans; Test_Permutation_ind; Test_Permutation_nil; Test_Permutation_nil_cons; Test_Permutation_refl; Test_Permutation_sym; Test_Permutation_trans; Test_Permutation_in; Test_Permutation_app_tail; Test_Permutation_app_head; Test_Permutation_app; Test_Permutation_app_swap; Test_Permutation_cons_app; Test_Permutation_length; Test_Permutation_rev; Test_Permutation_ind_bis; Test_Permutation_app_inv; Test_Permutation_cons_inv; Test_Permutation_cons_app_inv; Test_Permutation_app_inv_l; Test_Permutation_app_inv_r; Test_in_map; Test_in_map_iff; Test_map_length; Test_map_nth; Test_map_app; Test_map_rev; Test_Permutation_map; Test_in_flat_map; Test_map_map; Test_map_ext; Test_fold_left_app; Test_fold_left_length; Test_fold_right_app; Test_fold_left_rev_right; Test_fold_symmetric; Test_existsb_exists; Test_existsb_nth; Test_forallb_forall; Test_filter_In; Test_in_split_l; Test_list_ind; Test_in_split_r; Test_split_nth; Test_split_length_l; Test_split_length_r; Test_split_combine; Test_combine_split; Test_size_nil; Test_in_combine_l; Test_in_combine_r; Test_combine_length; Test_nil_cons; Test_combine_nth; Test_in_prod_aux; Test_head_nil; Test_head_cons; Test_in_prod; Test_in_eq; Test_in_prod_iff; Test_prod_length; Test_in_cons; Test_in_nil; Test_lel_refl; Test_In_split; Test_lel_trans; Test_in_inv; Test_lel_cons_cons; Test_lel_cons; Test_app_cons_not_nil; Test_lel_tail; Test_app_nil_end; Test_app_ass; Test_lel_nil; Test_ass_app; Test_app_comm_cons; Test_incl_refl; Test_incl_tl; Test_app_eq_nil; Test_app_eq_unit; Test_incl_tran; Test_app_inj_tail; Test_incl_appl; Test_incl_appr; Test_app_length; Test_in_app_or; Test_incl_cons; Test_incl_app; Test_in_or_app; Test_app_inv_head; Test_app_inv_tail; Test_firstn_skipn; Test_firstn_length; Test_removelast_firstn; Test_firstn_removelast; Test_nth_S_cons; Test_seq_length; Test_seq_nth; Test_nth_In; Test_nth_overflow; Test_seq_shift; Test_nth_indep; Test_app_nth1; Test_app_nth2; Test_remove_In; Test_app_removelast_last; Test_removelast_app; }; + Test_count_occ_In -> Test_list_ind [] ; +Test_count_occ_inv_nil [label="count_occ_inv_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_count_occ_inv_nil -> Test_list_ind [] ; +Test_count_occ_nil [label="count_occ_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_distr_rev [label="distr_rev", URL=, fillcolor="#7FFFD4"] ; + Test_distr_rev -> Test_app_ass [] ; + Test_distr_rev -> Test_app_nil_end [] ; Test_existsb_exists [label="existsb_exists", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_fold_symmetric [label="fold_symmetric", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_existsb_exists -> Test_list_ind [] ; +Test_existsb_nth [label="existsb_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_existsb_nth -> Test_list_ind [] ; +Test_filter_In [label="filter_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_filter_In -> Test_list_ind [] ; +Test_firstn_length [label="firstn_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_firstn_removelast [label="firstn_removelast", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_firstn_removelast -> Test_removelast_app [] ; +Test_firstn_skipn [label="firstn_skipn", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_fold_left_app [label="fold_left_app", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_fold_left_app -> Test_list_ind [] ; +Test_fold_left_length [label="fold_left_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_fold_left_length -> Test_list_ind [] ; Test_fold_left_rev_right [label="fold_left_rev_right", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_fold_left_rev_right -> Test_fold_right_app [] ; Test_fold_right_app [label="fold_right_app", URL=, fillcolor="#7FFFD4"] ; -Test_fold_left_length [label="fold_left_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_fold_left_app [label="fold_left_app", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_map_ext [label="map_ext", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_map_map [label="map_map", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_fold_right_app -> Test_list_ind [] ; +Test_fold_symmetric [label="fold_symmetric", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_fold_symmetric -> Test_list_ind [] ; +Test_forallb_forall [label="forallb_forall", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_forallb_forall -> Test_list_ind [] ; +Test_head_cons [label="head_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_head_nil [label="head_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_in_app_or [label="in_app_or", URL=, fillcolor="#7FFFD4"] ; + Test_in_app_or -> Test_list_ind [] ; +Test_incl_app [label="incl_app", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_incl_appl [label="incl_appl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_incl_appl -> Test_in_or_app [] ; +Test_incl_appr [label="incl_appr", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_incl_appr -> Test_in_or_app [] ; + Test_incl_app -> Test_in_app_or [] ; +Test_incl_cons [label="incl_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_incl_refl [label="incl_refl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_incl_tl [label="incl_tl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_incl_tl -> Test_in_cons [] ; +Test_incl_tran [label="incl_tran", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_in_combine_l [label="in_combine_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_in_combine_l -> Test_list_ind [] ; +Test_in_combine_r [label="in_combine_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_in_combine_r -> Test_list_ind [] ; +Test_in_cons [label="in_cons", URL=, fillcolor="#7FFFD4"] ; +Test_in_eq [label="in_eq", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_in_flat_map [label="in_flat_map", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_map [label="Permutation_map", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_map_rev [label="map_rev", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_map_app [label="map_app", URL=, fillcolor="#7FFFD4"] ; -Test_map_nth [label="map_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_map_length [label="map_length", URL=, fillcolor="#7FFFD4"] ; + Test_in_flat_map -> Test_in_app_or [] ; + Test_in_flat_map -> Test_in_or_app [] ; +Test_in_inv [label="in_inv", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_in_map_iff [label="in_map_iff", URL=, fillcolor="#7FFFD4"] ; + Test_in_map_iff -> Test_list_ind [] ; Test_in_map [label="in_map", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_app_inv_r [label="Permutation_app_inv_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_app_inv_l [label="Permutation_app_inv_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_cons_app_inv [label="Permutation_cons_app_inv", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_cons_inv [label="Permutation_cons_inv", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_app_inv [label="Permutation_app_inv", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_ind_bis [label="Permutation_ind_bis", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_rev [label="Permutation_rev", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_length [label="Permutation_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_cons_app [label="Permutation_cons_app", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_app_swap [label="Permutation_app_swap", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_app [label="Permutation_app", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_app_head [label="Permutation_app_head", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_app_tail [label="Permutation_app_tail", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_in [label="Permutation_in", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_trans [label="Permutation_trans", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_sym [label="Permutation_sym", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_refl [label="Permutation_refl", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_nil_cons [label="Permutation_nil_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_nil [label="Permutation_nil", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_ind [label="Permutation_ind", URL=, fillcolor="#7FFFD4"] ; -Test_perm_trans [label="perm_trans", URL=, fillcolor="#7FAAFF"] ; -Test_perm_swap [label="perm_swap", URL=, fillcolor="#7FAAFF"] ; -Test_perm_skip [label="perm_skip", URL=, fillcolor="#7FAAFF"] ; -Test_perm_nil [label="perm_nil", URL=, fillcolor="#7FAAFF"] ; -Test_rev_ind [label="rev_ind", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_rev_list_ind [label="rev_list_ind", URL=, fillcolor="#7FFFD4"] ; -Test_rev_alt [label="rev_alt", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_rev_append_rev [label="rev_append_rev", URL=, fillcolor="#7FFFD4"] ; -Test_rev_nth [label="rev_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_rev_length [label="rev_length", URL=, fillcolor="#7FFFD4"] ; -Test_In_rev [label="In_rev", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_rev_involutive [label="rev_involutive", URL=, fillcolor="#7FFFD4"] ; -Test_rev_unit [label="rev_unit", URL=, fillcolor="#7FFFD4"] ; -Test_distr_rev [label="distr_rev", URL=, fillcolor="#7FFFD4"] ; -Test_count_occ_cons_neq [label="count_occ_cons_neq", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_count_occ_cons_eq [label="count_occ_cons_eq", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_count_occ_nil [label="count_occ_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_count_occ_inv_nil [label="count_occ_inv_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_count_occ_In [label="count_occ_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; - Test_removelast_app -> Test_list_ind [] ; - Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_2 [] ; - Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_1 [] ; - Test_ReDun_NoDup_Permutation -> Test_Permutation_cons_app [] ; - Test_ReDun_NoDup_Permutation -> Test_In_split [] ; - Test_app_removelast_last -> Test_list_ind [] ; - Test_ReDun_NoDup_remove_2 -> Test_in_or_app [] ; - Test_ReDun_NoDup_remove_1 -> Test_ReDun_NoDup_cons [] ; - Test_ReDun_NoDup_remove_1 -> Test_in_or_app [] ; - Test_ReDun_NoDup_remove_1 -> Test_in_app_or [] ; - Test_remove_In -> Test_list_ind [] ; - Test_app_nth2 -> Test_list_ind [] ; - Test_app_nth1 -> Test_list_ind [] ; - Test_nth_indep -> Test_list_ind [] ; - Test_nth_overflow -> Test_list_ind [] ; - Test_firstn_removelast -> Test_removelast_app [] ; - Test_removelast_firstn -> Test_removelast_app [] ; - Test_app_inv_tail -> Test_app_length [] ; - Test_app_inv_head -> Test_list_ind [] ; - Test_incl_app -> Test_in_app_or [] ; + Test_in_map -> Test_list_ind [] ; +Test_in_nil [label="in_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_in_or_app [label="in_or_app", URL=, fillcolor="#7FFFD4"] ; Test_in_or_app -> Test_list_ind [] ; - Test_in_app_or -> Test_list_ind [] ; - Test_incl_appr -> Test_in_or_app [] ; - Test_app_length -> Test_list_ind [] ; - Test_incl_appl -> Test_in_or_app [] ; - Test_app_inj_tail -> Test_app_cons_not_nil [] ; - Test_app_inj_tail -> Test_list_ind [] ; - Test_app_eq_unit -> Test_app_nil_end [] ; - Test_app_eq_unit -> Test_app_cons_not_nil [] ; - Test_incl_tl -> Test_in_cons [] ; - Test_ass_app -> Test_app_ass [] ; - Test_lel_nil -> Test_list_ind [] ; - Test_app_ass -> Test_list_ind [] ; - Test_app_nil_end -> Test_list_ind [] ; - Test_In_split -> Test_list_ind [] ; - Test_prod_length -> Test_map_length [] ; - Test_prod_length -> Test_app_length [] ; - Test_in_prod_iff -> Test_in_prod [] ; - Test_in_prod_iff -> Test_in_map_iff [] ; +Test_in_prod_aux [label="in_prod_aux", URL=, fillcolor="#7FFFD4"] ; + Test_in_prod_aux -> Test_list_ind [] ; +Test_in_prod_iff [label="in_prod_iff", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_in_prod_iff -> Test_in_app_or [] ; - Test_in_prod -> Test_in_prod_aux [] ; + Test_in_prod_iff -> Test_in_map_iff [] ; + Test_in_prod_iff -> Test_in_prod [] ; +Test_in_prod [label="in_prod", URL=, fillcolor="#7FFFD4"] ; Test_in_prod -> Test_in_or_app [] ; - Test_in_prod_aux -> Test_list_ind [] ; - Test_combine_nth -> Test_list_ind [] ; - Test_combine_length -> Test_list_ind [] ; - Test_in_combine_r -> Test_list_ind [] ; - Test_in_combine_l -> Test_list_ind [] ; - Test_combine_split -> Test_list_ind [] ; - Test_split_combine -> Test_list_ind [] ; - Test_split_length_r -> Test_list_ind [] ; - Test_split_length_l -> Test_list_ind [] ; - Test_split_nth -> Test_list_ind [] ; - Test_in_split_r -> Test_list_ind [] ; + Test_in_prod -> Test_in_prod_aux [] ; +Test_In_rev [label="In_rev", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_In_rev -> Test_in_app_or [] ; + Test_In_rev -> Test_in_or_app [] ; +Test_In_split [label="In_split", URL=, fillcolor="#7FFFD4"] ; +Test_in_split_l [label="in_split_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_in_split_l -> Test_list_ind [] ; - Test_filter_In -> Test_list_ind [] ; - Test_forallb_forall -> Test_list_ind [] ; - Test_existsb_nth -> Test_list_ind [] ; - Test_existsb_exists -> Test_list_ind [] ; - Test_fold_symmetric -> Test_list_ind [] ; - Test_fold_left_rev_right -> Test_fold_right_app [] ; - Test_fold_right_app -> Test_list_ind [] ; - Test_fold_left_length -> Test_list_ind [] ; - Test_fold_left_app -> Test_list_ind [] ; +Test_in_split_r [label="in_split_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_in_split_r -> Test_list_ind [] ; + Test_In_split -> Test_list_ind [] ; +Test_lel_cons_cons [label="lel_cons_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_lel_cons [label="lel_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_lel_nil [label="lel_nil", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_lel_nil -> Test_list_ind [] ; +Test_lel_refl [label="lel_refl", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_lel_tail [label="lel_tail", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_lel_trans [label="lel_trans", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_list_ind [label="list_ind", URL=, fillcolor="#7FFFD4"] ; +Test_map_app [label="map_app", URL=, fillcolor="#7FFFD4"] ; + Test_map_app -> Test_list_ind [] ; +Test_map_ext [label="map_ext", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_map_ext -> Test_list_ind [] ; +Test_map_length [label="map_length", URL=, fillcolor="#7FFFD4"] ; + Test_map_length -> Test_list_ind [] ; +Test_map_map [label="map_map", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_map_map -> Test_list_ind [] ; - Test_in_flat_map -> Test_in_or_app [] ; - Test_in_flat_map -> Test_in_app_or [] ; - Test_Permutation_map -> Test_Permutation_ind [] ; - Test_Permutation_map -> Test_perm_trans [] ; - Test_Permutation_map -> Test_perm_swap [] ; - Test_Permutation_map -> Test_perm_skip [] ; - Test_Permutation_map -> Test_perm_nil [] ; - Test_map_rev -> Test_map_app [] ; - Test_map_app -> Test_list_ind [] ; +Test_map_nth [label="map_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_map_nth -> Test_list_ind [] ; - Test_map_length -> Test_list_ind [] ; - Test_in_map_iff -> Test_list_ind [] ; - Test_in_map -> Test_list_ind [] ; - Test_Permutation_app_inv_r -> Test_Permutation_app_inv [] ; - Test_Permutation_app_inv_r -> Test_app_nil_end [] ; +Test_map_rev [label="map_rev", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_map_rev -> Test_map_app [] ; +Test_nil_cons [label="nil_cons", URL=, fillcolor="#7FFFD4"] ; +Test_nth_indep [label="nth_indep", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_nth_indep -> Test_list_ind [] ; +Test_nth_In [label="nth_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_nth_overflow [label="nth_overflow", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_nth_overflow -> Test_list_ind [] ; +Test_nth_S_cons [label="nth_S_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_perm_nil [label="perm_nil", URL=, fillcolor="#7FAAFF"] ; +Test_perm_skip [label="perm_skip", URL=, fillcolor="#7FAAFF"] ; +Test_perm_swap [label="perm_swap", URL=, fillcolor="#7FAAFF"] ; +Test_perm_trans [label="perm_trans", URL=, fillcolor="#7FAAFF"] ; +Test_Permutation_app_head [label="Permutation_app_head", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_app_head -> Test_app_comm_cons [] ; + Test_Permutation_app_head -> Test_list_ind [] ; + Test_Permutation_app_head -> Test_perm_skip [] ; +Test_Permutation_app_inv [label="Permutation_app_inv", URL=, fillcolor="#7FFFD4"] ; +Test_Permutation_app_inv_l [label="Permutation_app_inv_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_Permutation_app_inv_l -> Test_Permutation_cons_inv [] ; - Test_Permutation_cons_app_inv -> Test_Permutation_app_inv [] ; - Test_Permutation_cons_inv -> Test_Permutation_app_inv [] ; - Test_Permutation_app_inv -> Test_Permutation_ind_bis [] ; +Test_Permutation_app_inv_r [label="Permutation_app_inv_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_Permutation_app_inv_r -> Test_app_nil_end [] ; + Test_Permutation_app_inv_r -> Test_Permutation_app_inv [] ; + Test_Permutation_app_inv -> Test_in_or_app [] ; + Test_Permutation_app_inv -> Test_In_split [] ; Test_Permutation_app_inv -> Test_Permutation_cons_app [] ; Test_Permutation_app_inv -> Test_Permutation_in [] ; + Test_Permutation_app_inv -> Test_Permutation_ind_bis [] ; Test_Permutation_app_inv -> Test_Permutation_sym [] ; - Test_Permutation_app_inv -> Test_in_or_app [] ; - Test_Permutation_app_inv -> Test_In_split [] ; - Test_Permutation_ind_bis -> Test_Permutation_refl [] ; - Test_Permutation_ind_bis -> Test_Permutation_ind [] ; - Test_Permutation_ind_bis -> Test_perm_swap [] ; - Test_Permutation_rev -> Test_Permutation_app_swap [] ; - Test_Permutation_length -> Test_Permutation_ind [] ; - Test_Permutation_cons_app -> Test_Permutation_refl [] ; - Test_Permutation_cons_app -> Test_perm_trans [] ; - Test_Permutation_cons_app -> Test_perm_swap [] ; - Test_Permutation_app_swap -> Test_Permutation_trans [] ; - Test_Permutation_app_swap -> Test_Permutation_sym [] ; - Test_Permutation_app_swap -> Test_Permutation_refl [] ; +Test_Permutation_app [label="Permutation_app", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_Permutation_app_swap [label="Permutation_app_swap", URL=, fillcolor="#7FFFD4"] ; Test_Permutation_app_swap -> Test_app_comm_cons [] ; Test_Permutation_app_swap -> Test_app_nil_end [] ; + Test_Permutation_app_swap -> Test_Permutation_refl [] ; + Test_Permutation_app_swap -> Test_Permutation_sym [] ; + Test_Permutation_app_swap -> Test_Permutation_trans [] ; +Test_Permutation_app_tail [label="Permutation_app_tail", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_app_tail -> Test_Permutation_refl [] ; + Test_Permutation_app_tail -> Test_Permutation_sym [] ; + Test_Permutation_app_tail -> Test_Permutation_trans [] ; Test_Permutation_app -> Test_Permutation_app_head [] ; Test_Permutation_app -> Test_Permutation_app_tail [] ; - Test_Permutation_app_head -> Test_perm_skip [] ; - Test_Permutation_app_head -> Test_app_comm_cons [] ; - Test_Permutation_app_head -> Test_list_ind [] ; - Test_Permutation_app_tail -> Test_Permutation_trans [] ; - Test_Permutation_app_tail -> Test_Permutation_sym [] ; - Test_Permutation_app_tail -> Test_Permutation_refl [] ; +Test_Permutation_cons_app_inv [label="Permutation_cons_app_inv", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_Permutation_cons_app_inv -> Test_Permutation_app_inv [] ; +Test_Permutation_cons_app [label="Permutation_cons_app", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_cons_app -> Test_perm_swap [] ; + Test_Permutation_cons_app -> Test_perm_trans [] ; + Test_Permutation_cons_app -> Test_Permutation_refl [] ; +Test_Permutation_cons_inv [label="Permutation_cons_inv", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_cons_inv -> Test_Permutation_app_inv [] ; +Test_Permutation_ind_bis [label="Permutation_ind_bis", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_ind_bis -> Test_perm_swap [] ; + Test_Permutation_ind_bis -> Test_Permutation_ind [] ; + Test_Permutation_ind_bis -> Test_Permutation_refl [] ; +Test_Permutation_ind [label="Permutation_ind", URL=, fillcolor="#7FFFD4"] ; +Test_Permutation_in [label="Permutation_in", URL=, fillcolor="#7FFFD4"] ; Test_Permutation_in -> Test_Permutation_ind [] ; - Test_Permutation_trans -> Test_perm_trans [] ; - Test_Permutation_sym -> Test_Permutation_ind [] ; - Test_Permutation_sym -> Test_perm_trans [] ; - Test_Permutation_sym -> Test_perm_swap [] ; - Test_Permutation_sym -> Test_perm_skip [] ; - Test_Permutation_sym -> Test_perm_nil [] ; - Test_Permutation_refl -> Test_perm_skip [] ; - Test_Permutation_refl -> Test_perm_nil [] ; - Test_Permutation_refl -> Test_list_ind [] ; +Test_Permutation_length [label="Permutation_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_Permutation_length -> Test_Permutation_ind [] ; +Test_Permutation_map [label="Permutation_map", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_Permutation_map -> Test_perm_nil [] ; + Test_Permutation_map -> Test_perm_skip [] ; + Test_Permutation_map -> Test_perm_swap [] ; + Test_Permutation_map -> Test_perm_trans [] ; + Test_Permutation_map -> Test_Permutation_ind [] ; +Test_Permutation_nil_cons [label="Permutation_nil_cons", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_Permutation_nil_cons -> Test_Permutation_nil [] ; - Test_Permutation_nil -> Test_Permutation_ind [] ; +Test_Permutation_nil [label="Permutation_nil", URL=, fillcolor="#7FFFD4"] ; Test_Permutation_nil -> Test_nil_cons [] ; - Test_rev_ind -> Test_rev_list_ind [] ; - Test_rev_ind -> Test_rev_involutive [] ; - Test_rev_list_ind -> Test_list_ind [] ; - Test_rev_alt -> Test_rev_append_rev [] ; + Test_Permutation_nil -> Test_Permutation_ind [] ; +Test_Permutation_refl [label="Permutation_refl", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_refl -> Test_list_ind [] ; + Test_Permutation_refl -> Test_perm_nil [] ; + Test_Permutation_refl -> Test_perm_skip [] ; +Test_Permutation_rev [label="Permutation_rev", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_Permutation_rev -> Test_Permutation_app_swap [] ; +Test_Permutation_sym [label="Permutation_sym", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_sym -> Test_perm_nil [] ; + Test_Permutation_sym -> Test_perm_skip [] ; + Test_Permutation_sym -> Test_perm_swap [] ; + Test_Permutation_sym -> Test_perm_trans [] ; + Test_Permutation_sym -> Test_Permutation_ind [] ; +Test_Permutation_trans [label="Permutation_trans", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_trans -> Test_perm_trans [] ; +Test_prod_length [label="prod_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_prod_length -> Test_app_length [] ; + Test_prod_length -> Test_map_length [] ; +Test_ReDun_NoDup_cons [label="NoDup_cons", URL=, fillcolor="#7FAAFF"] ; +Test_ReDun_NoDup_ind [label="NoDup_ind", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_ReDun_NoDup_nil [label="NoDup_nil", URL=, peripheries=3, fillcolor="#7FAAFF"] ; +Test_ReDun_NoDup_nil; Test_ReDun_NoDup_cons; Test_ReDun_NoDup_ind; Test_ReDun_NoDup_remove_1; Test_ReDun_NoDup_remove_2; Test_ReDun_NoDup_Permutation; }; +Test_ReDun_NoDup_Permutation [label="NoDup_Permutation", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_ReDun_NoDup_Permutation -> Test_In_split [] ; + Test_ReDun_NoDup_Permutation -> Test_Permutation_cons_app [] ; + Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_1 [] ; + Test_ReDun_NoDup_Permutation -> Test_ReDun_NoDup_remove_2 [] ; +Test_ReDun_NoDup_remove_1 [label="NoDup_remove_1", URL=, fillcolor="#7FFFD4"] ; + Test_ReDun_NoDup_remove_1 -> Test_in_app_or [] ; + Test_ReDun_NoDup_remove_1 -> Test_in_or_app [] ; + Test_ReDun_NoDup_remove_1 -> Test_ReDun_NoDup_cons [] ; +Test_ReDun_NoDup_remove_2 [label="NoDup_remove_2", URL=, fillcolor="#7FFFD4"] ; + Test_ReDun_NoDup_remove_2 -> Test_in_or_app [] ; +Test_remove_In [label="remove_In", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_remove_In -> Test_list_ind [] ; +Test_removelast_app [label="removelast_app", URL=, fillcolor="#7FFFD4"] ; + Test_removelast_app -> Test_list_ind [] ; +Test_removelast_firstn [label="removelast_firstn", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_removelast_firstn -> Test_removelast_app [] ; +Test_rev_alt [label="rev_alt", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_rev_alt -> Test_app_nil_end [] ; + Test_rev_alt -> Test_rev_append_rev [] ; +Test_rev_append_rev [label="rev_append_rev", URL=, fillcolor="#7FFFD4"] ; Test_rev_append_rev -> Test_ass_app [] ; - Test_rev_nth -> Test_rev_length [] ; - Test_rev_nth -> Test_app_nth2 [] ; - Test_rev_nth -> Test_app_nth1 [] ; - Test_rev_length -> Test_app_length [] ; - Test_In_rev -> Test_in_or_app [] ; - Test_In_rev -> Test_in_app_or [] ; +Test_rev_ind [label="rev_ind", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_rev_ind -> Test_rev_involutive [] ; + Test_rev_ind -> Test_rev_list_ind [] ; +Test_rev_involutive [label="rev_involutive", URL=, fillcolor="#7FFFD4"] ; Test_rev_involutive -> Test_rev_unit [] ; +Test_rev_length [label="rev_length", URL=, fillcolor="#7FFFD4"] ; + Test_rev_length -> Test_app_length [] ; +Test_rev_list_ind [label="rev_list_ind", URL=, fillcolor="#7FFFD4"] ; + Test_rev_list_ind -> Test_list_ind [] ; +Test_rev_nth [label="rev_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_rev_nth -> Test_app_nth1 [] ; + Test_rev_nth -> Test_app_nth2 [] ; + Test_rev_nth -> Test_rev_length [] ; +Test_rev_unit [label="rev_unit", URL=, fillcolor="#7FFFD4"] ; Test_rev_unit -> Test_distr_rev [] ; - Test_distr_rev -> Test_app_ass [] ; - Test_distr_rev -> Test_app_nil_end [] ; - Test_count_occ_inv_nil -> Test_list_ind [] ; - Test_count_occ_In -> Test_list_ind [] ; -subgraph cluster_Test { label="Test"; fillcolor="#FFFFC3"; labeljust=l; style=filled -subgraph cluster_Test_ReDun { label="ReDun"; fillcolor="#FFFFA3"; labeljust=l; style=filled -Test_ReDun_NoDup_nil; Test_ReDun_NoDup_cons; Test_ReDun_NoDup_ind; Test_ReDun_NoDup_remove_1; Test_ReDun_NoDup_remove_2; Test_ReDun_NoDup_Permutation; }; -Test_count_occ_In; Test_count_occ_inv_nil; Test_count_occ_nil; Test_count_occ_cons_eq; Test_count_occ_cons_neq; Test_distr_rev; Test_rev_unit; Test_rev_involutive; Test_In_rev; Test_rev_length; Test_rev_nth; Test_rev_append_rev; Test_rev_alt; Test_rev_list_ind; Test_rev_ind; Test_perm_nil; Test_perm_skip; Test_perm_swap; Test_perm_trans; Test_Permutation_ind; Test_Permutation_nil; Test_Permutation_nil_cons; Test_Permutation_refl; Test_Permutation_sym; Test_Permutation_trans; Test_Permutation_in; Test_Permutation_app_tail; Test_Permutation_app_head; Test_Permutation_app; Test_Permutation_app_swap; Test_Permutation_cons_app; Test_Permutation_length; Test_Permutation_rev; Test_Permutation_ind_bis; Test_Permutation_app_inv; Test_Permutation_cons_inv; Test_Permutation_cons_app_inv; Test_Permutation_app_inv_l; Test_Permutation_app_inv_r; Test_in_map; Test_in_map_iff; Test_map_length; Test_map_nth; Test_map_app; Test_map_rev; Test_Permutation_map; Test_in_flat_map; Test_map_map; Test_map_ext; Test_fold_left_app; Test_fold_left_length; Test_fold_right_app; Test_fold_left_rev_right; Test_fold_symmetric; Test_existsb_exists; Test_existsb_nth; Test_forallb_forall; Test_filter_In; Test_in_split_l; Test_list_ind; Test_in_split_r; Test_split_nth; Test_split_length_l; Test_split_length_r; Test_split_combine; Test_combine_split; Test_in_combine_l; Test_size_nil; Test_in_combine_r; Test_combine_length; Test_combine_nth; Test_nil_cons; Test_head_nil; Test_in_prod_aux; Test_head_cons; Test_in_prod; Test_in_eq; Test_in_prod_iff; Test_in_cons; Test_prod_length; Test_in_nil; Test_In_split; Test_lel_refl; Test_in_inv; Test_lel_trans; Test_lel_cons_cons; Test_app_cons_not_nil; Test_lel_cons; Test_app_nil_end; Test_lel_tail; Test_app_ass; Test_lel_nil; Test_ass_app; Test_app_comm_cons; Test_incl_refl; Test_app_eq_nil; Test_incl_tl; Test_app_eq_unit; Test_incl_tran; Test_app_inj_tail; Test_incl_appl; Test_app_length; Test_incl_appr; Test_in_app_or; Test_incl_cons; Test_in_or_app; Test_incl_app; Test_app_inv_head; Test_app_inv_tail; Test_firstn_skipn; Test_firstn_length; Test_removelast_firstn; Test_firstn_removelast; Test_nth_S_cons; Test_seq_length; Test_nth_In; Test_seq_nth; Test_nth_overflow; Test_seq_shift; Test_nth_indep; Test_app_nth1; Test_app_nth2; Test_remove_In; Test_app_removelast_last; Test_removelast_app; }; -} /* END */ +Test_seq_length [label="seq_length", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_seq_nth [label="seq_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_seq_shift [label="seq_shift", URL=, peripheries=3, fillcolor="#7FFFD4"] ; +Test_size_nil [label="size_nil", URL=, peripheries=3, fillcolor="#FFB57F"] ; +Test_split_combine [label="split_combine", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_split_combine -> Test_list_ind [] ; +Test_split_length_l [label="split_length_l", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_split_length_l -> Test_list_ind [] ; +Test_split_length_r [label="split_length_r", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_split_length_r -> Test_list_ind [] ; +Test_split_nth [label="split_nth", URL=, peripheries=3, fillcolor="#7FFFD4"] ; + Test_split_nth -> Test_list_ind [] ; diff --git a/tests/graph2.dot.oracle b/tests/graph2.dot.oracle index 53b16808d..dc32c3963 100644 --- a/tests/graph2.dot.oracle +++ b/tests/graph2.dot.oracle @@ -1,78 +1,78 @@ digraph tests/graph2 { +} /* END */ + _eq_ind -> _eq [] ; +_eq_ind [label="eq_ind", URL=<.html#eq_ind>, fillcolor="#7FFFD4"] ; + _eq_ind_r -> _eq_ind [] ; + _eq_ind_r -> _eq_sym [] ; +_eq_ind_r [label="eq_ind_r", URL=<.html#eq_ind_r>, fillcolor="#7FFFD4"] ; +_eq [label="eq", URL=<.html#eq>, fillcolor="#E2CDFA"] ; +_eq_refl [label="eq_refl", URL=<.html#eq_refl>, fillcolor="#7FAAFF"] ; + _eq_sym -> _eq [] ; + _eq_sym -> _eq_refl [] ; +_eq_sym [label="eq_sym", URL=<.html#eq_sym>, fillcolor="#7FFFD4"] ; graph [ratio=0.5] node [style=filled] -Test_Permutation_app_swap [label="Permutation_app_swap", URL=, peripheries=3, fillcolor="#7FFFD4"] ; -Test_Permutation_sym [label="Permutation_sym", URL=, fillcolor="#7FFFD4"] ; -Test_app_nil_end [label="app_nil_end", URL=, fillcolor="#7FFFD4"] ; +subgraph cluster_Test { label="Test"; fillcolor="#FFFFC3"; labeljust=l; style=filled + Test_app_comm_cons -> _eq [] ; + Test_app_comm_cons -> _eq_refl [] ; Test_app_comm_cons [label="app_comm_cons", URL=, fillcolor="#7FFFD4"] ; -Test_Permutation_refl [label="Permutation_refl", URL=, fillcolor="#7FFFD4"] ; -Test_list_ind [label="list_ind", URL=, fillcolor="#7FFFD4"] ; -_eq_ind [label="eq_ind", URL=<.html#eq_ind>, fillcolor="#7FFFD4"] ; -_eq_ind_r [label="eq_ind_r", URL=<.html#eq_ind_r>, fillcolor="#7FFFD4"] ; -Test_Permutation_trans [label="Permutation_trans", URL=, fillcolor="#7FFFD4"] ; + Test_app_comm_cons -> Test_app [] ; Test_app [label="app", URL=, fillcolor="#F070D1"] ; -Test_Permutation [label="Permutation", URL=, fillcolor="#E2CDFA"] ; + Test_app_nil_end -> _eq_ind [] ; + Test_app_nil_end -> _eq_refl [] ; +Test_app_nil_end [label="app_nil_end", URL=, fillcolor="#7FFFD4"] ; + Test_app_nil_end -> Test_app [] ; + Test_app_nil_end -> Test_list_ind [] ; + Test_app -> Test_cons [] ; + Test_app -> Test_list [] ; +Test_cons [label="cons", URL=, fillcolor="#7FAAFF"] ; +Test_list_ind [label="list_ind", URL=, fillcolor="#7FFFD4"] ; + Test_list_ind -> Test_cons [] ; + Test_list_ind -> Test_list [] ; + Test_list_ind -> Test_nil [] ; Test_list [label="list", URL=, fillcolor="#E2CDFA"] ; +Test_nil [label="nil", URL=, fillcolor="#7FAAFF"] ; +Test_perm_nil [label="perm_nil", URL=, fillcolor="#7FAAFF"] ; + Test_perm_nil -> Test_cons [] ; + Test_perm_nil -> Test_list [] ; + Test_perm_nil -> Test_nil [] ; Test_perm_skip [label="perm_skip", URL=, fillcolor="#7FAAFF"] ; + Test_perm_skip -> Test_cons [] ; + Test_perm_skip -> Test_list [] ; + Test_perm_skip -> Test_nil [] ; Test_perm_swap [label="perm_swap", URL=, fillcolor="#7FAAFF"] ; -Test_nil [label="nil", URL=, fillcolor="#7FAAFF"] ; -Test_cons [label="cons", URL=, fillcolor="#7FAAFF"] ; + Test_perm_swap -> Test_cons [] ; + Test_perm_swap -> Test_list [] ; + Test_perm_swap -> Test_nil [] ; Test_perm_trans [label="perm_trans", URL=, fillcolor="#7FAAFF"] ; -_eq_sym [label="eq_sym", URL=<.html#eq_sym>, fillcolor="#7FFFD4"] ; -_eq [label="eq", URL=<.html#eq>, fillcolor="#E2CDFA"] ; -_eq_refl [label="eq_refl", URL=<.html#eq_refl>, fillcolor="#7FAAFF"] ; -Test_perm_nil [label="perm_nil", URL=, fillcolor="#7FAAFF"] ; -Test_Permutation_ind [label="Permutation_ind", URL=, fillcolor="#7FFFD4"] ; - Test_Permutation_app_swap -> Test_Permutation_sym [] ; - Test_Permutation_app_swap -> Test_app_nil_end [] ; + Test_perm_trans -> Test_cons [] ; + Test_perm_trans -> Test_list [] ; + Test_perm_trans -> Test_nil [] ; + Test_Permutation_app_swap -> _eq_ind_r [] ; +Test_Permutation_app_swap [label="Permutation_app_swap", URL=, peripheries=3, fillcolor="#7FFFD4"] ; Test_Permutation_app_swap -> Test_app_comm_cons [] ; + Test_Permutation_app_swap -> Test_app_nil_end [] ; Test_Permutation_app_swap -> Test_Permutation_refl [] ; - Test_Permutation_app_swap -> _eq_ind_r [] ; + Test_Permutation_app_swap -> Test_Permutation_sym [] ; Test_Permutation_app_swap -> Test_Permutation_trans [] ; +Test_Permutation_ind [label="Permutation_ind", URL=, fillcolor="#7FFFD4"] ; +Test_Permutation_ind; Test_perm_nil; Test_perm_trans; Test_cons; Test_nil; Test_perm_swap; Test_perm_skip; Test_list; Test_Permutation; Test_app; Test_Permutation_trans; Test_list_ind; Test_Permutation_refl; Test_app_comm_cons; Test_app_nil_end; Test_Permutation_sym; Test_Permutation_app_swap; }; + Test_Permutation_ind -> Test_Permutation [] ; +Test_Permutation [label="Permutation", URL=, fillcolor="#E2CDFA"] ; +Test_Permutation_refl [label="Permutation_refl", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_refl -> Test_list_ind [] ; + Test_Permutation_refl -> Test_perm_nil [] ; + Test_Permutation_refl -> Test_perm_skip [] ; + Test_Permutation_refl -> Test_Permutation [] ; +Test_Permutation_sym [label="Permutation_sym", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_sym -> Test_perm_nil [] ; Test_Permutation_sym -> Test_perm_skip [] ; Test_Permutation_sym -> Test_perm_swap [] ; Test_Permutation_sym -> Test_perm_trans [] ; - Test_Permutation_sym -> Test_perm_nil [] ; Test_Permutation_sym -> Test_Permutation_ind [] ; - Test_app_nil_end -> Test_list_ind [] ; - Test_app_nil_end -> _eq_ind [] ; - Test_app_nil_end -> Test_app [] ; - Test_app_nil_end -> _eq_refl [] ; - Test_app_comm_cons -> Test_app [] ; - Test_app_comm_cons -> _eq [] ; - Test_app_comm_cons -> _eq_refl [] ; - Test_Permutation_refl -> Test_list_ind [] ; - Test_Permutation_refl -> Test_Permutation [] ; - Test_Permutation_refl -> Test_perm_skip [] ; - Test_Permutation_refl -> Test_perm_nil [] ; - Test_list_ind -> Test_list [] ; - Test_list_ind -> Test_nil [] ; - Test_list_ind -> Test_cons [] ; - _eq_ind -> _eq [] ; - _eq_ind_r -> _eq_ind [] ; - _eq_ind_r -> _eq_sym [] ; - Test_Permutation_trans -> Test_Permutation [] ; - Test_Permutation_trans -> Test_perm_trans [] ; - Test_app -> Test_list [] ; - Test_app -> Test_cons [] ; + Test_Permutation -> Test_cons [] ; Test_Permutation -> Test_list [] ; Test_Permutation -> Test_nil [] ; - Test_Permutation -> Test_cons [] ; - Test_perm_skip -> Test_list [] ; - Test_perm_skip -> Test_nil [] ; - Test_perm_skip -> Test_cons [] ; - Test_perm_swap -> Test_list [] ; - Test_perm_swap -> Test_nil [] ; - Test_perm_swap -> Test_cons [] ; - Test_perm_trans -> Test_list [] ; - Test_perm_trans -> Test_nil [] ; - Test_perm_trans -> Test_cons [] ; - _eq_sym -> _eq [] ; - _eq_sym -> _eq_refl [] ; - Test_perm_nil -> Test_list [] ; - Test_perm_nil -> Test_nil [] ; - Test_perm_nil -> Test_cons [] ; - Test_Permutation_ind -> Test_Permutation [] ; -subgraph cluster_Test { label="Test"; fillcolor="#FFFFC3"; labeljust=l; style=filled -Test_Permutation_ind; Test_perm_nil; Test_perm_trans; Test_cons; Test_nil; Test_perm_swap; Test_perm_skip; Test_list; Test_Permutation; Test_app; Test_Permutation_trans; Test_list_ind; Test_Permutation_refl; Test_app_comm_cons; Test_app_nil_end; Test_Permutation_sym; Test_Permutation_app_swap; }; -} /* END */ +Test_Permutation_trans [label="Permutation_trans", URL=, fillcolor="#7FFFD4"] ; + Test_Permutation_trans -> Test_perm_trans [] ; + Test_Permutation_trans -> Test_Permutation [] ; diff --git a/tests/graph2.dpd.oracle b/tests/graph2.dpd.oracle index 94f186f98..c39b75191 100644 --- a/tests/graph2.dpd.oracle +++ b/tests/graph2.dpd.oracle @@ -1,25 +1,3 @@ -N: 184 "Permutation_app_swap" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 205 "Permutation_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 188 "Permutation_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 185 "Permutation_sym" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 192 "Permutation_trans" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 193 "app" [body=yes, kind=cnst, prop=no, path="Test", ]; -N: 187 "app_comm_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 186 "app_nil_end" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 190 "eq_ind" [body=yes, kind=cnst, prop=yes, ]; -N: 191 "eq_ind_r" [body=yes, kind=cnst, prop=yes, ]; -N: 201 "eq_sym" [body=yes, kind=cnst, prop=yes, ]; -N: 189 "list_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; -N: 194 "Permutation" [kind=inductive, prop=no, path="Test", ]; -N: 202 "eq" [kind=inductive, prop=no, ]; -N: 195 "list" [kind=inductive, prop=no, path="Test", ]; -N: 204 "perm_nil" [kind=construct, prop=yes, path="Test", ]; -N: 203 "eq_refl" [kind=construct, prop=yes, ]; -N: 198 "nil" [kind=construct, prop=no, path="Test", ]; -N: 196 "perm_skip" [kind=construct, prop=yes, path="Test", ]; -N: 199 "cons" [kind=construct, prop=no, path="Test", ]; -N: 197 "perm_swap" [kind=construct, prop=yes, path="Test", ]; -N: 200 "perm_trans" [kind=construct, prop=yes, path="Test", ]; E: 184 185 [weight=3, ]; E: 184 186 [weight=2, ]; E: 184 187 [weight=1, ]; @@ -93,3 +71,25 @@ E: 205 194 [weight=14, ]; E: 205 195 [weight=30, ]; E: 205 198 [weight=4, ]; E: 205 199 [weight=12, ]; +N: 184 "Permutation_app_swap" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 185 "Permutation_sym" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 186 "app_nil_end" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 187 "app_comm_cons" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 188 "Permutation_refl" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 189 "list_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 190 "eq_ind" [body=yes, kind=cnst, prop=yes, ]; +N: 191 "eq_ind_r" [body=yes, kind=cnst, prop=yes, ]; +N: 192 "Permutation_trans" [body=yes, kind=cnst, prop=yes, path="Test", ]; +N: 193 "app" [body=yes, kind=cnst, prop=no, path="Test", ]; +N: 194 "Permutation" [kind=inductive, prop=no, path="Test", ]; +N: 195 "list" [kind=inductive, prop=no, path="Test", ]; +N: 196 "perm_skip" [kind=construct, prop=yes, path="Test", ]; +N: 197 "perm_swap" [kind=construct, prop=yes, path="Test", ]; +N: 198 "nil" [kind=construct, prop=no, path="Test", ]; +N: 199 "cons" [kind=construct, prop=no, path="Test", ]; +N: 200 "perm_trans" [kind=construct, prop=yes, path="Test", ]; +N: 201 "eq_sym" [body=yes, kind=cnst, prop=yes, ]; +N: 202 "eq" [kind=inductive, prop=no, ]; +N: 203 "eq_refl" [kind=construct, prop=yes, ]; +N: 204 "perm_nil" [kind=construct, prop=yes, path="Test", ]; +N: 205 "Permutation_ind" [body=yes, kind=cnst, prop=yes, path="Test", ]; diff --git a/tests/lexing.err.oracle b/tests/lexing.err.oracle index b6ee43a96..ccc007b13 100644 --- a/tests/lexing.err.oracle +++ b/tests/lexing.err.oracle @@ -1,2 +1,2 @@ -Info: read file tests/lexing.err.dpd Error: (line:2, character:11): illegal character '!'. +Info: read file tests/lexing.err.dpd diff --git a/tests/missing_node.err.oracle b/tests/missing_node.err.oracle index 795d2b22f..b7acf5881 100644 --- a/tests/missing_node.err.oracle +++ b/tests/missing_node.err.oracle @@ -1,2 +1,2 @@ -Info: read file tests/missing_node.err.dpd Error: no node with number 3: cannot build edge. +Info: read file tests/missing_node.err.dpd diff --git a/tests/parsing.err.oracle b/tests/parsing.err.oracle index 26d3a643c..beef9c76b 100644 --- a/tests/parsing.err.oracle +++ b/tests/parsing.err.oracle @@ -1,2 +1,2 @@ -Info: read file tests/parsing.err.dpd Error: parsing error (line:2, character:11-14). +Info: read file tests/parsing.err.dpd diff --git a/tests/search.oracle b/tests/search.oracle index 549951460..b59d2b01f 100644 --- a/tests/search.oracle +++ b/tests/search.oracle @@ -1,6 +1,6 @@ -Welcome to Coq -[Loading ML file dpdgraph.cmxs ... done] -Fetching opaque proofs from disk for dpdgraph.tests.Test +app_comm_cons(1) app_nil_end(2) Permutation_sym(3) ] [cons(42) nil(6) perm_swap(1) perm_skip(3) list(18) Permutation(11) app(43) +Fetching opaque proofs from disk for dpdgraph.tests.Test +[Loading ML file dpdgraph.cmxs ... done] Permutation_trans(3) eq_ind_r(1) eq_ind(2) list_ind(2) Permutation_refl(2) -app_comm_cons(1) app_nil_end(2) Permutation_sym(3) ] +Welcome to Coq diff --git a/tests/unterminated_comment.err.oracle b/tests/unterminated_comment.err.oracle index b9961ce87..6c11cb2ce 100644 --- a/tests/unterminated_comment.err.oracle +++ b/tests/unterminated_comment.err.oracle @@ -1,2 +1,2 @@ -Info: read file tests/unterminated_comment.err.dpd Error: unterminated comment (started near (line:3, character:13)). +Info: read file tests/unterminated_comment.err.dpd