# Proof by structural induction

Let BExpr be the variety of all boolean expressions that are defined by the following grammar:

I have two recursive functions numbinexprs and numexprs. numbinexprs returns the number of binary subformulas when given a boolean expression, and numexprs returns the number of subformulas.

I am supposed to prove the following statement by structural induction:

numbinexprs(b) ≤ numexprs(b) for every boolean expression b.

numbinexprs is defined as:

numbinexprs((¬ b)) = numbinexprs(b)

numbinexprs(bool) = 0

numbinexprs((b1 ∧ b2)) = numbinexprs(b1) + numbinexprs(b2) +1

numbinexprs((b1 ∨ b2)) = numbinexprs(b1) + numbinexprs(b2) +1

And numexprs is defined as:

numexprs((¬ b)) = numexprs(b) +1

numexprs(bool) = 1

numexprs((b1 ∧ b2)) = numexprs(b1) + numexprs(b2) +1

numexprs((b1 ∨ b2)) = numexprs(b1) + numexprs(b2) +1

My attempt :

Base case:

numbinexprs(bool) = 0, and countexprs(bool) = 1. This gives numbinexprs(bool) ≤ numexprs(bool).

Induction hypothesis: Assume that the statement numbinexprs(b) ≤ numexprs(b) is true for an arbitrarily boolean expression b.

I'm not sure how to do the inductive step. How do I prove this? Do I need three different inductive steps (one on the form b1∧b2, one on the form b1∨b2, and another ¬b)?

UPDATE:

Induction hypothesis:

Assume numbinexprs(b1) ≤ numexprs(b1) and numbinexprs(b2) ≤ numexprs(b2), where b1 and b2 are boolean expressions.

Inductive step:

• Case 1:

numbinexprs((¬ b1)) = {def. numbinexprs, arithmetic} = numbinexprs(b1) + 0 = {def. numbinexprs, b0 is a bool} = numbinexprs(b1) + numbinexprs(b0) ≤ {ind.hyp} = numexprs(b1) + numexprs(b0) = {def. numexprs} = numexprs(b1) + 1 = {def. numexprs} = numexprs((¬ b1))

• For any formula b, You're trying to prove numbinexprs(b) $\leq$ numexprs(b), given that it's true for all subexpressions of b. As you anticipate, this will have three cases. Nov 28 '21 at 16:21
• Same approach of your previous post Nov 28 '21 at 16:23
• So the base case and induction hypothesis are correct?@TomKern Nov 28 '21 at 16:34
• Your base case is correct, but your induction hypothesis should be that the statement is true for all subexpressions of b, from which you must prove your statement is true for b. Nov 28 '21 at 21:06
• Your argument looks perfectly valid, but your introduction of b0 is unnecessary. You can argue that nunbinexprs(b1) + 0 $\leq$ numexprs(b1)+1 more directly. Nov 29 '21 at 23:22