def Duper.mkDemodulationProof (sidePremiseLhs : LitSide) (mainPremisePos : ClausePos) (isForward : Bool) (premises : List Lean.Expr) (parents : List RuleM.ProofParent) (transferExprs : Array Lean.Expr) (c : Clause) : Lean.MetaM Lean.Expr

Equations

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

def Duper.forwardDemodulationWithPartner (mainPremise : MClause) (mainPremiseMVarIds : Array Lean.MVarId) (mainPremiseSubterm : Lean.Expr) (mainPremisePos : ClausePos) (sidePremise : MClause) (sidePremiseLhs : LitSide) : RuleM.RuleM (Option (MClause × Option RuleM.ProofReconstructor))

Equations

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

def Duper.forwardDemodulationAtExpr (e : Lean.Expr) (pos : ClausePos) (sideIdx : RootCFPTrie) (givenMainClause : MClause) (mainClauseMVarIds : Array Lean.MVarId) : RuleM.RuleM (Option (Array (Clause × RuleM.Proof)))

Equations

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

def Duper.forwardDemodulation (sideIdx : RootCFPTrie) : MSimpRule

Performs rewriting of positive and negative literals (demodulation) with the given clause c as the main clause. We only attempt to use c as the main clause (rather than attempt to use it as a side clause as well) because if we used c as a side clause, we would remove the wrong clause from the active set (we would remove c rather than the main clause that c is paired with). c will considered as a side clause in the backward simplificaiton loop (i.e. in backwardDemodulation)

Equations

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

def Duper.backwardDemodulationWithPartner (mainPremise : MClause) (mainPremiseMVarIds : Array Lean.MVarId) (mainPremiseSubterm : Lean.Expr) (mainPremisePos : ClausePos) (sidePremise : MClause) (sidePremiseLhs : LitSide) : RuleM.RuleM (Option (Clause × RuleM.Proof))

Equations

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

def Duper.backwardDemodulation (mainIdx : RootCFPTrie) : BackwardMSimpRule

Performs rewriting of positive and negative literals (demodulation) with the given clause as the side clause. Returns the list of original clauses that are to be removed by backward simplification.

Equations

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