[mizar] A general question on writing recursive functions in mizar

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

Hello All,

I want to write recursive functions in mizar and prove properties of them. I have found a paper by Yatsuka Nakamura which helped but not enough for me.  For the time being I am searching the MML for examples. Can anyone refer me to a tutorial, paper, notes, etc which provides info on 

1) the distinction between mizar functors and functions, 
2) how to write mizar recursive functions and prove their correctness.

I really appreciate that.

Regards,

Adem Ozyavas