-[],sizeof(Nodes) > 1;
-[forall node in Nodes],sizeof(node.~nextnodes)=1;
-
-
-
-
-
-
-
-
-
-
+[], sizeof(Nodes) >= literal(1);
+[forall node in Nodes], sizeof(node.~nextnodes) <= literal(1);
+[forall n in Nodes],
+ sizeof(n.nextnodes) = literal(0) or n.nextnodes.prevnodes = n;