Entry	Value
Package Name	natural-exp-thm
Count	25
Theorems	EQ_EXP : !x m n. x EXP m = x EXP n <=> (if x = 0 then m = 0 <=> n = 0 else x = 1 \/ m = n) EVEN_EXP : !m n. EVEN (m EXP n) <=> EVEN m /\ ~(n = 0) EVEN_ODD_DECOMPOSITION : !n. (?k m. ODD m /\ n = 2 EXP k * m) <=> ~(n = 0) EXP_1 : !n. n EXP 1 = n EXP_2 : !n. n EXP 2 = n * n EXP_ADD : !m n p. m EXP (n + p) = m EXP n * m EXP p EXP_EQ_0 : !m n. m EXP n = 0 <=> m = 0 /\ ~(n = 0) EXP_EQ_1 : !x n. x EXP n = 1 <=> x = 1 \/ n = 0 EXP_LT_0 : !n x. 0 < x EXP n <=> ~(x = 0) \/ n = 0 EXP_MONO_EQ : !x y n. x EXP n = y EXP n <=> x = y \/ n = 0 EXP_MONO_LE : !x y n. x EXP n <= y EXP n <=> x <= y \/ n = 0 EXP_MONO_LE_IMP : !x y n. x <= y ==> x EXP n <= y EXP n EXP_MONO_LT : !x y n. x EXP n < y EXP n <=> x < y /\ ~(n = 0) EXP_MONO_LT_IMP : !x y n. x < y /\ ~(n = 0) ==> x EXP n < y EXP n EXP_MULT : !m n p. m EXP (n * p) = m EXP n EXP p EXP_ONE : !n. 1 EXP n = 1 EXP_ZERO : !n. 0 EXP n = (if n = 0 then 1 else 0) LE_EXP : !x m n. x EXP m <= x EXP n <=> (if x = 0 then m = 0 ==> n = 0 else x = 1 \/ m <= n) LT_EXP : !x m n. x EXP m < x EXP n <=> 2 <= x /\ m < n \/ x = 0 /\ ~(m = 0) /\ n = 0 LT_POW2_REFL : !n. n < 2 EXP n MOD_EXP_MOD' : !n m p. ~(n = 0) ==> (m MOD n) EXP p MOD n = m EXP p MOD n MOD_MOD_EXP_MIN : !x p m n. ~(p = 0) ==> x MOD p EXP m MOD p EXP n = x MOD p EXP MIN m n MULT_EXP : !p m n. (m * n) EXP p = m EXP p * n EXP p ODD_EXP : !m n. ODD (m EXP n) <=> ODD m \/ n = 0 large_exp : !k n. 1 < k ==> (?m. n <= k EXP m)

Back to main package page