# Loop invariant initialisation confusion

Consider the algorithm LastMatch below, which returns the offset (shift) of the last occurrence of the pattern P in text T, or -1 if P does not occur in T:

LastMatch(T,P)
for(s = T.length - P.length downto 0)
j = 1
while(j =< P.length and P[j] == T[s + j])
j++
if(j == P.length + 1)
return s
return -1


I've been given a loop invariant for the while loop:

$$\forall k(1 \leq k

The initialisation of this invariant confuses me. Before we enter the while loop, $$j=1$$. So we're asking is there a $$1\leq k<1$$ such that $$P[k] ==T[s+k]$$?

I cannot find a $$k$$ which satisfies this inequality, so I do not understand what this is saying. So why is the invariant satisfied before we enter the loop? Is it because when I cannot find a $$k$$ it implies that $$P[k]$$ and $$T[s+k]$$ are both equal to the empty set?