no goals
f : Code → Code
hf : Computable f
g : ℕ → ℕ → Part ℕ :=
  fun x y => do
    let b ← eval (ofNat Code x) x
    eval (ofNat Code b) y
this : Partrec₂ g
cg : Code
eg : eval cg = fun n => Part.bind ↑(decode n) fun a => Part.map encode ((fun p => g p.fst p.snd) a)
⊢ ∀ (a n : ℕ), eval cg (Nat.pair a n) = Part.map encode (g a n)
simp [eg]
no goals
f : Code → Code
hf : Computable f
g : ℕ → ℕ → Part ℕ :=
  fun x y => do
    let b ← eval (ofNat Code x) x
    eval (ofNat Code b) y
this✝ : Partrec₂ g
cg : Code
eg : eval cg = fun n => Part.bind ↑(decode n) fun a => Part.map encode ((fun p => g p.fst p.snd) a)
eg' : ∀ (a n : ℕ), eval cg (Nat.pair a n) = Part.map encode (g a n)
F : ℕ → Code := fun x => f (curry cg x)
this : Computable F
cF : Code
eF : eval cF = fun n => Part.bind ↑(decode n) fun a => Part.map encode (↑F a)
⊢ eval cF (encode cF) = Part.some (encode (F (encode cF)))
simp [eF]
no goals
f : Code → Code
hf : Computable f
g : ℕ → ℕ → Part ℕ :=
  fun x y => do
    let b ← eval (ofNat Code x) x
    eval (ofNat Code b) y
this✝ : Partrec₂ g
cg : Code
eg : eval cg = fun n => Part.bind ↑(decode n) fun a => Part.map encode ((fun p => g p.fst p.snd) a)
eg' : ∀ (a n : ℕ), eval cg (Nat.pair a n) = Part.map encode (g a n)
F : ℕ → Code := fun x => f (curry cg x)
this : Computable F
cF : Code
eF : eval cF = fun n => Part.bind ↑(decode n) fun a => Part.map encode (↑F a)
eF' : eval cF (encode cF) = Part.some (encode (F (encode cF)))
n : ℕ
⊢ eval (f (curry cg (encode cF))) n = eval (curry cg (encode cF)) n
simp [eg', eF', Part.map_id']