Loop invariant initialisation confusion

Question

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<j \rightarrow P[k] ==T[s+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?

Answer 1

An implication is true if the antecedent is false.

If j is 1 then the antecedent is false no matter what k you choose, which means that the implication is vacuously true for every k. So the assertion is true.