Mathling.Lambek.ProductFree.Basic

ax {A : Tp} : [A] ⇒ A
rdiv_r {Γ : List Tp} {A B : Tp} : Γ ≠ [] → Γ ++ [A] ⇒ B → Γ ⇒ B ⧸ A
ldiv_r {Γ : List Tp} {A B : Tp} : Γ ≠ [] → [A] ++ Γ ⇒ B → Γ ⇒ A ⧹ B
rdiv_l {Δ : List Tp} {A : Tp} {Γ : List Tp} {B : Tp} {Λ : List Tp} {C : Tp} : Δ ⇒ A → Γ ++ [B] ++ Λ ⇒ C → Γ ++ [B ⧸ A] ++ Δ ++ Λ ⇒ C
ldiv_l {Δ : List Tp} {A : Tp} {Γ : List Tp} {B : Tp} {Λ : List Tp} {C : Tp} : Δ ⇒ A → Γ ++ [B] ++ Λ ⇒ C → Γ ++ Δ ++ [A ⧹ B] ++ Λ ⇒ C

Instances For

source

def Mathling.Lambek.ProductFree.«term_⇒_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

def Mathling.Lambek.ProductFree.tp_degree :

Tp → ℕ

Equations

Mathling.Lambek.ProductFree.tp_degree (#a) = 1
Mathling.Lambek.ProductFree.tp_degree (a ⧹ a_1) = Mathling.Lambek.ProductFree.tp_degree a + Mathling.Lambek.ProductFree.tp_degree a_1 + 1
Mathling.Lambek.ProductFree.tp_degree (a ⧸ a_1) = Mathling.Lambek.ProductFree.tp_degree a + Mathling.Lambek.ProductFree.tp_degree a_1 + 1

Instances For

source

def Mathling.Lambek.ProductFree.list_degree :

List Tp → ℕ

Equations

Instances For

source

theorem Mathling.Lambek.ProductFree.list_degree_traversible {Γ Δ : List Tp} :

list_degree (Γ ++ Δ) = list_degree Γ + list_degree Δ

source

theorem Mathling.Lambek.ProductFree.nonempty_premises {Γ : List Tp} {A : Tp} (h : Γ ⇒ A) :

Γ ≠ []

source

theorem Mathling.Lambek.ProductFree.nonempty_append {α✝ : Type u_1} {Γ Δ Λ : List α✝} (h : Γ ≠ []) :

Δ ++ Γ ++ Λ ≠ []

source

theorem Mathling.Lambek.ProductFree.list_split_2_cases {α✝ : Type u_1} {Γ₁ : List α✝} {α : α✝} {Γ₂ Δ₁ Δ₂ : List α✝} (h : Γ₁ ++ [α] ++ Γ₂ = Δ₁ ++ Δ₂) :

(∃ (R : List α✝), Δ₁ = Γ₁ ++ [α] ++ R ∧ Γ₂ = R ++ Δ₂) ∨ ∃ (L : List α✝), ∃ (R : List α✝), Δ₂ = L ++ [α] ++ R ∧ Γ₁ = Δ₁ ++ L ∧ Γ₂ = R

source

theorem Mathling.Lambek.ProductFree.list_split_3_cases {α✝ : Type u_1} {Γ₁ : List α✝} {α : α✝} {Γ₂ Δ₁ Δ₂ Δ₃ : List α✝} (h : Γ₁ ++ [α] ++ Γ₂ = Δ₁ ++ Δ₂ ++ Δ₃) :

(∃ (R : List α✝), Δ₁ = Γ₁ ++ [α] ++ R ∧ Γ₂ = R ++ Δ₂ ++ Δ₃) ∨ (∃ (L : List α✝), ∃ (R : List α✝), Δ₂ = L ++ [α] ++ R ∧ Γ₁ = Δ₁ ++ L ∧ Γ₂ = R ++ Δ₃) ∨ ∃ (L : List α✝), ∃ (R : List α✝), Δ₃ = L ++ [α] ++ R ∧ Γ₁ = Δ₁ ++ Δ₂ ++ L ∧ Γ₂ = R

source

theorem Mathling.Lambek.ProductFree.list_split_4_cases {α✝ : Type u_1} {Γ₁ : List α✝} {α : α✝} {Γ₂ Δ₁ Δ₂ Δ₃ Δ₄ : List α✝} (h : Γ₁ ++ [α] ++ Γ₂ = Δ₁ ++ Δ₂ ++ Δ₃ ++ Δ₄) :

(∃ (R : List α✝), Δ₁ = Γ₁ ++ [α] ++ R ∧ Γ₂ = R ++ Δ₂ ++ Δ₃ ++ Δ₄) ∨ (∃ (L : List α✝), ∃ (R : List α✝), Δ₂ = L ++ [α] ++ R ∧ Γ₁ = Δ₁ ++ L ∧ Γ₂ = R ++ Δ₃ ++ Δ₄) ∨ (∃ (L : List α✝), ∃ (R : List α✝), Δ₃ = L ++ [α] ++ R ∧ Γ₁ = Δ₁ ++ Δ₂ ++ L ∧ Γ₂ = R ++ Δ₄) ∨ ∃ (L : List α✝), ∃ (R : List α✝), Δ₄ = L ++ [α] ++ R ∧ Γ₁ = Δ₁ ++ Δ₂ ++ Δ₃ ++ L ∧ Γ₂ = R

source

theorem Mathling.Lambek.ProductFree.cut_admissible {Γ : List Tp} {A : Tp} {Δ Λ : List Tp} {B : Tp} (d_left : Γ ⇒ A) (d_right : Δ ++ [A] ++ Λ ⇒ B) :

Δ ++ Γ ++ Λ ⇒ B

source

theorem Mathling.Lambek.ProductFree.ldiv_invertible {Γ : List Tp} {A B : Tp} (h : Γ ⇒ A ⧹ B) :

[A] ++ Γ ⇒ B

source

theorem Mathling.Lambek.ProductFree.rdiv_invertible {Γ : List Tp} {A B : Tp} (h : Γ ⇒ B ⧸ A) :

Γ ++ [A] ⇒ B

source

def Mathling.Lambek.ProductFree.is_atom :

Tp → Prop

Equations

Mathling.Lambek.ProductFree.is_atom (#name) = True
Mathling.Lambek.ProductFree.is_atom x✝ = False

Instances For

source

theorem Mathling.Lambek.ProductFree.atom_generation {Γ : List Tp} {s : String} (h_ctx : ∀ (x : Tp), x ∈ Γ → is_atom x) (h_der : Γ ⇒ #s) :

Γ = [#s]