English
A conditional primitive recursive construction: if a < b then f else g remains Primrec'.
Русский
Условная конструкция via если a < b то f иначе g сохраняет примр'
LaTeX
$$$\forall {n} {a,b,f,g},\ ha:\ Primrec'\ n a,\ hb:\ Primrec'\ n b,\ hf:\ Primrec'\ n f,\ hg:\ Primrec'\ n g\Rightarrow\ Primrec'\ fun v => if a v < b v then f v else g v$$$
Lean4
theorem if_lt {n a b f g} (ha : @Primrec' n a) (hb : @Primrec' n b) (hf : @Primrec' n f) (hg : @Primrec' n g) :
@Primrec' n fun v => if a v < b v then f v else g v :=
(prec' (sub.comp₂ _ hb ha) hg (tail <| tail hf)).of_eq fun v =>
by
cases e : b v - a v
· simp [not_lt.2 (Nat.sub_eq_zero_iff_le.mp e)]
· simp [Nat.lt_of_sub_eq_succ e]
