Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
k n x : ℕ
h : n ≤ k ∧ 0 = x
⊢ x ∈ pure 0 n

pp: case succ
k n x : ℕ
h : n ≤ k ∧ n + 1 = x
⊢ x = n + 1

pp: case left
k n x : ℕ
h : n ≤ k ∧ (unpair n).1 = x
⊢ x = (unpair n).1

pp: case right
k n x : ℕ
h : n ≤ k ∧ (unpair n).2 = x
⊢ x = (unpair n).2

pp: case pair
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h : n ≤ k ∧ ∃ a, evaln (k + 1) a✝¹ n = some a ∧ ∃ a_1, evaln (k + 1) a✝ n = some a_1 ∧ Nat.pair a a_1 = x
⊢ ∃ a ∈ a✝¹.eval n, ∃ a_1 ∈ a✝.eval n, Nat.pair a a_1 = x

pp: case comp
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h : n ≤ k ∧ ∃ a, evaln (k + 1) a✝ n = some a ∧ evaln (k + 1) a✝¹ a = some x
⊢ ∃ a ∈ a✝.eval n, x ∈ a✝¹.eval a

pp: case prec
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h :
  n ≤ k ∧
    Nat.rec (evaln (k + 1) a✝¹ (unpair n).1)
        (fun n_1 n_ih ↦
          (evaln k (a✝¹.prec a✝) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
            evaln (k + 1) a✝ (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 =
      some x
⊢ x ∈
    Nat.rec (a✝¹.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ a✝.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
      (unpair n).2

pp: case rfind'
k : ℕ
a✝ : Code
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h :
  n ≤ k ∧
    ∃ a,
      evaln (k + 1) a✝ n = some a ∧
        (if a = 0 then some (unpair n).2 else evaln k a✝.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ ∃ a,
    (0 ∈ a✝.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ a✝.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x

Tactic:
<;>

Goal state after:
case zero
k n x : ℕ
h : n ≤ k ∧ 0 = x
⊢ x ∈ pure 0 n

case succ
k n x : ℕ
h : n ≤ k ∧ n + 1 = x
⊢ x = n + 1

case left
k n x : ℕ
h : n ≤ k ∧ (unpair n).1 = x
⊢ x = (unpair n).1

case right
k n x : ℕ
h : n ≤ k ∧ (unpair n).2 = x
⊢ x = (unpair n).2

case pair
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h : n ≤ k ∧ ∃ a, evaln (k + 1) a✝¹ n = some a ∧ ∃ a_1, evaln (k + 1) a✝ n = some a_1 ∧ Nat.pair a a_1 = x
⊢ ∃ a ∈ a✝¹.eval n, ∃ a_1 ∈ a✝.eval n, Nat.pair a a_1 = x

case comp
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h : n ≤ k ∧ ∃ a, evaln (k + 1) a✝ n = some a ∧ evaln (k + 1) a✝¹ a = some x
⊢ ∃ a ∈ a✝.eval n, x ∈ a✝¹.eval a

case prec
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h :
  n ≤ k ∧
    Nat.rec (evaln (k + 1) a✝¹ (unpair n).1)
        (fun n_1 n_ih ↦
          (evaln k (a✝¹.prec a✝) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
            evaln (k + 1) a✝ (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
        (unpair n).2 =
      some x
⊢ x ∈
    Nat.rec (a✝¹.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ a✝.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
      (unpair n).2

case rfind'
k : ℕ
a✝ : Code
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
h :
  n ≤ k ∧
    ∃ a,
      evaln (k + 1) a✝ n = some a ∧
        (if a = 0 then some (unpair n).2 else evaln k a✝.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ ∃ a,
    (0 ∈ a✝.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ a✝.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x