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: |
|---|---|---|---|
| sgn-05 | proved | all subs proved | sgn-04, |
| sgn-04 | proved | all subs proved | sgn-01, |
| sgn-03 | proved | all subs proved | Sign-neg, sgn-01, |
| odd-add | proved | all subs proved | even-add, odd-even-rew, |
| max-02 | proved | all subs proved | Max-right, max-c, max-a, max, |
| sgn-01 | proved | all subs proved | Sign-neg, sgn+1, |
| odd-even-rew | proved | all subs proved | even-odd-rew, |
| max | proved | all subs proved | Max-left, max-c, max-a, Max-right, |
| sr | proved | all subs proved | sgn+1, sgn-02, |
| sgn-09 | proved | all subs proved | sgn+1, |
| sgn-08 | proved | all subs proved | Sign-neg, sgn+1, |
| sgn-02-01 | proved | all subs proved | Sign-neg, sgn+1, |
| max-04 | proved | all subs proved | max-c, max-a, max-01, |
| max-03 | proved | all subs proved | max-c, max-a, max-01, |
| sgn+1 | proved | all subs proved | sgn-02, sgn, |
| even-odd-rew | proved | all subs proved | not-even-odd, |
| even-add | proved | all subs proved | odd-def-mod, even-def-mod, |
| max-c | proved | all subs proved | Max-left, max-a, Max-right, |
| sgn-07 | proved | all subs proved | sgn-06, |
| min-right | proved | all subs proved | Min-right, min-c, min-a, Min-left, |
| min-abs-zero-01 | proved | all subs proved | Min-right, min-c, min-a, Min-left, |
| min-abs-zero | proved | all subs proved | Min-right, min-c, min-a, Min-left, |
| min-03 | proved | all subs proved | Min-right, min-c, min-a, Min-left, |
| min-02 | proved | all subs proved | Min-right, min-c, min-a, Min-left, |
| min-01 | proved | all subs proved | Min-right, min-c, min-a, Min-left, |
| min | proved | all subs proved | Min-right, min-c, min-a, Min-left, |
| sgn-06 | proved | all subs proved | sgn-02, |
| sgn | proved | all subs proved | Sign-neg, Sign-pos, sgn-02, |
| min-c | proved | all subs proved | Min-right, min-a, Min-left, |
| max-a | proved | all subs proved | max-01, Max-left, Max-right, |
| not-even-odd | proved | all subs proved | even-def, not-odd-ex, |
| odd-def-mod | proved | all subs proved | not-odd-ex, |
| not-even-mod2 | proved | all subs proved | even-def-mod, |
| even-rec | proved | all subs proved | even-def, even-not, |
| even-mult | proved | all subs proved | even-def-mod, |
| even-2 | proved | all subs proved | even-def-mod, |
| sgn-02 | proved | all subs proved | Sign-neg, Sign-pos, |
| not-odd-ex | proved | all subs proved | odd-def, |
| min-a | proved | all subs proved | Min-right, Min-left, |
| max-01 | proved | all subs proved | Max-left, Max-right, |
| even-not | proved | all subs proved | even-def, |
| even-def-mod | proved | all subs proved | even-def, |
| sgn-1 | proved | all subs proved | Sign-neg, |
| sgn-01-01 | proved | all subs proved | Sign-neg, |
| odd-zero | proved | all subs proved | odd-def, |
| odd-two | proved | all subs proved | odd-def, |
| odd-rec | proved | all subs proved | odd-def, |
| odd-one | proved | all subs proved | odd-def, |
| even-zero | proved | all subs proved | even-def, |
| Sign-pos | axiom | ||
| Sign-neg | axiom | ||
| odd-def | axiom | ||
| Min-left | axiom | ||
| Min-right | axiom | ||
| Max-right | axiom | ||
| Max-left | axiom | ||
| even-def | axiom |