giles e202c81a0d mk: subo — contiguous sublist relation ...

Composes two appendos: l = front ++ s ++ back, equivalently
  (appendo front-and-s back l) and (appendo front s front-and-s).

Goal order matters: doing the (appendo ground:l) split first makes the
search finitary; the second appendo is then deterministic given
front-and-s and ground s. Reversing the order causes divergence on
failing inputs (the front search becomes unbounded).

7 new tests, 405/405 cumulative.

2026-05-08 11:45:31 +00:00

924 B

Raw Blame History

View Raw