Entry Value
Package Name natural-funpow-thm
Count 7
Theorems
  • funpow_I : !n. funpow I n = I
  • funpow_add : !f m n. funpow f (m + n) = funpow f m o funpow f n
  • funpow_mult : !f m n. funpow f (m * n) = funpow (funpow f m) n
  • funpow_one : !f. funpow f 1 = f
  • funpow_suc' : !f n. funpow f (SUC n) = funpow f n o f
  • funpow_suc_x : !f n x. funpow f (SUC n) x = f (funpow f n x)
  • funpow_suc_x' : !f n x. funpow f (SUC n) x = funpow f n (f x)
  • Back to main package page