1484 the inductive hypotheses state $\exists N_1. \forall s. \; \llbracket \rderssimp{r}{s} \rrbracket \leq N_1$ and

  1484 the inductive hypotheses state 

  1485 $\exists N_2. \forall s. \; \llbracket \rderssimp{r_2}{s} \rrbracket \leq N_2$. We can reason as follows

  1485 $\exists N_1. \forall s. \; \llbracket \rderssimp{r}{s} \rrbracket \leq N_1$ and

  1486 $\exists N_2. \forall s. \; \llbracket \rderssimp{r_2}{s} \rrbracket \leq N_2$. 

  1487 

  1488 When the string $s$ is not empty, we can reason as follows

  1502 (4) is by splitting the case when $s = []$ and $s \neq []$.

  1504 

  1503 

  1505 

  1504 We reason similarly for  $\STAR$.\medskip

  1506 Combining the cases when $s = []$ and $s \neq []$, we get (4):

  1507 \begin{center}

  1508 	\begin{tabular}{lcll}

  1509 		$\rsize{(r_1 \cdot r_2) \backslash_r s}$ & $\leq$ & 

  1510 		$max \; (2 + N_1 + 

  1511 		\llbracket r_2 \rrbracket_r + 

  1512 		N_2 * (card\; (\sizeNregex \; N_2))) \; \rsize{r_1\cdot r_2}$ & (4)

  1513 	\end{tabular}

  1514 \end{center}

  1515 

  1516 We reason similarly for  $\STAR$.

  1517 The inductive hypothesis is

  1518 $\exists N. \forall s. \; \llbracket \rderssimp{r}{s} \rrbracket \leq N$.

  1519 Let $\n_r = \llbracket r^* \rrbracket_r$.

  1520 When $s = c :: cs$ is not empty,

  1521 \begin{center}

  1522 \begin{tabular}{lcll}

  1523 & & $ \llbracket   \rderssimp{r^* }{c::cs} \rrbracket_r $\\

  1524 & $ = $ & $\llbracket \rsimp{(\sum (\map \; (\lambda s. (r \backslash_{rsimp} s) \cdot r^*) \; (\starupdates\; 

  1525 cs \; r \; [[c]] )) )} \rrbracket_r $ & (5) \\			

  1526 & $\leq$ & $\llbracket 

  1527 \rdistinct{

  1528 	(\map \; 

  1529 		(\lambda s. (r \backslash_{rsimp} s) \cdot r^*) \; 

  1530 		(\starupdates\; cs \; r \; [[c]] )

  1531 	)}

  1532 	{\varnothing} \rrbracket_r  + 1$ & (6) \\

  1533 					 & $\leq$ & $1 + (\textit{card} (\sizeNregex \; (N + n_r)))

  1534 	* (1 + (N + n_r)) $ & (7)\\

  1535 \end{tabular}

  1536 \end{center}

  1537 \noindent

  1538 (5) is by the lemma  \ref{starClosedForm}.

  1539 (6) is by \ref{altsSimpControl}.

  1540 (7) is by \ref{finiteSizeNCorollary}.

  1541 Combining with the case when $s = []$, one gets

  1542 \begin{center}

  1543 \begin{tabular}{lcll}

  1544 	$\rsize{r^* \backslash_r s}$ & $\leq$ & $max \; n_r \; 1 + (\textit{card} (\sizeNregex \; (N + n_r)))

  1545 	* (1 + (N + n_r)) $ & (8)\\

  1546 \end{tabular}

  1547 \end{center}

  1548 \noindent

  1549 

  1550 The alternative case is slightly less involved.

  1551 The inductive hypothesis 

  1552 is equivalent to $\exists N. \forall r \in (\map \; (\_ \backslash_r s) \; rs). \rsize{r} \leq N$.

  1553 In the case when $s = c::cs$, we have 

  1554 \begin{center}

  1555 \begin{tabular}{lcll}

  1556 & & $ \llbracket   \rderssimp{\sum rs }{c::cs} \rrbracket_r $\\

  1557 & $ = $ & $\llbracket \rsimp{(\sum (\map \; (\_ \backslash_{rsimp} s)  \; rs) )} \rrbracket_r $ & (9) \\			

  1558 & $\leq$ & $\llbracket (\sum (\map \; (\_ \backslash_{rsimp} s)  \; rs) ) \rrbracket_r $  & (10) \\

  1559 & $\leq$ & $1 + N * (length \; rs) $ & (11)\\

  1560 \end{tabular}

  1561 \end{center}

  1562 \noindent

  1563 (9) is by \ref{altsClosedForm}, (10) by \ref{rsimpSize} and (11) by inductive hypothesis.

  1564 

  1565 Combining with the case when $s = []$, one gets

  1566 \begin{center}

  1567 \begin{tabular}{lcll}

  1568 	$\rsize{\sum rs \backslash_r s}$ & $\leq$ & $max \; \rsize{\sum rs} \; 1+N*(length \; rs)$ 

  1569 	 & (12)\\

  1570 \end{tabular}

  1571 \end{center}

  1572 (4), (8), and (12) are all the inductive cases proven.