theory MySimplification+− imports Main+− begin+−