Re: [mizar] Another factor...

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

Dear Artur,

>how did you count theorems like theorem 4.2 of section "Meet
>Continuous Lattices" (CCL)? It is formalized in waybel_2:38
>.. 55 (18 Mizar theorems).

I counted it as one.  There's only one "theorem" in the
header of this "item"...

(Talking about equivalences: I always long for a special way
to prove equavalences in Mizar.  Something like that you can
write something like:

  A iff B
  proof
   per directions;
   suppose A;
    ...
    thus B;
   suppose B;
    ...
    thus A;
  end;

Where "per directions" behaves a bit like "per cases":
substitute a better syntax for this if you like, I'm not very
good at inventing syntaxes, but I know what I want it to be
structured like.

Currently I'm generally writing:

  A iff B
  proof
   hereby
    assume A;
    ...
    thus B;
   end;
   assume B;
   ...
   thus A;
  end;

and that feels asymmetrical.  Also, you cannot write "thus
thesis" for "thus B", which is irritating.)

For the record: here are the precise counts that I found.
I relied on the tables in
<http://megrez.mizar.org/ccl/state.html>, I didn't check
whether they were correct.

  CCL
    part that corresponds to WAYBEL series

    pages		 107
    "items"
      proposition         53
      definition          46
      theorem             39
      lemma               32
      corollary           19
      remark              16
      exercise             8
      examples             4
      notation             2
    total                219


  MML
    part that correspond to CCL
      WAYBEL series
	theorem		1509
	def theorem	 272
      total		1780
      YELLOW series
	theorem		1017
	def theorem	 138
      total		1155

    total		2935

And then the divisions went like: 1780/219 = 8.1 and 2935/219 = 13.4.

Freek