Functionality of as-pattern, non overlapping pattern through 'as pattern'

I am new to functional programming and haskell in particular and have two questions abound as-pattern and the reduction of overlappings through using it. Giving the following code example:

last1 :: [a]          ->  a
last1    [x]          =   x
last1    (x:xs)       =   last xs

last2 :: [a]          ->  a
last2    [y]          =   y
last2    (y:ys@(_:_)) =   last ys

last1 should be non overlapping in comparison to last2. Lets take a look at the specific String f:[]. It would match to [x] and (x:xs) in last1.

In last2it would match to [y]. But not to (y:ys@(_:_)), because ys has to match (_:_) and just fulfills the first any pattern with [].

Are my assumptions correct?

Now take a look at the specific String f:o:o:[]. Now the pattern (y:ys@(_:_)) matches. In this case I am curious how the binding works. What is ys after the first call? I assume it is o:o:[].

Your recursion is going to last in both cases, not last1/last2.

last1 should be non overlapping in comparison to last2. Lets take a look at the specific String f:[]. It would match to [x] and (x:xs) in last1.

It could match (x:xs) but it won't as pattern matching will only match the first success. Overlaps are not ambiguous in this regard (the first definition is always taken).

In last2it would match to [y]. But not to (y:ys@(_:_)), because ys has to match (_:_) and just fulfills the first any pattern with [].

Your phrasing is a bit odd but you are correct that f:[] cannot match to (y:ys@(_:_)) as the latter is basically matching on _:_:_ which isn't a match.

Now take a look at the specific String f:o:o:[]. Now the pattern (y:ys@(_:_)) matches. In this case I am curious how the binding works. What is ys after the first call? I assume it is o:o:[].

ys does equal o:o:[] (or "oo" or [o,o]).