(Deferred) Named predicates and list indexing: permutation, connected, acyclic, Q[i] #34

Problem

Some conditions can't be written compactly with quantifiers alone: orderings, connectivity and acyclicity. Without a way to say them, Hamiltonian Cycle, Spanning Tree, Feedback Arc Set and similar problems keep prose certificate grammars. Part of #32.

Wanted

• Indexing into lists: Q[i] and |Q|, index arithmetic like Q[i+1 mod |Q|], and for all i over a list's indices.
• A small library of named predicates, each with a fixed English phrase for the generated text:
  • Q is permutation of N: every element of N exactly once;
  • connected (N, E), acyclic (N, E), is path from s to t in (N, E);
  • partition of S into G: the groups are disjoint and cover S.

Examples

• Hamiltonian Cycle certificate: {Q | Q is permutation of N, for all i: {Q[i], Q[i+1 mod |Q|]} in E}
  • Generated Output: "True if there is an ordering Q of all the nodes in N, each exactly once, such that each node is joined by an edge in E to the next, and the last to the first; otherwise False."
• Feedback Arc Set: acyclic (N, E minus F).

Notes

The library should stay small and textbook-standard. A predicate earns a place when two or more Redux problems need it.