def Duper.equalitySubsumptionWithPartner (mainPremise : MClause) (mainPremiseMVarIds : Array Lean.MVarId) (mainPremisePos : ClausePos) (sidePremise : MClause) : RuleM.RuleM (SimpResult (List (MClause × Option RuleM.ProofReconstructor)))

Checks that (getAtPos mainPremise[pos.lit].lhs mainPremisePos.pos) can be matched with sidePremise[0].sidePremiseLhs and that (getAtPos mainPremise[pos.lit].rhs mainPremisePos.pos) can be matched with sidePremise[0].sidePremiseRhs. Importantly, this function does NOT check mainPremise[pos.lit].sign or that mainPremise[pos.lit].lhs and mainPremise[pos.lit].rhs agree outside of the given pos.

Equations

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

def Duper.forwardEqualitySubsumptionAtExpr (mainPremise : MClause) (pos : ClausePos) (potentialSubsumingClauses : Array Clause) (mainMVarIds : Array Lean.MVarId) : RuleM.RuleM Bool

Equations

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

def Duper.forwardEqualitySubsumption (subsumptionTrie : SubsumptionTrie) : MSimpRule

Returns Removed if there exists a clause that subsumes c, and returns Unapplicable otherwise

Equations

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

def Duper.backwardEqualitySubsumption (subsumptionTrie : SubsumptionTrie) : BackwardMSimpRule

Returns the list of clauses that givenSubsumingClause subsumes

Equations

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