fact: Fixpoint interp_carry (c: carry) : bool := match c with | Clit l => (Lit.interp rho l) | Cand c1 c2 => (interp_carry c1) && (interp_carry c2) | Cor c1 c2 => (interp_carry c1) || (interp_carry c2) | Cxor c1 c2 => xorb (interp_carry c1) (interp_carry c2) | Ciff c1 c2 => Bool.eqb (interp_carry c1) (interp_carry c2) end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance