f : ℕ →. ℕ
hf : Partrec f
⊢ Partrec (unpaired fun a b => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + b)))
f : ℕ →. ℕ
hf : Partrec f
⊢ Partrec₂ fun a m =>
    Part.map (fun x => x + m) (Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + m)))
refine'
  Partrec.map
    ((@Partrec₂.unpaired' fun a b : ℕ =>
          Nat.rfind fun n => (fun m => m = 0) <$> f (Nat.pair a (n + b))).1
      _)
    (Primrec.nat_add.comp Primrec.snd <| Primrec.snd.comp Primrec.fst).to_comp.to₂
f : ℕ →. ℕ
hf : Partrec f
this :
  Partrec fun a =>
    Nat.rfind fun n =>
      (fun m => decide (m = 0)) <$>
        unpaired (fun a b => f (Nat.pair (unpair a).fst (b + (unpair a).snd))) (Nat.pair a n)
⊢ Partrec (unpaired fun a b => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + b)))
f : ℕ →. ℕ
hf : Partrec f
⊢ Partrec (unpaired fun a b => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + b)))
have : Nat.Partrec (fun a => Nat.rfind (fun n => (fun m => decide (m = 0)) <$>
  Nat.unpaired (fun a b => f (Nat.pair (Nat.unpair a).1 (b + (Nat.unpair a).2)))
    (Nat.pair a n))) :=
  rfind
    (Partrec₂.unpaired'.2
      ((Partrec.nat_iff.2 hf).comp
          (Primrec₂.pair.comp (Primrec.fst.comp <| Primrec.unpair.comp Primrec.fst)
              (Primrec.nat_add.comp Primrec.snd
                (Primrec.snd.comp <| Primrec.unpair.comp Primrec.fst))).to_comp))
f : ℕ →. ℕ
hf : Partrec f
this :
  Partrec fun a =>
    Nat.rfind fun n => Part.map (fun m => decide (m = 0)) (f (Nat.pair (unpair a).fst (n + (unpair a).snd)))
⊢ Partrec (unpaired fun a b => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + b)))
f : ℕ →. ℕ
hf : Partrec f
this :
  Partrec fun a =>
    Nat.rfind fun n =>
      (fun m => decide (m = 0)) <$>
        unpaired (fun a b => f (Nat.pair (unpair a).fst (b + (unpair a).snd))) (Nat.pair a n)
⊢ Partrec (unpaired fun a b => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + b)))
simp at this
no goals
f : ℕ →. ℕ
hf : Partrec f
this :
  Partrec fun a =>
    Nat.rfind fun n => Part.map (fun m => decide (m = 0)) (f (Nat.pair (unpair a).fst (n + (unpair a).snd)))
⊢ Partrec (unpaired fun a b => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + b)))
exact this