If a Triple Graph Grammar rule counts as a Mathematical Proof
A TGG defines (generates) a language of triples of graphs.
This can be used for many things, including establishing a notion of correctness for forward and backward transformations.  So if you have some transformation A -> B, you can check if it is correct by checking if there exists some A &lt;-C->B that can be generated by the TGG.

Correct forward and backward transformations do not have to be bijections, although this could be enforced by analysing the TGG appropriately.

As a proof, one could use a TGG to generate proofs of consistency.  So given some A and B, I can prove that A and B are consistent (and whatever produced B from A or A from B correct), by determining a rule application sequence that takes you from some start triple graph to some A&lt;-C->B.

So for your concrete syntax tree and AST you could check for consistency without recomputing the trees.  In practice, however, such a consistency checker can actually be slower than a recomputation (but is sometimes still better, e.g., if the computation was non-deterministic or required some form of decision making).