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