fact: Fixpoint check_eq (bs1 bs2 bsres: list _lit) := match bs1, bs2, bsres with | nil, nil, nil => true | b1::bs1, b2::bs2, bres :: bsres => match bs1, bs2, bsres with | _::_, _::_, [] => if Lit.is_pos bres then match get_form (Lit.blit bres) with | Fand args => match to_list args with | bres :: bsres => if Lit.is_pos bres then let ires := match get_form (Lit.blit bres) with | Fiff a1 a2 => ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)) | _ => false end in if ires then check_eq bs1 bs2 bsres else false else false | _ => false end | _ => false end else false | _, _, _ => if Lit.is_pos bres then let ires := match get_form (Lit.blit bres) with | Fiff a1 a2 => ((a1 =? b1) && (a2 =? b2)) || ((a1 =? b2) && (a2 =? b1)) | _ => false end in if ires then check_eq bs1 bs2 bsres else false else false end | _, _, _ => 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