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:
Moreover, suppose f also unifies them: it's not hard to show that, for all variables v
(note (ko t' i) is extensionally equal to (iota[t'/i])>>)
How? koElim, of course! Cases:
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