update of my questions :)

Dear All,

In my earlier email I had a question:

Q3) This is another major question that I have. How can we use the
scheme

scheme :: NAT_1:sch 4
 CompInd { P[Nat] } : for k being Nat holds P[k]
provided
 for k being Nat st for n being Nat st n < k holds P[n] holds P[k];

in the proof (1)? (This scheme seems to be designed to be used with
one variable (the induction variable) but in Theorem 1, there are
two variables where m is the induction variable and n is arbitrary.)


I solved that question. My general question is about if there is a scheme in the MML on how to
prove a function (the egcd I sent before or function whose definitiens is IFEQ(...)). I am going
to start working on doing the existence and uniqueness proof without schemes first and then try
to write my own scheme. I truly appreciate any help. Again, have a good semester...

Adem Ozyavas