standardσ_comp_standardσ — Mathlib

English

Composition of standardσs satisfies standardσ L1 h ≫ standardσ L2 h' = standardσ (L2 ++ L1) (by grind).

Русский

Композиция σ-стандартов равна σ-стандарту от конкатенации списков.

LaTeX

$$$\\\\text{standardσ}(L_1) \\\\circ \\\\text{standardσ}(L_2) = \\\\text{standardσ}(L_2 \\!\\.concat\\! L_1).$$$

Lean4

@[reassoc]
theorem standardσ_comp_standardσ (L₁ L₂ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + L₂.length = m₂) :
    standardσ L₁ h ≫ standardσ L₂ h' = standardσ (L₂ ++ L₁) (by grind) := by
  induction L₂ generalizing L₁ m₁ m₂ m₃ with
  | nil =>
    obtain rfl : m₃ = m₂ := by grind
    simp
  | cons a t H =>
    dsimp at h' ⊢
    obtain rfl : m₂ = (m₃ + t.length) + 1 := by grind
    simp [reassoc_of% (H L₁ (m₁ := m₁) (m₂ := m₃ + t.length + 1) (m₃ := m₃ + 1) (by grind) (by grind))]

Похожие утверждения