Tomas Vondra <tomas(dot)vondra(at)2ndquadrant(dot)com> writes:
> BTW wouldn't it be possible to derive "traditional" proof in relational
> algebra, similarly to other transforms?
Perhaps. The patch depends on CTID, but you could probably model that
as a primary key in a proof.
regards, tom lane