| Metric | Count |
|---|
Definitionsappend, concat, concatRec, concatRecAux, copy, drop, dropLast, reverse, reverseAux, tail, take | 11 |
Theoremsappend, eq_copy_nil, tail, append_assoc, append_concat, append_copy_copy, append_nil, append_reverseAux, append_take_drop_eq, coe_support_append, coe_support_append', concatRec_concat, concatRec_nil, concat_append, concat_cons, concat_dropLast, concat_eq_append, concat_inj, concat_ne_nil, concat_nil, cons_append, cons_copy, cons_nil_append, cons_reverseAux, cons_support_tail, cons_tail_eq, copy_cons, copy_copy, copy_nil, copy_rfl_rfl, dart_snd_mem_support_of_mem_darts, darts_append, darts_concat, darts_copy, darts_drop, darts_reverse, darts_take, dropLast_concat, dropLast_cons_cons, dropLast_cons_nil, dropLast_cons_of_not_nil, dropLast_nil, drop_add_eq, drop_add_heq, drop_cons_eq, drop_getVert, drop_length, drop_of_length_le, drop_support_eq_support_drop_min, drop_zero, edgeSet_append, edgeSet_concat, edgeSet_copy, edgeSet_reverse, edges_append, edges_concat, edges_copy, edges_drop, edges_nodup_of_support_nodup, edges_reverse, edges_take, exists_concat_eq_cons, exists_cons_eq_concat, ext_getVert, ext_getVert_le_length, ext_support, fst_mem_support_of_mem_edges, getVert_append, getVert_copy, getVert_mem_tail_support, getVert_reverse, getVert_tail, length_append, length_concat, length_copy, length_reverse, length_reverseAux, length_tail_add_one, mem_darts_reverse, mem_support_append_iff, mem_support_of_mem_edges, mem_tail_support_append_iff, nil_append, nil_append_iff, nil_copy, nil_drop_iff, nil_drop_of_length_le, nil_reverse, nil_take_iff, nodup_tail_support_reverse, not_nil_of_tail_not_nil, penultimate_concat, penultimate_reverse, reverseAux_append, reverseAux_eq_reverse_append, reverse_append, reverse_bijective, reverse_concat, reverse_cons, reverse_copy, reverse_injective, reverse_nil, reverse_reverse, reverse_singleton, reverse_surjective, reverse_toWalk, snd_mem_support_of_mem_edges, snd_reverse, subset_support_append_left, subset_support_append_right, support_append, support_append_eq_support_dropLast_append, support_concat, support_copy, support_eq_concat, support_injective, support_reverse, support_subset_support_concat, support_tail, support_tail_of_not_nil, tail_cons, tail_cons_eq, tail_cons_nil, tail_nil, tail_support_append, take_add_eq, take_add_heq, take_cons_eq, take_getVert, take_length, take_of_length_le, take_support_eq_support_take_succ, take_zero | 133 |
| Total | 144 |
| Name | Category | Theorems |
|---|
append 📖 | CompOp | 41 mathmath: concat_eq_append, nil_append_iff, cons_append, reverse_append, getVert_append, cons_nil_append, subset_support_append_left, take_spec, append_take_drop_eq, append_copy_copy, coe_support_append, transfer_append, mem_support_iff_exists_append, append_reverseAux, mem_tail_support_append_iff, subset_support_append_right, append_assoc, length_append, take_add_heq, IsPath.mem_support_iff_exists_append, toSubgraph_append, support_append_eq_support_dropLast_append, support_append, reverseAux_append, Nil.append, darts_append, edges_append, edgeSet_append, takeUntil_append_of_mem_left, map_append, concat_append, reverse_cons, append_nil, tail_support_append, take_add_eq, nil_append, nil_isSubwalk_iff_exists, coe_support_append', append_concat, reverseAux_eq_reverse_append, mem_support_append_iff
|
concat 📖 | CompOp | 24 mathmath: concat_eq_append, SimpleGraph.walkLengthTwoEquivCommonNeighbors_symm_apply_coe, edges_concat, concatRec_concat, penultimate_concat, darts_concat, exists_concat_eq_cons, isSubwalk_concat, concat_dropLast, IsPath.concat, edgeSet_concat, support_concat, length_concat, support_subset_support_concat, exists_cons_eq_concat, SimpleGraph.IsAcyclic.path_concat, concat_nil, concat_cons, dropLast_concat, IsSubwalk.concat, concat_append, append_concat, concat_isPath_iff, reverse_concat
|
concatRec 📖 | CompOp | 2 mathmath: concatRec_concat, concatRec_nil
|
concatRecAux 📖 | CompOp | — |
copy 📖 | CompOp | 40 mathmath: edges_copy, nil_copy, copy_rfl_rfl, map_copy, take_zero, concat_inj, darts_copy, bypass_copy, drop_zero, IsSubwalk.copy, support_copy, tail_cons_eq, cons_copy, toDeleteEdges_copy, isCycle_copy, append_copy_copy, dropLast_cons_of_not_nil, edgeSet_copy, Nil.eq_copy_nil, take_of_length_le, reverse_copy, tail_cons, getVert_copy, isPath_copy, isTrail_copy, dropUntil_eq_drop, takeUntil_eq_take, length_copy, drop_add_eq, drop_of_length_le, copy_copy, isSubwalk_nil_iff, dropLast_concat, map_eq_of_eq, copy_nil, take_cons_eq, isCircuit_copy, take_add_eq, drop_cons_eq, copy_cons
|
drop 📖 | CompOp | 18 mathmath: drop_zero, nil_drop_of_length_le, drop_isSubwalk_drop, isSubwalk_drop, append_take_drop_eq, darts_drop, nil_drop_iff, drop_add_heq, dropUntil_eq_drop, take_add_heq, drop_getVert, drop_length, edges_drop, drop_add_eq, drop_of_length_le, take_add_eq, drop_cons_eq, drop_support_eq_support_drop_min
|
dropLast 📖 | CompOp | 7 mathmath: concat_dropLast, dropLast_cons_nil, dropLast_cons_of_not_nil, dropLast_nil, dropLast_cons_cons, dropLast_concat, IsSubwalk.dropLast
|
reverse 📖 | CompOp | 33 mathmath: reverse_nil, reverse_toWalk, reverse_injective, toSubgraph_reverse, penultimate_reverse, reverse_surjective, getVert_reverse, edgeSet_reverse, reverse_append, reverse_transfer, mem_darts_reverse, reverse_copy, darts_reverse, SimpleGraph.Path.reverse_coe, reverse_bijective, isPath_reverse_iff, reverse_map, snd_reverse, IsCycle.reverse, IsTrail.reverse, length_reverse, nodup_tail_support_reverse, edges_reverse, reverse_singleton, reverse_isTrail_iff, support_reverse, reverse_cons, nil_reverse, IsPath.reverse, isCycle_reverse, reverseAux_eq_reverse_append, reverse_reverse, reverse_concat
|
reverseAux 📖 | CompOp | 5 mathmath: length_reverseAux, cons_reverseAux, append_reverseAux, reverseAux_append, reverseAux_eq_reverse_append
|
tail 📖 | CompOp | 18 mathmath: length_tail_add_one, tail_nil, IsHamiltonianCycle.isHamiltonian_tail, isHamiltonianCycle_isCycle_and_isHamiltonian_tail, getVert_tail, tail_cons_nil, tail_cons_eq, isCycle_iff_isPath_tail_and_le_length, Nil.tail, tail_cons, IsPath.disjoint_support_of_append, support_tail, support_tail_of_not_nil, IsPath.tail, cons_support_tail, IsSubwalk.tail, cons_tail_eq, IsCycle.isPath_tail
|
take 📖 | CompOp | 15 mathmath: nil_take_iff, edges_take, darts_take, take_zero, append_take_drop_eq, take_of_length_le, take_length, isSubwalk_take, takeUntil_eq_take, take_add_heq, take_isSubwalk_take, take_cons_eq, take_getVert, take_add_eq, take_support_eq_support_take_succ
|