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 notation, not a theorem, axiom, predicate constant, or kernel rule. The elaboration layer must expand it before proof checking.

Definition neighborhood

Expands using

Used by definitions

Used by theorem statements or local proof propositions