So we're still being introduced to Formal math and we've been given a problem to solve through math induction. The base case worked out well without issues:

$\displaystyle len ( flt ( s ) ) <= len (s)$

Available rules:

$\displaystyle len(\emptyString) = 0$
$\displaystyle len(\alpha+s) = 1 + len(s)$
$\displaystyle flt(\emptyString) = \emptyString$
$\displaystyle flt(\alpha + s) = \alpha(flt(s)$ if $\displaystyle \alpha=a$
$\displaystyle flt(\alpha + s) = flt(s)$ if $\displaystyle \alpha = b$

Now the inductive case, we were given the assumption that $\displaystyle len(s)=k+1$

The inductive hypothesis is $\displaystyle \forall t : len(t)=k$

$\displaystyle s=\alpha t$ where $\displaystyle len(s) = 1 + len(t)$

I can do this induction if I assume that in the original formula, instead of s I place k+1 and k, and induce as usual. However this different take is supposed to be numerical induction, however I have no rules on $\displaystyle flt(x)$ that allow me to do anything with it which means I'm stuck on LHS.

I tried inducing it as best as I could but I'm honestly stumped as to what the assumption should be (for just k)