Entry	Value
Package Name	natural-add-thm
Count	34
Theorems	ADD1 : !m. SUC m = m + 1 ADD_0 : !m. m + 0 = m ADD_ASSOC : !m n p. m + n + p = (m + n) + p ADD_EQ_0 : !m n. m + n = 0 <=> m = 0 /\ n = 0 ADD_SUC : !m n. m + SUC n = SUC (m + n) ADD_SYM : !m n. m + n = n + m BOUNDS_IGNORE : !p q. (?b. !i. p i <= q i + b) <=> (?b n. !i. n <= i ==> p i <= q i + b) EQ_ADD_LCANCEL : !m n p. m + n = m + p <=> n = p EQ_ADD_LCANCEL_0 : !m n. m + n = m <=> n = 0 EQ_ADD_RCANCEL : !p m n. m + p = n + p <=> m = n EQ_ADD_RCANCEL_0 : !m n. m + n = n <=> m = 0 LET_ADD2 : !m n p q. m <= p /\ n < q ==> m + n < p + q LE_ADD : !m n. m <= m + n LE_ADD2 : !m n p q. m <= p /\ n <= q ==> m + n <= p + q LE_ADDR : !m n. n <= m + n LE_ADD_LCANCEL : !m n p. m + n <= m + p <=> n <= p LE_ADD_LCANCEL_0 : !m n. m + n <= m <=> n = 0 LE_ADD_RCANCEL : !m n p. n + m <= p + m <=> n <= p LE_ADD_RCANCEL_0 : !m n. n + m <= m <=> n = 0 LE_EXISTS : !m n. m <= n <=> (?d. n = m + d) LE_INDUCT : !p. (!m. p m m) /\ (!m n. m <= n /\ p m n ==> p m (SUC n)) ==> (!m n. m <= n ==> p m n) LTE_ADD2 : !m n p q. m < p /\ n <= q ==> m + n < p + q LT_ADD : !m n. m < m + n <=> 0 < n LT_ADD2 : !m n p q. m < p /\ n < q ==> m + n < p + q LT_ADDR : !m n. n < m + n <=> 0 < m LT_ADD_LCANCEL : !m n p. m + n < m + p <=> n < p LT_ADD_LCANCEL_0 : !m n. ~(m + n < m) LT_ADD_RCANCEL : !m n p. n + m < p + m <=> n < p LT_ADD_RCANCEL_0 : !m n. ~(n + m < m) LT_EXISTS : !m n. m < n <=> (?d. n = m + SUC d) MAX_ADD_LCANCEL : !m n p. MAX (m + n) (m + p) = m + MAX n p MAX_ADD_RCANCEL : !m n p. MAX (n + m) (p + m) = MAX n p + m MIN_ADD_LCANCEL : !m n p. MIN (m + n) (m + p) = m + MIN n p MIN_ADD_RCANCEL : !m n p. MIN (n + m) (p + m) = MIN n p + m

Back to main package page