Summary

The decreases clause is required on pure recursive functions for Z3 to discharge termination, but not on effectful recursive functions. SKILL.md states this rule but it's easy for an agent (or a human) to miss — the rule appears in passing inside the "Recursion" section, several thousand lines after the canonical FizzBuzz example which omits decreases without comment.

Discovery context

Two separate agents writing Conway's Life on current main reached the same uncertainty point: when implementing a recursive run_loop with <IO> effects, do I need a decreases clause? Both agents had to triangulate by:

1. Looking at FizzBuzz (recursive IO, no decreases) → suggests "no"
2. Looking at the State combinator example (recursive State, with decreases) → suggests "yes"
3. Searching SKILL.md for the rule explicitly → finds it eventually

Triangulation took multiple minutes per agent and one ended up adding decreases defensively before realising it wasn't needed.

The current language in SKILL.md (line 559 area):

"For pure recursive functions that need termination proofs, add a decreases clause (see Recursion). Effectful recursive functions like the loop above do not require decreases."

This is correct but buried inside a paragraph about a specific example.

Proposed fix

Add the rule as a one-line callout near the top of the recursion section, or as an explicit "Quick rules" entry near the function-definition template at the top of the SKILL. Suggested phrasing:

decreases is required when: the function is recursive and effects(pure). Effectful recursive functions (<IO>, <State>, <Http>, etc.) do not require decreases — termination is treated as an effect-system concern.

Plus: a quick checklist near the recursion section ("checklist before writing a recursive function: …") would help.

Acceptance

• An agent reading SKILL.md and reaching the recursion section can answer the question "do I need decreases here?" in one read, without cross-referencing two example programs.
• The rule is searchable for the keywords agents actually use: decreases, recursion, termination, effectful, pure.