Theorem: LRAT.DefaultFormula.reduce_fold_fn_preserves_induction_motive
Proof state before:
case right
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
res : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) res
i : PosFin n
b : Bool
h :
  (match res with
    | encounteredBoth => encounteredBoth
    | reducedToEmpty =>
      match assignment[c_arr[↑idx].fst.val]! with
      | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
      | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
      | both => encounteredBoth
      | unassigned => reducedToUnit c_arr[↑idx]
    | reducedToUnit l' =>
      match assignment[c_arr[↑idx].fst.val]! with
      | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'
      | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'
      | both => encounteredBoth
      | unassigned => reducedToNonunit
    | reducedToNonunit => reducedToNonunit) =
    reducedToUnit (i, b)
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
⊢ p ⊨ (i, b)
Tactic:
split at h
Proof state after:
case right.h_1
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) encounteredBoth
h : encounteredBoth = reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_2
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToEmpty
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | neg => if (!c_arr[↑idx].snd) = true then reducedToUnit c_arr[↑idx] else reducedToEmpty
    | both => encounteredBoth
    | unassigned => reducedToUnit c_arr[↑idx]) =
    reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_3
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
l'✝ : Literal (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) (reducedToUnit l'✝)
h :
  (match assignment[c_arr[↑idx].fst.val]! with
    | pos => if c_arr[↑idx].snd = true then reducedToNonunit else reducedToUnit l'✝
    | neg => if (!c_arr[↑idx].snd) = true then reducedToNonunit else reducedToUnit l'✝
    | both => encounteredBoth
    | unassigned => reducedToNonunit) =
    reducedToUnit (i, b)
⊢ p ⊨ (i, b)

case right.h_4
n : Nat
c_arr : Array (Literal (PosFin n))
assignment : Array Assignment
idx : Fin c_arr.size
i : PosFin n
b : Bool
p : PosFin n → Bool
hp : p ⊨ assignment
j : Fin c_arr.size
j_lt_idx_add_one : ↑j < ↑idx + 1
p_entails_c_arr_j : p ⊨ c_arr[↑j]
acc✝ : ReduceResult (PosFin n)
ih : reduce_postcondition_induction_motive c_arr assignment (↑idx) reducedToNonunit
h : reducedToNonunit = reducedToUnit (i, b)
⊢ p ⊨ (i, b)