[isabelle] Comparing two graphs
I have two graphs, f :: real => (real * real) and g :: real => (real *
real) -- the output is simply the x and y value for the input x value.
Now, if if I have a lemma "f < g", I get an error saying
"No type arity prod :: ord"
I see that two pairs can't be compared with each other, but in my
situation I'd like to say that one is less than another if its y
(second) value is lower. As for comparing two such graphs, then it's a
matter of summing up all of the y (second) values and see which is
Does anyone know of a good way of achieving this kind of comparison?
Thanks a lot for your time.
This archive was generated by a fusion of
Pipermail (Mailman edition) and