Theorem: LO.FirstOrder.UTerm.bv_bind (Logic/FirstOrder/Computability/Term.lean)

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
t : UTerm L μ₁
hb : ∀ x < t.bv, (b x).bv ≤ m
he : ∀ (x : μ₁), (e x).bv ≤ m
⊢ (bind b e t).bv ≤ m
Tactic:
induction t
State after:
case bvar
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : ℕ
hb : ∀ x < (bvar a✝).bv, (b x).bv ≤ m
⊢ (bind b e (bvar a✝)).bv ≤ m

case fvar
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : μ₁
hb : ∀ x < (fvar a✝).bv, (b x).bv ≤ m
⊢ (bind b e (fvar a✝)).bv ≤ m

case func
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → UTerm L μ₁
a_ih✝ : ∀ (a : Fin arity✝), (∀ x < (a✝ a).bv, (b x).bv ≤ m) → (bind b e (a✝ a)).bv ≤ m
hb : ∀ x < (func a✝¹ a✝).bv, (b x).bv ≤ m
⊢ (bind b e (func a✝¹ a✝)).bv ≤ m

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : ℕ
hb : ∀ x < (bvar a✝).bv, (b x).bv ≤ m
⊢ (bind b e (bvar a✝)).bv ≤ m
Tactic:
case bvar => simp[bind, bv] at hb ⊢; exact hb _ (Nat.lt_succ_self _)
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : μ₁
hb : ∀ x < (fvar a✝).bv, (b x).bv ≤ m
⊢ (bind b e (fvar a✝)).bv ≤ m
Tactic:
case fvar => simp[bind, bv] at he ⊢; exact he _
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
⊢ (bind b e (func f v)).bv ≤ m
Tactic:
case func k f v ih =>
  simp[bind, bv]; intro i; exact ih i (fun x hx => hb x (by simp[bv]; exact ⟨i, hx⟩))
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : ℕ
hb : ∀ x < (bvar a✝).bv, (b x).bv ≤ m
⊢ (bind b e (bvar a✝)).bv ≤ m
Tactic:
simp[bind, bv] at hb ⊢
State after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : ℕ
hb : ∀ x < a✝ + 1, (b x).bv ≤ m
⊢ (b a✝).bv ≤ m

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : ℕ
hb : ∀ x < a✝ + 1, (b x).bv ≤ m
⊢ (b a✝).bv ≤ m
Tactic:
exact hb _ (Nat.lt_succ_self _)
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : μ₁
hb : ∀ x < (fvar a✝).bv, (b x).bv ≤ m
⊢ (bind b e (fvar a✝)).bv ≤ m
Tactic:
simp[bind, bv] at he ⊢
State after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : μ₁
hb : ∀ x < (fvar a✝).bv, (b x).bv ≤ m
⊢ (e a✝).bv ≤ m

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
a✝ : μ₁
hb : ∀ x < (fvar a✝).bv, (b x).bv ≤ m
⊢ (e a✝).bv ≤ m
Tactic:
exact he _
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
⊢ (bind b e (func f v)).bv ≤ m
Tactic:
simp[bind, bv]
State after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
⊢ ∀ (b_1 : Fin k), (bind b e (v b_1)).bv ≤ m

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
⊢ ∀ (b_1 : Fin k), (bind b e (v b_1)).bv ≤ m
Tactic:
intro i
State after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
i : Fin k
⊢ (bind b e (v i)).bv ≤ m

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
i : Fin k
⊢ (bind b e (v i)).bv ≤ m
Tactic:
exact ih i (fun x hx => hb x (by simp[bv]; exact ⟨i, hx⟩))
State after:
no goals

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ x < (func f v).bv
Tactic:
simp[bv]
State after:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ ∃ b, x < (v b).bv

State before:
L : Language
μ : Type v
μ₂ : Type u_1
μ₁ : Type u_2
m : ℕ
b : ℕ → UTerm L μ₂
e : μ₁ → UTerm L μ₂
he : ∀ (x : μ₁), (e x).bv ≤ m
k : ℕ
f : L.Func k
v : Fin k → UTerm L μ₁
ih : ∀ (a : Fin k), (∀ x < (v a).bv, (b x).bv ≤ m) → (bind b e (v a)).bv ≤ m
hb : ∀ x < (func f v).bv, (b x).bv ≤ m
i : Fin k
x : ℕ
hx : x < (v i).bv
⊢ ∃ b, x < (v b).bv
Tactic:
exact ⟨i, hx⟩
State after:
no goals