import Pretty.Supports.Basic

/--
Cost factory interface definition (Figure 8)
-/
structure 
Factory: {α : Type} →
  (le : α → α → Bool) →
    (concat : α → α → α) →
      (text : ℕ → ℕ → α) →
        (nl : ℕ → α) →
          ℕ →
            (∀ {c c' l : ℕ}, c ≤ c' → le (text c l) (text c' l) = true) →
              (∀ {i i' : ℕ}, i ≤ i' → le (nl i) (nl i') = true) →
                (∀ {cost₁ cost₂ cost₃ cost₄ : α},
                    le cost₁ cost₂ = true →
                      le cost₃ cost₄ = true → le (concat cost₁ cost₃) (concat cost₂ cost₄) = true) →
                  (∀ {c₁ c₂ c₃ : α}, le c₁ c₂ = true → le c₂ c₃ = true → le c₁ c₃ = true) →
                    (∀ {c₁ c₂ : α}, le c₁ c₂ = true → le c₂ c₁ = true → c₁ = c₂) →
                      (∀ (c₁ c₂ : α), le c₁ c₂ = true ∨ le c₂ c₁ = true) → Factory α
Factory (
α: Type
α : 
Type: Type 1
Type) where
  
le: {α : Type} → Factory α → α → α → Bool
le : 
α: Type
α → 
α: Type
α → 
Bool: Type
Bool
  
concat: {α : Type} → Factory α → α → α → α
concat : 
α: Type
α → 
α: Type
α → 
α: Type
α 
  
text: {α : Type} → Factory α → ℕ → ℕ → α
text : 
ℕ: Type
ℕ → 
ℕ: Type
ℕ → 
α: Type
α 
  
nl: {α : Type} → Factory α → ℕ → α
nl : 
ℕ: Type
ℕ → 
α: Type
α
  
W: {α : Type} → Factory α → ℕ
W : 
ℕ: Type
ℕ

  
text_monotonic: ∀ {α : Type} (self : Factory α) {c c' l : ℕ},
  c ≤ c' → Factory.le self (Factory.text self c l) (Factory.text self c' l) = true
text_monotonic : 
c: ?m.33
c ≤ 
c': ?m.39
c' → 
le: α → α → Bool
le (
text: ℕ → ℕ → α
text 
c: ?m.33
c 
l: ?m.95
l) (
text: ℕ → ℕ → α
text 
c': ?m.39
c' 
l: ?m.95
l)
  
nl_monotonic: ∀ {α : Type} (self : Factory α) {i i' : ℕ}, i ≤ i' → Factory.le self (Factory.nl self i) (Factory.nl self i') = true
nl_monotonic : 
i: ?m.172
i ≤ 
i': ?m.178
i' → 
le: α → α → Bool
le (
nl: ℕ → α
nl 
i: ?m.172
i) (
nl: ℕ → α
nl 
i': ?m.178
i')
  
concat_monotonic: ∀ {α : Type} (self : Factory α) {cost₁ cost₂ cost₃ cost₄ : α},
  Factory.le self cost₁ cost₂ = true →
    Factory.le self cost₃ cost₄ = true →
      Factory.le self (Factory.concat self cost₁ cost₃) (Factory.concat self cost₂ cost₄) = true
concat_monotonic :  
le: α → α → Bool
le 
cost₁: ?m.249
cost₁ 
cost₂: ?m.254
cost₂ → 
                      
le: α → α → Bool
le 
cost₃: ?m.273
cost₃ 
cost₄: ?m.292
cost₄ → 
                      
le: α → α → Bool
le (
concat: α → α → α
concat 
cost₁: ?m.249
cost₁ 
cost₃: ?m.273
cost₃) (
concat: α → α → α
concat 
cost₂: ?m.254
cost₂ 
cost₄: ?m.292
cost₄)

  
le_trans: ∀ {α : Type} (self : Factory α) {c₁ c₂ c₃ : α},
  Factory.le self c₁ c₂ = true → Factory.le self c₂ c₃ = true → Factory.le self c₁ c₃ = true
le_trans : 
le: α → α → Bool
le 
c₁: ?m.339
c₁ 
c₂: ?m.344
c₂ → 
le: α → α → Bool
le 
c₂: ?m.344
c₂ 
c₃: ?m.363
c₃ → 
le: α → α → Bool
le 
c₁: ?m.339
c₁ 
c₃: ?m.363
c₃
  
le_antisymm: ∀ {α : Type} (self : Factory α) {c₁ c₂ : α}, Factory.le self c₁ c₂ = true → Factory.le self c₂ c₁ = true → c₁ = c₂
le_antisymm : 
le: α → α → Bool
le 
c₁: ?m.410
c₁ 
c₂: ?m.415
c₂ → 
le: α → α → Bool
le 
c₂: ?m.415
c₂ 
c₁: ?m.410
c₁ → 
c₁: ?m.410
c₁ = 
c₂: ?m.415
c₂
  
le_total: ∀ {α : Type} (self : Factory α) (c₁ c₂ : α), Factory.le self c₁ c₂ = true ∨ Factory.le self c₂ c₁ = true
le_total (
c₁: α
c₁ 
c₂: α
c₂ : 
α: Type
α) : 
le: α → α → Bool
le 
c₁: α
c₁ 
c₂: α
c₂ ∨ 
le: α → α → Bool
le 
c₂: α
c₂ 
c₁: α
c₁