Theorem: LO.FirstOrder.UFormula.shiftb_shiftb_zero (Logic/FirstOrder/Computability/Formula.lean)

State before:
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ : ℕ
⊢ shiftb (shiftb b m₁) m₂ = shiftb b (m₁ + m₂)
Tactic:
unfold shiftb
State after:
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ : ℕ
⊢ (fun x =>
      if x < m₂ then UTerm.bvar x
      else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    fun x => if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))

State before:
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ : ℕ
⊢ (fun x =>
      if x < m₂ then UTerm.bvar x
      else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    fun x => if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
funext x
State after:
case h
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))

State before:
case h
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
by_cases hm₂ : x < m₂
State after:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : x < m₂
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))

case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))

State before:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : x < m₂
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
have : x < m₁ + m₂ := lt_add_of_nonneg_of_lt (Nat.zero_le m₁) hm₂
State after:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : x < m₂
this : x < m₁ + m₂
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))

State before:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : x < m₂
this : x < m₁ + m₂
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
simp[hm₂, this]
State after:
no goals

State before:
case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
⊢ (if x < m₂ then UTerm.bvar x
    else UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁)))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
simp[hm₂]
State after:
case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))

State before:
case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
by_cases hm₁ : x < m₁ + m₂
State after:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : x < m₁ + m₂
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))

case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : ¬x < m₁ + m₂
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))

State before:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : x < m₁ + m₂
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
have : x - m₂ < m₁ := Nat.sub_lt_right_of_lt_add (Nat.not_lt.mp hm₂) hm₁
State after:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : x < m₁ + m₂
this : x - m₂ < m₁
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))

State before:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : x < m₁ + m₂
this : x - m₂ < m₁
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
simp[hm₁, this, UTerm.bShifts, UTerm.bind]
State after:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : x < m₁ + m₂
this : x - m₂ < m₁
⊢ x - m₂ + m₂ = x

State before:
case pos
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : x < m₁ + m₂
this : x - m₂ < m₁
⊢ x - m₂ + m₂ = x
Tactic:
exact tsub_add_cancel_of_le (Nat.not_lt.mp hm₂)
State after:
no goals

State before:
case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : ¬x < m₁ + m₂
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
have : ¬x - m₂ < m₁ := Nat.not_lt.mpr <| Nat.le_sub_of_add_le <| Nat.not_lt.mp hm₁
State after:
case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : ¬x < m₁ + m₂
this : ¬x - m₂ < m₁
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))

State before:
case neg
L : Language
μ : Type v
b : ℕ → UTerm L μ
m₁ m₂ x : ℕ
hm₂ : ¬x < m₂
hm₁ : ¬x < m₁ + m₂
this : ¬x - m₂ < m₁
⊢ UTerm.bShifts m₂ (if x - m₂ < m₁ then UTerm.bvar (x - m₂) else UTerm.bShifts m₁ (b (x - m₂ - m₁))) =
    if x < m₁ + m₂ then UTerm.bvar x else UTerm.bShifts (m₁ + m₂) (b (x - (m₁ + m₂)))
Tactic:
simp[hm₁, this, Nat.sub_sub, add_comm]
State after:
no goals