def Duper.ProverM.backwardSimpRules : ProverM (Array BackwardSimpRule)

Equations

• One or more equations did not get rendered due to their size.

def Duper.ProverM.backwardSimplify (givenClause : Clause) : ProverM Unit

Uses the givenClause to attempt to simplify other clauses in the active set. For each clause that backwardSimplify is able to produce a simplification for, backwardSimplify removes the clause adds any newly simplified clauses to the passive set. Additionally, for each clause removed from the active set in this way, all descendents of said clause should also be removed from the current state's allClauses and passiveSet

Equations

• One or more equations did not get rendered due to their size.