Proving recursive algorithms

Reading through the remainder of Chapter 2 (2.7 onward) in attempts to answer my below question, I wonder why the examples use an array of length 1 as the base case instead of an array of length 0.
Then I get to this:

and now I am puzzled.  That is not all the cases? a subarray of length 0 is definitely still a subarray.  Hopefully reading on will solve the mystery, else I'll have to work through it on my own.

------------------------------

Got it. Well, half of it.

The precondition was that A is a non-empty array.  So I suppose that's why the base case is an array of length 1?

Still mediumly confused though because an array of length 1 can have a subarray of length 0.

--------------------------
I suppose a "correctness specification" is the recursive analogue of an iterative loop invairant?
-------------------------

Aside :   Can you have an array of infinite length?!

Motivation:
It seems that for termination it suffices to show that a recursive call operates on a smaller section of the array each time. But if the array was infinitely long, would that actually make it end?

First Thought:
But we have the theorem that all decreasing sequences of Natural numbers are finite, so does that mean that smaller and smaller sections of the array must eventually culminate in a subarray of size 0 ? (or of size 1 if we're adhering to the strange base case specifications above?).
Is a countdown from infinity still a veritable countdown?
Does this theorem hold if there's no defined start of the sequence?
------------------------------