def Trestle.IVar.toPropFun (v : IVar) : Model.PropFun IVar

Equations

• v.toPropFun = Trestle.Model.PropFun.var v

instance Trestle.IVar.instCoePropFun : Coe IVar (Model.PropFun IVar)

Equations

• Trestle.IVar.instCoePropFun = { coe := Trestle.IVar.toPropFun }

theorem Trestle.IVar.eq_PNat : IVar = ℕ+

@[simp]

theorem Trestle.IVar.ne_zero (v : IVar) : ↑v ≠ 0

@[simp]

theorem Trestle.IVar.pos (v : IVar) : 0 < ↑v

def Trestle.IVar.natPred : IVar → ℕ

Equations

• Trestle.IVar.natPred = PNat.natPred

@[simp]

theorem Trestle.IVar.natPred_inj {m n : IVar} : m.natPred = n.natPred ↔ m = n

@[simp]

theorem Trestle.IVar.index_eq_iff {v₁ v₂ : IVar} : v₁.index = v₂.index ↔ v₁ = v₂

@[simp]

theorem Trestle.IVar.index_ne_iff {v₁ v₂ : IVar} : v₁.index ≠ v₂.index ↔ v₁ ≠ v₂

@[simp]

theorem Trestle.IVar.toPosILit_negate (v : IVar) : -v.toPosILit = v.toNegILit

@[simp]

theorem Trestle.IVar.toNegILit_negate (v : IVar) : -v.toNegILit = v.toPosILit

@[simp]

theorem Trestle.ILit.toIVar_negate (l : ILit) : (-l).toIVar = l.toIVar

@[simp]

theorem Trestle.ILit.toIVar_mkPos (v : IVar) : (LitVar.mkPos v).toIVar = v

@[simp]

theorem Trestle.ILit.toIVar_mkNeg (v : IVar) : (LitVar.mkNeg v).toIVar = v

@[reducible, inline]

abbrev Trestle.ILit.toPropFun (l : ILit) : Model.PropFun IVar

Equations

• l.toPropFun = Trestle.LitVar.toPropFun l

instance Trestle.ILit.instCoeILit : Coe ILit (Model.PropFun IVar)

Equations

• Trestle.ILit.instCoeILit = { coe := Trestle.LitVar.toPropFun }

theorem Trestle.ILit.exists_succ_toVar (l : ILit) : ∃ (n : ℕ), ↑(LitVar.toVar l) = n + 1

@[simp]

theorem Trestle.ILit.toVar_index (l : ILit) : (LitVar.toVar l).index = l.index

@[simp]

theorem Trestle.ILit.index_mkPos (v : IVar) : (LitVar.mkPos v).index = v.index

@[simp]

theorem Trestle.ILit.index_mkNeg (v : IVar) : (LitVar.mkNeg v).index = v.index

@[simp]

theorem Trestle.ILit.index_negate (l : ILit) : (-l).index = l.index

theorem Trestle.ILit.index_eq_iff_toVar_eq {l₁ l₂ : ILit} : l₁.index = l₂.index ↔ LitVar.toVar l₁ = LitVar.toVar l₂

theorem Trestle.ILit.index_ne_of_var_ne {l₁ l₂ : ILit} : LitVar.toVar l₁ ≠ LitVar.toVar l₂ → l₁.index ≠ l₂.index

theorem Trestle.ILit.index_eq_iff_eq_or_negate_eq {l₁ l₂ : ILit} : l₁.index = l₂.index ↔ l₁ = l₂ ∨ -l₁ = l₂