diff --git a/papers/scp/PLFA.tex b/papers/scp/PLFA.tex index cd74ac64..1c6196cf 100755 --- a/papers/scp/PLFA.tex +++ b/papers/scp/PLFA.tex @@ -499,7 +499,7 @@ cases deal with the situation where there are potentially two different reductions; each case is trivially shown to be impossible. Five of the ten cases are redundant, as they just involve switching the order of the arguments. We had to copy the cases -nsuitably permuted. It would be preferable to reinvoke the proof on +suitably permuted. It would be preferable to reinvoke the proof on switched arguments, but this would not pass Agda's termination checker since swapping the arguments doesn't yield a recursive call on structurally smaller arguments. The proof of determinism in SF