Added more theorems. Added derive1 and derive0.