A question on recursive partial function correctness

Dear All,

Attached is a Mizar article called order.miz (part of what I have been working on) and its .voc file called seql.voc. 

I am interested in finishing the correctness proof of a partial recursive function called 'order' in the order.miz article.

I have done the correctness proof of a recursive function before (that adds all the natural numbers upto a given natural number to the function)
without using any of the schemes used for recursive functions' correctness (there was none at the time and I think still there is none). 

It looks like I need help with this one. First I would like to give some information about the partial recursive function called order:

1) It is a partial function. 
    Its domain is a subset of the set of FinSequence's (which I called FinSequenceS). The definition of the set of all FinSequence' s is given 
    there and I hope this is the right (or a rigth) way of defining such a set. The function is defined for a subset of the set of FinSequence's 
    and actually a description of its domain can be given precisely to make it a quasi-total or total function. But I want to keep it a 
    partial function because I have other partial recursive functions which have to be partial and I want
    to know how to prove correctness of a partial recursive function with this given domain of FinSequenceS. 

2) I would like to give some examples of the mapping order performs:
    
    order.<*C,4*> = 0
    order.<*S,<C,6*>*> = 1
    order.<*S,<*C,8*>,<*S,<*C,7*>*>*> = 2

    It basically maps 'certain finite sequences' to natural numbers showing how deep they are (basically how deep the S's are). 

3) I can change the definition of the order function (keeping the above meaning) if there is an easier way of proving its correctness. 

4) I checked the MML and the only helpful shceme was PARTFUN1:sch 2. 

5) There some comments in the order.miz file that I think might be helpful. 


I appreciate all the help and hope you are all having a good semester.


Adem Ozyavas
Texas Tech University
Computer Science Department