A x. E y. x = 2y
