[mizar] A question on "registrations"

["Ozyavas, Adem" <adem.ozyavas@ttu.edu>]

Dear All,

Attached is my file sequenceL.miz and its .voc file. 

Line 6711 has a functor defintion whose argument type is FinSequence-yielding FinSequence.

I am getting the error *136 (non registered cluster). I believe the existence of that type should be proved.

I checked the PRE_POLY.miz and there is the existence cluster: 

registration
   cluster FinSequence-yielding Function;
end;

I included the PRE_POLY to "registrations" directive but this time I am getting the error *103 (unknown functor) at line 6718
where 'fs' is the FinSequence-yielding FinSequence.

I am using the 7.11.05 version of Mizar.

Note: I tried the transh and trans functors (starting at line 6711) defintions inside the PRE_POLY and the verifier compiled with no complaint.

Thank you very much for all the help.

Adem Ozyavas
Texas Tech University

Attachment: sequencel.miz
Description: sequencel.miz

Attachment: seql.voc
Description: seql.voc