what scheme to use?

[Ozyavas, Adem]

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

[trybulec]

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
>
>
>  
>