Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_assignments_size
Proof state before:
case isFalse.h_1.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
l✝ : PosFin n
b✝ : Bool
heq✝ : c✝.reduce assignments = ReduceResult.reducedToUnit (l✝, b✝)
⊢ (if hasAssignment b✝ assignments[l✝.val]! = true then (assignments, derivedLits, false, false)
        else (assignments.modify l✝.val (addAssignment b✝), (l✝, b✝) :: derivedLits, false, false)).fst.size =
    assignments.size

case isFalse.h_1.h_4
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
heq✝ : c✝.reduce assignments = ReduceResult.reducedToNonunit
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_2
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = some none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size
Tactic:
split
Proof state after:
case isFalse.h_1.h_3.isTrue
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝¹ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
l✝ : PosFin n
b✝ : Bool
heq✝ : c✝.reduce assignments = ReduceResult.reducedToUnit (l✝, b✝)
h✝ : hasAssignment b✝ assignments[l✝.val]! = true
⊢ (assignments, derivedLits, false, false).fst.size = assignments.size

case isFalse.h_1.h_3.isFalse
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝¹ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
l✝ : PosFin n
b✝ : Bool
heq✝ : c✝.reduce assignments = ReduceResult.reducedToUnit (l✝, b✝)
h✝ : ¬hasAssignment b✝ assignments[l✝.val]! = true
⊢ (assignments.modify l✝.val (addAssignment b✝), (l✝, b✝) :: derivedLits, false, false).fst.size = assignments.size

case isFalse.h_1.h_4
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝¹ : Option (Option (DefaultClause n))
c✝ : DefaultClause n
heq✝¹ : clauses[id]? = some (some c✝)
x✝ : ReduceResult (PosFin n)
heq✝ : c✝.reduce assignments = ReduceResult.reducedToNonunit
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_2
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = some none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size

case isFalse.h_3
n : Nat
clauses : Array (Option (DefaultClause n))
assignments : Array Assignment
derivedLits : List (Literal (PosFin n))
b1 b2 : Bool
id : Nat
h✝ : ¬(b2 || b1) = true
x✝ : Option (Option (DefaultClause n))
heq✝ : clauses[id]? = none
⊢ (assignments, derivedLits, false, true).fst.size = assignments.size