That's part of it. The core difficulties here are the definition of "inverse" and knowing when it's applicable to use the transformations. The former is difficu

That's part of it. The core difficulties here are the definition of "inverse" and knowing when it's applicable to use the transformations. The former is difficult to pin down in a totally formal yet useful form. The latter will in practice depend upon intuition; no one is going to back-compute invariants ("d = ab/c" is always legitimate in the larger context of "given b = ac*d ...")