primrec₂_comp — Mathlib

English

The two-argument composition operator comp is primitive recursive.

Русский

Оператор композиции двух входов comp является примитивно рекурсивным.

LaTeX

$$$\\operatorname{Primrec}_2(\\text{comp})$$$

Lean4

theorem primrec₂_comp : Primrec₂ comp :=
  Primrec₂.ofNat_iff.2 <|
    Primrec₂.encode_iff.1 <|
      nat_add.comp
        (nat_double.comp <|
          nat_double_succ.comp <|
            Primrec₂.natPair.comp (encode_iff.2 <| (Primrec.ofNat Code).comp fst)
              (encode_iff.2 <| (Primrec.ofNat Code).comp snd))
        (Primrec₂.const 4)

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