如何用归纳法证明滑动窗口法求解最长无重复子串的正确性

我在解决最长无重复字符的子串问题时，写出了如下Python滑动窗口解法：

def lengthOfLongestSubstring(self, s: str) -> int:
        left = 0
        right = 0 
        currstring= ""
        maxlength=0
        for i in range(len(s)):
            
            while s[i] in currstring: 
                left+=1
                currstring = currstring[1::]
            currstring+=s[i]
            right+=1
            maxlength = max(maxlength, right-left)
        return maxlength

我尝试用归纳法证明该算法的正确性，但遇到了瓶颈。我的归纳假设如下：

P(n)：对于任意长度为n的字符串，该算法能给出最长无重复子串的长度。

基础情况n=0时，算法返回0，显然正确。

在归纳步骤中，假设当n=k时P(k)成立（即长度为k的字符串能被正确求解），处理长度为k+1的字符串时，我分为两种情况分析：

• 第k+1个字符不在最长子串中，则P(k+1)=P(k)，由归纳假设可知算法正确；
• 第k+1个字符在最长子串中，此时若P(k)=l，我推测最后k+1-l个字符必须互不相同，但在这里陷入了瓶颈，不确定该思路是否可行，或是需要换一种证明方法。

内容的提问来源于stack exchange，提问作者Javier Lázaro