The name "sorted_wrt" came from Manuel and I would like to keep it. For
transtive predicates it is the same as sorted (I will add that lemma to List).
I looked into your theory but did not find any further generic lemmas about
"linked". Let me know if I missed any that should go into List.
To
I agree that this predicate probably has more general uses than
sortedness. Other possible names could be "successively" or "consecutively".
One might, however, still consider keeping "sorted_wrt" around (perhaps
as an (input) abbreviation, perhaps with a more restrictive type class
constraint) be
Dear Tobias,
I think your "sorted_wrt" is almost (modulo "fun" vs. "inductive") my
"linked" from the AFP (Efficient_Mergesort).
https://www.isa-afp.org/browser_info/current/AFP/Efficient-Mergesort/Efficient_Sort.html
Maybe we could unify the constants/names somehow?
At the moment I somewhat pr
