Theorem: LRAT.DefaultFormula.ofArray_readyForRatAdd (LeanSAT/LRAT/Formula/Basic.lean)

State before:
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).readyForRatAdd
Tactic:
constructor
State after:
case left
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).ratUnits = #[]

case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).readyForRupAdd

State before:
case left
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).ratUnits = #[]

case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).readyForRupAdd
Tactic:
. simp only [ofArray]
State after:
case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).readyForRupAdd

State before:
case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).readyForRupAdd
Tactic:
. exact ofArray_readyForRupAdd arr
State after:
no goals

State before:
case left
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).ratUnits = #[]
Tactic:
simp only [ofArray]
State after:
no goals

State before:
case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).readyForRupAdd
Tactic:
exact ofArray_readyForRupAdd arr
State after:
no goals