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