[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
if n is not known to us. how to implement the above process using PVS
any comments are welcome!
thanks in advance.