[mizar] strict

[Jesse Alama <alama@stanford.edu>]

I'm working on defining the field 2 = {0,1} with the usual operations
and thus want to define a term, say F2, which looks like

definition
  func F2 -> Field equals doubleLoopStr (# ... #);
end;

The proof that F2 is a field is going to be fairly long, as far as I
can see, so I've decided to do things somewhat less directly.  I
define F2 as

definition
  func F2 -> doubleLoopStr equals
  doubleLoopStr(# {0,1}, add2, prod2, unit2,  zero2 #);
  coherence;
end;

(I've defined add2, prod2, unit2, and zero2 in the required ways.)  My
goal is

theorem F2 is Field;

I accomplish this by proving that F2 has the attributes

- non degenerated

- Field-like

- right_complementable

- Abelian

- right_complementable

- associative

- commutative

- left_unital

- non empty

- right_zeroed

- add-associative, and

- strict.

The last attribute is troubling me; I don't see how to prove that my
doubleLoopStr is strict.  Actually, I don't even know what "strict"
means.  What confuses me is that unlike all the other attributes,
there doesn't seem to be a definition of what it means to be a strict
doubleLoopStr; moreover, when I browse

http://mmlquery.mizar.org/mmlquery/fillin.php?filledfilename=phparticle.mqt&argument=article+vectsp_1

I see that there appears to be something like a definition:

definition
  let a1 be doubleLoopStr;
  attr a1 is strict;
end;

but when I browse VECTSP_1.MIZ, I don't see any definition of strict
for doubleLoopStr's.  What's going on?  What does "strict" mean?  How
can I prove that a doubleLoopStr is strict?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*10: Too many basic sentences in an inference