reduce_isReduced — Mathlib

English

For every state, the reduced state is reduced; defined recursively by a well-founded descent.

Русский

Для каждого состояния сокращенное состояние является сокращенным; доказано по нормальному основанию на нисхождении.

LaTeX

$$$\\forall u:\\,XgcdType, (u.reduce).IsReduced$$$

Lean4

theorem reduce_isReduced : ∀ u : XgcdType, u.reduce.IsReduced
  | u =>
    dite (u.r = 0)
      (fun h => by
        rw [reduce_a h]
        exact u.finish_isReduced)
      fun h => by
      have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
      rw [reduce_b h, flip_isReduced]
      apply reduce_isReduced

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