Next: conclusions | Prev: bounded mgu | Up: contents


Green knockout-extension is just red (constructor) knockout-extension lifted to handle failure.

The flex-rigid case just calls the occur check, which either signals failure or manufactures the compressed term ready for knockout. It's correct provided t is not a leaf, which you can check from bmgu is always the case; applying checkElim, there are two possibilities:

The flex-flex case just uses thick to compare and compress j. Unsurprisingly, the correctness proof proceeds by thickElim, yielding trivial maximality for the identity, or the same proof as above in the case of variable coalescence.


Next: conclusions | Prev: bounded mgu | Up: contents


Conor's Work Page