import Pretty.Claims.ResolveDet
import Pretty.Supports.DocSize

/-!
## Totality of resolving theorems
-/

mutual 
  /--
  The totality of resolving (Page 19, Section 5.6)
  -/
  theorem Resolve_total: ∀ {α : Type} (F : Factory α) (d : Doc) (c i : ℕ), ∃ ms, Resolve F d c i ms
Resolve_total (F: Factory α
F : Factory: Type → Type
Factory α: ?m.3
α) (d: Doc
d : Doc: Type
Doc) (c: ℕ
c i: ℕ
i : ℕ: Type
ℕ) : ∃ ms: ?m.17
ms, Resolve: {α : Type} → Factory α → Doc → ℕ → ℕ → MeasureSet → Prop
Resolve F: Factory α
F d: Doc
d c: ℕ
c i: ℕ
i ms: ?m.17
ms := by
Goals accomplished! 🐙 
    α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F d c i msmatch d: Doc
d with
    α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F d c i ms| Doc.text: String → Doc
Doc.text s: String
s =>α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

∃ ms, Resolve F (Doc.text s) c i ms 
      α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F d c i msby_cases h_i: ?m.379
h_i : i: ℕ
i ≤ F: Factory α
F.W: {α : Type} → Factory α → ℕ
Wα: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

pos∃ ms, Resolve F (Doc.text s) c i ms
α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: ¬i ≤ F.W

neg∃ ms, Resolve F (Doc.text s) c i ms
      α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

∃ ms, Resolve F (Doc.text s) c i mscase pos => 
        α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

∃ ms, Resolve F (Doc.text s) c i msby_cases h_c: ?m.458
h_c : c: ℕ
c + s: String
s.length: String → ℕ
length ≤ F: Factory α
F.W: {α : Type} → Factory α → ℕ
Wα: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

pos∃ ms, Resolve F (Doc.text s) c i ms
α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: ¬c + String.length s ≤ F.W

neg∃ ms, Resolve F (Doc.text s) c i ms 
        α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

∃ ms, Resolve F (Doc.text s) c i mscase pos => 
          α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

∃ ms, Resolve F (Doc.text s) c i mslet ⟨m: Meas
m, h: MeasRender F (Doc.text s) c i m
h⟩ := MeasRender_total: ∀ {α : Type} (F : Factory α) (d : Doc) (c i : ℕ), Choiceless d → ∃ m, MeasRender F d c i m
MeasRender_total F: Factory α
F (Doc.text: String → Doc
Doc.text s: String
s) c: ℕ
c i: ℕ
i (α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

∃ ms, Resolve F (Doc.text s) c i msby
Goals accomplished! 🐙 α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

Choiceless (Doc.text s)constructor
Goals accomplished! 🐙)α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

∃ ms, Resolve F (Doc.text s) c i ms
          α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

∃ ms, Resolve F (Doc.text s) c i msexists MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set [m: Meas
m] (α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

∃ ms, Resolve F (Doc.text s) c i msby
Goals accomplished! 🐙 α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

[m] ≠ []simp
Goals accomplished! 🐙)α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

Resolve F (Doc.text s) c i (MeasureSet.set [m] (_ : ¬[m] = [])) 
          α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

∃ ms, Resolve F (Doc.text s) c i msconstructorα: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

h_cc + String.length s ≤ F.W
α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

h_ii ≤ F.W
α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

hMeasRender F (Doc.text s) c i m α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

Resolve F (Doc.text s) c i (MeasureSet.set [m] (_ : ¬[m] = []))<;>α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

h_cc + String.length s ≤ F.W
α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

h_ii ≤ F.W
α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

hMeasRender F (Doc.text s) c i m α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s ≤ F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

Resolve F (Doc.text s) c i (MeasureSet.set [m] (_ : ¬[m] = []))assumption
Goals accomplished! 🐙
        α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

∃ ms, Resolve F (Doc.text s) c i mscase neg => 
          α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: ¬c + String.length s ≤ F.W

∃ ms, Resolve F (Doc.text s) c i msreplace h_c: ?m.1268
h_c := Nat.gt_of_not_le: ∀ {n m : ℕ}, ¬n ≤ m → n > m
Nat.gt_of_not_le h_c: ?m.465
h_cα: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s > F.W

∃ ms, Resolve F (Doc.text s) c i ms
          α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: ¬c + String.length s ≤ F.W

∃ ms, Resolve F (Doc.text s) c i mslet ⟨m: Meas
m, h: MeasRender F (Doc.text s) c i m
h⟩ := MeasRender_total: ∀ {α : Type} (F : Factory α) (d : Doc) (c i : ℕ), Choiceless d → ∃ m, MeasRender F d c i m
MeasRender_total F: Factory α
F (Doc.text: String → Doc
Doc.text s: String
s) c: ℕ
c i: ℕ
i (α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s > F.W

∃ ms, Resolve F (Doc.text s) c i msby
Goals accomplished! 🐙 α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s > F.W

Choiceless (Doc.text s)constructor
Goals accomplished! 🐙)α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s > F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

∃ ms, Resolve F (Doc.text s) c i ms
          α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: ¬c + String.length s ≤ F.W

∃ ms, Resolve F (Doc.text s) c i msexists MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted m: Meas
mα: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s > F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

Resolve F (Doc.text s) c i (MeasureSet.tainted m)
          α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: ¬c + String.length s ≤ F.W

∃ ms, Resolve F (Doc.text s) c i msconstructorα: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s > F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

h_badc + String.length s > F.W ∨ i > F.W
α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s > F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

hMeasRender F (Doc.text s) c i m 
          α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: ¬c + String.length s ≤ F.W

∃ ms, Resolve F (Doc.text s) c i mscase h_bad => α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s > F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

c + String.length s > F.W ∨ i > F.Wsimp [h_c: ?m.1268
h_c]
Goals accomplished! 🐙
          α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: ¬c + String.length s ≤ F.W

∃ ms, Resolve F (Doc.text s) c i mscase h => α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i ≤ F.W

h_c: c + String.length s > F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

MeasRender F (Doc.text s) c i massumption
Goals accomplished! 🐙
      α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

∃ ms, Resolve F (Doc.text s) c i mscase neg => 
        α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: ¬i ≤ F.W

∃ ms, Resolve F (Doc.text s) c i msreplace h_i: ?m.2282
h_i := Nat.gt_of_not_le: ∀ {n m : ℕ}, ¬n ≤ m → n > m
Nat.gt_of_not_le h_i: ?m.386
h_iα: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i > F.W

∃ ms, Resolve F (Doc.text s) c i ms
        α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: ¬i ≤ F.W

∃ ms, Resolve F (Doc.text s) c i mslet ⟨m: Meas
m, h: MeasRender F (Doc.text s) c i m
h⟩ := MeasRender_total: ∀ {α : Type} (F : Factory α) (d : Doc) (c i : ℕ), Choiceless d → ∃ m, MeasRender F d c i m
MeasRender_total F: Factory α
F (Doc.text: String → Doc
Doc.text s: String
s) c: ℕ
c i: ℕ
i (α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i > F.W

∃ ms, Resolve F (Doc.text s) c i msby
Goals accomplished! 🐙 α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i > F.W

Choiceless (Doc.text s)constructor
Goals accomplished! 🐙)α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i > F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

∃ ms, Resolve F (Doc.text s) c i ms
        α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: ¬i ≤ F.W

∃ ms, Resolve F (Doc.text s) c i msexists MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted m: Meas
mα: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i > F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

Resolve F (Doc.text s) c i (MeasureSet.tainted m)
        α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: ¬i ≤ F.W

∃ ms, Resolve F (Doc.text s) c i msconstructorα: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i > F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

h_badc + String.length s > F.W ∨ i > F.W
α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i > F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

hMeasRender F (Doc.text s) c i m 
        α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: ¬i ≤ F.W

∃ ms, Resolve F (Doc.text s) c i mscase h_bad => α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i > F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

c + String.length s > F.W ∨ i > F.Wsimp [h_i: ?m.2282
h_i]
Goals accomplished! 🐙
        α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: ¬i ≤ F.W

∃ ms, Resolve F (Doc.text s) c i mscase h => α: Type

F: Factory α

d: Doc

c, i: ℕ

s: String

h_i: i > F.W

m: Meas

h: MeasRender F (Doc.text s) c i m

MeasRender F (Doc.text s) c i massumption
Goals accomplished! 🐙
    α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F d c i ms| Doc.nl: Doc
Doc.nl =>α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F Doc.nl c i ms
      α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F d c i msby_cases h_i: ?m.3181
h_i : i: ℕ
i ≤ F: Factory α
F.W: {α : Type} → Factory α → ℕ
Wα: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

pos∃ ms, Resolve F Doc.nl c i ms
α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: ¬i ≤ F.W

neg∃ ms, Resolve F Doc.nl c i ms
      α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F Doc.nl c i mscase pos => 
        α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

∃ ms, Resolve F Doc.nl c i mslet ⟨m: Meas
m, h: MeasRender F Doc.nl c i m
h⟩ := MeasRender_total: ∀ {α : Type} (F : Factory α) (d : Doc) (c i : ℕ), Choiceless d → ∃ m, MeasRender F d c i m
MeasRender_total F: Factory α
F Doc.nl: Doc
Doc.nl c: ℕ
c i: ℕ
i (α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

∃ ms, Resolve F Doc.nl c i msby
Goals accomplished! 🐙 α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

Choiceless Doc.nlconstructor
Goals accomplished! 🐙)α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

∃ ms, Resolve F Doc.nl c i ms
        α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

∃ ms, Resolve F Doc.nl c i msby_cases h_c: ?m.3324
h_c : c: ℕ
c ≤ F: Factory α
F.W: {α : Type} → Factory α → ℕ
Wα: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c ≤ F.W

pos∃ ms, Resolve F Doc.nl c i ms
α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: ¬c ≤ F.W

neg∃ ms, Resolve F Doc.nl c i ms 
        α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

∃ ms, Resolve F Doc.nl c i mscase pos => 
          α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c ≤ F.W

∃ ms, Resolve F Doc.nl c i msexists MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set [m: Meas
m] (α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c ≤ F.W

∃ ms, Resolve F Doc.nl c i msby
Goals accomplished! 🐙 α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c ≤ F.W

[m] ≠ []simp
Goals accomplished! 🐙)α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c ≤ F.W

Resolve F Doc.nl c i (MeasureSet.set [m] (_ : ¬[m] = []))
          α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c ≤ F.W

∃ ms, Resolve F Doc.nl c i msconstructorα: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c ≤ F.W

h_cc ≤ F.W
α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c ≤ F.W

h_ii ≤ F.W
α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c ≤ F.W

hMeasRender F Doc.nl c i m α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c ≤ F.W

Resolve F Doc.nl c i (MeasureSet.set [m] (_ : ¬[m] = []))<;>α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c ≤ F.W

h_cc ≤ F.W
α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c ≤ F.W

h_ii ≤ F.W
α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c ≤ F.W

hMeasRender F Doc.nl c i m α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c ≤ F.W

Resolve F Doc.nl c i (MeasureSet.set [m] (_ : ¬[m] = []))assumption
Goals accomplished! 🐙
        α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

∃ ms, Resolve F Doc.nl c i mscase neg => 
          α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: ¬c ≤ F.W

∃ ms, Resolve F Doc.nl c i msreplace h_c: ?m.3938
h_c := Nat.gt_of_not_le: ∀ {n m : ℕ}, ¬n ≤ m → n > m
Nat.gt_of_not_le h_c: ?m.3331
h_cα: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c > F.W

∃ ms, Resolve F Doc.nl c i ms
          α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: ¬c ≤ F.W

∃ ms, Resolve F Doc.nl c i msexists MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted m: Meas
mα: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c > F.W

Resolve F Doc.nl c i (MeasureSet.tainted m)
          α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: ¬c ≤ F.W

∃ ms, Resolve F Doc.nl c i msconstructorα: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c > F.W

h_badc > F.W ∨ i > F.W
α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c > F.W

hMeasRender F Doc.nl c i m α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c > F.W

Resolve F Doc.nl c i (MeasureSet.tainted m)<;>α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c > F.W

h_badc > F.W ∨ i > F.W
α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c > F.W

hMeasRender F Doc.nl c i m α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i ≤ F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_c: c > F.W

Resolve F Doc.nl c i (MeasureSet.tainted m)simp [*]
Goals accomplished! 🐙
      α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F Doc.nl c i mscase neg => 
        α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: ¬i ≤ F.W

∃ ms, Resolve F Doc.nl c i msreplace h_i: ?m.4744
h_i := Nat.gt_of_not_le: ∀ {n m : ℕ}, ¬n ≤ m → n > m
Nat.gt_of_not_le h_i: ?m.3188
h_iα: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i > F.W

∃ ms, Resolve F Doc.nl c i ms
        α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: ¬i ≤ F.W

∃ ms, Resolve F Doc.nl c i mslet ⟨m: Meas
m, h: MeasRender F Doc.nl c i m
h⟩ := MeasRender_total: ∀ {α : Type} (F : Factory α) (d : Doc) (c i : ℕ), Choiceless d → ∃ m, MeasRender F d c i m
MeasRender_total F: Factory α
F Doc.nl: Doc
Doc.nl c: ℕ
c i: ℕ
i (α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i > F.W

∃ ms, Resolve F Doc.nl c i msby
Goals accomplished! 🐙 α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i > F.W

Choiceless Doc.nlconstructor
Goals accomplished! 🐙)α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i > F.W

m: Meas

h: MeasRender F Doc.nl c i m

∃ ms, Resolve F Doc.nl c i ms
        α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: ¬i ≤ F.W

∃ ms, Resolve F Doc.nl c i msexists MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted m: Meas
mα: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i > F.W

m: Meas

h: MeasRender F Doc.nl c i m

Resolve F Doc.nl c i (MeasureSet.tainted m)
        α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: ¬i ≤ F.W

∃ ms, Resolve F Doc.nl c i msconstructorα: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i > F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_badc > F.W ∨ i > F.W
α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i > F.W

m: Meas

h: MeasRender F Doc.nl c i m

hMeasRender F Doc.nl c i m α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i > F.W

m: Meas

h: MeasRender F Doc.nl c i m

Resolve F Doc.nl c i (MeasureSet.tainted m)<;>α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i > F.W

m: Meas

h: MeasRender F Doc.nl c i m

h_badc > F.W ∨ i > F.W
α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i > F.W

m: Meas

h: MeasRender F Doc.nl c i m

hMeasRender F Doc.nl c i m α: Type

F: Factory α

d: Doc

c, i: ℕ

h_i: i > F.W

m: Meas

h: MeasRender F Doc.nl c i m

Resolve F Doc.nl c i (MeasureSet.tainted m)simp [*]
Goals accomplished! 🐙
    α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F d c i ms| Doc.nest: ℕ → Doc → Doc
Doc.nest n: ℕ
n d: Doc
d =>α: Type

F: Factory α

d✝: Doc

c, i, n: ℕ

d: Doc

∃ ms, Resolve F (Doc.nest n d) c i ms 
      α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F d c i mslet ⟨ms: MeasureSet
ms, h: Resolve F d c (i + n) ms
h⟩ := Resolve_total: ∀ {α : Type} (F : Factory α) (d : Doc) (c i : ℕ), ∃ ms, Resolve F d c i ms
Resolve_total F: Factory α
F d: Doc
d c: ℕ
c (i: ℕ
i + n: ℕ
n)α: Type

F: Factory α

d✝: Doc

c, i, n: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c (i + n) ms

∃ ms, Resolve F (Doc.nest n d) c i ms
      α: Type

F: Factory α

d✝: Doc

c, i, n: ℕ

d: Doc

∃ ms, Resolve F (Doc.nest n d) c i msexists ms: MeasureSet
ms.lift: {α : Type} → (Meas → Meas) → MeasureSet → MeasureSet
lift (Meas.adjust_nest: {α : Type} → ℕ → Meas → Meas
Meas.adjust_nest n: ℕ
n)α: Type

F: Factory α

d✝: Doc

c, i, n: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c (i + n) ms

Resolve F (Doc.nest n d) c i (MeasureSet.lift (Meas.adjust_nest n) ms) 
      α: Type

F: Factory α

d✝: Doc

c, i, n: ℕ

d: Doc

∃ ms, Resolve F (Doc.nest n d) c i msconstructorα: Type

F: Factory α

d✝: Doc

c, i, n: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c (i + n) ms

hResolve F d c (i + n) ms
      α: Type

F: Factory α

d✝: Doc

c, i, n: ℕ

d: Doc

∃ ms, Resolve F (Doc.nest n d) c i msassumption
Goals accomplished! 🐙
    α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F d c i ms| Doc.align: Doc → Doc
Doc.align d: Doc
d =>α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

∃ ms, Resolve F (Doc.align d) c i ms 
      α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F d c i mslet ⟨ms: MeasureSet
ms, h: Resolve F d c c ms
h⟩ := Resolve_total: ∀ {α : Type} (F : Factory α) (d : Doc) (c i : ℕ), ∃ ms, Resolve F d c i ms
Resolve_total F: Factory α
F d: Doc
d c: ℕ
c c: ℕ
cα: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

∃ ms, Resolve F (Doc.align d) c i ms
      α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

∃ ms, Resolve F (Doc.align d) c i msby_cases h_i: ?m.7431
h_i : i: ℕ
i ≤ F: Factory α
F.W: {α : Type} → Factory α → ℕ
Wα: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i ≤ F.W

pos∃ ms, Resolve F (Doc.align d) c i ms
α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: ¬i ≤ F.W

neg∃ ms, Resolve F (Doc.align d) c i ms 
      α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

∃ ms, Resolve F (Doc.align d) c i mscase pos => 
        α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i ≤ F.W

∃ ms, Resolve F (Doc.align d) c i msexists ms: MeasureSet
ms.lift: {α : Type} → (Meas → Meas) → MeasureSet → MeasureSet
lift (Meas.adjust_align: {α : Type} → ℕ → Meas → Meas
Meas.adjust_align i: ℕ
i)α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i ≤ F.W

Resolve F (Doc.align d) c i (MeasureSet.lift (Meas.adjust_align i) ms) 
        α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i ≤ F.W

∃ ms, Resolve F (Doc.align d) c i msconstructorα: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i ≤ F.W

h_oki ≤ F.W
α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i ≤ F.W

hResolve F d c c ms α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i ≤ F.W

Resolve F (Doc.align d) c i (MeasureSet.lift (Meas.adjust_align i) ms)<;>α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i ≤ F.W

h_oki ≤ F.W
α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i ≤ F.W

hResolve F d c c ms α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i ≤ F.W

Resolve F (Doc.align d) c i (MeasureSet.lift (Meas.adjust_align i) ms)assumption
Goals accomplished! 🐙
      α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

∃ ms, Resolve F (Doc.align d) c i mscase neg => 
        α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: ¬i ≤ F.W

∃ ms, Resolve F (Doc.align d) c i msreplace h_i: ?m.9208
h_i := Nat.gt_of_not_le: ∀ {n m : ℕ}, ¬n ≤ m → n > m
Nat.gt_of_not_le h_i: ?m.7431
h_iα: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i > F.W

∃ ms, Resolve F (Doc.align d) c i ms
        α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: ¬i ≤ F.W

∃ ms, Resolve F (Doc.align d) c i msexists ms: MeasureSet
ms.taint: {α : Type} → MeasureSet → MeasureSet
taint.lift: {α : Type} → (Meas → Meas) → MeasureSet → MeasureSet
lift (Meas.adjust_align: {α : Type} → ℕ → Meas → Meas
Meas.adjust_align i: ℕ
i)α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i > F.W

Resolve F (Doc.align d) c i (MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms)) 
        α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: ¬i ≤ F.W

∃ ms, Resolve F (Doc.align d) c i msconstructorα: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i > F.W

h_badi > F.W
α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i > F.W

hResolve F d c c ms α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i > F.W

Resolve F (Doc.align d) c i (MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms))<;>α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i > F.W

h_badi > F.W
α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i > F.W

hResolve F d c c ms α: Type

F: Factory α

d✝: Doc

c, i: ℕ

d: Doc

ms: MeasureSet

h: Resolve F d c c ms

h_i: i > F.W

Resolve F (Doc.align d) c i (MeasureSet.lift (Meas.adjust_align i) (MeasureSet.taint ms))assumption
Goals accomplished! 🐙
    α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F d c i ms| Doc.choice: Doc → Doc → Doc
Doc.choice d₁: Doc
d₁ d₂: Doc
d₂ =>α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

∃ ms, Resolve F (Doc.choice d₁ d₂) c i ms 
      α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F d c i mslet ⟨ms₁: MeasureSet
ms₁, h₁: Resolve F d₁ c i ms₁
h₁⟩ := Resolve_total: ∀ {α : Type} (F : Factory α) (d : Doc) (c i : ℕ), ∃ ms, Resolve F d c i ms
Resolve_total F: Factory α
F d₁: Doc
d₁ c: ℕ
c i: ℕ
iα: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms₁: MeasureSet

h₁: Resolve F d₁ c i ms₁

∃ ms, Resolve F (Doc.choice d₁ d₂) c i ms
      α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

∃ ms, Resolve F (Doc.choice d₁ d₂) c i mslet ⟨ms₂: MeasureSet
ms₂, h₂: Resolve F d₂ c i ms₂
h₂⟩ := Resolve_total: ∀ {α : Type} (F : Factory α) (d : Doc) (c i : ℕ), ∃ ms, Resolve F d c i ms
Resolve_total F: Factory α
F d₂: Doc
d₂ c: ℕ
c i: ℕ
iα: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms₁: MeasureSet

h₁: Resolve F d₁ c i ms₁

ms₂: MeasureSet

h₂: Resolve F d₂ c i ms₂

∃ ms, Resolve F (Doc.choice d₁ d₂) c i ms 
      α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

∃ ms, Resolve F (Doc.choice d₁ d₂) c i msexists MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union F: Factory α
F ms₁: MeasureSet
ms₁ ms₂: MeasureSet
ms₂α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms₁: MeasureSet

h₁: Resolve F d₁ c i ms₁

ms₂: MeasureSet

h₂: Resolve F d₂ c i ms₂

Resolve F (Doc.choice d₁ d₂) c i (MeasureSet.union F ms₁ ms₂)
      α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

∃ ms, Resolve F (Doc.choice d₁ d₂) c i msconstructorα: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms₁: MeasureSet

h₁: Resolve F d₁ c i ms₁

ms₂: MeasureSet

h₂: Resolve F d₂ c i ms₂

h_leftResolve F d₁ c i ms₁
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms₁: MeasureSet

h₁: Resolve F d₁ c i ms₁

ms₂: MeasureSet

h₂: Resolve F d₂ c i ms₂

h_rightResolve F d₂ c i ms₂ α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms₁: MeasureSet

h₁: Resolve F d₁ c i ms₁

ms₂: MeasureSet

h₂: Resolve F d₂ c i ms₂

Resolve F (Doc.choice d₁ d₂) c i (MeasureSet.union F ms₁ ms₂)<;>α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms₁: MeasureSet

h₁: Resolve F d₁ c i ms₁

ms₂: MeasureSet

h₂: Resolve F d₂ c i ms₂

h_leftResolve F d₁ c i ms₁
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms₁: MeasureSet

h₁: Resolve F d₁ c i ms₁

ms₂: MeasureSet

h₂: Resolve F d₂ c i ms₂

h_rightResolve F d₂ c i ms₂ α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms₁: MeasureSet

h₁: Resolve F d₁ c i ms₁

ms₂: MeasureSet

h₂: Resolve F d₂ c i ms₂

Resolve F (Doc.choice d₁ d₂) c i (MeasureSet.union F ms₁ ms₂)assumption
Goals accomplished! 🐙
    α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F d c i ms| Doc.concat: Doc → Doc → Doc
Doc.concat d₁: Doc
d₁ d₂: Doc
d₂ =>α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

∃ ms, Resolve F (Doc.concat d₁ d₂) c i ms 
      α: Type

F: Factory α

d: Doc

c, i: ℕ

∃ ms, Resolve F d c i mslet ⟨ms₁: MeasureSet
ms₁, h₁: Resolve F d₁ c i ms₁
h₁⟩ := Resolve_total: ∀ {α : Type} (F : Factory α) (d : Doc) (c i : ℕ), ∃ ms, Resolve F d c i ms
Resolve_total F: Factory α
F d₁: Doc
d₁ c: ℕ
c i: ℕ
iα: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms₁: MeasureSet

h₁: Resolve F d₁ c i ms₁

∃ ms, Resolve F (Doc.concat d₁ d₂) c i ms
      α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

∃ ms, Resolve F (Doc.concat d₁ d₂) c i mscases ms₁: MeasureSet
ms₁α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m✝: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m✝)

tainted∃ ms, Resolve F (Doc.concat d₁ d₂) c i ms
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms✝: List Meas

h✝: ms✝ ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms✝ h✝)

set∃ ms, Resolve F (Doc.concat d₁ d₂) c i ms 
      α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

∃ ms, Resolve F (Doc.concat d₁ d₂) c i mscase tainted m₁: Meas
m₁ => 
        α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

∃ ms, Resolve F (Doc.concat d₁ d₂) c i mslet ⟨ms₂: MeasureSet
ms₂, h₂: Resolve F d₂ m₁.last i ms₂
h₂⟩ := Resolve_total: ∀ {α : Type} (F : Factory α) (d : Doc) (c i : ℕ), ∃ ms, Resolve F d c i ms
Resolve_total F: Factory α
F d₂: Doc
d₂ m₁: Meas
m₁.last: {α : Type} → Meas → ℕ
last i: ℕ
iα: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

∃ ms, Resolve F (Doc.concat d₁ d₂) c i ms
        α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

∃ ms, Resolve F (Doc.concat d₁ d₂) c i mshave : ∃ m₂: ?m.14553
m₂, ms₂: MeasureSet
ms₂.taint: {α : Type} → MeasureSet → MeasureSet
taint = MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted m₂: ?m.14553
m₂ := α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

∃ ms, Resolve F (Doc.concat d₁ d₂) c i msby
Goals accomplished! 🐙 α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂{α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂
          α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂cases ms₂: MeasureSet
ms₂α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

m✝: Meas

h₂: Resolve F d₂ m₁.last i (MeasureSet.tainted m✝)

tainted∃ m₂, MeasureSet.taint (MeasureSet.tainted m✝) = MeasureSet.tainted m₂
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms✝: List Meas

h✝: ms✝ ≠ []

h₂: Resolve F d₂ m₁.last i (MeasureSet.set ms✝ h✝)

set∃ m₂, MeasureSet.taint (MeasureSet.set ms✝ h✝) = MeasureSet.tainted m₂
          α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂all_goals α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

m✝: Meas

h₂: Resolve F d₂ m₁.last i (MeasureSet.tainted m✝)

tainted∃ m₂, MeasureSet.taint (MeasureSet.tainted m✝) = MeasureSet.tainted m₂
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms✝: List Meas

h✝: ms✝ ≠ []

h₂: Resolve F d₂ m₁.last i (MeasureSet.set ms✝ h✝)

set∃ m₂, MeasureSet.taint (MeasureSet.set ms✝ h✝) = MeasureSet.tainted m₂{α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

m✝: Meas

h₂: Resolve F d₂ m₁.last i (MeasureSet.tainted m✝)

tainted∃ m₂, MeasureSet.taint (MeasureSet.tainted m✝) = MeasureSet.tainted m₂ α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms✝: List Meas

h✝: ms✝ ≠ []

h₂: Resolve F d₂ m₁.last i (MeasureSet.set ms✝ h✝)

set∃ m₂, MeasureSet.taint (MeasureSet.set ms✝ h✝) = MeasureSet.tainted m₂simp [MeasureSet.taint: {α : Type} → MeasureSet → MeasureSet
MeasureSet.taint]
Goals accomplished! 🐙 }
Goals accomplished! 🐙
        }
Goals accomplished! 🐙
        α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

∃ ms, Resolve F (Doc.concat d₁ d₂) c i mslet ⟨m₂: Meas
m₂, h₂': MeasureSet.taint ms₂ = MeasureSet.tainted m₂
h₂'⟩ := this: ∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂
thisα: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

this: ∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂

m₂: Meas

h₂': MeasureSet.taint ms₂ = MeasureSet.tainted m₂

∃ ms, Resolve F (Doc.concat d₁ d₂) c i ms 
        α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

∃ ms, Resolve F (Doc.concat d₁ d₂) c i msexists MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted (Meas.concat: {α : Type} → Factory α → Meas → Meas → Meas
Meas.concat F: Factory α
F m₁: Meas
m₁ m₂: Meas
m₂)α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

this: ∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂

m₂: Meas

h₂': MeasureSet.taint ms₂ = MeasureSet.tainted m₂

Resolve F (Doc.concat d₁ d₂) c i (MeasureSet.tainted (Meas.concat F m₁ m₂))
        α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

∃ ms, Resolve F (Doc.concat d₁ d₂) c i msconstructorα: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

this: ∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂

m₂: Meas

h₂': MeasureSet.taint ms₂ = MeasureSet.tainted m₂

h_leftResolve F d₁ c i (MeasureSet.tainted m₁)
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

this: ∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂

m₂: Meas

h₂': MeasureSet.taint ms₂ = MeasureSet.tainted m₂

h_rightResolve F d₂ m₁.last i ?ms'
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

this: ∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂

m₂: Meas

h₂': MeasureSet.taint ms₂ = MeasureSet.tainted m₂

h_taintMeasureSet.taint ?ms' = MeasureSet.tainted m₂
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

this: ∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂

m₂: Meas

h₂': MeasureSet.taint ms₂ = MeasureSet.tainted m₂

ms'MeasureSet α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

this: ∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂

m₂: Meas

h₂': MeasureSet.taint ms₂ = MeasureSet.tainted m₂

Resolve F (Doc.concat d₁ d₂) c i (MeasureSet.tainted (Meas.concat F m₁ m₂))<;>α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

this: ∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂

m₂: Meas

h₂': MeasureSet.taint ms₂ = MeasureSet.tainted m₂

h_leftResolve F d₁ c i (MeasureSet.tainted m₁)
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

this: ∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂

m₂: Meas

h₂': MeasureSet.taint ms₂ = MeasureSet.tainted m₂

h_rightResolve F d₂ m₁.last i ?ms'
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

this: ∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂

m₂: Meas

h₂': MeasureSet.taint ms₂ = MeasureSet.tainted m₂

h_taintMeasureSet.taint ?ms' = MeasureSet.tainted m₂
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

this: ∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂

m₂: Meas

h₂': MeasureSet.taint ms₂ = MeasureSet.tainted m₂

ms'MeasureSet α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

m₁: Meas

h₁: Resolve F d₁ c i (MeasureSet.tainted m₁)

ms₂: MeasureSet

h₂: Resolve F d₂ m₁.last i ms₂

this: ∃ m₂, MeasureSet.taint ms₂ = MeasureSet.tainted m₂

m₂: Meas

h₂': MeasureSet.taint ms₂ = MeasureSet.tainted m₂

Resolve F (Doc.concat d₁ d₂) c i (MeasureSet.tainted (Meas.concat F m₁ m₂))assumption
Goals accomplished! 🐙
      α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

∃ ms, Resolve F (Doc.concat d₁ d₂) c i mscase set ms: List Meas
ms h_non_empty: ms ≠ []
h_non_empty => 
        α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

∃ ms, Resolve F (Doc.concat d₁ d₂) c i mslet ⟨msr: MeasureSet
msr, h': ResolveConcat F ms d₂ i msr
h'⟩ := ResolveConcat_total: ∀ {α : Type} (F : Factory α) (ms : List Meas) (d : Doc) (i : ℕ), ms ≠ [] → ∃ msr, ResolveConcat F ms d i msr
ResolveConcat_total F: Factory α
F ms: List Meas
ms d₂: Doc
d₂ i: ℕ
i h_non_empty: ms ≠ []
h_non_emptyα: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

msr: MeasureSet

h': ResolveConcat F ms d₂ i msr

∃ ms, Resolve F (Doc.concat d₁ d₂) c i ms
        α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

∃ ms, Resolve F (Doc.concat d₁ d₂) c i msexists msr: MeasureSet
msrα: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

msr: MeasureSet

h': ResolveConcat F ms d₂ i msr

Resolve F (Doc.concat d₁ d₂) c i msr
        α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

∃ ms, Resolve F (Doc.concat d₁ d₂) c i msconstructorα: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

msr: MeasureSet

h': ResolveConcat F ms d₂ i msr

h_leftResolve F d₁ c i (MeasureSet.set ?ms ?h_non_empty)
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

msr: MeasureSet

h': ResolveConcat F ms d₂ i msr

hResolveConcat F ?ms d₂ i msr
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

msr: MeasureSet

h': ResolveConcat F ms d₂ i msr

msList Meas
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

msr: MeasureSet

h': ResolveConcat F ms d₂ i msr

h_non_empty?ms ≠ [] α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

msr: MeasureSet

h': ResolveConcat F ms d₂ i msr

Resolve F (Doc.concat d₁ d₂) c i msr<;>α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

msr: MeasureSet

h': ResolveConcat F ms d₂ i msr

h_leftResolve F d₁ c i (MeasureSet.set ?ms ?h_non_empty)
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

msr: MeasureSet

h': ResolveConcat F ms d₂ i msr

hResolveConcat F ?ms d₂ i msr
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

msr: MeasureSet

h': ResolveConcat F ms d₂ i msr

msList Meas
α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

msr: MeasureSet

h': ResolveConcat F ms d₂ i msr

h_non_empty?ms ≠ [] α: Type

F: Factory α

d: Doc

c, i: ℕ

d₁, d₂: Doc

ms: List Meas

h_non_empty: ms ≠ []

h₁: Resolve F d₁ c i (MeasureSet.set ms h_non_empty)

msr: MeasureSet

h': ResolveConcat F ms d₂ i msr

Resolve F (Doc.concat d₁ d₂) c i msrassumption
Goals accomplished! 🐙

  theorem ResolveConcatOne_total: ∀ {α : Type} (F : Factory α) (d : Doc) (m : Meas) (i : ℕ), ∃ msr, ResolveConcatOne F d m i msr
ResolveConcatOne_total (F: Factory α
F : Factory: Type → Type
Factory α: ?m.26
α) (d: Doc
d : Doc: Type
Doc) (m: Meas
m : Meas: {α : Type} → Type
Meas) (i: ℕ
i : ℕ: Type
ℕ) : ∃ msr: ?m.41
msr, ResolveConcatOne: {α : Type} → Factory α → Doc → Meas → ℕ → MeasureSet → Prop
ResolveConcatOne F: Factory α
F d: Doc
d m: Meas
m i: ℕ
i msr: ?m.41
msr := by
Goals accomplished! 🐙 
    α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

∃ msr, ResolveConcatOne F d m i msrlet ⟨ms: MeasureSet
ms, h: Resolve F d m.last i ms
h⟩ := Resolve_total: ∀ {α : Type} (F : Factory α) (d : Doc) (c i : ℕ), ∃ ms, Resolve F d c i ms
Resolve_total F: Factory α
F d: Doc
d m: Meas
m.last: {α : Type} → Meas → ℕ
last i: ℕ
iα: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: MeasureSet

h: Resolve F d m.last i ms

∃ msr, ResolveConcatOne F d m i msr
    α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

∃ msr, ResolveConcatOne F d m i msrcases ms: MeasureSet
msα: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

m✝: Meas

h: Resolve F d m.last i (MeasureSet.tainted m✝)

tainted∃ msr, ResolveConcatOne F d m i msr
α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms✝: List Meas

h✝: ms✝ ≠ []

h: Resolve F d m.last i (MeasureSet.set ms✝ h✝)

set∃ msr, ResolveConcatOne F d m i msr 
    α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

∃ msr, ResolveConcatOne F d m i msrcase set ms: List Meas
ms h': ms ≠ []
h' =>
      α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

∃ msr, ResolveConcatOne F d m i msrexists MeasureSet.set: {α : Type} → (ms : List Meas) → ms ≠ [] → MeasureSet
MeasureSet.set (dedup: {α : Type} → Factory α → List Meas → List Meas
dedup F: Factory α
F (ms: List Meas
ms.map: {α : Type ?u.20152} → {β : Type ?u.20151} → (α → β) → List α → List β
map (fun m': ?m.20160
m' => Meas.concat: {α : Type} → Factory α → Meas → Meas → Meas
Meas.concat F: Factory α
F m: Meas
m m': ?m.20160
m'))) (α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

∃ msr, ResolveConcatOne F d m i msrby
Goals accomplished! 🐙 α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

dedup F (List.map (fun m' => Meas.concat F m m') ms) ≠ []{α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

dedup F (List.map (fun m' => Meas.concat F m m') ms) ≠ []
        α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

dedup F (List.map (fun m' => Meas.concat F m m') ms) ≠ []apply dedup_not_empty: ∀ {α : Type} {ms : List Meas} {F : Factory α}, ms ≠ [] → dedup F ms ≠ []
dedup_not_emptyα: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

hList.map (fun m' => Meas.concat F m m') ms ≠ []
        α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

dedup F (List.map (fun m' => Meas.concat F m m') ms) ≠ []simp [h': ms ≠ []
h']
Goals accomplished! 🐙
      }
Goals accomplished! 🐙)α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

ResolveConcatOne F d m i
  (MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms) ≠ []))
      α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

∃ msr, ResolveConcatOne F d m i msrconstructorα: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

hResolve F d m.last i (MeasureSet.set ms ?h_non_empty)
α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

h_non_emptyms ≠ [] α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

ResolveConcatOne F d m i
  (MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms) ≠ []))<;>α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

hResolve F d m.last i (MeasureSet.set ms ?h_non_empty)
α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

h_non_emptyms ≠ [] α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

ms: List Meas

h': ms ≠ []

h: Resolve F d m.last i (MeasureSet.set ms h')

ResolveConcatOne F d m i
  (MeasureSet.set (dedup F (List.map (fun m' => Meas.concat F m m') ms))
    (_ : dedup F (List.map (fun m' => Meas.concat F m m') ms) ≠ []))assumption
Goals accomplished! 🐙
    α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

∃ msr, ResolveConcatOne F d m i msrcase tainted m': Meas
m' => 
      α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

m': Meas

h: Resolve F d m.last i (MeasureSet.tainted m')

∃ msr, ResolveConcatOne F d m i msrexists MeasureSet.tainted: {α : Type} → Meas → MeasureSet
MeasureSet.tainted (Meas.concat: {α : Type} → Factory α → Meas → Meas → Meas
Meas.concat F: Factory α
F m: Meas
m m': Meas
m')α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

m': Meas

h: Resolve F d m.last i (MeasureSet.tainted m')

ResolveConcatOne F d m i (MeasureSet.tainted (Meas.concat F m m'))
      α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

m': Meas

h: Resolve F d m.last i (MeasureSet.tainted m')

∃ msr, ResolveConcatOne F d m i msrconstructorα: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

m': Meas

h: Resolve F d m.last i (MeasureSet.tainted m')

hResolve F d m.last i (MeasureSet.tainted m')
      α: Type

F: Factory α

d: Doc

m: Meas

i: ℕ

m': Meas

h: Resolve F d m.last i (MeasureSet.tainted m')

∃ msr, ResolveConcatOne F d m i msrassumption
Goals accomplished! 🐙

  theorem ResolveConcat_total: ∀ {α : Type} (F : Factory α) (ms : List Meas) (d : Doc) (i : ℕ), ms ≠ [] → ∃ msr, ResolveConcat F ms d i msr
ResolveConcat_total  (F: Factory α
F : Factory: Type → Type
Factory α: ?m.51
α) (ms: List Meas
ms : List: Type ?u.56 → Type ?u.56
List Meas: {α : Type} → Type
Meas) (d: Doc
d : Doc: Type
Doc)
      (i: ℕ
i : ℕ: Type
ℕ)
      (h_non_empty: ms ≠ []
h_non_empty : ms: List Meas
ms ≠ []: List ?m.68
[]) : 
      ∃ msr: ?m.74
msr, ResolveConcat: {α : Type} → Factory α → List Meas → Doc → ℕ → MeasureSet → Prop
ResolveConcat F: Factory α
F ms: List Meas
ms d: Doc
d i: ℕ
i msr: ?m.74
msr := by
Goals accomplished! 🐙 
    α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

h_non_empty: ms ≠ []

∃ msr, ResolveConcat F ms d i msrmatch ms: List Meas
ms with 
    α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

h_non_empty: ms ≠ []

∃ msr, ResolveConcat F ms d i msr| [] =>α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

h_non_empty: [] ≠ []

∃ msr, ResolveConcat F [] d i msr α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

h_non_empty: ms ≠ []

∃ msr, ResolveConcat F ms d i msrcontradiction
Goals accomplished! 🐙
    α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

h_non_empty: ms ≠ []

∃ msr, ResolveConcat F ms d i msr| [m: Meas
m] =>α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m: Meas

h_non_empty: [m] ≠ []

∃ msr, ResolveConcat F [m] d i msr 
      α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

h_non_empty: ms ≠ []

∃ msr, ResolveConcat F ms d i msrlet ⟨msr: MeasureSet
msr, h: ResolveConcatOne F d m i msr
h⟩ := ResolveConcatOne_total: ∀ {α : Type} (F : Factory α) (d : Doc) (m : Meas) (i : ℕ), ∃ msr, ResolveConcatOne F d m i msr
ResolveConcatOne_total F: Factory α
F d: Doc
d m: Meas
m i: ℕ
iα: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m: Meas

h_non_empty: [m] ≠ []

msr: MeasureSet

h: ResolveConcatOne F d m i msr

∃ msr, ResolveConcat F [m] d i msr
      α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m: Meas

h_non_empty: [m] ≠ []

∃ msr, ResolveConcat F [m] d i msrexists msr: MeasureSet
msrα: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m: Meas

h_non_empty: [m] ≠ []

msr: MeasureSet

h: ResolveConcatOne F d m i msr

ResolveConcat F [m] d i msr 
      α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m: Meas

h_non_empty: [m] ≠ []

∃ msr, ResolveConcat F [m] d i msrconstructorα: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m: Meas

h_non_empty: [m] ≠ []

msr: MeasureSet

h: ResolveConcatOne F d m i msr

h_currentResolveConcatOne F d m i msr
      α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m: Meas

h_non_empty: [m] ≠ []

∃ msr, ResolveConcat F [m] d i msrassumption
Goals accomplished! 🐙
    α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

h_non_empty: ms ≠ []

∃ msr, ResolveConcat F ms d i msr| m: Meas
m :: hd: Meas
hd :: tl: List Meas
tl =>α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m, hd: Meas

tl: List Meas

h_non_empty: m :: hd :: tl ≠ []

∃ msr, ResolveConcat F (m :: hd :: tl) d i msr 
      α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

h_non_empty: ms ≠ []

∃ msr, ResolveConcat F ms d i msrlet ⟨msr: MeasureSet
msr, h: ResolveConcat F (hd :: tl) d i msr
h⟩ := ResolveConcat_total: ∀ {α : Type} (F : Factory α) (ms : List Meas) (d : Doc) (i : ℕ), ms ≠ [] → ∃ msr, ResolveConcat F ms d i msr
ResolveConcat_total F: Factory α
F (hd: Meas
hd :: tl: List Meas
tl) d: Doc
d i: ℕ
i (α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m, hd: Meas

tl: List Meas

h_non_empty: m :: hd :: tl ≠ []

∃ msr, ResolveConcat F (m :: hd :: tl) d i msrby
Goals accomplished! 🐙 α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m, hd: Meas

tl: List Meas

h_non_empty: m :: hd :: tl ≠ []

hd :: tl ≠ []simp
Goals accomplished! 🐙)α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m, hd: Meas

tl: List Meas

h_non_empty: m :: hd :: tl ≠ []

msr: MeasureSet

h: ResolveConcat F (hd :: tl) d i msr

∃ msr, ResolveConcat F (m :: hd :: tl) d i msr
      α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m, hd: Meas

tl: List Meas

h_non_empty: m :: hd :: tl ≠ []

∃ msr, ResolveConcat F (m :: hd :: tl) d i msrlet ⟨msr': MeasureSet
msr', h': ResolveConcatOne F d m i msr'
h'⟩ := ResolveConcatOne_total: ∀ {α : Type} (F : Factory α) (d : Doc) (m : Meas) (i : ℕ), ∃ msr, ResolveConcatOne F d m i msr
ResolveConcatOne_total F: Factory α
F d: Doc
d m: Meas
m i: ℕ
iα: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m, hd: Meas

tl: List Meas

h_non_empty: m :: hd :: tl ≠ []

msr: MeasureSet

h: ResolveConcat F (hd :: tl) d i msr

msr': MeasureSet

h': ResolveConcatOne F d m i msr'

∃ msr, ResolveConcat F (m :: hd :: tl) d i msr 
      α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m, hd: Meas

tl: List Meas

h_non_empty: m :: hd :: tl ≠ []

∃ msr, ResolveConcat F (m :: hd :: tl) d i msrexists MeasureSet.union: {α : Type} → Factory α → MeasureSet → MeasureSet → MeasureSet
MeasureSet.union F: Factory α
F msr': MeasureSet
msr' msr: MeasureSet
msrα: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m, hd: Meas

tl: List Meas

h_non_empty: m :: hd :: tl ≠ []

msr: MeasureSet

h: ResolveConcat F (hd :: tl) d i msr

msr': MeasureSet

h': ResolveConcatOne F d m i msr'

ResolveConcat F (m :: hd :: tl) d i (MeasureSet.union F msr' msr)
      α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m, hd: Meas

tl: List Meas

h_non_empty: m :: hd :: tl ≠ []

∃ msr, ResolveConcat F (m :: hd :: tl) d i msrdwi { α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m, hd: Meas

tl: List Meas

h_non_empty: m :: hd :: tl ≠ []

msr: MeasureSet

h: ResolveConcat F (hd :: tl) d i msr

msr': MeasureSet

h': ResolveConcatOne F d m i msr'

ResolveConcat F (m :: hd :: tl) d i (MeasureSet.union F msr' msr)constructorα: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m, hd: Meas

tl: List Meas

h_non_empty: m :: hd :: tl ≠ []

msr: MeasureSet

h: ResolveConcat F (hd :: tl) d i msr

msr': MeasureSet

h': ResolveConcatOne F d m i msr'

h_restResolveConcat F (hd :: tl) d i msr
α: Type

F: Factory α

ms: List Meas

d: Doc

i: ℕ

m, hd: Meas

tl: List Meas

h_non_empty: m :: hd :: tl ≠ []

msr: MeasureSet

h: ResolveConcat F (hd :: tl) d i msr

msr': MeasureSet

h': ResolveConcatOne F d m i msr'

h_currentResolveConcatOne F d m i msr' }
Goals accomplished! 🐙
end
termination_by 
  ResolveConcatOne_total => (d: Doc
d.size: Doc → ℕ
size, 1: ?m.32290
1, 0: ?m.32297
0)
  ResolveConcat_total => (d: Doc
d.size: Doc → ℕ
size, 2: ?m.32224
2, ms: List Meas
ms.length: {α : Type ?u.32233} → List α → ℕ
length)
  Resolve_total => (d: Doc
d.size: Doc → ℕ
size, 0: ?m.32090
0, 0: ?m.32101
0)