fact: Definition check_rowneq cl := match cl with | leqij :: leqrow :: nil => if Lit.is_pos leqij && Lit.is_pos leqrow then match get_form (Lit.blit leqij), get_form (Lit.blit leqrow) with | Fatom eqij, Fatom eqrow => match get_atom eqij, get_atom eqrow with | Abop (BO_eq ti) i j, Abop (BO_eq te) xa x => match get_atom xa, get_atom x with | Abop (BO_select ti1 te1) sa j1, Abop (BO_select ti2 te2) sa2 j2 => if Typ.eqb ti ti1 && Typ.eqb ti ti2 && Typ.eqb te te1 && Typ.eqb te te2 then match store_of_me sa sa2, store_of_me sa2 sa with | Some (ti3, te3, i1), None | None, Some (ti3, te3, i1) => if Typ.eqb ti ti3 && Typ.eqb te te3 && (((i1 =? i) && (j1 =? j) && (j2 =? j)) || ((i1 =? j) && (j1 =? i) && (j2 =? i))) then cl else C._true | _, _ => C._true end else C._true | _, _ => C._true end | _, _ => C._true end | _, _ => C._true end else C._true | _ => C._true end.
imports: Bool List Int63 PArray Psatz ZArith Misc State SMT_terms FArray SMT_classes