> For the complete documentation index, see [llms.txt](https://docs.moduluszk.io/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.moduluszk.io/predicates-in-practice/what-the-examples-establish-and-their-limits.md).

# What the examples establish, and their limits

Both contracts fit on a page because the rule and the artifact are the same object. Neither uses anything beyond arithmetic, order, and equality, plus the abstract authorisation relation and the flagged stand-ins of the ground rules, so the distance between these illustrations and predicates the shipped language accepts is exactly the set of open items this documentation already names, never the shape of the logic. Every inequality on this page was checked mechanically against the behaviour it renders: the trading rule against the exact output formula of the design it mirrors, across two hundred thousand random cases and tight at the boundary, and the lending inequalities against exact rational arithmetic. That designs of exactly this kind, markets and lending pools, render onto a predicate chain is a published result; the reference page carries the citation. 

Both contracts are written in the language itself. Every predicate on this page compiles and runs: the two trade directions and their disjunction, the exact quote, deposit and withdrawal, per-touch accrual, the draw against the loan-to-value limit, repayment, collateral withdrawal, liquidation eligibility, and liquidation on the stated terms. Each was checked at its boundary, the admitted case and the refused case one unit apart: for the pool of the quote example, an output of 367 is admitted and 368 is refused. The market swap proves and verifies on the backend in single-digit milliseconds on a laptop. The rendering is the artifact. 

The standing limit travels with the generality: composing these two applications atomically inside one transaction, the flash-loan shape, does not carry over to this model, as stated wherever this documentation claims generality. Each application above stands on its own predicates, and that is the composition this page demonstrates.

<br>