Entry	Value
Package Name	natural-order-min-max-thm
Count	25
Theorems	LE_MAX : !m n p. m <= MAX n p <=> m <= n \/ m <= p LE_MAX1 : !m n. m <= MAX m n LE_MAX2 : !m n. n <= MAX m n LE_MIN : !m n p. m <= MIN n p <=> m <= n /\ m <= p LT_MAX : !m n p. m < MAX n p <=> m < n \/ m < p LT_MIN : !m n p. m < MIN n p <=> m < n /\ m < p MAX_COMM : !m n. MAX m n = MAX n m MAX_EQ_ZERO : !m n. MAX m n = 0 <=> m = 0 /\ n = 0 MAX_L0 : !n. MAX 0 n = n MAX_LE : !m n p. MAX n p <= m <=> n <= m /\ p <= m MAX_LT : !m n p. MAX n p < m <=> n < m /\ p < m MAX_R0 : !n. MAX n 0 = n MAX_REFL : !n. MAX n n = n MAX_SUC : !m n. MAX (SUC m) (SUC n) = SUC (MAX m n) MINIMAL_EQ : !p n. p n /\ (!m. m < n ==> ~p m) ==> (minimal) p = n MINIMAL_T : (minimal n. T) = 0 MIN_COMM : !m n. MIN m n = MIN n m MIN_L0 : !n. MIN 0 n = 0 MIN_LE : !m n p. MIN n p <= m <=> n <= m \/ p <= m MIN_LE1 : !m n. MIN m n <= m MIN_LE2 : !m n. MIN m n <= n MIN_LT : !m n p. MIN n p < m <=> n < m \/ p < m MIN_R0 : !n. MIN n 0 = 0 MIN_REFL : !n. MIN n n = n MIN_SUC : !m n. MIN (SUC m) (SUC n) = SUC (MIN m n)

Back to main package page