fact: Definition check_bbSextend pos lres := match S.get s pos with | l1::nil => if (Lit.is_pos l1) && (Lit.is_pos lres) then match get_form (Lit.blit l1), get_form (Lit.blit lres) with | FbbT a1 bs, FbbT a bsres => match get_atom a with | Auop (UO_BVsextn n i) a1' => if ((a1 =? a1') ) && (check_sextend bs bsres i) && (N.of_nat (length bs) =? n)%N then lres::nil else C._true | _ => C._true end | _, _ => C._true end else C._true | _ => C._true end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance