Prove this in mathematics induction step

2. (10 points) Let Bin Num be the inductive set defined by the following constructors: Zero : BinNum. One : Bin Num. JoinZero : Bin Num Bin Num. Join One : BinNum Bin Num. The members of BinNum represent binary numerals like 1011 and 010. Zero represents 0; One represents 1; and if u represents U, then JoinZero(u) represents U0 and Join One(u) represents Ul. For example, Join One (JoinZero(Join One(One))) represents the binary number 1101. The function len : Bin Num+N maps a member of BinNum to its length. len is defined by the following equations using recursion and pattern matching: len(Zero) = 1. len(One) = 1. len (JoinZero(u)) = len(u) +1. len (Join One(u)) = len(u) +1. The function val: Bin Num+N maps a member of Bin Num to the value of the binary numeral it rep- resents. For example, val(Join One(JoinZero(Join One (One)))) = (1101)2 = 13. val is defined by the following equations using recursion and pattern matching: val(Zero) = 0. val(One) = 1. val(JoinZero(u) = 2 * val(u). val(Join One(u) = (2 * val(u)) +1. The function add : BinNum Bin Num Bin Num is intended to implement addition on members of BinNum. It is defined by the following equations using recursion and pattern matching: =u. add(u, Zero) = u. add(Zero, u) add(One, One) = JoinZero (One). add(JoinZero(u), One) = Join One(u). add(One, JoinZero(u)) = Join One(u). add(Join One(u), One) = JoinZero(add(u, One). add(One, Join One(u)) = JoinZero(add(u, One). add (JoinZero(u), JoinZero(v)) = JoinZero(add(u, v). add (Join One(u), JoinZero(v)) = JoinOne(add(u, v). add (JoinZero(u), Join One()) = Join One(add(u, v). add (Join One(u), Join One()) = JoinZero(add(add(u, v), One)). Notice that the algorithm behind the definition is essentially the same algorithm that children learn to add numbers represented as decimal numerals. The last equation is a bit complicated because it involves a carry of 1. Lemma 1. For all u, v Bin Num, len(add(u, v))