reduce_isSpecial — Mathlib

English

If u is IsSpecial, then u.reduce.IsSpecial; if not, flip and recurse via the reduced step.

Русский

Если u является IsSpecial, то u.reduce.IsSpecial; иначе применяем flip и рекурсивно снижаем.

LaTeX

$$$\\forall u:\\,XgcdType, u.IsSpecial \\rightarrow u.reduce.IsSpecial$$$

Lean4

theorem reduce_isSpecial : ∀ u : XgcdType, u.IsSpecial → u.reduce.IsSpecial
  | u =>
    dite (u.r = 0)
      (fun h hs => by
        rw [reduce_a h]
        exact u.finish_isSpecial hs)
      fun h hs => by
      have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
      rw [reduce_b h]
      exact (flip_isSpecial _).mpr (reduce_isSpecial _ (u.step_isSpecial hs))

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