Clockwise successors in appended-scope coordinates

The actual old-body occurrences retain their original cyclic successor. The appended scope's successor is exactly finRotate on its positional argument indices, including repeated labels and arities zero and one. These original identities do not reflect or reorder original bodies.

theorem Cslib.Complexity.CSP.argumentSuccessor_appendOfFnOccurrenceEquiv_inl {Rel V : Type} (F : Logic.PL.CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (o : F.Occurrence) : argumentSuccessor ((F.appendOfFnOccurrenceEquiv r scope) (Sum.inl o)) = (F.appendOfFnOccurrenceEquiv r scope) (Sum.inl (argumentSuccessor o))

Old occurrences retain exactly the original directed argument successor after a scope is appended, including duplicate constraints and repeated variables.

theorem Cslib.Complexity.CSP.argumentSuccessor_appendOfFnOccurrenceEquiv_inr {Rel V : Type} (F : Logic.PL.CSP Rel V) (r : Rel) {n : ℕ} (scope : Fin n → V) (j : Fin n) : argumentSuccessor ((F.appendOfFnOccurrenceEquiv r scope) (Sum.inr j)) = (F.appendOfFnOccurrenceEquiv r scope) (Sum.inr ((finRotate n) j))

The appended scope's actual cyclic successor is the positive finRotate permutation on its original argument positions. No condition on repeated variable labels is used.