Theorem: Etch.Verification.Stream.LawfulOfStream.get_fold
Proof state before:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ evalFinsupp
        (Readable.get
          (if hr : s.ready q = true then
            Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))
          else b)
          i) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      ((if h₂ : s.ready q = true then fun₀ | s.index q => evalFinsupp (s.value { val := q, property := h₂ }) else 0) i +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)

case pos.a
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ WfRel s (s.seek q (toOrder s q)) ↑q
Tactic:
split_ifs with hr
Proof state after:
case pos
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : s.ready q = true
⊢ evalFinsupp
        (Readable.get (Modifiable.update b (s.index q) (OfStream.eval (s.value { val := q, property := hr }))) i) +
      (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) +
      ((fun₀ | s.index q => evalFinsupp (s.value { val := q, property := hr })) i +
        (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)

case neg
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
hr : ¬s.ready q = true
⊢ evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i =
    evalFinsupp (Readable.get b i) + (0 i + (eval (map (⇑evalFinsupp) s) (s.seek q (toOrder s q))) i)

case pos.a
ι : Type
inst✝⁹ : LinearOrder ι
α : Type u_1
β : Type u_2
m : Type u_3
γ : Type u_4
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : Zero m
inst✝⁵ : AddCommMonoid γ
inst✝⁴ : EvalToFinsupp α γ
inst✝³ : EvalToFinsupp β γ
inst✝² : LawfulOfStream α β γ
inst✝¹ : LawfulModifiable ι β m
s : Stream ι α
inst✝ : IsBounded s
i : ι
b : m
q : { t // s.valid t = true }
ih :
  ∀ (y : s.σ),
    WfRel s y ↑q →
      ∀ (b : m),
        evalFinsupp (Readable.get (fold_wf Modifiable.update (map OfStream.eval s) y b) i) =
          evalFinsupp (Readable.get b i) + (eval (map (⇑evalFinsupp) s) y) i
⊢ WfRel s (s.seek q (toOrder s q)) ↑q