Theorem: LRAT.Literal.unsat_of_limplies_complement (LeanSAT/LRAT/CNF.lean)

State before:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
⊢ limplies α x l → limplies α x l.negateLiteral → unsatisfiable α x
Tactic:
intro h1 h2 p px
State after:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
h1 : limplies α x l
h2 : limplies α x l.negateLiteral
p : α → Bool
px : p ⊨ x
⊢ False

State before:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
h1 : limplies α x l
h2 : limplies α x l.negateLiteral
p : α → Bool
px : p ⊨ x
⊢ False
Tactic:
specialize h1 p px
State after:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
h2 : limplies α x l.negateLiteral
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
⊢ False

State before:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
h2 : limplies α x l.negateLiteral
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
⊢ False
Tactic:
specialize h2 p px
State after:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
h2 : p ⊨ l.negateLiteral
⊢ False

State before:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
h2 : p ⊨ l.negateLiteral
⊢ False
Tactic:
rw [sat_negate_iff_not_sat] at h2
State after:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
h2 : ¬(p ⊨ l)
⊢ False

State before:
α : Type u_1
t : Type u_2
inst✝ : HSat α t
x : t
l : Literal α
p : α → Bool
px : p ⊨ x
h1 : p ⊨ l
h2 : ¬(p ⊨ l)
⊢ False
Tactic:
exact h2 h1
State after:
no goals