The post condition of valid_index is clearly wrong in LINEAR_SUBSET 
It will be fixed.