[forall f in Frags], !(f.m_next=null) => <f,f.m_next> in Next;
[forall f in Frags], !(f.m_prev=null) => <f,f.m_prev> in Prev;
[forall f in Frags], (f.m_next=null) => f in Last;
[forall f in Frags], !(f.m_next=null) => <f,f.m_next> in Next;
[forall f in Frags], !(f.m_prev=null) => <f,f.m_prev> in Prev;
[forall f in Frags], (f.m_next=null) => f in Last;