Previous
Top
Next
General Recursion in Type Theory : Unification :
Termination?
Fortunately, there is a measure that allows us to prove that
unify'
terminates for all arguments.
...