fact: Definition bop_eqb o o' := match o, o' with | BO_Zplus, BO_Zplus | BO_Zminus, BO_Zminus | BO_Zmult, BO_Zmult | BO_Zlt, BO_Zlt | BO_Zle, BO_Zle | BO_Zge, BO_Zge | BO_Zgt, BO_Zgt => true | BO_eq t, BO_eq t' => Typ.eqb t t' | BO_BVand s1, BO_BVand s2 => N.eqb s1 s2 | BO_BVor s1, BO_BVor s2 | BO_BVxor s1, BO_BVxor s2 | BO_BVadd s1, BO_BVadd s2 | BO_BVmult s1, BO_BVmult s2 => N.eqb s1 s2 | BO_BVult s1, BO_BVult s2 => N.eqb s1 s2 | BO_BVslt s1, BO_BVslt s2 => N.eqb s1 s2 | BO_BVconcat s1 s2, BO_BVconcat s3 s4 => N.eqb s1 s3 && N.eqb s2 s4 | BO_BVshl s1, BO_BVshl s2 => N.eqb s1 s2 | BO_BVshr s1, BO_BVshr s2 => N.eqb s1 s2 | BO_select ti te, BO_select ti' te' | BO_diffarray ti te, BO_diffarray ti' te' => Typ.eqb ti ti' && Typ.eqb te te' | _,_ => false end.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList