1	import Base
2	import ../../../spec/containers/doubly_linked_list.bend as S
3	import ../../../src/containers/doubly_linked_list.bend as D
4	import ../../../src/containers/types/doubly_linked_list.bend as E
5	import ./state.bend as ST
6	import ./ok.bend as OK
7	import ./trace.bend as TR
8	import ./api.bend as API
9	import ../../lib/logic.bend as L
10	import ../../lib/list.bend as LL
11	import ../../../spec/lib/common.bend as SC
12	import ../../lib/nat.bend as N
13	import ../../lib/nat_list.bend as NL
14	import ../../../spec/lib/sequence.bend as V
15	import ../../lib/sequence.bend as VL
16	
17	# Doubly linked list with generational handles
18	# (src/containers/doubly_linked_list.bend over
19	# src/containers/internal/dlist_storage.bend): public proof entry point.
20	#   shadow       ST.Sh: the list's U32 fields and depth, a mirror tree for
21	#                each block (values, prev links, next links, generations),
22	#                and two ghost lists: the ids of the list in order and the
23	#                free stack; ST.real(sh) is the list
24	#   abstraction  ST.model(sh): the order, the values and generations of the
25	#                issued ids, and the free stack, as a
26	#                proofs/spec/doubly_linked_list.bend list
27	#   invariant    ST.good(sh): the blocks perfect at the depth, the capacity
28	#                2^depth (depth < 30) and the counter within it; the order
29	#                linked both ways with its head and tail, live, below the
30	#                counter and without repeats; every live slot on the order;
31	#                the free stack chained through the next links, vacant and
32	#                without repeats; the generations of unissued ids 0
33	#                (proofs/doubly_linked_list/state.bend, generated by
34	#                tools/generators/dll_state.py)
35	#
36	# Proved for every shadow satisfying the invariant, every value type T
37	# (Data), every handle (foreign, stale by capacity, generation, counter or
38	# vacancy, or live) and every operation:
39	#   new            a good shadow whose model is the specification's empty list
40	#   step           every trace operation refines the specification's step
41	#   trace/run      every trace refines the specification's run, so a new
42	#                  list observes exactly what the specification does
43	#   get, set, remove, next, prev, insert_before, insert_after
44	#                  the direct operation returns the projection of the
45	#                  specification's step (and the new shadow is good)
46	#   push_front, push_back
47	#                  the specification's push
48	#   length, to_list
49	#                  the specification's length and values, list unchanged
50	# Allocating operations (push, insert) assume fewer than 2^29 issued ids
51	# before the operation (TR.room / TR.fits over the specification's state):
52	# the blocks then stay below 2^30 slots, and links never wrap.
53	
54	def new_ok(~T: Data, +tag: U32) -> {ST.real(~T, TR.new_sh(T, tag)) == D.new(~T, tag) : D.DList<T>} & ({ST.model(~T, TR.new_sh(T, tag)) == S.empty(T, tag) : S.DS<T>} & {ST.good(~T, TR.new_sh(T, tag)) == True{} : Bool}):
55	  TR.new_ok(~T, tag)
56	
57	def step_ok(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +hr: {TR.room(T, ST.model(~T, sh), cz) == True{} : Bool}, +op: E.Op<T>) -> OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, sh), op), D.step(~T, ST.real(~T, sh), op)):
58	  TR.step_sh(~T, 1n, {==}, cz, hcz, sh, hg, hr, op)
59	
60	def trace_ok(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +ops: List<&2, E.Op<T>>, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +hf: {TR.fits(T, ops, ST.model(~T, sh), cz) == True{} : Bool}) -> TR.TraceOK(~T, ops, sh):
61	  TR.trace_ok(~T, 1n, {==}, cz, hcz, ops, sh, hg, hf)
62	
63	def run_ok(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +tag: U32, +ops: List<&2, E.Op<T>>, +hf: {TR.fits(T, ops, S.empty(T, tag), cz) == True{} : Bool}) -> {Pair.snd(D.DList<T>, List<&2, E.Obs<T>>, D.run(~T, ops, D.new(~T, tag))) == Pair.snd(S.DS<T>, List<&2, E.Obs<T>>, S.run(T, ops, S.empty(T, tag))) : List<&2, E.Obs<T>>}:
64	  API.obs_eq(~T, ops, TR.new_sh(T, tag), TR.run_new(~T, 1n, {==}, cz, hcz, tag, ops, hf))
65	
66	def get_ok(~T: Data, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +h: E.Handle) -> API.DOK(~T, Result<&2, &2, E.Error, T>, r => D.project_value(~T, r), D.get(~T, ST.real(~T, sh), h), S.step(T, ST.model(~T, sh), E.Get{h})):
67	  API.get_ok(~T, 1n, {==}, sh, hg, h)
68	
69	def set_ok(~T: Data, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +h: E.Handle, +x: T) -> API.DOK(~T, Result<&2, &2, E.Error, Unit>, r => D.project_unit(~T, r), D.set(~T, ST.real(~T, sh), h, x), S.step(T, ST.model(~T, sh), E.Set{h, x})):
70	  API.set_ok(~T, 1n, {==}, sh, hg, h, x)
71	
72	def remove_ok(~T: Data, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +h: E.Handle) -> API.DOK(~T, Result<&2, &2, E.Error, T>, r => D.project_value(~T, r), D.remove(~T, ST.real(~T, sh), h), S.step(T, ST.model(~T, sh), E.Remove{h})):
73	  API.remove_ok(~T, 1n, {==}, sh, hg, h)
74	
75	def next_ok(~T: Data, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +h: E.Handle) -> API.DOK(~T, Result<&2, &2, E.Error, Maybe<&2, E.Handle>>, r => D.project_neighbour(~T, r), D.next(~T, ST.real(~T, sh), h), S.step(T, ST.model(~T, sh), E.Next{h})):
76	  API.next_ok(~T, 1n, {==}, sh, hg, h)
77	
78	def prev_ok(~T: Data, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +h: E.Handle) -> API.DOK(~T, Result<&2, &2, E.Error, Maybe<&2, E.Handle>>, r => D.project_neighbour(~T, r), D.prev(~T, ST.real(~T, sh), h), S.step(T, ST.model(~T, sh), E.Prev{h})):
79	  API.prev_ok(~T, 1n, {==}, sh, hg, h)
80	
81	def insert_before_ok(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +hr: {TR.room(T, ST.model(~T, sh), cz) == True{} : Bool}, +h: E.Handle, +x: T) -> API.DOK(~T, Result<&2, &2, E.Error, E.Handle>, r => D.project_insert(~T, r), D.insert_before(~T, ST.real(~T, sh), h, x), S.step(T, ST.model(~T, sh), E.InsertBefore{h, x})):
82	  API.before_ok(~T, 1n, {==}, cz, hcz, sh, hg, hr, h, x)
83	
84	def insert_after_ok(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +hr: {TR.room(T, ST.model(~T, sh), cz) == True{} : Bool}, +h: E.Handle, +x: T) -> API.DOK(~T, Result<&2, &2, E.Error, E.Handle>, r => D.project_insert(~T, r), D.insert_after(~T, ST.real(~T, sh), h, x), S.step(T, ST.model(~T, sh), E.InsertAfter{h, x})):
85	  API.after_ok(~T, 1n, {==}, cz, hcz, sh, hg, hr, h, x)
86	
87	def push_front_ok(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +hr: {TR.room(T, ST.model(~T, sh), cz) == True{} : Bool}, +x: T) -> OK.POK(~T, E.Handle, S.push_front(T, ST.model(~T, sh), x), D.push_front(~T, ST.real(~T, sh), x)):
88	  API.front_ok(~T, 1n, {==}, cz, hcz, sh, hg, hr, x)
89	
90	def push_back_ok(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +hr: {TR.room(T, ST.model(~T, sh), cz) == True{} : Bool}, +x: T) -> OK.POK(~T, E.Handle, S.push_back(T, ST.model(~T, sh), x), D.push_back(~T, ST.real(~T, sh), x)):
91	  API.back_ok(~T, 1n, {==}, cz, hcz, sh, hg, hr, x)
92	
93	def length_ok(~T: Data, +sh: ST.Sh<T>) -> {D.length(~T, ST.real(~T, sh)) == (ST.real(~T, sh), S.len_of(T, ST.model(~T, sh))) : D.DList<T> & Nat}:
94	  API.length_ok(~T, sh)
95	
96	def to_list_ok(~T: Data, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}) -> {D.to_list(~T, ST.real(~T, sh)) == (ST.real(~T, sh), S.list_of(T, ST.model(~T, sh))) : D.DList<T> & List<&2, T>}:
97	  API.to_list_ok(~T, 1n, {==}, sh, hg)
98	
99	# ==== the contract of doubly_linked_list (stated in spec/containers/doubly_linked_list.bend) ====================
100	
101	# ---- the implementation ----
102	def Impl(~T: Data, sh: ST.Sh<T>, op: E.Op<T>, Post: (S.DS<T> & E.Obs<T>) -> Type) -> Type:
103	  Sigma<&1, &1, ST.Sh<T>, sh2 => Sigma<&1, &1, E.Obs<T>, o => {D.step(~T, ST.real(~T, sh), op) == (ST.real(~T, sh2), o) : D.DList<T> & E.Obs<T>} & ({ST.good(~T, sh2) == True{} : Bool} & Post((ST.model(~T, sh2), o)))>>
104	
105	def impl_of(~T: Data, -sh: ST.Sh<T>, -op: E.Op<T>, -Post: (S.DS<T> & E.Obs<T>) -> Type, k: OK.POK(~T, E.Obs<T>, S.step(T, ST.model(~T, sh), op), D.step(~T, ST.real(~T, sh), op)), pf: Post(S.step(T, ST.model(~T, sh), op))) -> Impl(~T, sh, op, Post):
106	  match k:
107	    case Tuple{sh2, Tuple{o, Tuple{er, Tuple{es, g2}}}}:
108	      (sh2, (o, (er, (g2, L.subst(S.DS<T> & E.Obs<T>, Post, S.step(T, ST.model(~T, sh), op), (ST.model(~T, sh2), o), es, pf)))))
109	
110	# a good list with room for one more element (TR.room, 2^29 ids)
111	def impl(~T: Data, +cz: Nat, +hcz: {cz == 29n : Nat}, +sh: ST.Sh<T>, +hg: {ST.good(~T, sh) == True{} : Bool}, +hr: {TR.room(T, ST.model(~T, sh), cz) == True{} : Bool}, +op: E.Op<T>, -Post: (S.DS<T> & E.Obs<T>) -> Type, pf: Post(S.step(T, ST.model(~T, sh), op))) -> Impl(~T, sh, op, Post):
112	  impl_of(~T, sh, op, Post, step_ok(~T, cz, hcz, sh, hg, hr, op), pf)
113	
114	def fs_up(+x: Nat, +i: Nat, +t: List<&2, Nat>, +hx: {Nat.is_eq(x, i) == False{} : Bool}, r: S.FSplit(i, t)) -> S.FSplit(i, Con{x, t}):
115	  match r:
116	    case Tuple{+a, Tuple{+b, Tuple{e, +hn}}}:
117	      (Con{x, a}, (b, (LL.cons_cong(Nat, x, t, SC.append(Nat, a, Con{i, b}), e), L.subst(Bool, z => {Bool.or(z, SC.memn(i, a)) == False{} : Bool}, False{}, Nat.is_eq(x, i), Equal.sym(Bool, Nat.is_eq(x, i), False{}, hx), hn))))
118	
119	def fs_c(+x: Nat, +i: Nat, +t: List<&2, Nat>, +c: Bool, +hc: {Nat.is_eq(x, i) == c : Bool}, +hm: {Bool.or(c, SC.memn(i, t)) == True{} : Bool}, rec: @h: {SC.memn(i, t) == True{} : Bool} -> S.FSplit(i, t)) -> S.FSplit(i, Con{x, t}):
120	  match c:
121	    case True{}:
122	      (Nil{}, (t, (Equal.cong(Nat, List<&2, Nat>, z => Con{z, t}, x, i, N.eq_from_is_eq(x, i, hc)), {==})))
123	    case False{}:
124	      fs_up(x, i, t, hc, rec(hm))
125	
126	def fsplit(+i: Nat, +xs: List<&2, Nat>, +hm: {SC.memn(i, xs) == True{} : Bool}) -> S.FSplit(i, xs):
127	  match xs:
128	    case Nil{}:
129	      Empty.absurd(S.FSplit(i, Nil{}), L.false_true(hm))
130	    case Con{+x, +t}:
131	      fs_c(x, i, t, Nat.is_eq(x, i), {==}, hm, h => fsplit(i, t, h))
132	
133	# ---- the order operations on a split order ----
134	def ib_app(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>, +n: Nat, +hn: {SC.memn(i, a) == False{} : Bool}) -> {S.ins_before(SC.append(Nat, a, Con{i, b}), i, n) == SC.append(Nat, a, Con{n, Con{i, b}}) : List<&2, Nat>}:
135	  match a:
136	    case Nil{}:
137	      %Equal.sym(Bool, Nat.is_eq(i, i), True{}, N.is_eq_refl(i)) : {S.pick_list(_, Con{n, Con{i, b}}, Con{i, S.ins_before(b, i, n)}) == Con{n, Con{i, b}} : List<&2, Nat>}
138	      {==}
139	    case Con{+x, +t}:
140	      %Equal.sym(Bool, Nat.is_eq(x, i), False{}, NL.or_ff_l(Nat.is_eq(x, i), SC.memn(i, t), hn)) : {S.pick_list(_, Con{n, Con{x, SC.append(Nat, t, Con{i, b})}}, Con{x, S.ins_before(SC.append(Nat, t, Con{i, b}), i, n)}) == Con{x, SC.append(Nat, t, Con{n, Con{i, b}})} : List<&2, Nat>}
141	      LL.cons_cong(Nat, x, S.ins_before(SC.append(Nat, t, Con{i, b}), i, n), SC.append(Nat, t, Con{n, Con{i, b}}), ib_app(t, i, b, n, NL.or_ff_r(Nat.is_eq(x, i), SC.memn(i, t), hn)))
142	
143	def ia_app(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>, +n: Nat, +hn: {SC.memn(i, a) == False{} : Bool}) -> {S.ins_after(SC.append(Nat, a, Con{i, b}), i, n) == SC.append(Nat, a, Con{i, Con{n, b}}) : List<&2, Nat>}:
144	  match a:
145	    case Nil{}:
146	      %Equal.sym(Bool, Nat.is_eq(i, i), True{}, N.is_eq_refl(i)) : {S.pick_list(_, Con{i, Con{n, b}}, Con{i, S.ins_after(b, i, n)}) == Con{i, Con{n, b}} : List<&2, Nat>}
147	      {==}
148	    case Con{+x, +t}:
149	      %Equal.sym(Bool, Nat.is_eq(x, i), False{}, NL.or_ff_l(Nat.is_eq(x, i), SC.memn(i, t), hn)) : {S.pick_list(_, Con{x, Con{n, SC.append(Nat, t, Con{i, b})}}, Con{x, S.ins_after(SC.append(Nat, t, Con{i, b}), i, n)}) == Con{x, SC.append(Nat, t, Con{i, Con{n, b}})} : List<&2, Nat>}
150	      LL.cons_cong(Nat, x, S.ins_after(SC.append(Nat, t, Con{i, b}), i, n), SC.append(Nat, t, Con{i, Con{n, b}}), ia_app(t, i, b, n, NL.or_ff_r(Nat.is_eq(x, i), SC.memn(i, t), hn)))
151	
152	def del_app(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>, +hn: {SC.memn(i, a) == False{} : Bool}) -> {S.delete(SC.append(Nat, a, Con{i, b}), i) == SC.append(Nat, a, b) : List<&2, Nat>}:
153	  match a:
154	    case Nil{}:
155	      %Equal.sym(Bool, Nat.is_eq(i, i), True{}, N.is_eq_refl(i)) : {S.pick_list(_, b, Con{i, S.delete(b, i)}) == b : List<&2, Nat>}
156	      {==}
157	    case Con{+x, +t}:
158	      %Equal.sym(Bool, Nat.is_eq(x, i), False{}, NL.or_ff_l(Nat.is_eq(x, i), SC.memn(i, t), hn)) : {S.pick_list(_, SC.append(Nat, t, Con{i, b}), Con{x, S.delete(SC.append(Nat, t, Con{i, b}), i)}) == Con{x, SC.append(Nat, t, b)} : List<&2, Nat>}
159	      LL.cons_cong(Nat, x, S.delete(SC.append(Nat, t, Con{i, b}), i), SC.append(Nat, t, b), del_app(t, i, b, NL.or_ff_r(Nat.is_eq(x, i), SC.memn(i, t), hn)))
160	
161	def after_app(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>, +hn: {SC.memn(i, a) == False{} : Bool}) -> {S.after(SC.append(Nat, a, Con{i, b}), i) == S.first(b) : Maybe<&2, Nat>}:
162	  match a:
163	    case Nil{}:
164	      %Equal.sym(Bool, Nat.is_eq(i, i), True{}, N.is_eq_refl(i)) : {S.pick_maybe(_, S.first(b), S.after(b, i)) == S.first(b) : Maybe<&2, Nat>}
165	      {==}
166	    case Con{+x, +t}:
167	      %Equal.sym(Bool, Nat.is_eq(x, i), False{}, NL.or_ff_l(Nat.is_eq(x, i), SC.memn(i, t), hn)) : {S.pick_maybe(_, S.first(SC.append(Nat, t, Con{i, b})), S.after(SC.append(Nat, t, Con{i, b}), i)) == S.first(b) : Maybe<&2, Nat>}
168	      after_app(t, i, b, NL.or_ff_r(Nat.is_eq(x, i), SC.memn(i, t), hn))
169	
170	def before_app(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>, +p: Maybe<&2, Nat>, +hn: {SC.memn(i, a) == False{} : Bool}) -> {S.before(SC.append(Nat, a, Con{i, b}), i, p) == S.lastm(a, p) : Maybe<&2, Nat>}:
171	  match a:
172	    case Nil{}:
173	      %Equal.sym(Bool, Nat.is_eq(i, i), True{}, N.is_eq_refl(i)) : {S.pick_maybe(_, p, S.before(b, i, Some{i})) == p : Maybe<&2, Nat>}
174	      {==}
175	    case Con{+x, +t}:
176	      %Equal.sym(Bool, Nat.is_eq(x, i), False{}, NL.or_ff_l(Nat.is_eq(x, i), SC.memn(i, t), hn)) : {S.pick_maybe(_, p, S.before(SC.append(Nat, t, Con{i, b}), i, Some{x})) == S.lastm(t, Some{x}) : Maybe<&2, Nat>}
177	      before_app(t, i, b, Some{x}, NL.or_ff_r(Nat.is_eq(x, i), SC.memn(i, t), hn))
178	
179	# Next is the element at Position + 1
180	def next_position(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>) -> S.Next.next_position(a, i, b):
181	  match a:
182	    case Nil{}:
183	      match b:
184	        case Nil{}:
185	          {==}
186	        case Con{y, r}:
187	          {==}
188	    case Con{+x, +t}:
189	      next_position(t, i, b)
190	
191	# Previous is the element at Position - 1 (none at the first position)
192	def prev_position(+t: List<&2, Nat>, +x: Nat, +i: Nat, +b: List<&2, Nat>, +p: Maybe<&2, Nat>) -> S.Previous.prev_position(t, x, i, b, p):
193	  match t:
194	    case Nil{}:
195	      {==}
196	    case Con{+y, +r}:
197	      prev_position(r, y, i, b, Some{x})
198	
199	# ---- values by id ----
200	def val_update_same(-T: Data, +vs: List<&2, Maybe<&2, T>>, +i: Nat, +m: Maybe<&2, T>, +h: {Nat.is_lt(i, SC.length(Maybe<&2, T>, vs)) == True{} : Bool}) -> {S.val_of(T, SC.update(Maybe<&2, T>, vs, i, m), i) == m : Maybe<&2, T>}:
201	  match vs i:
202	    case Nil{} _:
203	      Empty.absurd({S.val_of(T, SC.update(Maybe<&2, T>, Nil{}, i, m), i) == m : Maybe<&2, T>}, N.lt_zero_absurd(i, h))
204	    case Con{v, t} 0n:
205	      {==}
206	    case Con{v, +t} 1n+ +p:
207	      val_update_same(T, t, p, m, h)
208	
209	def val_update_other(-T: Data, +vs: List<&2, Maybe<&2, T>>, +i: Nat, +j: Nat, +m: Maybe<&2, T>, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> {S.val_of(T, SC.update(Maybe<&2, T>, vs, i, m), j) == S.val_of(T, vs, j) : Maybe<&2, T>}:
210	  match vs i j:
211	    case Nil{} _ _:
212	      {==}
213	    case Con{v, t} 0n 0n:
214	      Empty.absurd({S.val_of(T, SC.update(Maybe<&2, T>, Con{v, t}, 0n, m), 0n) == S.val_of(T, Con{v, t}, 0n) : Maybe<&2, T>}, L.true_false(ne))
215	    case Con{v, t} 0n 1n+q:
216	      {==}
217	    case Con{v, t} 1n+p 0n:
218	      {==}
219	    case Con{v, +t} 1n+ +p 1n+ +q:
220	      val_update_other(T, t, p, q, m, ne)
221	
222	def val_lt(-T: Data, +vs: List<&2, Maybe<&2, T>>, +i: Nat, +v: T, +h: {S.val_of(T, vs, i) == Some{v} : Maybe<&2, T>}) -> {Nat.is_lt(i, SC.length(Maybe<&2, T>, vs)) == True{} : Bool}:
223	  match vs i:
224	    case Nil{} _:
225	      Empty.absurd({Nat.is_lt(i, 0n) == True{} : Bool}, L.none_some(T, v, h))
226	    case Con{w, t} 0n:
227	      {==}
228	    case Con{w, +t} 1n+ +p:
229	      val_lt(T, t, p, v, h)
230	
231	# a valid handle names a live element (Has_Element => Element is defined)
232	def vl_m(-T: Data, +m: Maybe<&2, T>, +same: Bool, +hv: {S.live_gen(T, m, same) == None{} : Maybe<&2, E.Error>}) -> Sigma<&1, &1, T, v => {m == Some{v} : Maybe<&2, T>}>:
233	  match m same:
234	    case None{} _:
235	      Empty.absurd(Sigma<&1, &1, T, v => {None{} == Some{v} : Maybe<&2, T>}>, L.none_some(E.Error, E.StaleHandle{}, Equal.sym(Maybe<&2, E.Error>, Some{E.StaleHandle{}}, None{}, hv)))
236	    case Some{+v} True{}:
237	      (v, {==})
238	    case Some{v} False{}:
239	      Empty.absurd(Sigma<&1, &1, T, w => {Some{v} == Some{w} : Maybe<&2, T>}>, L.none_some(E.Error, E.StaleHandle{}, Equal.sym(Maybe<&2, E.Error>, Some{E.StaleHandle{}}, None{}, hv)))
240	
241	def vl_own(-T: Data, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +i: Nat, +g: U32, +mine: Bool, +hv: {S.valid_own(T, vals, gens, i, g, mine) == None{} : Maybe<&2, E.Error>}) -> Sigma<&1, &1, T, v => {S.val_of(T, vals, i) == Some{v} : Maybe<&2, T>}>:
242	  match mine:
243	    case False{}:
244	      Empty.absurd(Sigma<&1, &1, T, v => {S.val_of(T, vals, i) == Some{v} : Maybe<&2, T>}>, L.none_some(E.Error, E.ForeignHandle{}, Equal.sym(Maybe<&2, E.Error>, Some{E.ForeignHandle{}}, None{}, hv)))
245	    case True{}:
246	      vl_m(T, S.val_of(T, vals, i), U32.is_eq(S.gen_of(gens, i), g), hv)
247	
248	def valid_live(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> S.Has_Element.valid_live(T, tag, order, vals, gens, free, h, hv):
249	  match h:
250	    case E.H{+owner, +id, +g}:
251	      vl_own(T, vals, gens, U32.to_nat(id), g, U32.is_eq(owner, tag), hv)
252	
253	# ---- the step on a valid handle is the live operation ----
254	def live(-T: Data, +s: S.DS<T>, +op: E.Op<T>, +h: E.Handle, +hv: {S.validate(T, s, h) == None{} : Maybe<&2, E.Error>}) -> {S.checked(T, s, op, h, S.validate(T, s, h)) == S.live_op(T, s, op, S.handle_id(h)) : S.DS<T> & E.Obs<T>}:
255	  %Equal.sym(Maybe<&2, E.Error>, S.validate(T, s, h), None{}, hv) : {S.checked(T, s, op, h, _) == S.live_op(T, s, op, S.handle_id(h)) : S.DS<T> & E.Obs<T>}
256	  {==}
257	
258	# ---- Length, iteration, Empty_List ----
259	def length_result(-T: Data, +s: S.DS<T>) -> S.Length.length_result(T, s):
260	  {==}
261	
262	def length_frame(-T: Data, +s: S.DS<T>) -> S.Length.length_frame(T, s):
263	  {==}
264	
265	def to_list_model(-T: Data, +s: S.DS<T>) -> S.Iteration.to_list_model(T, s):
266	  {==}
267	
268	def to_list_frame(-T: Data, +s: S.DS<T>) -> S.Iteration.to_list_frame(T, s):
269	  {==}
270	
271	def new_empty(-T: Data, +tag: U32) -> S.Empty_List.new_empty(T, tag):
272	  {==}
273	
274	# ---- Element: the value of the handle's element; nothing changes ----
275	def get_step(-T: Data, +s: S.DS<T>, +h: E.Handle, +hv: {S.validate(T, s, h) == None{} : Maybe<&2, E.Error>}) -> {S.step(T, s, E.Get{h}) == S.get_live(T, s, S.handle_id(h)) : S.DS<T> & E.Obs<T>}:
276	  live(T, s, E.Get{h}, h, hv)
277	
278	def get_frame(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> S.Element.get_frame(T, tag, order, vals, gens, free, h, hv):
279	  %Equal.sym(S.DS<T> & E.Obs<T>, S.step(T, S.DS{tag, order, vals, gens, free}, E.Get{h}), S.get_live(T, S.DS{tag, order, vals, gens, free}, S.handle_id(h)), get_step(T, S.DS{tag, order, vals, gens, free}, h, hv)) : {Pair.fst(S.DS<T>, E.Obs<T>, _) == S.DS{tag, order, vals, gens, free} : S.DS<T>}
280	  {==}
281	
282	def get_element(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> S.Element.get_element(T, tag, order, vals, gens, free, h, hv, v, hval):
283	  %Equal.sym(S.DS<T> & E.Obs<T>, S.step(T, S.DS{tag, order, vals, gens, free}, E.Get{h}), S.get_live(T, S.DS{tag, order, vals, gens, free}, S.handle_id(h)), get_step(T, S.DS{tag, order, vals, gens, free}, h, hv)) : {Pair.snd(S.DS<T>, E.Obs<T>, _) == E.OVal{Done{v}} : E.Obs<T>}
284	  %Equal.sym(Maybe<&2, T>, S.val_of(T, vals, S.handle_id(h)), Some{v}, hval) : {E.OVal{S.maybe_done(T, E.StaleHandle{}, _)} == E.OVal{Done{v}} : E.Obs<T>}
285	  {==}
286	
287	# ---- Replace_Element: positions and generations kept, the handle's value is x, others kept ----
288	def set_step(-T: Data, +s: S.DS<T>, +h: E.Handle, +x: T, +hv: {S.validate(T, s, h) == None{} : Maybe<&2, E.Error>}) -> {S.step(T, s, E.Set{h, x}) == S.set_live(T, s, S.handle_id(h), x) : S.DS<T> & E.Obs<T>}:
289	  live(T, s, E.Set{h, x}, h, hv)
290	
291	def set_is(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> {S.nx(T, S.DS{tag, order, vals, gens, free}, E.Set{h, x}) == S.DS{tag, order, SC.update(Maybe<&2, T>, vals, S.handle_id(h), Some{x}), gens, free} : S.DS<T>}:
292	  %Equal.sym(S.DS<T> & E.Obs<T>, S.step(T, S.DS{tag, order, vals, gens, free}, E.Set{h, x}), S.set_live(T, S.DS{tag, order, vals, gens, free}, S.handle_id(h), x), set_step(T, S.DS{tag, order, vals, gens, free}, h, x, hv)) : {Pair.fst(S.DS<T>, E.Obs<T>, _) == S.DS{tag, order, SC.update(Maybe<&2, T>, vals, S.handle_id(h), Some{x}), gens, free} : S.DS<T>}
293	  {==}
294	
295	def set_positions(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> S.Replace_Element.set_positions(T, tag, order, vals, gens, free, h, x, hv):
296	  %Equal.sym(S.DS<T>, S.nx(T, S.DS{tag, order, vals, gens, free}, E.Set{h, x}), S.DS{tag, order, SC.update(Maybe<&2, T>, vals, S.handle_id(h), Some{x}), gens, free}, set_is(T, tag, order, vals, gens, free, h, x, hv)) : {S.ord(T, _) == order : List<&2, Nat>}
297	  {==}
298	
299	def set_gens(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> S.Replace_Element.set_gens(T, tag, order, vals, gens, free, h, x, hv):
300	  %Equal.sym(S.DS<T>, S.nx(T, S.DS{tag, order, vals, gens, free}, E.Set{h, x}), S.DS{tag, order, SC.update(Maybe<&2, T>, vals, S.handle_id(h), Some{x}), gens, free}, set_is(T, tag, order, vals, gens, free, h, x, hv)) : {S.gns(T, _) == gens : List<&2, U32>}
301	  {==}
302	
303	def set_element(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> S.Replace_Element.set_element(T, tag, order, vals, gens, free, h, x, hv, v, hval):
304	  %Equal.sym(S.DS<T>, S.nx(T, S.DS{tag, order, vals, gens, free}, E.Set{h, x}), S.DS{tag, order, SC.update(Maybe<&2, T>, vals, S.handle_id(h), Some{x}), gens, free}, set_is(T, tag, order, vals, gens, free, h, x, hv)) : {S.val_of(T, S.vls(T, _), S.handle_id(h)) == Some{x} : Maybe<&2, T>}
305	  val_update_same(T, vals, S.handle_id(h), Some{x}, val_lt(T, vals, S.handle_id(h), v, hval))
306	
307	def set_others(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, order, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +j: Nat, +ne: {Nat.is_eq(S.handle_id(h), j) == False{} : Bool}) -> S.Replace_Element.set_others(T, tag, order, vals, gens, free, h, x, hv, j, ne):
308	  %Equal.sym(S.DS<T>, S.nx(T, S.DS{tag, order, vals, gens, free}, E.Set{h, x}), S.DS{tag, order, SC.update(Maybe<&2, T>, vals, S.handle_id(h), Some{x}), gens, free}, set_is(T, tag, order, vals, gens, free, h, x, hv)) : {S.val_of(T, S.vls(T, _), j) == S.val_of(T, vals, j) : Maybe<&2, T>}
309	  val_update_other(T, vals, S.handle_id(h), j, Some{x}, ne)
310	
311	# ---- inserting: the order gains the new id n at its place ----
312	def alloc_order(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T, +pos: S.Pos) -> {S.ord(T, Pair.fst(S.DS<T>, E.Handle, S.inserted(T, S.alloc(T, S.DS{tag, order, vals, gens, free}), x, pos))) == S.place_order(pos, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))) : List<&2, Nat>}:
313	  match free:
314	    case Nil{}:
315	      {==}
316	    case Con{+i, +rest}:
317	      {==}
318	
319	def push_front_order(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> {S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushFront{x})) == Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free})), order} : List<&2, Nat>}:
320	  match free:
321	    case Nil{}:
322	      {==}
323	    case Con{+i, +rest}:
324	      {==}
325	
326	def push_front_positions(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> S.Prepend.push_front_positions(T, tag, order, vals, gens, free, x):
327	  L.subst(List<&2, Nat>, z => V.RangeShifted(Nat, order, z, 0n, SC.length(Nat, order), 1n), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free})), order}, S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushFront{x})), Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushFront{x})), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free})), order}, push_front_order(T, tag, order, vals, gens, free, x)), VL.cons_shifted(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))))
328	
329	def push_front_first(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> S.Prepend.push_front_first(T, tag, order, vals, gens, free, x):
330	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushFront{x})), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free})), order}, push_front_order(T, tag, order, vals, gens, free, x)) : {SC.nth(Nat, _, 0n) == Some{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))} : Maybe<&2, Nat>}
331	  {==}
332	
333	def push_front_length(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> S.Prepend.push_front_length(T, tag, order, vals, gens, free, x):
334	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushFront{x})), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free})), order}, push_front_order(T, tag, order, vals, gens, free, x)) : {SC.length(Nat, _) == 1n+SC.length(Nat, order) : Nat}
335	  {==}
336	
337	def push_back_order(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> {S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushBack{x})) == SC.snoc(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))) : List<&2, Nat>}:
338	  match free:
339	    case Nil{}:
340	      {==}
341	    case Con{+i, +rest}:
342	      {==}
343	
344	def push_back_positions(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> S.Append.push_back_positions(T, tag, order, vals, gens, free, x):
345	  L.subst(List<&2, Nat>, z => V.EqualPrefix(Nat, order, z), SC.snoc(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))), S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushBack{x})), Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushBack{x})), SC.snoc(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))), push_back_order(T, tag, order, vals, gens, free, x)), VL.snoc_prefix(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))))
346	
347	def push_back_last(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> S.Append.push_back_last(T, tag, order, vals, gens, free, x):
348	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushBack{x})), SC.snoc(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))), push_back_order(T, tag, order, vals, gens, free, x)) : {SC.nth(Nat, _, SC.length(Nat, order)) == Some{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))} : Maybe<&2, Nat>}
349	  VL.snoc_last(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free})))
350	
351	def push_back_length(-T: Data, +tag: U32, +order: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +x: T) -> S.Append.push_back_length(T, tag, order, vals, gens, free, x):
352	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, order, vals, gens, free}, E.PushBack{x})), SC.snoc(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free}))), push_back_order(T, tag, order, vals, gens, free, x)) : {SC.length(Nat, _) == 1n+SC.length(Nat, order) : Nat}
353	  VL.snoc_length(Nat, order, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, order, vals, gens, free})))
354	
355	# ---- Insert (Before) ----
356	def ib_free(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> {S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x}, S.handle_id(h)))) == SC.append(Nat, a, Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), Con{S.handle_id(h), b}}) : List<&2, Nat>}:
357	  match free:
358	    case Nil{}:
359	      ib_app(a, S.handle_id(h), b, SC.length(Maybe<&2, T>, vals), hn)
360	    case Con{+i, +rest}:
361	      ib_app(a, S.handle_id(h), b, i, hn)
362	
363	def insert_before_order(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> {S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})) == SC.append(Nat, a, Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), Con{S.handle_id(h), b}}) : List<&2, Nat>}:
364	  %Equal.sym(S.DS<T> & E.Obs<T>, S.checked(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x}, h, S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h)), S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x}, S.handle_id(h)), live(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x}, h, hv)) : {S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, _)) == SC.append(Nat, a, Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), Con{S.handle_id(h), b}}) : List<&2, Nat>}
365	  ib_free(T, tag, a, b, vals, gens, free, h, x, hn)
366	
367	# positions before the new element are unchanged
368	def insert_before_equal(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_before_equal(T, tag, a, b, vals, gens, free, h, x, hv, hn):
369	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})), SC.append(Nat, a, Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), Con{S.handle_id(h), b}}), insert_before_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : V.RangeEqual(Nat, SC.append(Nat, a, Con{S.handle_id(h), b}), _, 0n, SC.length(Nat, a))
370	  VL.mid_equal(Nat, a, Con{S.handle_id(h), b}, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
371	
372	# the new element is at Before's old position
373	def insert_before_at(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_before_at(T, tag, a, b, vals, gens, free, h, x, hv, hn):
374	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})), SC.append(Nat, a, Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), Con{S.handle_id(h), b}}), insert_before_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : {SC.nth(Nat, _, SC.length(Nat, a)) == Some{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}))} : Maybe<&2, Nat>}
375	  VL.mid_at(Nat, a, Con{S.handle_id(h), b}, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
376	
377	# Before and the positions after it move up by one
378	def insert_before_shifted(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_before_shifted(T, tag, a, b, vals, gens, free, h, x, hv, hn):
379	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})), SC.append(Nat, a, Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), Con{S.handle_id(h), b}}), insert_before_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : V.RangeShifted(Nat, SC.append(Nat, a, Con{S.handle_id(h), b}), _, SC.length(Nat, a), SC.length(Nat, SC.append(Nat, a, Con{S.handle_id(h), b})), 1n)
380	  VL.mid_shifted(Nat, a, Con{S.handle_id(h), b}, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
381	
382	def insert_before_length(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_before_length(T, tag, a, b, vals, gens, free, h, x, hv, hn):
383	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertBefore{h, x})), SC.append(Nat, a, Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), Con{S.handle_id(h), b}}), insert_before_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : {SC.length(Nat, _) == 1n+SC.length(Nat, SC.append(Nat, a, Con{S.handle_id(h), b})) : Nat}
384	  VL.mid_length(Nat, a, Con{S.handle_id(h), b}, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
385	
386	# ---- Insert after (SPARK: Insert before Next (Position)) ----
387	def ia_free(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> {S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x}, S.handle_id(h)))) == SC.append(Nat, a, Con{S.handle_id(h), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}}) : List<&2, Nat>}:
388	  match free:
389	    case Nil{}:
390	      ia_app(a, S.handle_id(h), b, SC.length(Maybe<&2, T>, vals), hn)
391	    case Con{+i, +rest}:
392	      ia_app(a, S.handle_id(h), b, i, hn)
393	
394	def insert_after_order(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> {S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})) == SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}) : List<&2, Nat>}:
395	  %Equal.sym(S.DS<T> & E.Obs<T>, S.checked(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x}, h, S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h)), S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x}, S.handle_id(h)), live(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x}, h, hv)) : {S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, _)) == SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}) : List<&2, Nat>}
396	  %Equal.sym(List<&2, Nat>, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), SC.append(Nat, a, Con{S.handle_id(h), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}}), LL.snoc_append_cons(Nat, a, S.handle_id(h), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b})) : {S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x}, S.handle_id(h)))) == _ : List<&2, Nat>}
397	  ia_free(T, tag, a, b, vals, gens, free, h, x, hn)
398	
399	# the old order split after Position
400	def split_after(+a: List<&2, Nat>, +i: Nat, +b: List<&2, Nat>) -> {SC.append(Nat, a, Con{i, b}) == SC.append(Nat, SC.snoc(Nat, a, i), b) : List<&2, Nat>}:
401	  Equal.sym(List<&2, Nat>, SC.append(Nat, SC.snoc(Nat, a, i), b), SC.append(Nat, a, Con{i, b}), LL.snoc_append_cons(Nat, a, i, b))
402	
403	# Position and the positions before it are unchanged
404	def insert_after_equal(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_after_equal(T, tag, a, b, vals, gens, free, h, x, hv, hn):
405	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), insert_after_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : V.RangeEqual(Nat, SC.append(Nat, a, Con{S.handle_id(h), b}), _, 0n, 1n+SC.length(Nat, a))
406	  %Equal.sym(List<&2, Nat>, SC.append(Nat, a, Con{S.handle_id(h), b}), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), b), split_after(a, S.handle_id(h), b)) : V.RangeEqual(Nat, _, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), 0n, 1n+SC.length(Nat, a))
407	  %LL.length_snoc(Nat, a, S.handle_id(h)) : V.RangeEqual(Nat, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), b), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), 0n, _)
408	  VL.mid_equal(Nat, SC.snoc(Nat, a, S.handle_id(h)), b, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
409	
410	# the new element is right after Position
411	def insert_after_at(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_after_at(T, tag, a, b, vals, gens, free, h, x, hv, hn):
412	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), insert_after_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : {SC.nth(Nat, _, 1n+SC.length(Nat, a)) == Some{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}))} : Maybe<&2, Nat>}
413	  %LL.length_snoc(Nat, a, S.handle_id(h)) : {SC.nth(Nat, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), _) == Some{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}))} : Maybe<&2, Nat>}
414	  VL.mid_at(Nat, SC.snoc(Nat, a, S.handle_id(h)), b, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
415	
416	# the positions after Position move up by one
417	def insert_after_shifted(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_after_shifted(T, tag, a, b, vals, gens, free, h, x, hv, hn):
418	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), insert_after_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : V.RangeShifted(Nat, SC.append(Nat, a, Con{S.handle_id(h), b}), _, 1n+SC.length(Nat, a), SC.length(Nat, SC.append(Nat, a, Con{S.handle_id(h), b})), 1n)
419	  %Equal.sym(List<&2, Nat>, SC.append(Nat, a, Con{S.handle_id(h), b}), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), b), split_after(a, S.handle_id(h), b)) : V.RangeShifted(Nat, _, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), 1n+SC.length(Nat, a), SC.length(Nat, _), 1n)
420	  %LL.length_snoc(Nat, a, S.handle_id(h)) : V.RangeShifted(Nat, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), b), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), _, SC.length(Nat, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), b)), 1n)
421	  VL.mid_shifted(Nat, SC.snoc(Nat, a, S.handle_id(h)), b, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
422	
423	def insert_after_length(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +x: T, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Insert.insert_after_length(T, tag, a, b, vals, gens, free, h, x, hv, hn):
424	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.InsertAfter{h, x})), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b}), insert_after_order(T, tag, a, b, vals, gens, free, h, x, hv, hn)) : {SC.length(Nat, _) == 1n+SC.length(Nat, SC.append(Nat, a, Con{S.handle_id(h), b})) : Nat}
425	  %Equal.sym(List<&2, Nat>, SC.append(Nat, a, Con{S.handle_id(h), b}), SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), b), split_after(a, S.handle_id(h), b)) : {SC.length(Nat, SC.append(Nat, SC.snoc(Nat, a, S.handle_id(h)), Con{Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})), b})) == 1n+SC.length(Nat, _) : Nat}
426	  VL.mid_length(Nat, SC.snoc(Nat, a, S.handle_id(h)), b, Pair.snd(S.DS<T>, Nat, S.alloc(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free})))
427	
428	# ---- Delete ----
429	def remove_step(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> {S.step(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h}) == S.removed(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295))) : S.DS<T> & E.Obs<T>}:
430	  %Equal.sym(S.DS<T> & E.Obs<T>, S.checked(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h}, h, S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h)), S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h}, S.handle_id(h)), live(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h}, h, hv)) : {_ == S.removed(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295))) : S.DS<T> & E.Obs<T>}
431	  %Equal.sym(Maybe<&2, T>, S.val_of(T, vals, S.handle_id(h)), Some{v}, hval) : {S.remove_m(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free, S.handle_id(h), _) == S.removed(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295))) : S.DS<T> & E.Obs<T>}
432	  {==}
433	
434	def rm_ord(-T: Data, +tag: U32, +o: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +i: Nat, +v: T, r: List<&2, U32> & List<&2, Nat>) -> {S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, S.removed(T, tag, o, vals, i, v, r))) == S.delete(o, i) : List<&2, Nat>}:
435	  match r:
436	    case Tuple{g, f}:
437	      {==}
438	
439	def rm_obs(-T: Data, +tag: U32, +o: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +i: Nat, +v: T, r: List<&2, U32> & List<&2, Nat>) -> {Pair.snd(S.DS<T>, E.Obs<T>, S.removed(T, tag, o, vals, i, v, r)) == E.OVal{Done{v}} : E.Obs<T>}:
440	  match r:
441	    case Tuple{g, f}:
442	      {==}
443	
444	def remove_order(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> {S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h})) == SC.append(Nat, a, b) : List<&2, Nat>}:
445	  %Equal.sym(S.DS<T> & E.Obs<T>, S.step(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h}), S.removed(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295))), remove_step(T, tag, a, b, vals, gens, free, h, hv, v, hval)) : {S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, _)) == SC.append(Nat, a, b) : List<&2, Nat>}
446	  %Equal.sym(List<&2, Nat>, S.ord(T, Pair.fst(S.DS<T>, E.Obs<T>, S.removed(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295))))), S.delete(SC.append(Nat, a, Con{S.handle_id(h), b}), S.handle_id(h)), rm_ord(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295)))) : {_ == SC.append(Nat, a, b) : List<&2, Nat>}
447	  del_app(a, S.handle_id(h), b, hn)
448	
449	# the returned element is the deleted one
450	def remove_result(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> S.Delete.remove_result(T, tag, a, b, vals, gens, free, h, hv, v, hval):
451	  %Equal.sym(S.DS<T> & E.Obs<T>, S.step(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h}), S.removed(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295))), remove_step(T, tag, a, b, vals, gens, free, h, hv, v, hval)) : {Pair.snd(S.DS<T>, E.Obs<T>, _) == E.OVal{Done{v}} : E.Obs<T>}
452	  rm_obs(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295)))
453	
454	# positions before Position are unchanged
455	def remove_equal(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> S.Delete.remove_equal(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval):
456	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h})), SC.append(Nat, a, b), remove_order(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval)) : V.RangeEqual(Nat, _, SC.append(Nat, a, Con{S.handle_id(h), b}), 0n, SC.length(Nat, a))
457	  VL.mid_equal(Nat, a, b, S.handle_id(h))
458	
459	# the positions after it move down by one
460	def remove_shifted(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> S.Delete.remove_shifted(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval):
461	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h})), SC.append(Nat, a, b), remove_order(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval)) : V.RangeShifted(Nat, _, SC.append(Nat, a, Con{S.handle_id(h), b}), SC.length(Nat, a), SC.length(Nat, _), 1n)
462	  VL.mid_shifted(Nat, a, b, S.handle_id(h))
463	
464	def remove_length(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> S.Delete.remove_length(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval):
465	  %Equal.sym(List<&2, Nat>, S.ord(T, S.nx(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h})), SC.append(Nat, a, b), remove_order(T, tag, a, b, vals, gens, free, h, hv, hn, v, hval)) : {SC.length(Nat, SC.append(Nat, a, Con{S.handle_id(h), b})) == 1n+SC.length(Nat, _) : Nat}
466	  VL.mid_length(Nat, a, b, S.handle_id(h))
467	
468	# the handle no longer designates an element (SPARK: Position = No_Element)
469	def stale_own(-T: Data, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +i: Nat, +g: U32, +mine: Bool, +hl: {Nat.is_lt(i, SC.length(Maybe<&2, T>, vals)) == True{} : Bool}) -> {S.has_of(S.valid_own(T, SC.update(Maybe<&2, T>, vals, i, None{}), gens, i, g, mine)) == False{} : Bool}:
470	  match mine:
471	    case False{}:
472	      {==}
473	    case True{}:
474	      %Equal.sym(Maybe<&2, T>, S.val_of(T, SC.update(Maybe<&2, T>, vals, i, None{}), i), None{}, val_update_same(T, vals, i, None{}, hl)) : {S.has_of(S.live_gen(T, _, U32.is_eq(S.gen_of(gens, i), g))) == False{} : Bool}
475	      {==}
476	
477	def stale_h(-T: Data, +h: E.Handle, +tag: U32, +o: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +g2: List<&2, U32>, +f2: List<&2, Nat>, +hl: {Nat.is_lt(S.handle_id(h), SC.length(Maybe<&2, T>, vals)) == True{} : Bool}) -> {S.has_element(T, S.DS{tag, S.delete(o, S.handle_id(h)), SC.update(Maybe<&2, T>, vals, S.handle_id(h), None{}), g2, f2}, h) == False{} : Bool}:
478	  match h:
479	    case E.H{+owner, +id, +g}:
480	      stale_own(T, vals, g2, U32.to_nat(id), g, U32.is_eq(owner, tag), hl)
481	
482	def stale_r(-T: Data, +tag: U32, +o: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +h: E.Handle, +v: T, +hl: {Nat.is_lt(S.handle_id(h), SC.length(Maybe<&2, T>, vals)) == True{} : Bool}, r: List<&2, U32> & List<&2, Nat>) -> {S.has_element(T, Pair.fst(S.DS<T>, E.Obs<T>, S.removed(T, tag, o, vals, S.handle_id(h), v, r)), h) == False{} : Bool}:
483	  match r:
484	    case Tuple{+g2, +f2}:
485	      stale_h(T, h, tag, o, vals, g2, f2, hl)
486	
487	def remove_stale(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +v: T, +hval: {S.val_of(T, vals, S.handle_id(h)) == Some{v} : Maybe<&2, T>}) -> S.Delete.remove_stale(T, tag, a, b, vals, gens, free, h, hv, v, hval):
488	  %Equal.sym(S.DS<T> & E.Obs<T>, S.step(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Remove{h}), S.removed(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, S.handle_id(h), v, S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295))), remove_step(T, tag, a, b, vals, gens, free, h, hv, v, hval)) : {S.has_element(T, Pair.fst(S.DS<T>, E.Obs<T>, _), h) == False{} : Bool}
489	  stale_r(T, tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, h, v, val_lt(T, vals, S.handle_id(h), v, hval), S.retire(gens, S.handle_id(h), free, S.gen_of(gens, S.handle_id(h)), U32.is_eq(S.gen_of(gens, S.handle_id(h)), 4294967295)))
490	
491	# ---- Next / Previous ----
492	def next_result(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Next.next_result(T, tag, a, b, vals, gens, free, h, hv, hn):
493	  %Equal.sym(S.DS<T> & E.Obs<T>, S.checked(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Next{h}, h, S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h)), S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Next{h}, S.handle_id(h)), live(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Next{h}, h, hv)) : {Pair.snd(S.DS<T>, E.Obs<T>, _) == E.ONbr{Done{S.nbr(tag, gens, S.first(b))}} : E.Obs<T>}
494	  %Equal.sym(Maybe<&2, Nat>, S.after(SC.append(Nat, a, Con{S.handle_id(h), b}), S.handle_id(h)), S.first(b), after_app(a, S.handle_id(h), b, hn)) : {E.ONbr{Done{S.nbr(tag, gens, _)}} == E.ONbr{Done{S.nbr(tag, gens, S.first(b))}} : E.Obs<T>}
495	  {==}
496	
497	def next_frame(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> S.Next.next_frame(T, tag, a, b, vals, gens, free, h, hv):
498	  %Equal.sym(S.DS<T> & E.Obs<T>, S.checked(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Next{h}, h, S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h)), S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Next{h}, S.handle_id(h)), live(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Next{h}, h, hv)) : {Pair.fst(S.DS<T>, E.Obs<T>, _) == S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free} : S.DS<T>}
499	  {==}
500	
501	def prev_result(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}, +hn: {SC.memn(S.handle_id(h), a) == False{} : Bool}) -> S.Previous.prev_result(T, tag, a, b, vals, gens, free, h, hv, hn):
502	  %Equal.sym(S.DS<T> & E.Obs<T>, S.checked(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Prev{h}, h, S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h)), S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Prev{h}, S.handle_id(h)), live(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Prev{h}, h, hv)) : {Pair.snd(S.DS<T>, E.Obs<T>, _) == E.ONbr{Done{S.nbr(tag, gens, S.lastm(a, None{}))}} : E.Obs<T>}
503	  %Equal.sym(Maybe<&2, Nat>, S.before(SC.append(Nat, a, Con{S.handle_id(h), b}), S.handle_id(h), None{}), S.lastm(a, None{}), before_app(a, S.handle_id(h), b, None{}, hn)) : {E.ONbr{Done{S.nbr(tag, gens, _)}} == E.ONbr{Done{S.nbr(tag, gens, S.lastm(a, None{}))}} : E.Obs<T>}
504	  {==}
505	
506	# the first element has no previous one
507	def prev_first(-T: Data, +tag: U32, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, Con{S.handle_id(h), b}, vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> S.Previous.prev_first(T, tag, b, vals, gens, free, h, hv):
508	  prev_result(T, tag, Nil{}, b, vals, gens, free, h, hv, {==})
509	
510	def prev_frame(-T: Data, +tag: U32, +a: List<&2, Nat>, +b: List<&2, Nat>, +vals: List<&2, Maybe<&2, T>>, +gens: List<&2, U32>, +free: List<&2, Nat>, +h: E.Handle, +hv: {S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h) == None{} : Maybe<&2, E.Error>}) -> S.Previous.prev_frame(T, tag, a, b, vals, gens, free, h, hv):
511	  %Equal.sym(S.DS<T> & E.Obs<T>, S.checked(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Prev{h}, h, S.validate(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, h)), S.live_op(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Prev{h}, S.handle_id(h)), live(T, S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free}, E.Prev{h}, h, hv)) : {Pair.fst(S.DS<T>, E.Obs<T>, _) == S.DS{tag, SC.append(Nat, a, Con{S.handle_id(h), b}), vals, gens, free} : S.DS<T>}
512	  {==}