@[inline]

def Std.Tactic.BVDecide.LRAT.Internal.State.add (s : State) (clause : Sat.CNF.Clause Nat) : State

Equations

• s.add clause = { formula := s.formula.push (some clause) }

@[simp]

theorem Std.Tactic.BVDecide.LRAT.Internal.State.add_toCNF_eq_toCNF_add {s : State} {c : Sat.CNF.Clause Nat} : (s.add c).toCNF = s.toCNF.add c

theorem Std.Tactic.BVDecide.LRAT.Internal.State.entails_add_of_entails_clause {s : State} {c : Sat.CNF.Clause Nat} (h : s.toCNF.EntailsClause c) : s.toCNF.Entails (s.add c).toCNF