[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] how to number 1...n!

Dear PVS user:
can you give me an expression about numbered from 1 to n!
i.e. if give n mubers and their orders
can we determine its number using PVS sepcifications.

we want to give a uniqiue number for each different order.

for example n=3:

unique_number(x1,x2,x3 ): upto(3!) =
cond x1<=x2<=x3 ->1
x1<=x3<=x2 -> 2
x2<=x1<=x3 ->3
x2<=x3<=x1 ->4
x3<=x1<=x2 ->5
x3<=x2<=x1 -> 6

if n is not known to us. how to implement the above process using PVS

any comments are welcome!

thanks in advance.

Q.G., XU.