Re: [isabelle] how to proof termination in "function" command?



Dear Yucy,

apply (relation "measure (\<lambda>(i,j). j + 1 - i)")

Your function has three arguments, so your measure function must be on triples. Then it works:

termination
by (relation "measure (\<lambda>(i,j,_). j + 1 - i)") auto

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.