How to do amortized analysis of binomial heap?

Question

Algorithms

In Chris Okasaki's book Purely Functional Data Structures, the challenge is to prove that the amortized cost of a merge operation for a binomial heap is O(log n).

Given code in Standard ML

datatype Tree = Node of int * Elem.T * Tree list
type Heap = Tree list

fun rank (Node (r,x,c)) = r

fun link (t1 as Node (r1, x1, c1), t2 as Node (r2, x2, c2)) =
  if Elem.leq (x1, x2) then Node (r+1, x1, t2::c1)
  else Node (r+1, x2, t1::c2)

fun insTree (t, []) = [t]
  | insTree (t, ts as t'::ts') =
     if rank t < rank t' then t::ts else insTree (link (t, t'), ts')

fun merge (ts1, []) = ts1
  | merge ([], ts2) = ts2
  | merge (ts1 as t1::ts1', ts2 as t2::ts2') =
     if rank t1 < rank t2 then t1::merge (ts1', ts2)
     else if rank t2 < rank t1 then t2::merge (ts1, ts2')
     else insTree (link (t1, t2), merge (ts1', ts2'))

Answer 1

I have not read the book, but I believe that there is such a task. Probably, it is assumed that the material that was presented earlier allows the student to independently prove the specified thesis. What do you want from us? What if we read this book, along the way, having studied the Standard ML that few people really need and proving something for you?
PS Hint. The complexity of the algorithm for inserting an element into a binary heap does not exceed O(logN). For an elementary explanation, see for example here - https://habr.com/ru/post/112222/