∀ (n x x_1 : ℕ),
  Nat.log.go n x x_1 =
    match x, x_1 with
    | x, 0 => (n, 0)
    | b, fuel.succ =>
      if n < b then (n, 0)
      else
        match Nat.log.go n (b * b) fuel with
        | (q, e) => if q < b then (q, 2 * e) else (q / b, 2 * e + 1)