Entry | Value |
---|---|
Name | MIN_L0 |
Conclusion | !n. MIN 0 n = 0 |
Constructive Proof | Yes |
Axiom | (\a. a = (\b. (\c. c) = (\c. c))) (\d. (\e. d e) = d) (\a. a = (\b. (\c. c) = (\c. c))) (\d. (\e. e = (\f. (\c. c) = (\c. c))) (\g. (\h i. (\j k. (\l. l j k) = (\m. m ((\c. c) = (\c. c)) ((\c. c) = (\c. c)))) h i <=> h) (d g) (d ((@) d)))) |
Classical Lemmas | N|A |
Constructive Lemmas | |
Contained Package | natural-order-min-max-thm |
Comment | Standard HOL library retrieved from OpenTheory |