Finite function order check

[wwitzel]

trafficstars

In order to avoid Curry's paradox, we need to check that every expression (including and especially instantiations that are lambda maps) has an acyclic graph of edges from operators to operands. If there is a cycle, that would mean that we cannot assign a finite order to every operator. If there are no such cycles in any expression that shows up in a proof (including instantiations), it should be possible to assign a finite order to every operator (and lambda map instantiation which may not show up explicitly in any judgement because we immediately perform beta reduction).

Let's take our time in deciding how to implement this efficiently and with full rigor. But we can start thinking about this.