Documentation Verification Report

MergeSort

📁 Source: Cslib/Algorithms/Lean/MergeSort/MergeSort.lean

Statistics

Metric	Count
Definitions `IsSorted`, `MinOfList`, `T`, `merge`, `mergeSort`, `timeMergeSortRec`	6
Theorems `clog2_floor_half_le`, `clog2_half_le`, `mem_either_merge`, `mergeSort_correct`, `mergeSort_perm`, `mergeSort_same_length`, `mergeSort_sorted`, `mergeSort_time`, `mergeSort_time_le`, `merge_perm`, `merge_ret_length_eq_sum`, `merge_time`, `min_all_merge`, `sorted_merge`, `timeMergeSortRec_le`	15
Total	21

Cslib.Algorithms.Lean.TimeM

Definitions

Name	Category	Theorems
`IsSorted` 📖	MathDef	2 math math: `mergeSort_sorted`, `mergeSort_correct`
`MinOfList` 📖	MathDef	—
`T` 📖	CompOp	1 math math: `timeMergeSortRec_le`
`merge` 📖	CompOp	5 math math: `merge_time`, `sorted_merge`, `merge_ret_length_eq_sum`, `merge_perm`, `min_all_merge`
`mergeSort` 📖	CompOp	6 math math: `mergeSort_time`, `mergeSort_sorted`, `mergeSort_same_length`, `mergeSort_time_le`, `mergeSort_perm`, `mergeSort_correct`
`timeMergeSortRec` 📖	CompOp	2 math math: `timeMergeSortRec_le`, `mergeSort_time_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clog2_floor_half_le` 📖	—	—	—	—	`clog2_half_le`
`clog2_half_le` 📖	—	—	—	—	—
`mem_either_merge` 📖	—	`ret` `merge`	—	—	`merge.induct_unfolding`
`mergeSort_correct` 📖	mathematical	—	`IsSorted` `ret` `mergeSort`	—	`mergeSort_sorted` `mergeSort_perm`
`mergeSort_perm` 📖	mathematical	—	`ret` `mergeSort`	—	`mergeSort.induct_unfolding` `merge_perm`
`mergeSort_same_length` 📖	mathematical	—	`ret` `mergeSort`	—	`mergeSort.induct_unfolding`
`mergeSort_sorted` 📖	mathematical	—	`IsSorted` `ret` `mergeSort`	—	`mergeSort.induct_unfolding` `sorted_merge`
`mergeSort_time` 📖	mathematical	—	`time` `mergeSort`	—	—
`mergeSort_time_le` 📖	mathematical	—	`time` `mergeSort` `timeMergeSortRec`	—	`mergeSort.induct_unfolding` `merge_time` `mergeSort_same_length` `timeMergeSortRec.eq_def`
`merge_perm` 📖	mathematical	—	`ret` `merge`	—	`merge.induct_unfolding`
`merge_ret_length_eq_sum` 📖	mathematical	—	`ret` `merge`	—	`merge.induct_unfolding`
`merge_time` 📖	mathematical	—	`time` `merge`	—	`merge.induct_unfolding`
`min_all_merge` 📖	mathematical	`MinOfList`	`ret` `merge`	—	—
`sorted_merge` 📖	mathematical	`IsSorted`	`ret` `merge`	—	`merge.induct_unfolding`
`timeMergeSortRec_le` 📖	mathematical	—	`timeMergeSortRec` `T`	—	`timeMergeSortRec.induct_unfolding`

---

← Back to Index