theorem Duper.equality_factoring_soundness1 {α : Sort u_1} {s t : α} (v : α) (h : s = t) : t ≠ v ∨ s = v

theorem Duper.equality_factoring_soundness2 {α : Sort u_1} {s t : α} (u : α) (h : s = t) : t ≠ u ∨ u = s

theorem Duper.equality_factoring_soundness3 {α : Sort u_1} {s t : α} (v : α) (h : s = t) : s ≠ v ∨ t = v

theorem Duper.equality_factoring_soundness4 {α : Sort u_1} {s t : α} (u : α) (h : s = t) : s ≠ u ∨ u = t

def Duper.mkEqualityFactoringProof (i j : Nat) (litside_i litside_j : LitSide) (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.equalityFactoringWithAllConstraints (given : Clause) (c : MClause) (i j : Nat) (litside_i litside_j : LitSide) : RuleM.RuleM ClauseStream

Attempts to perform equality factoring on clause c with c.lits[i] as the literal to be transformed subject to the following constraints:

1. c.lits[i].litside_i can be unified with c.lits[j].litside_j
2. c.lits[i].litside_i is not less than c.lits[i].(LitSide.toggleSide litside_i) by the ground reduction ordering after the unification from (1)
3. c.lits[i] is maximal and nothing is selected

If any of these constraints fail to hold, then equalityFactoringWithAllConstraints should not do anything

Equations

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

def Duper.equalityFactoringAtLit (given : Clause) (c : MClause) (i j : Nat) : RuleM.RuleM (Array ClauseStream)

Attempts to perform equality factoring with c.lits[i] as the literal to be transformed

Equations

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

def Duper.equalityFactoring (given : Clause) (c : MClause) (cNum : Nat) : RuleM.RuleM (Array ClauseStream)

Equations

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