English
A function f is RecursiveIn empty if and only if f is Nat.Partrec.
Русский
Функция f является RecursiveIn пустого множества тогда и только тогда, когда она частично рекурсивна.
LaTeX
$$$ \text{RecursiveIn } \emptyset\ f \iff Nat.Partrec f $$$
Lean4
@[simp]
theorem recursiveIn_empty_iff_partrec : RecursiveIn { } f ↔ Nat.Partrec f
where
mp
fRecInNone := by
induction fRecInNone with
repeat { constructor
}
| oracle _ hg => simp at hg
| pair
| comp
| prec
| rfind =>
repeat { constructor; assumption; try assumption
}
mpr
pF := by
induction pF with
repeat { constructor
}
| pair _ _ ih₁ ih₂ => exact RecursiveIn.pair ih₁ ih₂
| comp _ _ ih₁ ih₂ => exact RecursiveIn.comp ih₁ ih₂
| prec _ _ ih₁ ih₂ => exact RecursiveIn.prec ih₁ ih₂
| rfind _ ih => exact RecursiveIn.rfind ih
