1	import Base
2	import ../../lib/array.bend as A
3	import ../../../spec/lib/common.bend as SC
4	import ../../../spec/containers/bitset.bend as S
5	import ../../../src/containers/bitset.bend as B
6	import ../../../src/containers/types/bitset.bend as E
7	import ./lists.bend as BL
8	import ./word.bend as W
9	import ./index.bend as IX
10	import ./depth.bend as DP
11	import ./arr.bend as AR
12	import ./state.bend as ST
13	import ./steps.bend as BS
14	import ./trace.bend as BT
15	import ../../lib/logic.bend as L
16	import ../../lib/nat.bend as N
17	import ../../lib/list.bend as LL
18	
19	# Packed bitset: public proof entry point.
20	#   abstraction  ST.abs(n, t)  (first n bits of the stored U32 words)
21	#   invariant    ST.rep(n, d, t)  (the depth is the one `depth_for` picks, the
22	#                word array is a perfect tree of that depth, n <= stored bits,
23	#                every stored bit at a position >= n is zero)
24	#   shadow       ST.Sh / ST.real / ST.good / ST.model  (Base.Array is linear,
25	#                so every law is about the array built from a Data mirror
26	#                tree, exactly as in proofs/dynamic_array)
27	#   word facts   W.*     (U32 and/or/xor/not/shifts from Base's Word defs)
28	#   index facts  IX.*    (i / 32 and i % 32 peel 32 bits at a time)
29	#   array facts  AR.*    (Base.Array get/set against the slot list)
30	#   operations   BS.step_ok (every op; IndexOutOfRange / LengthMismatch keep
31	#                the state)
32	#   traces       trace_new (arbitrary op lists from B.new(n))
33	#
34	# `capacity(n)` is the documented capacity condition of the packed
35	# representation: 2^31 words = 2^36 bits (see src/bitset.bend). It is a
36	# premise only of the laws about `new`; every other law holds at every state
37	# satisfying the invariant, and the invariant itself implies it
38	# (ST.rep_fits).
39	
40	def capacity(+n: Nat) -> Type:
41	  {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}
42	
43	def new_abs(+n: Nat, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> {ST.model(BT.initial(n)) == S.new(n) : List<&2, Bool>}:
44	  BT.new_model(n, h)
45	
46	def new_inv(+n: Nat, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> {ST.good(BT.initial(n)) == True{} : Bool}:
47	  BT.new_good(n, h)
48	
49	def new_real(+n: Nat) -> {B.new(n) == ST.real(BT.initial(n)) : B.Bitset}:
50	  BT.new_real(n)
51	
52	def from_bools(+ys: List<&2, Bool>, +hf: {Nat.is_le(B.bool_count(ys), Nat.mul(SC.pow2(B.depth_for(B.bool_count(ys))), 32n)) == True{} : Bool}) -> BS.FromOK(ys):
53	  BS.from_ok(ys, hf)
54	
55	def step_ok(sh: ST.Sh, op: E.Op, +g: {ST.good(sh) == True{} : Bool}) -> BS.StepOK(sh, op):
56	  BS.step_ok(sh, op, g)
57	
58	# A runtime bitset determines its shadow, so "the operation lands on the array
59	# of THIS shadow, whose model is the spec's" pins the abstract state: the laws
60	# above cannot be satisfied by naming a different shadow.
61	def shadow_unique(+a: ST.Sh, +b: ST.Sh, +e: {ST.real(a) == ST.real(b) : B.Bitset}) -> {a == b : ST.Sh}:
62	  ST.real_inj(a, b, e)
63	
64	# Arbitrary finite operation traces from the real constructor.
65	def trace_new(+n: Nat, +ops: List<&2, E.Op>, +h: {Nat.is_le(n, Nat.mul(SC.pow2(B.depth_for(n)), 32n)) == True{} : Bool}) -> BT.TraceOK(ops, BT.initial(n)):
66	  BT.trace_from(ops, BT.initial(n), BT.new_good(n, h))
67	
68	# ==== the contract of bitset (stated in spec/containers/bitset.bend) ====================
69	
70	# ---- the implementation ----
71	def Impl(sh: ST.Sh, op: E.Op, Post: (List<&2, Bool> & E.Obs) -> Type) -> Type:
72	  Sigma<&1, &1, ST.Sh, sh2 => Sigma<&1, &1, E.Obs, o => {B.step(ST.real(sh), op) == (ST.real(sh2), o) : B.Bitset & E.Obs} & ({ST.good(sh2) == True{} : Bool} & Post((ST.model(sh2), o)))>>
73	
74	def impl_of(-sh: ST.Sh, -op: E.Op, -Post: (List<&2, Bool> & E.Obs) -> Type, k: BS.StepOK(sh, op), pf: Post(S.step(ST.model(sh), op))) -> Impl(sh, op, Post):
75	  match k:
76	    case Tuple{sh2, Tuple{o, Tuple{e1, Tuple{g2, e2}}}}:
77	      (sh2, (o, (e1, (g2, L.subst(List<&2, Bool> & E.Obs, Post, S.step(ST.model(sh), op), (ST.model(sh2), o), Equal.sym(List<&2, Bool> & E.Obs, (ST.model(sh2), o), S.step(ST.model(sh), op), e2), pf)))))
78	
79	def impl(sh: ST.Sh, op: E.Op, +g: {ST.good(sh) == True{} : Bool}, -Post: (List<&2, Bool> & E.Obs) -> Type, pf: Post(S.step(ST.model(sh), op))) -> Impl(sh, op, Post):
80	  impl_of(sh, op, Post, step_ok(sh, op, g), pf)
81	
82	# ---- arithmetic and Boolean facts ----
83	def succ_ne_zero(+a: Nat, +e: {1n+a == 0n : Nat}) -> Empty:
84	  L.false_true(Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), 1n+a, 0n, e))
85	
86	def zero_ne_succ(+a: Nat, +e: {0n == 1n+a : Nat}) -> Empty:
87	  L.true_false(Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), 0n, 1n+a, e))
88	
89	def succ_pick(+b: Bool, +x: Nat, +y: Nat) -> {1n+Bool.pick(Nat, b, x, y) == Bool.pick(Nat, b, 1n+x, 1n+y) : Nat}:
90	  match b:
91	    case True{}:
92	      {==}
93	    case False{}:
94	      {==}
95	
96	def zero_add(+n: Nat) -> {Nat.add(0n, n) == n : Nat}:
97	  Equal.trans(Nat, Nat.add(0n, n), Nat.add(n, 0n), n, N.add_comm(0n, n), N.add_zero(n))
98	
99	def succ_add(+a: Nat, +b: Nat) -> {Nat.add(1n+a, b) == Nat.add(a, 1n+b) : Nat}:
100	  Equal.trans(Nat, Nat.add(1n+a, b), Nat.add(b, 1n+a), Nat.add(a, 1n+b), N.add_comm(1n+a, b),
101	    Equal.trans(Nat, Nat.add(b, 1n+a), 1n+Nat.add(b, a), Nat.add(a, 1n+b), N.add_succ(b, a),
102	      Equal.trans(Nat, 1n+Nat.add(b, a), 1n+Nat.add(a, b), Nat.add(a, 1n+b), N.succ_cong(Nat.add(b, a), Nat.add(a, b), N.add_comm(b, a)), Equal.sym(Nat, Nat.add(a, 1n+b), 1n+Nat.add(a, b), N.add_succ(a, b)))))
103	
104	# ---- Contains ----
105	def inset_nth(+xs: List<&2, Bool>, +k: Nat, +b: Bool, +h: {SC.nth(Bool, xs, k) == Some{b} : Maybe<&2, Bool>}) -> {S.inset(xs, k) == b : Bool}:
106	  %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, k), Some{b}, h) : {S.ins(_) == b : Bool}
107	  {==}
108	
109	def gr_y(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}, +y: Maybe<&2, Bool>, +hy: {SC.nth(Bool, xs, i) == y : Maybe<&2, Bool>}) -> {S.ob(xs, E.Get{i}) == E.OBit{Done{S.inset(xs, i)}} : E.Obs}:
110	  match y:
111	    case None{}:
112	      Empty.absurd({S.ob(xs, E.Get{i}) == E.OBit{Done{S.inset(xs, i)}} : E.Obs}, LL.sc_nth_some(Bool, xs, i, h, hy))
113	    case Some{+b}:
114	      %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), Some{b}, hy) : {E.OBit{S.bit(_)} == E.OBit{Done{S.ins(_)}} : E.Obs}
115	      {==}
116	
117	def get_result(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Contains.get_result(xs, i, h):
118	  gr_y(xs, i, h, SC.nth(Bool, xs, i), {==})
119	
120	def get_frame(+xs: List<&2, Bool>, +i: Nat) -> S.Contains.get_frame(xs, i):
121	  {==}
122	
123	def get_outside(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_le(SC.length(Bool, xs), i) == True{} : Bool}) -> S.Contains.get_outside(xs, i, h):
124	  %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), None{}, LL.nth_none(Bool, xs, i, h)) : {E.OBit{S.bit(_)} == E.OBit{Fail{E.IndexOutOfRange{}}} : E.Obs}
125	  {==}
126	
127	# ---- Length (the member count), Capacity (the universe) ----
128	def count_result(+xs: List<&2, Bool>) -> S.Length.count_result(xs):
129	  {==}
130	
131	def count_frame(+xs: List<&2, Bool>) -> S.Length.count_frame(xs):
132	  {==}
133	
134	def length_result(+xs: List<&2, Bool>) -> S.Capacity.length_result(xs):
135	  {==}
136	
137	def length_frame(+xs: List<&2, Bool>) -> S.Capacity.length_frame(xs):
138	  {==}
139	
140	# ---- Empty_Set: no member, Length 0, over the universe [0, n) ----
141	def new_contains(+n: Nat, +k: Nat) -> S.Empty_Set.new_contains(n, k):
142	  match n k:
143	    case 0n _:
144	      {==}
145	    case 1n+m 0n:
146	      {==}
147	    case 1n+ +m 1n+ +j:
148	      new_contains(m, j)
149	
150	def new_count(+n: Nat) -> S.Empty_Set.new_count(n):
151	  match n:
152	    case 0n:
153	      {==}
154	    case 1n+ +m:
155	      new_count(m)
156	
157	def new_length(+n: Nat) -> S.Empty_Set.new_length(n):
158	  LL.length_replicate(Bool, n, False{})
159	
160	# ---- the update of one bit ----
161	def assign_is(+xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}, +y: Maybe<&2, Bool>, +hy: {SC.nth(Bool, xs, i) == y : Maybe<&2, Bool>}) -> {S.assign(xs, i, v) == (SC.update(Bool, xs, i, v), E.OUnit{Done{Unit{}}}) : List<&2, Bool> & E.Obs}:
162	  match y:
163	    case None{}:
164	      Empty.absurd({S.assign(xs, i, v) == (SC.update(Bool, xs, i, v), E.OUnit{Done{Unit{}}}) : List<&2, Bool> & E.Obs}, LL.sc_nth_some(Bool, xs, i, h, hy))
165	    case Some{b}:
166	      %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), Some{b}, hy) : {S.assign_at(_, xs, i, v) == (SC.update(Bool, xs, i, v), E.OUnit{Done{Unit{}}}) : List<&2, Bool> & E.Obs}
167	      {==}
168	
169	def inset_update_same(+xs: List<&2, Bool>, +i: Nat, +v: Bool, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.inset(SC.update(Bool, xs, i, v), i) == v : Bool}:
170	  inset_nth(SC.update(Bool, xs, i, v), i, v, LL.nth_update_same(Bool, xs, i, v, h))
171	
172	def inset_update_other(+xs: List<&2, Bool>, +i: Nat, +j: Nat, +v: Bool, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> {S.inset(SC.update(Bool, xs, i, v), j) == S.inset(xs, j) : Bool}:
173	  Equal.cong(Maybe<&2, Bool>, Bool, z => S.ins(z), SC.nth(Bool, SC.update(Bool, xs, i, v), j), SC.nth(Bool, xs, j), LL.nth_update_other(Bool, xs, i, j, v, ne))
174	
175	# count after setting a bit: one more unless it was set
176	def cu_set(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.count(SC.update(Bool, xs, i, True{})) == Bool.pick(Nat, S.inset(xs, i), S.count(xs), 1n+S.count(xs)) : Nat}:
177	  match xs i:
178	    case Nil{} _:
179	      Empty.absurd({S.count(SC.update(Bool, Nil{}, i, True{})) == Bool.pick(Nat, S.inset(Nil{}, i), S.count(Nil{}), 1n+S.count(Nil{})) : Nat}, N.lt_zero_absurd(i, h))
180	    case Con{True{}, t} 0n:
181	      {==}
182	    case Con{False{}, t} 0n:
183	      {==}
184	    case Con{True{}, +t} 1n+ +p:
185	      %Equal.sym(Nat, S.count(SC.update(Bool, t, p, True{})), Bool.pick(Nat, S.inset(t, p), S.count(t), 1n+S.count(t)), cu_set(t, p, h)) : {1n+_ == Bool.pick(Nat, S.inset(t, p), 1n+S.count(t), 1n+(1n+S.count(t))) : Nat}
186	      succ_pick(S.inset(t, p), S.count(t), 1n+S.count(t))
187	    case Con{False{}, +t} 1n+ +p:
188	      cu_set(t, p, h)
189	
190	# count after clearing a bit: one less if it was set
191	def cu_clear(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.count(xs) == Bool.pick(Nat, S.inset(xs, i), 1n+S.count(SC.update(Bool, xs, i, False{})), S.count(SC.update(Bool, xs, i, False{}))) : Nat}:
192	  match xs i:
193	    case Nil{} _:
194	      Empty.absurd({S.count(Nil{}) == Bool.pick(Nat, S.inset(Nil{}, i), 1n+S.count(SC.update(Bool, Nil{}, i, False{})), S.count(SC.update(Bool, Nil{}, i, False{}))) : Nat}, N.lt_zero_absurd(i, h))
195	    case Con{True{}, t} 0n:
196	      {==}
197	    case Con{False{}, t} 0n:
198	      {==}
199	    case Con{True{}, +t} 1n+ +p:
200	      %Equal.sym(Nat, S.count(t), Bool.pick(Nat, S.inset(t, p), 1n+S.count(SC.update(Bool, t, p, False{})), S.count(SC.update(Bool, t, p, False{}))), cu_clear(t, p, h)) : {1n+_ == Bool.pick(Nat, S.inset(t, p), 1n+(1n+S.count(SC.update(Bool, t, p, False{}))), 1n+S.count(SC.update(Bool, t, p, False{}))) : Nat}
201	      succ_pick(S.inset(t, p), 1n+S.count(SC.update(Bool, t, p, False{})), S.count(SC.update(Bool, t, p, False{})))
202	    case Con{False{}, +t} 1n+ +p:
203	      cu_clear(t, p, h)
204	
205	# ---- Include / Insert (set) ----
206	def set_model(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.nx(xs, E.Set{i}) == SC.update(Bool, xs, i, True{}) : List<&2, Bool>}:
207	  %Equal.sym(List<&2, Bool> & E.Obs, S.assign(xs, i, True{}), (SC.update(Bool, xs, i, True{}), E.OUnit{Done{Unit{}}}), assign_is(xs, i, True{}, h, SC.nth(Bool, xs, i), {==})) : {Pair.fst(List<&2, Bool>, E.Obs, _) == SC.update(Bool, xs, i, True{}) : List<&2, Bool>}
208	  {==}
209	
210	def set_contains(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Include.set_contains(xs, i, h):
211	  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Set{i}), SC.update(Bool, xs, i, True{}), set_model(xs, i, h)) : {S.inset(_, i) == True{} : Bool}
212	  inset_update_same(xs, i, True{}, h)
213	
214	def set_others(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}, +j: Nat, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> S.Include.set_others(xs, i, h, j, ne):
215	  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Set{i}), SC.update(Bool, xs, i, True{}), set_model(xs, i, h)) : {S.inset(_, j) == S.inset(xs, j) : Bool}
216	  inset_update_other(xs, i, j, True{}, ne)
217	
218	def set_universe(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Include.set_universe(xs, i, h):
219	  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Set{i}), SC.update(Bool, xs, i, True{}), set_model(xs, i, h)) : {SC.length(Bool, _) == SC.length(Bool, xs) : Nat}
220	  LL.length_update(Bool, xs, i, True{})
221	
222	def set_outside(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_le(SC.length(Bool, xs), i) == True{} : Bool}) -> S.Include.set_outside(xs, i, h):
223	  %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), None{}, LL.nth_none(Bool, xs, i, h)) : {S.assign_at(_, xs, i, True{}) == (xs, E.OUnit{Fail{E.IndexOutOfRange{}}}) : List<&2, Bool> & E.Obs}
224	  {==}
225	
226	# ---- Exclude / Delete (clear) ----
227	def clear_model(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> {S.nx(xs, E.Clear{i}) == SC.update(Bool, xs, i, False{}) : List<&2, Bool>}:
228	  %Equal.sym(List<&2, Bool> & E.Obs, S.assign(xs, i, False{}), (SC.update(Bool, xs, i, False{}), E.OUnit{Done{Unit{}}}), assign_is(xs, i, False{}, h, SC.nth(Bool, xs, i), {==})) : {Pair.fst(List<&2, Bool>, E.Obs, _) == SC.update(Bool, xs, i, False{}) : List<&2, Bool>}
229	  {==}
230	
231	def clear_contains(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Exclude.clear_contains(xs, i, h):
232	  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Clear{i}), SC.update(Bool, xs, i, False{}), clear_model(xs, i, h)) : {S.inset(_, i) == False{} : Bool}
233	  inset_update_same(xs, i, False{}, h)
234	
235	def clear_others(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}, +j: Nat, +ne: {Nat.is_eq(i, j) == False{} : Bool}) -> S.Exclude.clear_others(xs, i, h, j, ne):
236	  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Clear{i}), SC.update(Bool, xs, i, False{}), clear_model(xs, i, h)) : {S.inset(_, j) == S.inset(xs, j) : Bool}
237	  inset_update_other(xs, i, j, False{}, ne)
238	
239	def clear_universe(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Exclude.clear_universe(xs, i, h):
240	  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Clear{i}), SC.update(Bool, xs, i, False{}), clear_model(xs, i, h)) : {SC.length(Bool, _) == SC.length(Bool, xs) : Nat}
241	  LL.length_update(Bool, xs, i, False{})
242	
243	def clear_outside(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_le(SC.length(Bool, xs), i) == True{} : Bool}) -> S.Exclude.clear_outside(xs, i, h):
244	  %Equal.sym(Maybe<&2, Bool>, SC.nth(Bool, xs, i), None{}, LL.nth_none(Bool, xs, i, h)) : {S.assign_at(_, xs, i, False{}) == (xs, E.OUnit{Fail{E.IndexOutOfRange{}}}) : List<&2, Bool> & E.Obs}
245	  {==}
246	
247	# Include: one more member unless it was one (Insert's Pre: it was not)
248	def set_count(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Include.set_count(xs, i, h):
249	  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Set{i}), SC.update(Bool, xs, i, True{}), set_model(xs, i, h)) : {S.count(_) == Bool.pick(Nat, S.inset(xs, i), S.count(xs), 1n+S.count(xs)) : Nat}
250	  cu_set(xs, i, h)
251	
252	# Exclude: one member less if it was one (Delete's Pre: it was)
253	def clear_count(+xs: List<&2, Bool>, +i: Nat, +h: {Nat.is_lt(i, SC.length(Bool, xs)) == True{} : Bool}) -> S.Exclude.clear_count(xs, i, h):
254	  %Equal.sym(List<&2, Bool>, S.nx(xs, E.Clear{i}), SC.update(Bool, xs, i, False{}), clear_model(xs, i, h)) : {S.count(xs) == Bool.pick(Nat, S.inset(xs, i), 1n+S.count(_), S.count(_)) : Nat}
255	  cu_clear(xs, i, h)
256	
257	# ---- Union (1180) ----
258	def union_pt(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> {S.inset(S.zip_or(xs, ys), k) == Bool.or(S.inset(xs, k), S.inset(ys, k)) : Bool}:
259	  match xs ys k:
260	    case Nil{} Nil{} _:
261	      {==}
262	    case Nil{} Con{b, t} _:
263	      Empty.absurd({S.inset(S.zip_or(Nil{}, Con{b, t}), k) == Bool.or(S.inset(Nil{}, k), S.inset(Con{b, t}, k)) : Bool}, zero_ne_succ(SC.length(Bool, t), h))
264	    case Con{a, s} Nil{} _:
265	      Empty.absurd({S.inset(S.zip_or(Con{a, s}, Nil{}), k) == Bool.or(S.inset(Con{a, s}, k), S.inset(Nil{}, k)) : Bool}, succ_ne_zero(SC.length(Bool, s), h))
266	    case Con{a, s} Con{b, t} 0n:
267	      {==}
268	    case Con{a, +s} Con{b, +t} 1n+ +p:
269	      union_pt(s, t, p, N.succ_inj(SC.length(Bool, s), SC.length(Bool, t), h))
270	
271	def union_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> S.Union.union_contains(xs, ys, k, h):
272	  %h : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(Nat.is_eq(SC.length(Bool, xs), _), xs, S.zip_or(xs, ys))), k) == Bool.or(S.inset(xs, k), S.inset(ys, k)) : Bool}
273	  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, xs)), True{}, N.is_eq_refl(SC.length(Bool, xs))) : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(_, xs, S.zip_or(xs, ys))), k) == Bool.or(S.inset(xs, k), S.inset(ys, k)) : Bool}
274	  union_pt(xs, ys, k, h)
275	
276	def union_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)) == False{} : Bool}) -> S.Union.union_mismatch(xs, ys, h):
277	  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)), False{}, h) : {S.combine_if(_, xs, S.zip_or(xs, ys)) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}
278	  {==}
279	
280	# ---- Intersection (1279) ----
281	def intersection_pt(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> {S.inset(S.zip_and(xs, ys), k) == Bool.and(S.inset(xs, k), S.inset(ys, k)) : Bool}:
282	  match xs ys k:
283	    case Nil{} Nil{} _:
284	      {==}
285	    case Nil{} Con{b, t} _:
286	      Empty.absurd({S.inset(S.zip_and(Nil{}, Con{b, t}), k) == Bool.and(S.inset(Nil{}, k), S.inset(Con{b, t}, k)) : Bool}, zero_ne_succ(SC.length(Bool, t), h))
287	    case Con{a, s} Nil{} _:
288	      Empty.absurd({S.inset(S.zip_and(Con{a, s}, Nil{}), k) == Bool.and(S.inset(Con{a, s}, k), S.inset(Nil{}, k)) : Bool}, succ_ne_zero(SC.length(Bool, s), h))
289	    case Con{a, s} Con{b, t} 0n:
290	      {==}
291	    case Con{a, +s} Con{b, +t} 1n+ +p:
292	      intersection_pt(s, t, p, N.succ_inj(SC.length(Bool, s), SC.length(Bool, t), h))
293	
294	def intersection_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> S.Intersection.intersection_contains(xs, ys, k, h):
295	  %h : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(Nat.is_eq(SC.length(Bool, xs), _), xs, S.zip_and(xs, ys))), k) == Bool.and(S.inset(xs, k), S.inset(ys, k)) : Bool}
296	  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, xs)), True{}, N.is_eq_refl(SC.length(Bool, xs))) : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(_, xs, S.zip_and(xs, ys))), k) == Bool.and(S.inset(xs, k), S.inset(ys, k)) : Bool}
297	  intersection_pt(xs, ys, k, h)
298	
299	def intersection_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)) == False{} : Bool}) -> S.Intersection.intersection_mismatch(xs, ys, h):
300	  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)), False{}, h) : {S.combine_if(_, xs, S.zip_and(xs, ys)) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}
301	  {==}
302	
303	# ---- Difference (1340) ----
304	def difference_pt(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> {S.inset(S.zip_diff(xs, ys), k) == Bool.and(S.inset(xs, k), Bool.not(S.inset(ys, k))) : Bool}:
305	  match xs ys k:
306	    case Nil{} Nil{} _:
307	      {==}
308	    case Nil{} Con{b, t} _:
309	      Empty.absurd({S.inset(S.zip_diff(Nil{}, Con{b, t}), k) == Bool.and(S.inset(Nil{}, k), Bool.not(S.inset(Con{b, t}, k))) : Bool}, zero_ne_succ(SC.length(Bool, t), h))
310	    case Con{a, s} Nil{} _:
311	      Empty.absurd({S.inset(S.zip_diff(Con{a, s}, Nil{}), k) == Bool.and(S.inset(Con{a, s}, k), Bool.not(S.inset(Nil{}, k))) : Bool}, succ_ne_zero(SC.length(Bool, s), h))
312	    case Con{a, s} Con{b, t} 0n:
313	      {==}
314	    case Con{a, +s} Con{b, +t} 1n+ +p:
315	      difference_pt(s, t, p, N.succ_inj(SC.length(Bool, s), SC.length(Bool, t), h))
316	
317	def difference_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> S.Difference.difference_contains(xs, ys, k, h):
318	  %h : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(Nat.is_eq(SC.length(Bool, xs), _), xs, S.zip_diff(xs, ys))), k) == Bool.and(S.inset(xs, k), Bool.not(S.inset(ys, k))) : Bool}
319	  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, xs)), True{}, N.is_eq_refl(SC.length(Bool, xs))) : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(_, xs, S.zip_diff(xs, ys))), k) == Bool.and(S.inset(xs, k), Bool.not(S.inset(ys, k))) : Bool}
320	  difference_pt(xs, ys, k, h)
321	
322	def difference_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)) == False{} : Bool}) -> S.Difference.difference_mismatch(xs, ys, h):
323	  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)), False{}, h) : {S.combine_if(_, xs, S.zip_diff(xs, ys)) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}
324	  {==}
325	
326	# ---- Symmetric_Difference (1404) ----
327	def symmetric_difference_pt(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> {S.inset(S.zip_xor(xs, ys), k) == Bool.xor(S.inset(xs, k), S.inset(ys, k)) : Bool}:
328	  match xs ys k:
329	    case Nil{} Nil{} _:
330	      {==}
331	    case Nil{} Con{b, t} _:
332	      Empty.absurd({S.inset(S.zip_xor(Nil{}, Con{b, t}), k) == Bool.xor(S.inset(Nil{}, k), S.inset(Con{b, t}, k)) : Bool}, zero_ne_succ(SC.length(Bool, t), h))
333	    case Con{a, s} Nil{} _:
334	      Empty.absurd({S.inset(S.zip_xor(Con{a, s}, Nil{}), k) == Bool.xor(S.inset(Con{a, s}, k), S.inset(Nil{}, k)) : Bool}, succ_ne_zero(SC.length(Bool, s), h))
335	    case Con{a, s} Con{b, t} 0n:
336	      {==}
337	    case Con{a, +s} Con{b, +t} 1n+ +p:
338	      symmetric_difference_pt(s, t, p, N.succ_inj(SC.length(Bool, s), SC.length(Bool, t), h))
339	
340	def symmetric_difference_contains(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +k: Nat, +h: {SC.length(Bool, xs) == SC.length(Bool, ys) : Nat}) -> S.Symmetric_Difference.symmetric_difference_contains(xs, ys, k, h):
341	  %h : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(Nat.is_eq(SC.length(Bool, xs), _), xs, S.zip_xor(xs, ys))), k) == Bool.xor(S.inset(xs, k), S.inset(ys, k)) : Bool}
342	  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, xs)), True{}, N.is_eq_refl(SC.length(Bool, xs))) : {S.inset(Pair.fst(List<&2, Bool>, E.Obs, S.combine_if(_, xs, S.zip_xor(xs, ys))), k) == Bool.xor(S.inset(xs, k), S.inset(ys, k)) : Bool}
343	  symmetric_difference_pt(xs, ys, k, h)
344	
345	def xor_mismatch(+xs: List<&2, Bool>, +ys: List<&2, Bool>, +h: {Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)) == False{} : Bool}) -> S.Symmetric_Difference.xor_mismatch(xs, ys, h):
346	  %Equal.sym(Bool, Nat.is_eq(SC.length(Bool, xs), SC.length(Bool, ys)), False{}, h) : {S.combine_if(_, xs, S.zip_xor(xs, ys)) == (xs, E.OUnit{Fail{E.LengthMismatch{}}}) : List<&2, Bool> & E.Obs}
347	  {==}
348	
349	def to_list_result(+xs: List<&2, Bool>) -> S.Elements.to_list_result(xs):
350	  {==}
351	
352	def to_list_frame(+xs: List<&2, Bool>) -> S.Elements.to_list_frame(xs):
353	  {==}
354	
355	# no member below the offset
356	def members_above(+xs: List<&2, Bool>, +off: Nat, +j: Nat, +h: {Nat.is_lt(j, off) == True{} : Bool}) -> {S.nmem(j, S.members(xs, off)) == False{} : Bool}:
357	  match xs:
358	    case Nil{}:
359	      {==}
360	    case Con{False{}, +t}:
361	      members_above(t, 1n+off, j, N.lt_trans(j, off, 1n+off, h, N.lt_succ(off)))
362	    case Con{True{}, +t}:
363	      %Equal.sym(Bool, Nat.is_eq(off, j), False{}, N.is_eq_sym_false(j, off, N.is_eq_lt(j, off, h))) : {Bool.or(_, S.nmem(j, S.members(t, 1n+off))) == False{} : Bool}
364	      members_above(t, 1n+off, j, N.lt_trans(j, off, 1n+off, h, N.lt_succ(off)))
365	
366	def rel_add(+off: Nat, +p: Nat) -> {Nat.add(1n+off, p) == Nat.add(1n+p, off) : Nat}:
367	  Equal.trans(Nat, Nat.add(1n+off, p), Nat.add(off, 1n+p), Nat.add(1n+p, off), succ_add(off, p), N.add_comm(off, 1n+p))
368	
369	def ne_add_succ(+off: Nat, +p: Nat) -> {Nat.is_eq(off, Nat.add(1n+p, off)) == False{} : Bool}:
370	  N.is_eq_lt(off, Nat.add(1n+p, off), N.lt_le_trans(off, 1n+off, Nat.add(1n+p, off), N.lt_succ(off), L.subst(Nat, z => {Nat.is_le(1n+off, z) == True{} : Bool}, Nat.add(1n+off, p), Nat.add(1n+p, off), rel_add(off, p), N.le_add_right(1n+off, p))))
371	
372	# the member at relative index k is there exactly when bit k is set
373	def members_pt(+xs: List<&2, Bool>, +k: Nat, +off: Nat) -> {S.nmem(Nat.add(k, off), S.members(xs, off)) == S.inset(xs, k) : Bool}:
374	  match xs k:
375	    case Nil{} _:
376	      {==}
377	    case Con{False{}, +t} 0n:
378	      %Equal.sym(Nat, Nat.add(0n, off), off, zero_add(off)) : {S.nmem(_, S.members(t, 1n+off)) == False{} : Bool}
379	      members_above(t, 1n+off, off, N.lt_succ(off))
380	    case Con{True{}, +t} 0n:
381	      %Equal.sym(Nat, Nat.add(0n, off), off, zero_add(off)) : {Bool.or(Nat.is_eq(off, _), S.nmem(_, S.members(t, 1n+off))) == True{} : Bool}
382	      %Equal.sym(Bool, Nat.is_eq(off, off), True{}, N.is_eq_refl(off)) : {Bool.or(_, S.nmem(off, S.members(t, 1n+off))) == True{} : Bool}
383	      {==}
384	    case Con{False{}, +t} 1n+ +p:
385	      %Equal.sym(Nat, Nat.add(1n+p, off), Nat.add(p, 1n+off), succ_add(p, off)) : {S.nmem(_, S.members(t, 1n+off)) == S.inset(t, p) : Bool}
386	      members_pt(t, p, 1n+off)
387	    case Con{True{}, +t} 1n+ +p:
388	      %Equal.sym(Bool, Nat.is_eq(off, Nat.add(1n+p, off)), False{}, ne_add_succ(off, p)) : {Bool.or(_, S.nmem(Nat.add(1n+p, off), S.members(t, 1n+off))) == S.inset(t, p) : Bool}
389	      %Equal.sym(Nat, Nat.add(1n+p, off), Nat.add(p, 1n+off), succ_add(p, off)) : {Bool.or(False{}, S.nmem(_, S.members(t, 1n+off))) == S.inset(t, p) : Bool}
390	      members_pt(t, p, 1n+off)
391	
392	def elements_contains(+xs: List<&2, Bool>, +k: Nat) -> S.Elements.elements_contains(xs, k):
393	  %N.add_zero(k) : {S.nmem(_, S.members(xs, 0n)) == S.inset(xs, k) : Bool}
394	  members_pt(xs, k, 0n)
395	
396	# as many elements as members (SPARK: Length (Elements) = Length (Container))
397	def elements_length(+xs: List<&2, Bool>, +off: Nat) -> S.Elements.elements_length(xs, off):
398	  match xs:
399	    case Nil{}:
400	      {==}
401	    case Con{False{}, +t}:
402	      elements_length(t, 1n+off)
403	    case Con{True{}, +t}:
404	      N.succ_cong(SC.length(Nat, S.members(t, 1n+off)), S.count(t), elements_length(t, 1n+off))