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
Attachment:
order.miz
Description: order.miz
Attachment:
seql.voc
Description: seql.voc