Struct LinkedListOwner Copy item path

{
    &&& self.perms.contains_key(i)
    &&& self.perms[i].addr() == self.list[i].paddr
    &&& self.perms[i].points_to.addr() == self.list[i].paddr
    &&& self.perms[i].wf()
    &&& self.perms[i].addr() % META_SLOT_SIZE() == 0
    &&& FRAME_METADATA_RANGE().start <= self.perms[i].addr()
        < FRAME_METADATA_RANGE().start + MAX_NR_PAGES() * META_SLOT_SIZE()
    &&& self.perms[i].is_init()
    &&& self.perms[i].value().wf(self.list[i])
    &&& i == 0 <==> self.perms[i].mem_contents().value().prev is None
    &&& i == self.list.len() - 1 <==> self.perms[i].value().next is None
    &&& 0 < i
        ==> self.perms[i].value().prev is Some
            && self.perms[i].value().prev.unwrap() == self.perms[i - 1].pptr()
    &&& i < self.list.len() - 1
        ==> self.perms[i].value().next is Some
            && self.perms[i].value().next.unwrap() == self.perms[i + 1].pptr()
    &&& self.list[i].inv()
    &&& self.list[i].in_list == self.list_id

}

{
    if owners.len() == 0 {
        Seq::<LinkModel>::empty()
    } else {
        seq![owners[0].view()].add(Self::view_helper(owners.remove(0)))
    }
}

Self::view_helper(owners).len() == owners.len(),

{ forall |i: int| 0 <= i < self.list.len() ==> self.inv_at(i) }

{
    LinkedListModel {
        list: Self::view_helper(self.list),
    }
}