Re: [mizar] quite some questions about functions

[Jesse Alama <alama@stanford.edu>]

Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:

> Hi Ad[ae]m :-),
>
> On Mon, 12 May 2008, Adam Naumowicz wrote:
>
>> On Mon, 12 May 2008, Ozyavas, Adem wrote:
>>
>>> 3) Is there any method/tool to know what the current thesis is at
>>> any point of proof?
>>>
>>> definition
>>>  func exp -> Function of COMPLEX, COMPLEX means
>>>  :Def18:
>>>  for z being Element of COMPLEX holds it.z=Sum(z ExpSeq);
>>>  existence
>>>  proof
>>>    deffunc U(Element of COMPLEX) = Sum($1 ExpSeq);
>>>    consider f being Function of COMPLEX, COMPLEX such that
>>> A1: for x being Element of COMPLEX holds f.x = U(x) from FUNCT_2:sch 4;
>>>    take f;
>>>    thus thesis by A1;
>>>  end;
>>>  uniqueness
>>>  proof
>>>  ...
>>
>> Fortunately Josef has added such functionality to his XML rendering
>> of Mizar articles. Just run Mizar on an article and then view the
>> *.xml file created in an XML-supporting web browser - you should be
>> able to click on some items to see the thesis at certain proof
>> steps.
>
> Or, if it is an existing MML article like in this case, just go to:
> http://mmlquery.mizar.org/mml/current/sin_cos.html#D18 . Clicking on
> the 'existence' keyword will show you the existence condition, and
> clicking on the followng 'proof' keyword will expand the proof, where
> the ':: thesis:' after each natural deduction step can again be
> clicked on.
>
> If it is a new article (not yet in MML), either use the method Adam
> described, or you can also paste the article into
> http://octopi.mizar.org/~mptp/MizAR.html and press the Send button.

What's going on at octopi.mizar.org?

Jesse

-- 
Jesse Alama (alama@stanford.edu)