>> We have a finite succession of objects with a beginning and an end. The >> first element, by definition has no predecessor. The last element, by >> definition has no successor. I'd say your work-around isn't up to spec.
That's your unworkable criteria. All of the difficultiest that you haven't been able to resolved are smmothly handled by allowing Sm.
My version is done can complete. Yours, which I see no point in persuing, has problems that you haven't. The worse being the complexity of describing the partiality of addistion.
BTW, just as I told you, in naive finite arithmatic it's a theorem, ie provalbe, that for all x /= m, x /= Sx by induction over the equivalent statement P(x) when x = m or x /= Sx.