fact: Definition BV_full_adder_sum := (fix F (l : list bool) : list bool -> bool -> BV := match l with | nil => (fix F0 (l0 : list bool) : bool -> BV := match l0 with | nil => fun _ : bool => nilbv | b :: l1 => fun z : bool => consbv (half_adder_sum b z) (F0 l1 (half_adder_carry b z)) end) | b :: l0 => fun x2 : list bool => match x2 with | nil => fun y z : bool => consbv (half_adder_sum y z) (F l0 nil (half_adder_carry y z)) | b0 :: l1 => fun y z : bool => consbv (full_adder_sum y b0 z) (F l0 l1 (full_adder_carry y b0 z)) end b end).
imports: BV FullAdder