no goals
⊢ encodeCode (ofNatCode 0) = 0
simp [ofNatCode, encodeCode]
no goals
⊢ encodeCode (ofNatCode 1) = 1
simp [ofNatCode, encodeCode]
no goals
⊢ encodeCode (ofNatCode 2) = 2
simp [ofNatCode, encodeCode]
no goals
⊢ encodeCode (ofNatCode 3) = 3
simp [ofNatCode, encodeCode]
n : ℕ
m : ℕ := div2 (div2 n)
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
n : ℕ
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
let m := n.div2.div2
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
n : ℕ
m : ℕ := div2 (div2 n)
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
have hm : m < n + 4 := by
  simp [Nat.div2_val]
  exact
    lt_of_le_of_lt (le_trans (Nat.div_le_self _ _) (Nat.div_le_self _ _))
      (Nat.succ_le_succ (Nat.le_add_right _ _))
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
_m1 : (unpair m).fst < n + 4
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
have _m1 : m.unpair.1 < n + 4 := lt_of_le_of_lt m.unpair_left_le hm
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
_m1 : (unpair m).fst < n + 4
_m2 : (unpair m).snd < n + 4
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
_m1 : (unpair m).fst < n + 4
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
have _m2 : m.unpair.2 < n + 4 := lt_of_le_of_lt m.unpair_right_le hm
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
_m1 : (unpair m).fst < n + 4
_m2 : (unpair m).snd < n + 4
IH : encodeCode (ofNatCode m) = m
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
_m1 : (unpair m).fst < n + 4
_m2 : (unpair m).snd < n + 4
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
have IH := encode_ofNatCode m
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
_m1 : (unpair m).fst < n + 4
_m2 : (unpair m).snd < n + 4
IH : encodeCode (ofNatCode m) = m
IH1 : encodeCode (ofNatCode (unpair m).fst) = (unpair m).fst
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
_m1 : (unpair m).fst < n + 4
_m2 : (unpair m).snd < n + 4
IH : encodeCode (ofNatCode m) = m
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
have IH1 := encode_ofNatCode m.unpair.1
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
_m1 : (unpair m).fst < n + 4
_m2 : (unpair m).snd < n + 4
IH : encodeCode (ofNatCode m) = m
IH1 : encodeCode (ofNatCode (unpair m).fst) = (unpair m).fst
IH2 : encodeCode (ofNatCode (unpair m).snd) = (unpair m).snd
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
_m1 : (unpair m).fst < n + 4
_m2 : (unpair m).snd < n + 4
IH : encodeCode (ofNatCode m) = m
IH1 : encodeCode (ofNatCode (unpair m).fst) = (unpair m).fst
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
have IH2 := encode_ofNatCode m.unpair.2
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
_m1 : (unpair m).fst < n + 4
_m2 : (unpair m).snd < n + 4
IH : encodeCode (ofNatCode m) = m
IH1 : encodeCode (ofNatCode (unpair m).fst) = (unpair m).fst
IH2 : encodeCode (ofNatCode (unpair m).snd) = (unpair m).snd
⊢ encodeCode (ofNatCode (n + 4)) = bit (bodd n) (bit (bodd (div2 n)) (div2 (div2 n))) + 4
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
_m1 : (unpair m).fst < n + 4
_m2 : (unpair m).snd < n + 4
IH : encodeCode (ofNatCode m) = m
IH1 : encodeCode (ofNatCode (unpair m).fst) = (unpair m).fst
IH2 : encodeCode (ofNatCode (unpair m).snd) = (unpair m).snd
⊢ encodeCode (ofNatCode (n + 4)) = n + 4
conv_rhs => rw [← Nat.bit_decomp n, ← Nat.bit_decomp n.div2]
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
_m1 : (unpair m).fst < n + 4
_m2 : (unpair m).snd < n + 4
IH : encodeCode (ofNatCode m) = m
IH1 : encodeCode (ofNatCode (unpair m).fst) = (unpair m).fst
IH2 : encodeCode (ofNatCode (unpair m).snd) = (unpair m).snd
⊢ encodeCode
      (match bodd n, bodd (div2 n) with
      | false, false => pair (ofNatCode (unpair (div2 (div2 n))).fst) (ofNatCode (unpair (div2 (div2 n))).snd)
      | false, true => comp (ofNatCode (unpair (div2 (div2 n))).fst) (ofNatCode (unpair (div2 (div2 n))).snd)
      | true, false => prec (ofNatCode (unpair (div2 (div2 n))).fst) (ofNatCode (unpair (div2 (div2 n))).snd)
      | true, true => rfind' (ofNatCode (div2 (div2 n)))) =
    bit (bodd n) (bit (bodd (div2 n)) (div2 (div2 n))) + 4
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
_m1 : (unpair m).fst < n + 4
_m2 : (unpair m).snd < n + 4
IH : encodeCode (ofNatCode m) = m
IH1 : encodeCode (ofNatCode (unpair m).fst) = (unpair m).fst
IH2 : encodeCode (ofNatCode (unpair m).snd) = (unpair m).snd
⊢ encodeCode (ofNatCode (n + 4)) = bit (bodd n) (bit (bodd (div2 n)) (div2 (div2 n))) + 4
simp [encodeCode, ofNatCode]
no goals
n : ℕ
m : ℕ := div2 (div2 n)
hm : m < n + 4
_m1 : (unpair m).fst < n + 4
_m2 : (unpair m).snd < n + 4
IH : encodeCode (ofNatCode m) = m
IH1 : encodeCode (ofNatCode (unpair m).fst) = (unpair m).fst
IH2 : encodeCode (ofNatCode (unpair m).snd) = (unpair m).snd
⊢ encodeCode
      (match bodd n, bodd (div2 n) with
      | false, false => pair (ofNatCode (unpair (div2 (div2 n))).fst) (ofNatCode (unpair (div2 (div2 n))).snd)
      | false, true => comp (ofNatCode (unpair (div2 (div2 n))).fst) (ofNatCode (unpair (div2 (div2 n))).snd)
      | true, false => prec (ofNatCode (unpair (div2 (div2 n))).fst) (ofNatCode (unpair (div2 (div2 n))).snd)
      | true, true => rfind' (ofNatCode (div2 (div2 n)))) =
    bit (bodd n) (bit (bodd (div2 n)) (div2 (div2 n))) + 4
cases n.bodd <;> cases n.div2.bodd <;>
  simp [encodeCode, ofNatCode, IH, IH1, IH2, Nat.bit_val]
n : ℕ
m : ℕ := div2 (div2 n)
⊢ n / 2 / 2 < n + 4
n : ℕ
m : ℕ := div2 (div2 n)
⊢ m < n + 4
simp [Nat.div2_val]
no goals
n : ℕ
m : ℕ := div2 (div2 n)
⊢ n / 2 / 2 < n + 4
exact
  lt_of_le_of_lt (le_trans (Nat.div_le_self _ _) (Nat.div_le_self _ _))
    (Nat.succ_le_succ (Nat.le_add_right _ _))