fact: Fixpoint check_add (bs1 bs2 bsres : list _lit) (carry : carry) := match bs1, bs2, bsres with | nil, nil, nil => true | b1::bs1, b2::bs2, bres::bsres => if Lit.is_pos bres then match get_form (Lit.blit bres) with | Fxor xab c => if Lit.is_pos xab then match get_form (Lit.blit xab) with | Fxor a1 a2 => let carry' := Cor (Cand (Clit b1) (Clit b2)) (Cand (Cxor (Clit b1) (Clit b2)) carry) in (((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1))) && eq_carry_lit carry c && check_add bs1 bs2 bsres carry' | _ => false end else false | _ => false end else false | _, _, _ => false end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance