Реализовать операцию добавления для связанного списка в dafny со сложностью O (1)

В dafny мы можем использовать set<T> в качестве динамического фрейма для проверки завершения связанного списка:

class Node {
  // the sequence of data values stored in a node and its successors.
  ghost var list: seq<Data>;
  // `footprint` is a set consisting of the node and its successors.
  // it is actually the dynamic frame mentioned in the paper.
  ghost var footprint: set<Node>;

  var data: Data;
  var next: Node?;

  // A "Valid" linked list is one without ring. 
  function Valid(): bool
    reads this, footprint
  {
    this in footprint &&
    (next == null ==> list  == [data]) &&
    (next != null ==> next in footprint &&
                      next.footprint <= footprint &&
                      !(this in next.footprint) &&
                      list == [data] + next.list &&
                      next.Valid())
  }
  ...
}

(Это реализация в Спецификация и проверка объектно-ориентированного программного обеспечения.)

Однако footprint затрудняет реализацию операции append. Потому что при добавлении нового узла в связанный список нам нужно обновить footprint всех предыдущих узлов. Интересно, можно ли реализовать append со сложностью O(1) в dafny (кроме методов-призраков) или нужно убрать Valid и использовать decreases *?

Спасибо:)