2. (10 pointsLet Bit be the inductive set defined by the following con- structors: Zero : Bit. One : Bit. The members of Bit represent 0 and 1. Let BinNum be the inductive set defined by the following constructors: Nil : Bin Num. Join : BinNum x Bit Bin Num. The members of Bin Num not equal to Nil represent binary numerals; Nil represents an empty numeral. For example, Join(Join(Join(Nil, One), Zero), One), represents the binary number 101. The function len : Bin Num +N maps a member of Bin Num to its length. len is defined by the following equations using recursion and pattern matching: len(Nil) = 0. len(Join(u,b)) = len(u) +1. The function val : BinNum N maps a member of Bin Num to the value of the binary numeral it rep- resents. For example, val(Join(Join(Join(Nil, One), Zero), One)) = (101)2 = 5. val is defined by the following equations using recursion and pattern matching val(Nil) = 0. val(Join(u, Zero)) = 2 * val(u). val(Join(u, One)) = (2 * val(u)) +1. The function add : Bin Num x Bin Num Bin Num is intended to implement addition on members of Bin Num. It is defined by the following equations using recursion and pattern matching: add(u, Nil) = u. add(Nil, u) = u. add(Join(u, Zero), Join(v, Zero)) = Join(add(u, v), Zero). add(Join(u, One), Join(v, Zero)) = Join(add(u, v), One). add(Join(u, Zero), Join(v, One)) = Join(add(u, v), One). add(Join(u, One), Join(v, One)) = Join(add(add(u, v), Join(Nil, One)), Zero). 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 E Bin Num, len(add(u, v))