linked-list - ACSL 中的归纳谓词表明一个链表是另一个链表的子表

Question

我需要在 ACSL 中编写一个归纳谓词，说明一个链表是另一个链表的子表。

谓词的签名应该是这样的：

inductive subLinkedList{L1,L2} (LinkedList l) {
...
}

所以基本上我想要一个谓词来说明状态 L1 上的链表 l 是同一个链表 l 的子列表，但在这种情况下是状态 L2。