mk: subo — contiguous sublist relation
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 32s

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.
This commit is contained in:
2026-05-08 11:45:31 +00:00
parent fc14a8063b
commit e202c81a0d
3 changed files with 70 additions and 0 deletions

View File

@@ -73,6 +73,15 @@
(define suffixo (fn (s l) (fresh (front) (appendo front s l))))
(define
subo
(fn
(s l)
(fresh
(front-and-s back front)
(appendo front-and-s back l)
(appendo front s front-and-s))))
(define
lengtho
(fn