proposition: Lemma chkHc_rew : forall (m: hmap) (f:LForm) (i:int) (b:bool), chkHc m f i b = match f with | LAT a => match IntMap.get' i m with | Some(b',LAT a') => (a =? a') && Bool.eqb b (AT_is_dec a) && Bool.eqb b b' | _ => false end | LOP o l => List.forallb (fun f => chkHc m f.(elt) f.(id) f.(is_dec)) l && match IntMap.get' i m with | Some (b',LOP o' l') => lop_eqb o o' && Bool.eqb b (forallb (fun f => f.(is_dec)) l) && Bool.eqb b b' && chkHc_list l l' | _ => false end | LIMPL l r => List.forallb (fun f => chkHc m f.(elt) f.(id) f.(is_dec)) l && chkHc m r.(elt) r.(id) r.(is_dec) && match IntMap.get' i m with | Some (b',LIMPL l' r') => Bool.eqb b ((forallb is_dec l) && (is_dec r)) && Bool.eqb b b' && chkHc_list l l' && HCons.eq_hc r r' | _ => false end end.
proof: Proof. destruct f; reflexivity. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause