A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas
above its position. This means the list is a topological order of the dependency graph.
An entry 'all subs proved' means that all used lemmas are (transitively) proved.
| Name: | Status: | Subs proved? | Used: |
|---|
| permut-correct | proved | all subs proved
| perm-all-perms-eq,
max-smaller-perms-all-perms,
greater-perms,
next-perm-greaterPerms,
next-perm-smallerPerms,
next-permutation,
smaller-perms,
toSet,
ordered-append,
next-proper-permutation,
ordered-smallerPerms,
nil-toSet,
ordered-arraylist-base0,
sort-def,
permut,
|
| next-proper-permutation | proved | all subs proved
| ordered-all-rev,
minimum-permutation,
ascending-order-is-min-permuted,
array-neg-le-eq-2,
lexicographic-rec1,
subarray-inc-offset0,
array-le-kill-prefix,
array-le-trans,
array-le-one-diffrent-position,
next-permutation,
rev-subarray-split-last-swap,
rev-subarray-split-step,
get-rev,
subarray-write-above,
remains-ordered-by-swap,
array-le-swap,
descending-order-is-max-permuted,
ordered-step-down,
ordered-size-smaller-one,
lexicographic-base1,
maximum-permutation,
next,
|
| ordered-smallerPerms | proved | all subs proved
| ordered-notsmaller,
smaller-perms,
|
| array-le-kill-prefix | proved | all subs proved
| array-le-refl,
array-le-same-prefix3,
array-split-into-subarrays,
array-le-trans,
array-le-same-prepart2,
|
| next-perm-smallerPerms | proved | all subs proved
| array-neg-le-eq,
array-le-trans,
array-neg-le-eq-2,
smaller-perms,
next-permutation,
|
| next-perm-greaterPerms | proved | all subs proved
| array-neg-le-eq,
array-neg-le-eq-2,
array-le-trans,
greater-perms,
next-permutation,
|
| ordered-notsmaller | proved | all subs proved
| array-neg-le-eq-2,
minimum-permutation,
ascending-order-is-min-permuted,
|
| array-le-same-prepart2 | proved | all subs proved
| array-le-same-prepart,
array-le-trans,
|
| ordered-append | proved | all subs proved
| smaller-perms,
toSet,
ordered-arraylist-append-last,
ordered-arraylist-base1,
ordered-arraylist-base0,
nil-toSet,
|
| array-le-swap | proved | all subs proved
| array-le-refl,
lexicographic-rec1,
|
| array-neg-le-eq-2 | proved | all subs proved
| lexicographic-rec1,
lexicographic-base3,
array-le-refl,
array-le-trans,
|
| array-le-same-prepart | proved | all subs proved
| array-le-same-prefix,
array-le-trans,
array-split-into-subarrays,
|
| ordered-arraylist-append-last | proved | all subs proved
| ordered-arraylist-base1,
ordered-arraylist-rec,
ordered-arraylist-two,
|
| array-le-same-prefix | proved | all subs proved
| lexicographic-base3,
lexicographic-rec1,
array-le-trans,
|
| array-le-same-prefix3 | proved | all subs proved
| array-le-same-prefix2,
|
| array-le-refl | proved | all subs proved
| array-le-trans,
lexicographic-rec1,
lexicographic-base1,
|
| max-smaller-perms-all-perms | proved | all subs proved
| maximum-permutation,
smaller-perms,
all-perms,
|
| perm-all-perms-eq | proved | all subs proved
| all-perms,
|
| ordered-arraylist-two | proved | all subs proved
| ordered-arraylist-base1,
ordered-arraylist-rec,
|
| nil-toSet | proved | all subs proved
| toSet,
|
| ordered-step-down | proved | all subs proved
| rev-mkarray-empty,
subarray-inc-offset0,
|
| descending-order-is-max-permuted | proved | all subs proved
| not-ordered,
lexicographic-rec1,
lexicographic-base1,
maximum-permutation,
|
| remains-ordered-by-swap | proved | all subs proved
| get-rev,
|
| rev-subarray-split-step | proved | all subs proved
| get-rev,
|
| rev-subarray-split-last-swap | proved | all subs proved
| get-rev,
|
| array-le-one-diffrent-position | proved | all subs proved
| subarray-inc-offset0,
lexicographic-rec1,
|
| ascending-order-is-min-permuted | proved | all subs proved
| lexicographic-rec1,
lexicographic-base1,
minimum-permutation,
|
| array-neg-le-eq | proved | all subs proved
| lexicographic-rec1,
lexicographic-base3,
lexicographic-base2,
|
| array-le-same-prefix2 | proved | all subs proved
| lexicographic-rec1,
|
| array-le-trans | proved | all subs proved
| lexicographic-rec1,
lexicographic-base3,
lexicographic-base2,
|
| next-perm | proved | all subs proved
| next,
|
| rev-subarray-last | proved | all subs proved
| subarray-inc,
|
| subarray-inc | proved | all subs proved
| |
| permut | axiom | | |
| sort-def | axiom | | |
| rev-mkarray-empty | proved | all subs proved
| |
| ordered-arraylist-rec | axiom | | |
| ordered-arraylist-base0 | axiom | | |
| ordered-arraylist-base1 | axiom | | |
| toSet | axiom | | |
| ordered-size-smaller-one | proved | all subs proved
| |
| subarray-write-above | proved | all subs proved
| |
| get-rev | proved | all subs proved
| |
| ordered-all-rev | proved | all subs proved
| |
| next-permutation | axiom | | |
| greater-perms | axiom | | |
| next | axiom | | |
| all-perms | axiom | | |
| smaller-perms | axiom | | |
| maximum-permutation | axiom | | |
| not-ordered | proved | all subs proved
| |
| minimum-permutation | axiom | | |
| lexicographic-base2 | axiom | | |
| lexicographic-base3 | axiom | | |
| lexicographic-base1 | axiom | | |
| lexicographic-rec1 | axiom | | |
| subarray-inc-offset0 | proved | all subs proved
| |
| array-split-into-subarrays | proved | all subs proved
| |