Valid indices for native cyclic argument successors

The native next-index program stays inside the actual occurrence list, and its selected constraint/scope pair occurs in that list. Existing positional occurrence and rotation successor identities supply both facts, including wraparound and repeated variables. These original program bounds do not require a supplied rotation or numerical genus.

theorem Cslib.Complexity.CSP.argumentNextIndex_lt_occurrences {Rel V : Type} {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : argumentNextIndex F ↑o.fst ↑o.snd < F.occurrences.length

The actual next argument has an occurrence-list index bounded by that list's length.

theorem Cslib.Complexity.CSP.argumentNextPosition_mem {Rel V : Type} {F : Logic.PL.CSP Rel V} (o : F.Occurrence) : (↑o.fst, if ↑o.snd + 1 < scopeLength F ↑o.fst then ↑o.snd + 1 else 0) ∈ argumentPositions F

The cyclic next-position pair really occurs, including the last-to-first wrap.