Entry	Value
Package Name	set-fold-def
Count	1
Theorems	FINITE_RECURSION : !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 (x INSERT s) = (if x IN s then ITSET f b s else f x (ITSET f b s)))

Back to main package page