a & ( G (a -> ( X a ) ) ) 
G (a -> ( X ( X ( - a ) ) ) ) 
