[mizar] the latest version of my question

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

Dear All,

For the past week I have been both searching MML for a suitable scheme for a recursive function that I wrote and looking into the schemes for proof of recursive functions to get a feeling on how to write my own. I looked into every scheme in the MML not to miss anything. Finally, I focused more on  NAT_1:shc 12 yesterday which seemed more promising.

scheme :: NAT_1:sch 12
LambdaRecExD{ F1() -> non empty set , F2() -> Element of F1(), F3( set , set ) -> Element of F1() } :
ex f being Function of NAT ,F1() st
( f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F3(n,(f . n)) ) )
proof end;


and those in the recdef_1 and _2. So far, I am unable to make connections or drive some conclusions on where to start. The scheme I am trying to write for existence and uniqueness proofs is "for now" could be very specific to my function definition. For example, going back to NAT_1:shc 12, the last part could be
....
   (for m,n being Nat holds f.[m,n] = F(m,n,f.[(n mod m), m]);
....
,that is, all parameters are passed together with what needs to be constructed. If I can write this scheme, I will try the following scheme later:
...
  (for m,n being Nat holds f.[m,n] = F(m,n,f));
...
if it could be done in mizar like this (passing just "f" without its application to arguments so that I can make this scheme work for any function with two arguments no matter how it is defined.

By the way, the function I am trying to write a scheme for is the following one:

definition
  func megcd -> Function of [:NAT, NAT:], NAT means
  :Defmegcd:
  for m,n being Element of NAT holds
   it.[m,n] = IFEQ(m,0,n,it.[n mod m, m]);
  existence;
  uniqueness;
end;


I appreciate any guideline on how to write a scheme for recursive functions. I really need some instructions on where to start. Any referral to any link, tutorial, notes...Thank you all...

Adem Ozyavas
Graduate Student
Texas Tech University