theorem Duper.not_of_eq_false {p : Prop} (h : p = False) : ¬p

theorem Duper.of_not_eq_false {p : Prop} (h : (¬p) = False) : p

theorem Duper.eq_true_of_not_eq_false {p : Prop} (h : (¬p) = False) : p = True

theorem Duper.eq_false_of_not_eq_true {p : Prop} (h : (¬p) = True) : p = False

theorem Duper.clausify_and_left {p q : Prop} (h : (p ∧ q) = True) : p = True

theorem Duper.clausify_and_right {p q : Prop} (h : (p ∧ q) = True) : q = True

theorem Duper.clausify_and_false {p q : Prop} (h : (p ∧ q) = False) : p = False ∨ q = False

theorem Duper.clausify_or {p q : Prop} (h : (p ∨ q) = True) : p = True ∨ q = True

theorem Duper.clausify_or_false_left {p q : Prop} (h : (p ∨ q) = False) : p = False

theorem Duper.clausify_or_false_right {p q : Prop} (h : (p ∨ q) = False) : q = False

theorem Duper.clausify_not {p : Prop} (h : (¬p) = True) : p = False

theorem Duper.clausify_not_false {p : Prop} (h : (¬p) = False) : p = True

theorem Duper.clausify_imp {p q : Prop} (h : (p → q) = True) : p = False ∨ q = True

theorem Duper.clausify_imp_false_left {p q : Prop} (h : (p → q) = False) : p = True

theorem Duper.clausify_imp_false_right {p : Sort u_1} {q : Prop} (h : (∀ (a : p), q) = False) : q = False

theorem Duper.clausify_forall {α : Sort u_1} {p : α → Prop} (x : α) (h : (∀ (x : α), p x) = True) : p x = True

theorem Duper.clausify_exists {α : Sort u_1} {p : α → Prop} (h : (∃ (x : α), p x) = True) : p (Classical.choose ⋯) = True

theorem Duper.clausify_exists_exists {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop} (h : (∃ (a : α), ∃ (b : β), p a b) = True) : (∃ (x : α ×' β), p x.fst x.snd) = True

theorem Duper.clausify_forall_forall {α : Sort u_1} {β : Sort u_2} {p : α → β → Prop} (h : (∀ (a : α) (b : β), p a b) = False) : (∀ (x : α ×' β), p x.fst x.snd) = False

theorem Duper.nonempty_of_exists {α : Sort u_1} {p : α → Prop} (h : (∃ (x : α), p x) = True) : Nonempty α

theorem Duper.clausify_exists_false {α : Sort u_1} {p : α → Prop} (x : α) (h : (∃ (x : α), p x) = False) : p x = False

theorem Duper.nonempty_of_forall_eq_false {α : Sort u_1} {p : α → Prop} (h : (∀ (x : α), p x) = False) : Nonempty α

noncomputable def Duper.Skolem.some {α : Sort u_1} (p : α → Prop) (x : α) : α

Equations

• Duper.Skolem.some p x = if hp : ∃ (a : α), p a then Classical.choose hp else x

theorem Duper.Skolem.spec {α : Sort u_1} {p : α → Prop} (x : α) (hp : ∃ (a : α), p a) : p (some p x)

theorem Duper.exists_of_forall_eq_false {α : Sort u_1} {p : α → Prop} (h : (∀ (x : α), p x) = False) : ∃ (x : α), ¬p x

theorem Duper.false_neq_true : False ≠ True

theorem Duper.true_neq_false : True ≠ False

theorem Duper.clausify_iff {p q : Prop} (h : (p ↔ q) = True) : p = q

theorem Duper.clausify_iff1 {p q : Prop} (h : (p ↔ q) = True) : p = True ∨ q = False

theorem Duper.clausify_iff2 {p q : Prop} (h : (p ↔ q) = True) : p = False ∨ q = True

theorem Duper.clausify_not_iff {p q : Prop} (h : (p ↔ q) = False) : p ≠ q

theorem Duper.clausify_not_iff1 {p q : Prop} (h : (p ↔ q) = False) : p = False ∨ q = False

theorem Duper.clausify_not_iff2 {p q : Prop} (h : (p ↔ q) = False) : p = True ∨ q = True

theorem Duper.clausify_prop_inequality1 {p q : Prop} (h : p ≠ q) : p = False ∨ q = False

theorem Duper.clausify_prop_inequality2 {p q : Prop} (h : p ≠ q) : p = True ∨ q = True

structure Duper.ClausificationResult : Type

• resultLits : Array Lit
• proof : Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
• transferExprs : Array Lean.Expr

def Duper.makeSkTerm (ty b : Lean.Expr) : RuleM.RuleM (Lean.Expr × Lean.Expr)

Equations

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

def Duper.clausifyForall (e : Lean.Expr) : RuleM.RuleM (Array ClausificationResult)

If e has the form ∀ x : ty, b, then clausifies e = False by skolemizing x

Equations

• One or more equations did not get rendered due to their size.
• Duper.clausifyForall e = Lean.throwError (Lean.toMessageData "clausifySingleForall given invalid expression")

def Duper.clausifyExists (e : Lean.Expr) : RuleM.RuleM (Array ClausificationResult)

If e has the form ∃ x : ty, b, then clausifies e = True by skolemizing x

def Duper.clausificationStepE (e : Lean.Expr) (sign : Bool) : RuleM.RuleM (Array ClausificationResult)

Equations

• One or more equations did not get rendered due to their size.
• Duper.clausificationStepE (((Lean.Expr.const `Exists us).app arg).app arg_1) true = Duper.clausifyExists (((Lean.Expr.const `Exists us).app arg).app arg_1)
• Duper.clausificationStepE (Lean.Expr.forallE binderName binderType body binderInfo) false = Duper.clausifyForall (Lean.Expr.forallE binderName binderType body binderInfo)

def Duper.clausificationStepLit (c : MClause) (i : Nat) : RuleM.RuleM (Array ClausificationResult)

Equations

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

def Duper.clausificationStep : MSimpRule

Equations

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