Theorem: Nat.ArithPart₁.of_partrec (Logic/Vorspiel/Arith.lean)

State before:
n : ℕ
f : Vector ℕ n →. ℕ
hf : Partrec' f
⊢ ArithPart₁ f
Tactic:
induction hf
State after:
case prim
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : Vector ℕ n✝ → ℕ
a✝ : Primrec' f✝
⊢ ArithPart₁ ↑f✝

case comp
n : ℕ
f : Vector ℕ n →. ℕ
m✝ n✝ : ℕ
f✝ : Vector ℕ n✝ →. ℕ
g✝ : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : Partrec' f✝
a✝ : ∀ (i : Fin n✝), Partrec' (g✝ i)
a_ih✝¹ : ArithPart₁ f✝
a_ih✝ : ∀ (i : Fin n✝), ArithPart₁ (g✝ i)
⊢ ArithPart₁ fun v => (mOfFn fun i => g✝ i v) >>= f✝

case rfind
n : ℕ
f : Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f✝
a_ih✝ : ArithPart₁ ↑f✝
⊢ ArithPart₁ fun v => rfind fun n => Part.some (decide (f✝ (n ::ᵥ v) = 0))

State before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
n✝ : ℕ
f : Vector ℕ n✝ → ℕ
hf : Primrec' f
⊢ ArithPart₁ ↑f
Tactic:
case prim f hf          => exact of_primrec hf
State after:
no goals

State before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
m✝ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : Partrec' f
a✝ : ∀ (i : Fin n✝), Partrec' (g i)
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
⊢ ArithPart₁ fun v => (mOfFn fun i => g i v) >>= f
Tactic:
case comp f g _ _ hf hg => exact hf.comp _ hg
State after:
no goals

State before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f
hf : ArithPart₁ ↑f
⊢ ArithPart₁ fun v => rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
Tactic:
case rfind f _ hf       => exact ArithPart₁.rfind hf
State after:
no goals

State before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
n✝ : ℕ
f : Vector ℕ n✝ → ℕ
hf : Primrec' f
⊢ ArithPart₁ ↑f
Tactic:
exact of_primrec hf
State after:
no goals

State before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
m✝ n✝ : ℕ
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : Partrec' f
a✝ : ∀ (i : Fin n✝), Partrec' (g i)
hf : ArithPart₁ f
hg : ∀ (i : Fin n✝), ArithPart₁ (g i)
⊢ ArithPart₁ fun v => (mOfFn fun i => g i v) >>= f
Tactic:
exact hf.comp _ hg
State after:
no goals

State before:
n : ℕ
f✝ : Vector ℕ n →. ℕ
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : Partrec' ↑f
hf : ArithPart₁ ↑f
⊢ ArithPart₁ fun v => rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
Tactic:
exact ArithPart₁.rfind hf
State after:
no goals