discrete math

Let BinNum be the inductive set defined by the following constructors: Zero : BinNum. One : BinNum. JoinZero : BinNum 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 : BinNum+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: BinNum+N maps a member of BinNum to the value of the binary numeral it rep- resents. For example, val(JoinOne(JoinZero(JoinOne(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(JoinOne(u) = (2 * val(u)) +1. The function add : BinNum BinNum 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, Zero) = u. add(Zero, u)=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(u)) = Join One(add(u, v). add (JoinZero(u), Join One(v)) = JoinOne(add(u, v). add(Join One(u), JoinOne(u)) = 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 2, v E BinNum, len(add(u, v))