|
Theorems |
FINITE_RECURSION_DELETE : !f b.
(!x y s. ~(x = y) ==> f x (f y s) = f y (f x s))
==> ITSET f b {} = b /\
(!x s.
FINITE s
==> ITSET f b s =
(if x IN s
then f x (ITSET f b (s DELETE x))
else ITSET f b (s DELETE x)))ITSET_EQ : !f g b s.
FINITE s /\
(!x. x IN s ==> f x = g x) /\
(!x y s. ~(x = y) ==> f x (f y s) = f y (f x s)) /\
(!x y s. ~(x = y) ==> g x (g y s) = g y (g x s))
==> ITSET f b s = ITSET g b s |
