ink

structure Factory (α : Type) : Type

• le : α → α → Bool
• concat : α → α → α
• text : ℕ → ℕ → α
• nl : ℕ → α
• W : ℕ
• text_monotonic : ∀ {c c' l : ℕ}, c ≤ c' → le (text c l) (text c' l) = true
• nl_monotonic : ∀ {i i' : ℕ}, i ≤ i' → le (nl i) (nl i') = true
• concat_monotonic : ∀ {cost₁ cost₂ cost₃ cost₄ : α}, le cost₁ cost₂ = true → le cost₃ cost₄ = true → le (concat cost₁ cost₃) (concat cost₂ cost₄) = true
• le_trans : ∀ {c₁ c₂ c₃ : α}, le c₁ c₂ = true → le c₂ c₃ = true → le c₁ c₃ = true
• le_antisymm : ∀ {c₁ c₂ : α}, le c₁ c₂ = true → le c₂ c₁ = true → c₁ = c₂
• le_total : ∀ (c₁ c₂ : α), le c₁ c₂ = true ∨ le c₂ c₁ = true

Cost factory interface definition (Figure 8)