AG(((lamp = lit)->EX(lamp=unlit))*((lamp=unlit)->EX(lamp=lit)));