Sorted

Readable signature

Sorted(b, c, l)

Exact expansion

forall dp_i. (exists dp_gap. dp_gap + S (S dp_i) = l) -> exists dp_p dp_q. ((((exists ff_h_defined_sorted_left. ff_h_defined_sorted_left + S (dp_p) = S ((S (dp_i)) * c)) /\ exists ff_q_defined_sorted_left. b = ff_q_defined_sorted_left * S ((S (dp_i)) * c) + (dp_p))) /\ ((((exists dp_beta_h_defined_sorted_right. dp_beta_h_defined_sorted_right + S (dp_q) = S ((S (S dp_i)) * c)) /\ exists dp_beta_q_defined_sorted_right. b = dp_beta_q_defined_sorted_right * S ((S (S dp_i)) * c) + (dp_q))) /\ (exists dp_le. dp_le + dp_p = dp_q)))

This node is conservative notation, not a theorem, axiom, predicate constant, or kernel rule. Its expansion remains in the unchanged first-order language.

Definition neighborhood

Depends on conservative definitions

Used by conservative definitions

All transitive conservative prerequisites

Used by theorem statements or local proof propositions

Grand-campaign planning vocabulary

Locate Sorted in the global campaign vocabulary →

Reviewed Sorted corresponds to blueprint Sorted with checked argument positions [0, 1, 2].

The global atlas describes planning vocabulary and does not itself certify a definition or theorem. The reviewed expansion and conservative dependency DAG on this page are the actual family-local reading definitions.