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