tr_succ — Mathlib

English

Another presentation of the same succ-case for the transformation tr, confirming the definitional equality.

Русский

Еще одно представление случая succ для преобразования tr, подтверждающее определённое равенство.

LaTeX

$$$\\forall q,\\; tr(q.succ) = pop' main\\; (branch(\\ldots))$$$

Lean4

@[simp]
theorem tr_succ (q) :
    tr (Λ'.succ q) =
      pop' main
        (branch (fun s => s = some Γ'.bit1) ((push rev fun _ => Γ'.bit0) <| goto fun _ => Λ'.succ q) <|
          branch (fun s => s = some Γ'.cons)
            ((push main fun _ => Γ'.cons) <| (push main fun _ => Γ'.bit1) <| goto fun _ => unrev q)
            ((push main fun _ => Γ'.bit1) <| goto fun _ => unrev q)) :=
  rfl

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