(and
 (=> (and (= X Y) (= X {+ 1 {* -1 Y}})) (= {* 2 X} 1))
 (= (F {+ X Y}) (F {+ Y X}))
 (=> (and (= X {* 2 Y}) (= Y {* 4 X})) (= (G X Y) (G 0 0)))
 (= (F 1) (F {+ {* 2 X} {* -1 {+ -1 {* 2 X}}}}))
 (=> (and (= X Y) (= X {+ 1 {* -1 Y}})) (= (FOO {+ X Y}) (FOO 1))))