Theorem: LRAT.DefaultFormula.encounteredBoth_entails_unsat
Proof state before:
case h_3.h_1
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = pos
h : (if l.snd = true then reducedToNonunit else reducedToUnit l'✝) = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_2
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = neg
h : (if (!l.snd) = true then reducedToNonunit else reducedToUnit l'✝) = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_3
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = both
h : encounteredBoth = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_4
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = unassigned
h : reducedToNonunit = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment
Tactic:
. split at h <;> simp only at h
Proof state after:
case h_3.h_2
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = neg
h : (if (!l.snd) = true then reducedToNonunit else reducedToUnit l'✝) = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_3
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = both
h : encounteredBoth = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment

case h_3.h_4
n : Nat
c : DefaultClause n
assignment : Array Assignment
hb : reducedToEmpty = encounteredBoth → unsatisfiable (PosFin n) assignment
l : Literal (PosFin n)
x✝¹ : l ∈ c.clause
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reducedToUnit l'✝ = encounteredBoth → unsatisfiable (PosFin n) assignment
x✝ : Assignment
heq✝ : assignment[l.fst.val]! = unassigned
h : reducedToNonunit = encounteredBoth
⊢ unsatisfiable (PosFin n) assignment