[mizar] Reference distances?

[Freek Wiedijk <freek@cs.ru.nl>]

Hello!

I wonder whether anyone here can tell me the answer to the
following:

I would like to know the statistics about the "distances" of
references to labels in justifications.  Specifically:

In the article that you're interested in, put _one_ label on
everything that you can put a label on.  Then, restrict
yourself to labels that are "inside" a proof/end (or now/end,
hereby/end, etc.) block.  Then, for a justification "count
back" to accessible labels.  So the label of the statement
accessible with "then" would be counted as "1", the one before
that as "2", etc.  For instance in

  theorem Th1: ...
  proof
    ...
  end;

  theorem Th2: ...
  proof
  A1: ...
  consider ... such that A2: ...
  assume A3: ...
   proof
  A4: ...
   end;
  A5: ...
  then A6: ... by Th1,A1;
  end;

the distances for this "by" at the justification of A6 would
be 1 (for the implicit A5 that's in the "then") and 4 (for the
A1).  The "Th1" label should be ignored as it is outside the
proof/end blocks.

So what I would like to see is a table of how many times any
specific distance (defined like this) occurs in MML.  In
particular: I'm curious what kind of "power law" would fit
these numbers.

If anyone can say anything interesting about this, I would be
very much interested!

Freek