case zero
f : ℕ →. ℕ
⊢ ∃ c, eval c = pure 0

case succ
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑Nat.succ

case left
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).fst

case right
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).snd

case pair
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> f✝ n) fun x => g✝ n

case comp
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => g✝ n >>= f✝

case prec
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
f : ℕ →. ℕ
h : Partrec f
⊢ ∃ c, eval c = f
induction h
case succ
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑Nat.succ

case left
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).fst

case right
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).snd

case pair
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> f✝ n) fun x => g✝ n

case comp
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => g✝ n >>= f✝

case prec
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case zero
f : ℕ →. ℕ
⊢ ∃ c, eval c = pure 0

case succ
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑Nat.succ

case left
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).fst

case right
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).snd

case pair
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> f✝ n) fun x => g✝ n

case comp
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => g✝ n >>= f✝

case prec
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case zero => exact ⟨zero, rfl⟩
case left
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).fst

case right
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).snd

case pair
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> f✝ n) fun x => g✝ n

case comp
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => g✝ n >>= f✝

case prec
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case succ
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑Nat.succ

case left
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).fst

case right
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).snd

case pair
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> f✝ n) fun x => g✝ n

case comp
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => g✝ n >>= f✝

case prec
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case succ => exact ⟨succ, rfl⟩
case right
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).snd

case pair
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> f✝ n) fun x => g✝ n

case comp
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => g✝ n >>= f✝

case prec
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case left
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).fst

case right
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).snd

case pair
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> f✝ n) fun x => g✝ n

case comp
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => g✝ n >>= f✝

case prec
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case left => exact ⟨left, rfl⟩
case pair
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> f✝ n) fun x => g✝ n

case comp
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => g✝ n >>= f✝

case prec
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case right
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).snd

case pair
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> f✝ n) fun x => g✝ n

case comp
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => g✝ n >>= f✝

case prec
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case right => exact ⟨right, rfl⟩
case comp
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => g✝ n >>= f✝

case prec
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case pair
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> f✝ n) fun x => g✝ n

case comp
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => g✝ n >>= f✝

case prec
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case pair f g pf pg hf hg =>
  rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
  exact ⟨pair cf cg, rfl⟩
case prec
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case comp
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c, eval c = fun n => g✝ n >>= f✝

case prec
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case comp f g pf pg hf hg =>
  rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
  exact ⟨comp cf cg, rfl⟩
case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case prec
f f✝ g✝ : ℕ →. ℕ
a✝¹ : Partrec f✝
a✝ : Partrec g✝
a_ih✝¹ : ∃ c, eval c = f✝
a_ih✝ : ∃ c, eval c = g✝
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case prec f g pf pg hf hg =>
  rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
  exact ⟨prec cf cg, rfl⟩
no goals
case rfind
f f✝ : ℕ →. ℕ
a✝ : Partrec f✝
a_ih✝ : ∃ c, eval c = f✝
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)
case rfind f pf hf =>
  rcases hf with ⟨cf, rfl⟩
  refine' ⟨comp (rfind' cf) (pair Code.id zero), _⟩
  simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']
no goals
f : ℕ →. ℕ
⊢ ∃ c, eval c = pure 0
exact ⟨zero, rfl⟩
no goals
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑Nat.succ
exact ⟨succ, rfl⟩
no goals
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).fst
exact ⟨left, rfl⟩
no goals
f : ℕ →. ℕ
⊢ ∃ c, eval c = ↑fun n => (unpair n).snd
exact ⟨right, rfl⟩
case intro
f g : ℕ →. ℕ
pg : Partrec g
hg : ∃ c, eval c = g
cf : Code
pf : Partrec (eval cf)
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> eval cf n) fun x => g n
f✝ f g : ℕ →. ℕ
pf : Partrec f
pg : Partrec g
hf : ∃ c, eval c = f
hg : ∃ c, eval c = g
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> f n) fun x => g n
rcases hf with ⟨cf, rfl⟩
case intro.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec (eval cf)
cg : Code
pg : Partrec (eval cg)
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> eval cf n) fun x => eval cg n
case intro
f g : ℕ →. ℕ
pg : Partrec g
hg : ∃ c, eval c = g
cf : Code
pf : Partrec (eval cf)
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> eval cf n) fun x => g n
rcases hg with ⟨cg, rfl⟩
no goals
case intro.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec (eval cf)
cg : Code
pg : Partrec (eval cg)
⊢ ∃ c, eval c = fun n => Seq.seq (Nat.pair <$> eval cf n) fun x => eval cg n
exact ⟨pair cf cg, rfl⟩
case intro
f g : ℕ →. ℕ
pg : Partrec g
hg : ∃ c, eval c = g
cf : Code
pf : Partrec (eval cf)
⊢ ∃ c, eval c = fun n => g n >>= eval cf
f✝ f g : ℕ →. ℕ
pf : Partrec f
pg : Partrec g
hf : ∃ c, eval c = f
hg : ∃ c, eval c = g
⊢ ∃ c, eval c = fun n => g n >>= f
rcases hf with ⟨cf, rfl⟩
case intro.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec (eval cf)
cg : Code
pg : Partrec (eval cg)
⊢ ∃ c, eval c = fun n => eval cg n >>= eval cf
case intro
f g : ℕ →. ℕ
pg : Partrec g
hg : ∃ c, eval c = g
cf : Code
pf : Partrec (eval cf)
⊢ ∃ c, eval c = fun n => g n >>= eval cf
rcases hg with ⟨cg, rfl⟩
no goals
case intro.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec (eval cf)
cg : Code
pg : Partrec (eval cg)
⊢ ∃ c, eval c = fun n => eval cg n >>= eval cf
exact ⟨comp cf cg, rfl⟩
case intro
f g : ℕ →. ℕ
pg : Partrec g
hg : ∃ c, eval c = g
cf : Code
pf : Partrec (eval cf)
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (eval cf a)
          (fun y IH => do
            let i ← IH
            g (Nat.pair a (Nat.pair y i)))
          n
f✝ f g : ℕ →. ℕ
pf : Partrec f
pg : Partrec g
hf : ∃ c, eval c = f
hg : ∃ c, eval c = g
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (f a)
          (fun y IH => do
            let i ← IH
            g (Nat.pair a (Nat.pair y i)))
          n
rcases hf with ⟨cf, rfl⟩
case intro.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec (eval cf)
cg : Code
pg : Partrec (eval cg)
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (eval cf a)
          (fun y IH => do
            let i ← IH
            eval cg (Nat.pair a (Nat.pair y i)))
          n
case intro
f g : ℕ →. ℕ
pg : Partrec g
hg : ∃ c, eval c = g
cf : Code
pf : Partrec (eval cf)
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (eval cf a)
          (fun y IH => do
            let i ← IH
            g (Nat.pair a (Nat.pair y i)))
          n
rcases hg with ⟨cg, rfl⟩
no goals
case intro.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec (eval cf)
cg : Code
pg : Partrec (eval cg)
⊢ ∃ c,
    eval c =
      unpaired fun a n =>
        Nat.rec (eval cf a)
          (fun y IH => do
            let i ← IH
            eval cg (Nat.pair a (Nat.pair y i)))
          n
exact ⟨prec cf cg, rfl⟩
case intro
f : ℕ →. ℕ
cf : Code
pf : Partrec (eval cf)
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> eval cf (Nat.pair a n)
f✝ f : ℕ →. ℕ
pf : Partrec f
hf : ∃ c, eval c = f
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a n)
rcases hf with ⟨cf, rfl⟩
case intro
f : ℕ →. ℕ
cf : Code
pf : Partrec (eval cf)
⊢ eval (comp (rfind' cf) (pair Code.id zero)) = fun a =>
    Nat.rfind fun n => (fun m => decide (m = 0)) <$> eval cf (Nat.pair a n)
case intro
f : ℕ →. ℕ
cf : Code
pf : Partrec (eval cf)
⊢ ∃ c, eval c = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> eval cf (Nat.pair a n)
refine' ⟨comp (rfind' cf) (pair Code.id zero), _⟩
no goals
case intro
f : ℕ →. ℕ
cf : Code
pf : Partrec (eval cf)
⊢ eval (comp (rfind' cf) (pair Code.id zero)) = fun a =>
    Nat.rfind fun n => (fun m => decide (m = 0)) <$> eval cf (Nat.pair a n)
simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']
case intro
c : Code
⊢ Partrec (eval c)
f : ℕ →. ℕ
h : ∃ c, eval c = f
⊢ Partrec f
rcases h with ⟨c, rfl⟩
case intro.zero

⊢ Partrec (eval zero)

case intro.succ

⊢ Partrec (eval succ)

case intro.left

⊢ Partrec (eval left)

case intro.right

⊢ Partrec (eval right)

case intro.pair
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (pair a✝¹ a✝))

case intro.comp
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (comp a✝¹ a✝))

case intro.prec
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (prec a✝¹ a✝))

case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case intro
c : Code
⊢ Partrec (eval c)
induction c
case intro.succ

⊢ Partrec (eval succ)

case intro.left

⊢ Partrec (eval left)

case intro.right

⊢ Partrec (eval right)

case intro.pair
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (pair a✝¹ a✝))

case intro.comp
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (comp a✝¹ a✝))

case intro.prec
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (prec a✝¹ a✝))

case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case intro.zero

⊢ Partrec (eval zero)

case intro.succ

⊢ Partrec (eval succ)

case intro.left

⊢ Partrec (eval left)

case intro.right

⊢ Partrec (eval right)

case intro.pair
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (pair a✝¹ a✝))

case intro.comp
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (comp a✝¹ a✝))

case intro.prec
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (prec a✝¹ a✝))

case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case zero => exact Nat.Partrec.zero
case intro.left

⊢ Partrec (eval left)

case intro.right

⊢ Partrec (eval right)

case intro.pair
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (pair a✝¹ a✝))

case intro.comp
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (comp a✝¹ a✝))

case intro.prec
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (prec a✝¹ a✝))

case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case intro.succ

⊢ Partrec (eval succ)

case intro.left

⊢ Partrec (eval left)

case intro.right

⊢ Partrec (eval right)

case intro.pair
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (pair a✝¹ a✝))

case intro.comp
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (comp a✝¹ a✝))

case intro.prec
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (prec a✝¹ a✝))

case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case succ => exact Nat.Partrec.succ
case intro.right

⊢ Partrec (eval right)

case intro.pair
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (pair a✝¹ a✝))

case intro.comp
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (comp a✝¹ a✝))

case intro.prec
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (prec a✝¹ a✝))

case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case intro.left

⊢ Partrec (eval left)

case intro.right

⊢ Partrec (eval right)

case intro.pair
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (pair a✝¹ a✝))

case intro.comp
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (comp a✝¹ a✝))

case intro.prec
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (prec a✝¹ a✝))

case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case left => exact Nat.Partrec.left
case intro.pair
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (pair a✝¹ a✝))

case intro.comp
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (comp a✝¹ a✝))

case intro.prec
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (prec a✝¹ a✝))

case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case intro.right

⊢ Partrec (eval right)

case intro.pair
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (pair a✝¹ a✝))

case intro.comp
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (comp a✝¹ a✝))

case intro.prec
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (prec a✝¹ a✝))

case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case right => exact Nat.Partrec.right
case intro.comp
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (comp a✝¹ a✝))

case intro.prec
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (prec a✝¹ a✝))

case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case intro.pair
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (pair a✝¹ a✝))

case intro.comp
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (comp a✝¹ a✝))

case intro.prec
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (prec a✝¹ a✝))

case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case pair cf cg pf pg => exact pf.pair pg
case intro.prec
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (prec a✝¹ a✝))

case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case intro.comp
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (comp a✝¹ a✝))

case intro.prec
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (prec a✝¹ a✝))

case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case comp cf cg pf pg => exact pf.comp pg
case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case intro.prec
a✝¹ a✝ : Code
a_ih✝¹ : Partrec (eval a✝¹)
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (prec a✝¹ a✝))

case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case prec cf cg pf pg => exact pf.prec pg
no goals
case intro.rfind'
a✝ : Code
a_ih✝ : Partrec (eval a✝)
⊢ Partrec (eval (rfind' a✝))
case rfind' cf pf => exact pf.rfind'
no goals
⊢ Partrec (eval zero)
exact Nat.Partrec.zero
no goals
⊢ Partrec (eval succ)
exact Nat.Partrec.succ
no goals
⊢ Partrec (eval left)
exact Nat.Partrec.left
no goals
⊢ Partrec (eval right)
exact Nat.Partrec.right
no goals
cf cg : Code
pf : Partrec (eval cf)
pg : Partrec (eval cg)
⊢ Partrec (eval (pair cf cg))
exact pf.pair pg
no goals
cf cg : Code
pf : Partrec (eval cf)
pg : Partrec (eval cg)
⊢ Partrec (eval (comp cf cg))
exact pf.comp pg
no goals
cf cg : Code
pf : Partrec (eval cf)
pg : Partrec (eval cg)
⊢ Partrec (eval (prec cf cg))
exact pf.prec pg
no goals
cf : Code
pf : Partrec (eval cf)
⊢ Partrec (eval (rfind' cf))
exact pf.rfind'