Proving that $a \dot{-} (b+1) = (a \dot{-} b) \dot{-} 1$ This should be an easy exercise from Hodel's Introduction to Mathematical Logic, but for some reason I'm not getting it right. Define $a \dot{-} b$ as $a-b$ if $a \geq b$ and as $0$ otherwise. Recursively, this can be defined as $\mu x [(a=b+x) \vee (a<b)]$. Using this information, I'm supposed to prove that $a \dot{-} (b+1) = (a \dot{-} b) \dot{-} 1$. I've tried using induction on $a$ and induction on $b$ to get the desired result, but I got stuck as I see no way of applying the induction step (basically, I couldn't reduce the case, say, $a \dot{-} ((n+1)+1)$ to the induction hypothesis). Any hints?
 A: The proof is mechanical if one uses the universal property of the $\,\rm max\,$ function
$$ x \ge y,z\color{#c00}\iff x \ge m(y,z),\ \ m = \rm max\qquad\qquad\qquad\ \ $$  
Using this property to eliminate then reintroduce $\,m = \rm max\,$ we obtain (in gory detail)
$$\begin{array}{rrl} 
&x\ \ge&\ \,(a \dot- b)\! \dot-\! 1\\
\iff &x\ \ge&\!\!\!m( a \dot- b\! -\!1, 0)\\
\color{#c00}\iff &x\ \ge& \ \ \ a\dot- b\!-\!1, 0\\
\iff &1\!+\!x\ \ge& \ \ \ a \dot- b,\quad \ \, 1\\
\iff &1\!+\!x\ \ge&\!\!\!m(a\!-\!b,0), 1\\
\color{#c00}\iff &1\!+\!x\ \ge&\ \ \,a\!-\!b,\,0, \  1\\
\iff &1\!+\!x\ \ge&\,\ \  a\!-\!b,\quad\,\ 1\\
\iff &x\ \ge&\ \ \  a\!-\!b\!-\!1, 0\\
\color{#c00}\iff &x\ \ge&\!\!\! m(a\!-\!b\!-\!1, 0)\\
\iff &x\ \ge&\ \ \ a\dot- (b\!+\!1)
\end{array}\qquad\quad$$
Remark $\ $ With hindsight, one can abstract from the proof a lemma about max, $\ m(x,y)-z\, =\, m(x\!-\!z,y\!-\!z).\,$ Using this shortens the above proof to
$$\begin{align} (a \dot- b) \dot- 1\, &=\,m(m(a\!-\!b,0) -1,\ 0)\\ &=\, m(m(a\!-\!b\!-\!1,-1),0)\\ & =\, m(a\!-\!b\!-\!1,0)\\ &=\,a\dot- (b\!+\!1)\end{align}\qquad\quad $$
A: fix $b.$ and consider three cases:
$$(a\dot{-} b) \dot{-} 1 = 
\begin{cases} 0 \dot{-} 1 = 0 & \text{ if } a < b \\
               (a-b)\dot{-}1 = 0  & \text{ if } b < a < b + 1\\
               a-b-1 =a-(b+1) & \text{ if } b + 1 < a \end{cases} $$
therefore $$ (a\dot{-} b) \dot{-} 1 = a\dot{-}(b+1).$$
