def WGCL.Boolean : Type

Booleans are Bools where b₁ + b₂ = b₁ ∨ b₂ rather than b₁ ^^ b₂.

Equations

• WGCL.Boolean = Bool

instance WGCL.instPartialOrderBoolean : PartialOrder Boolean

Equations

• WGCL.instPartialOrderBoolean = inferInstanceAs (PartialOrder Bool)

instance WGCL.instOrderBotBoolean : OrderBot Boolean

Equations

• WGCL.instOrderBotBoolean = inferInstanceAs (OrderBot Bool)

instance WGCL.instOrderTopBoolean : OrderTop Boolean

Equations

• WGCL.instOrderTopBoolean = inferInstanceAs (OrderTop Bool)

noncomputable instance WGCL.instOmegaCompletePartialOrderBoolean : OmegaCompletePartialOrder Boolean

Equations

• One or more equations did not get rendered due to their size.

instance WGCL.instAddBoolean : Add Boolean

Equations

• WGCL.instAddBoolean = { add := fun (a b : WGCL.Boolean) => a || b }

instance WGCL.instMulBoolean : Mul Boolean

Equations

• WGCL.instMulBoolean = { mul := fun (a b : WGCL.Boolean) => a && b }

instance WGCL.instZeroBoolean : Zero Boolean

Equations

• WGCL.instZeroBoolean = { zero := ⊥ }

@[simp]

theorem WGCL.Boolean.add_eq_inf (a b : Boolean) : a + b = (a || b)

@[simp]

theorem WGCL.Boolean.mul_eq_add (a b : Boolean) : a ⊙ b = (a && b)

@[simp]

theorem WGCL.Boolean.bot_or (a : Boolean) : (⊥ || a) = a

@[simp]

theorem WGCL.Boolean.or_bot (a : Boolean) : (a || ⊥) = a

@[simp]

theorem WGCL.Boolean.bot_le (a : Boolean) : ⊥ ≤ a

@[simp]

theorem WGCL.Boolean.le_top (a : Boolean) : a ≤ ⊤

@[simp]

theorem WGCL.Boolean.zero_eq_bot : 0 = ⊥

instance WGCL.instSemiringBoolean : Semiring Boolean

Equations

• One or more equations did not get rendered due to their size.

instance WGCL.instAddLeftMonoBoolean : AddLeftMono Boolean

instance WGCL.instMulLeftMonoBoolean : MulLeftMono Boolean

def WGCL.TNat : Type

Equations

• WGCL.TNat = ℕ∞

def WGCL.TNat.ofENat (n : ℕ∞) : TNat

Equations

• WGCL.TNat.ofENat n = n

def WGCL.TNat.toENat (n : TNat) : ℕ∞

Equations

• n.toENat = n

instance WGCL.instLETNat : LE TNat

Equations

• WGCL.instLETNat = { le := fun (a b : WGCL.TNat) => a.toENat ≤ b }

instance WGCL.instBotTNat : Bot TNat

Equations

• WGCL.instBotTNat = { bot := WGCL.TNat.ofENat 0 }

instance WGCL.instTopTNat : Top TNat

Equations

• WGCL.instTopTNat = { top := WGCL.TNat.ofENat ⊤ }

instance WGCL.instOrderBotTNat : OrderBot TNat

Equations

• WGCL.instOrderBotTNat = { toBot := WGCL.instBotTNat, bot_le := WGCL.instOrderBotTNat._proof_22 }

instance WGCL.instPartialOrderTNat : PartialOrder TNat

Equations

• One or more equations did not get rendered due to their size.

instance WGCL.instSemilatticeInfTNat : SemilatticeInf TNat

Equations

• One or more equations did not get rendered due to their size.

instance WGCL.instOmegaCompletePartialOrderTNat : OmegaCompletePartialOrder TNat

Equations

• WGCL.instOmegaCompletePartialOrderTNat = inferInstanceAs (OmegaCompletePartialOrder ℕ∞)

instance WGCL.instOneTNat : One TNat

Equations

• WGCL.instOneTNat = { one := WGCL.TNat.ofENat 0 }

instance WGCL.instZeroTNat : Zero TNat

Equations

• WGCL.instZeroTNat = { zero := WGCL.TNat.ofENat ⊤ }

instance WGCL.instAddTNat : Add TNat

Equations

• WGCL.instAddTNat = { add := fun (x y : WGCL.TNat) => x.toENat ⊓ y.toENat }

instance WGCL.instMulTNat : Mul TNat

Equations

• WGCL.instMulTNat = { mul := fun (x y : WGCL.TNat) => x.toENat + y.toENat }

instance WGCL.instMonoidTNat : Monoid TNat

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WGCL.TNat.add_eq_inf {a b : TNat} : a + b = a ⊓ b

@[simp]

theorem WGCL.TNat.mul_eq_add {a b : TNat} : a ⊙ b = a.toENat + b.toENat

@[simp]

theorem WGCL.TNat.zero_eq : 0 = ofENat ⊤

@[simp]

theorem WGCL.TNat.one_eq : 1 = ofENat 0

@[simp]

theorem WGCL.TNat.top_eq : ⊤ = ofENat ⊤

@[simp]

theorem WGCL.TNat.bot_eq : ⊥ = ofENat ⊥

instance WGCL.instAddCommMonoidTNat : AddCommMonoid TNat

Equations

• One or more equations did not get rendered due to their size.

instance WGCL.instAddLeftMonoTNat : AddLeftMono TNat

instance WGCL.instCovariantClassTNatHSMulLe : CovariantClass TNat TNat HSMul.hSMul LE.le

instance WGCL.instSemiringTNat : Semiring TNat

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WGCL.ahsjdahsd {x : TNat} : x ⊓ ⊤ = x

@[simp]

theorem WGCL.TNat.le_top {x : ℕ∞} : x ≤ ⊤

def WGCL.SkiRental {Var : Type} (n y : Var) : wGCL ℕ TNat Var

Equations

• One or more equations did not get rendered due to their size.

def WGCL.Bottleneck : Type

Equations

• WGCL.Bottleneck = EReal

noncomputable instance WGCL.instLinearOrderBottleneck : LinearOrder Bottleneck

Equations

• WGCL.instLinearOrderBottleneck = inferInstanceAs (LinearOrder EReal)

noncomputable instance WGCL.instCompleteLatticeBottleneck : CompleteLattice Bottleneck

Equations

• WGCL.instCompleteLatticeBottleneck = inferInstanceAs (CompleteLattice EReal)

noncomputable instance WGCL.instOmegaCompletePartialOrderBottleneck : OmegaCompletePartialOrder Bottleneck

Equations

• WGCL.instOmegaCompletePartialOrderBottleneck = inferInstanceAs (OmegaCompletePartialOrder EReal)

noncomputable instance WGCL.instOrderBotBottleneck : OrderBot Bottleneck

Equations

• WGCL.instOrderBotBottleneck = inferInstanceAs (OrderBot EReal)

noncomputable instance WGCL.instOrderTopBottleneck : OrderTop Bottleneck

Equations

• WGCL.instOrderTopBottleneck = inferInstanceAs (OrderTop EReal)

noncomputable instance WGCL.instAddBottleneck : Add Bottleneck

Equations

• WGCL.instAddBottleneck = { add := fun (a b : WGCL.Bottleneck) => max a b }

noncomputable instance WGCL.instMulBottleneck : Mul Bottleneck

Equations

• WGCL.instMulBottleneck = { mul := fun (a b : WGCL.Bottleneck) => min a b }

noncomputable instance WGCL.instZeroBottleneck : Zero Bottleneck

Equations

• WGCL.instZeroBottleneck = { zero := ⊥ }

@[simp]

theorem WGCL.Bottleneck.add_eq_inf (a b : Bottleneck) : a + b = max a b

@[simp]

theorem WGCL.Bottleneck.mul_eq_add (a b : Bottleneck) : a ⊙ b = min a b

@[simp]

theorem WGCL.Bottleneck.bot_le (a : Bottleneck) : ⊥ ≤ a

@[simp]

theorem WGCL.Bottleneck.le_top (a : Bottleneck) : a ≤ ⊤

@[simp]

theorem WGCL.Bottleneck.zero_eq_bot : 0 = ⊥

noncomputable instance WGCL.instSemiringBottleneck : Semiring Bottleneck

Equations

• One or more equations did not get rendered due to their size.

instance WGCL.instAddLeftMonoBottleneck : AddLeftMono Bottleneck

instance WGCL.instMulLeftMonoBottleneck : MulLeftMono Bottleneck

@[reducible, inline]

abbrev WGCL.ε {Γ : Type} : List Γ

Equations

• WGCL.ε = []

def WGCL.instMonoidList_wGCL {Γ : Type} : Monoid (List Γ)

Equations

• WGCL.instMonoidList_wGCL = { mul := List.append, mul_assoc := ⋯, one := WGCL.ε, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

@[simp]

theorem WGCL.one_append {Γ : Type} {w : List Γ} : 1 ++ w = w

def WGCL.instDistribMulActionListLanguage_wGCL {Γ : Type} : DistribMulAction (List Γ) (Language Γ)

Equations

• WGCL.instDistribMulActionListLanguage_wGCL = { smul := fun (w : List Γ) (S : Language Γ) => (fun (x : List Γ) => w ++ x) '' S, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

theorem WGCL.instCovariantClassListLanguageHSMulLe_wGCL {Γ : Type} : CovariantClass (List Γ) (Language Γ) HSMul.hSMul LE.le

def WGCL.instCoeList𝕎MemNat {Γ Var : Type} : Coe (List Γ) (𝕎 (List Γ) (Mem ℕ Var))

Equations

• WGCL.instCoeList𝕎MemNat = { coe := fun (S : List Γ) (x : WGCL.Mem ℕ Var) => S }

def WGCL.instSingletonListWeightingNatLanguage {Γ Var : Type} : Singleton (List Γ) (Weighting ℕ (Language Γ) Var)

Equations

• WGCL.instSingletonListWeightingNatLanguage = { singleton := fun (S : List Γ) (x : WGCL.Mem ℕ Var) => {S} }

def WGCL.instInsertListWeightingNatLanguage {Γ Var : Type} : Insert (List Γ) (Weighting ℕ (Language Γ) Var)

Equations

• WGCL.instInsertListWeightingNatLanguage = { insert := fun (w : List Γ) (S : WGCL.Weighting ℕ (Language Γ) Var) (σ : WGCL.Mem ℕ Var) => insert w (S σ) }

@[simp]

theorem WGCL.Language.mem_singleton_iff {Γ : Type} {b a : List Γ} : a ∈ {b} ↔ a = b

@[simp]

theorem WGCL.Language.mem_insert_iff {Γ : Type} {b a : List Γ} {S : Language Γ} : a ∈ insert b S ↔ a = b ∨ a ∈ S

noncomputable instance WGCL.instSupSetTropicalENat_wGCL : SupSet (Tropical ℕ∞)

Equations

• WGCL.instSupSetTropicalENat_wGCL = { sSup := fun (S : Set (Tropical ℕ∞)) => if h : S.Nonempty ∧ BddAbove S then Exists.choose ⋯ else 0 }

def WGCL.Chain.upperBounds {α : Type u_1} [Preorder α] (s : OmegaCompletePartialOrder.Chain α) : Set α

The set of upper bounds of a set.

Equations

• WGCL.Chain.upperBounds s = {x : α | ∀ ⦃a : α⦄, a ∈ s → a ≤ x}

def WGCL.Chain.BddAbove {α : Type u_1} [Preorder α] (s : OmegaCompletePartialOrder.Chain α) : Prop

A set is bounded above if there exists an upper bound.

Equations

• WGCL.Chain.BddAbove s = (WGCL.Chain.upperBounds s).Nonempty

def WGCL.Chain.BddAbove_choose_spec {α : Type u_1} [Preorder α] {s : OmegaCompletePartialOrder.Chain α} (h : BddAbove s) ⦃a : α⦄ : a ∈ s → a ≤ Exists.choose h

Equations

• ⋯ = ⋯

instance WGCL.instOrderBotTropicalENat_wGCL : OrderBot (Tropical ℕ∞)

Equations

• WGCL.instOrderBotTropicalENat_wGCL = { bot := ⊤, bot_le := WGCL.instOrderBotTropicalENat_wGCL._proof_80 }

noncomputable instance WGCL.instCompleteLinearOrderENat_wGCL : CompleteLinearOrder ℕ∞

Equations

• WGCL.instCompleteLinearOrderENat_wGCL = inferInstance

noncomputable instance WGCL.instCompleteLatticeENat_wGCL : CompleteLattice ℕ∞

Equations

• WGCL.instCompleteLatticeENat_wGCL = inferInstance

noncomputable instance WGCL.instPartialOrderTropicalENat_wGCL : PartialOrder (Tropical ℕ∞)

Equations

• WGCL.instPartialOrderTropicalENat_wGCL = inferInstance

noncomputable instance WGCL.instOmegaCompletePartialOrderTropicalENat_wGCL : OmegaCompletePartialOrder (Tropical ℕ∞)

Equations

• One or more equations did not get rendered due to their size.