Let $n \ge 0$ and $(a_i)_{\,0 \le i \le n}$, $(b_i)_{\,0 \le i \le n}$ be given where, for all $i$, $a_i, b_i \in \{0,1\}$.
Let
$\quad \displaystyle {a = \sum_{0 \le i \le n} a_i 2^i}$
and
$\quad \displaystyle {b = \sum_{0 \le i \le n} b_i 2^i}$
and assume that $b \lt a$ so that if $c = a - b$ we can write
$\quad \displaystyle {c = \sum_{0 \le i \le n} c_i 2^i \quad \text{where } c_i \in \{0,1\} }$
Recall the $\text{XOR }$ (numeric) truth tables,
$$\begin{array}{cc|c} p & q & p \nleftrightarrow q \\ \hline 0 & 0 & 0 \\ 0 & 1 & 1 \\ 1 & 0 & 1 \\ 1 & 1 & 0 \\ \end{array} $$
and its negation,
$$\begin{array}{cc|c} p & q & p \leftrightarrow q \\ \hline 0 & 0 & 1 \\ 0 & 1 & 0 \\ 1 & 0 & 0 \\ 1 & 1 & 1 \\ \end{array} $$
Claim: There is a symbolic processing algorithm that takes the inputs $(a_i)_{\,0 \le i \le n}$ and $(b_i)_{\,0 \le i \le n}$ and constructs a function
$\quad \mu: \{0,1,\dots,n\} \to \{\nleftrightarrow,\leftrightarrow\}$
such that for each $0 \le i \le n$, $\;c_i = a_i \, \mu(i) \, b_i$.
I tried proving this by (strong) induction, but I get off course and wind up just pointing to the simple algorithmic highlights of this subtraction technique.
Please supply a proof of my claim, and if convenient use your own formulation/notation to express the above thinking.
My work
As I worked on concrete subtraction problems I realized that before calculating any numbers I could figure out all the logic gates to use for each $a_i$ | $b_i$ pair.
I also observed that if whenever $a_i =0$ it had to be the case that $b_i = 0$, then there would be no $\leftrightarrow$ processing gates.
Example 1: To calculate $11000_2 - 1011_2$ one writes out in a completely mechanical fashion (by examining the two expressions digit by digit from right to left)
$$ \begin{array}{c} &1&1&0&0&0\\ &0&1 & 0 & 1 & 1\\\hline &\leftrightarrow&\leftrightarrow&\leftrightarrow&\leftrightarrow&\nleftrightarrow \end{array} $$
and then by applying the digit by digit boolean calculations,
$$ \begin{array}{c} &1&1&0&0&0\\ &0&1 & 0 & 1 & 1\\\hline &\leftrightarrow&\leftrightarrow&\leftrightarrow&\leftrightarrow&\nleftrightarrow\\\hline &0&1 & 1 & 0 & 1 \end{array} $$
we know that $11000_2 - 1011_2 = 1101_2$.
Example 2: To calculate $110111000101_2 - 101101011100_2$, we put up our two string work area,
$$ \begin{array}{c} &1&1&0&1&1&1&0&0&0&1&0&1\\ &1&0&1&1&0&1&0&1&1&1&0&0 \end{array} $$
and inspect it from right to left looking looking for the first $0$ over $1$. We find it and paint the corresponding segment (up to the first $1$ over $0$ occurrence) after it red,
$$ \begin{array}{c} &1&1&0&1&\color{red}1&\color{red}1&\color{red}0&\color{red}0&0&1&0&1\\ &1&0&1&1&\color{red}0&\color{red}1&\color{red}0&\color{red}1&1&1&0&0 \end{array} $$
Repeating we see one final segment,
$$ \begin{array}{c} &1&\color{red}1&0&1&\color{red}1&\color{red}1&\color{red}0&\color{red}0&0&1&0&1\\ &1&\color{red}0&1&1&\color{red}0&\color{red}1&\color{red}0&\color{red}1&1&1&0&0 \end{array} $$
and then by applying the digit by digit boolean calculations,
$$ \begin{array}{c} &1&\color{red}1&0&1&\color{red}1&\color{red}1&\color{red}0&\color{red}0&0&1&0&1\\ &1&\color{red}0&1&1&\color{red}0&\color{red}1&\color{red}0&\color{red}1&1&1&0&0\\\hline &\nleftrightarrow&\leftrightarrow&\nleftrightarrow&\nleftrightarrow&\leftrightarrow&\leftrightarrow&\leftrightarrow&\leftrightarrow&\nleftrightarrow&\nleftrightarrow&\nleftrightarrow&\nleftrightarrow\\\hline & 0 & 0 & 1 & 0 & 0 & 1 & 1 & 0 & 1 & 0 & 0 & 1 \end{array} $$
we know that $110111000101_2 - 101101011100_2 = 1001101001_2$.