fact: Definition check_form_aux a b := match a, b with | Fatom ha, Fand diseq => check_distinct ha diseq | Fatom a, Fatom b => a =? b | Ftrue, Ftrue => true | Ffalse, Ffalse => true | Fnot2 i1 l1, Fnot2 i2 l2 => (i1 =? i2) && (check_lit l1 l2) | Fand a1, Fand a2 => (length a1 =? length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1) | For a1, For a2 => (length a1 =? length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1) | Fimp a1, Fimp a2 => (length a1 =? length a2) && (aforallbi (fun i l => check_lit l (a2.[i])) a1) | Fxor l1 l2, Fxor j1 j2 => check_lit l1 j1 && check_lit l2 j2 | Fiff l1 l2, Fiff j1 j2 => check_lit l1 j1 && check_lit l2 j2 | Fite l1 l2 l3, Fite j1 j2 j3 => check_lit l1 j1 && check_lit l2 j2 && check_lit l3 j3 | _, _ => false end.
imports: List PArray Bool Int63 ZMicromega Misc State SMT_terms