what scheme to use?

View: New views
2 Messages — Rating Filter:   Alert me  

what scheme to use?

by Ozyavas, Adem :: Rate this Message:

Reply to Author | View Threaded | Show Only this Message

Hello All,

I wrote a recursive function in Mizar which takes two arguments, two natural numbers, and maps them to another natural number. I searched the MML and could not find a scheme that I could use in the proof of correctness (existence and uniqueness) of that function. I appreciate any help.

Adem Ozyavas

Re: what scheme to use?

by trybulec :: Rate this Message:

Reply to Author | View Threaded | Show Only this Message

Hi:

Could you attach your Mizar article, it will be easier to find out how
to solve the problem.

Regards,
Andrzej Trybulec

Ozyavas, Adem wrote:

>Hello All,
>
>I wrote a recursive function in Mizar which takes two arguments, two natural numbers, and maps them to another natural number. I searched the MML and could not find a scheme that I could use in the proof of correctness (existence and uniqueness) of that function. I appreciate any help.
>
>Adem Ozyavas
>
>
>  
>