% Recursion is admitted only with a termination proof. Length
% decreases structurally: T sits strictly inside #(H | T), and the
% checker that validates this is extracted from Rocq.

Rule name: "an empty list has length zero"
     head: [Length list: #() result: 0]
     body: [True]

Rule name: "a cons adds one"
     head: [Length list: #(H | T) result: R]
     body: [Length list: T result: P] :and
           [Plus left: 1 right: P result: R]

Query expression: [Length list: #(1 2 3) result: R]
Query expression: [Length list: #("a" "b") result: R]

% Mutual recursion under a shared lexicographic measure: Even and
% Odd pass a shrinking list back and forth.

Rule name: "the empty list is even"
     head: [Even list: #()]
     body: [True]

Rule name: "a cons flips even to odd"
     head: [Even list: #(H | T)]
     body: [Odd list: T]

Rule name: "a cons flips odd to even"
     head: [Odd list: #(H | T)]
     body: [Even list: T]

Query expression: [Even list: #(1 2 3 4)]
Query expression: [Even list: #(1 2 3)]