1	import Base
2	import ../../lib/logic.bend as L
3	import ../../../spec/lib/common.bend as SC
4	import ./frame.bend as FR
5	import ./path.bend as P
6	import ../../lib/nat_list.bend as NL
7	
8	# Membership bookkeeping for id lists without repeats: an id of one part is
9	# absent from the others, absence splits over appends, and an absent id
10	# differs from a present one. (source: tools/generators/tm_hand/dj.src)
11	
12	
13	def nm_l(+z: Nat, +a: List<&2, Nat>, +b: List<&2, Nat>, +h: {NL.memn(z, SC.append(Nat, a, b)) == False{} : Bool}) -> {NL.memn(z, a) == False{} : Bool}:
14	  FR.or_f_l(NL.memn(z, a), NL.memn(z, b), L.subst(Bool, w => {w == False{} : Bool}, NL.memn(z, SC.append(Nat, a, b)), Bool.or(NL.memn(z, a), NL.memn(z, b)), NL.memn_app(z, a, b), h))
15	
16	def nm_r(+z: Nat, +a: List<&2, Nat>, +b: List<&2, Nat>, +h: {NL.memn(z, SC.append(Nat, a, b)) == False{} : Bool}) -> {NL.memn(z, b) == False{} : Bool}:
17	  FR.or_f_r(NL.memn(z, a), NL.memn(z, b), L.subst(Bool, w => {w == False{} : Bool}, NL.memn(z, SC.append(Nat, a, b)), Bool.or(NL.memn(z, a), NL.memn(z, b)), NL.memn_app(z, a, b), h))
18	
19	def nm_ch(+z: Nat, +i: Nat, +t: List<&2, Nat>, +h: {NL.memn(z, Con{i, t}) == False{} : Bool}) -> {Nat.is_eq(i, z) == False{} : Bool}:
20	  FR.or_f_l(Nat.is_eq(i, z), NL.memn(z, t), h)
21	
22	def nm_ct(+z: Nat, +i: Nat, +t: List<&2, Nat>, +h: {NL.memn(z, Con{i, t}) == False{} : Bool}) -> {NL.memn(z, t) == False{} : Bool}:
23	  FR.or_f_r(Nat.is_eq(i, z), NL.memn(z, t), h)
24	
25	def nm_app(+z: Nat, +a: List<&2, Nat>, +b: List<&2, Nat>, +ha: {NL.memn(z, a) == False{} : Bool}, +hb: {NL.memn(z, b) == False{} : Bool}) -> {NL.memn(z, SC.append(Nat, a, b)) == False{} : Bool}:
26	  %Equal.sym(Bool, NL.memn(z, SC.append(Nat, a, b)), Bool.or(NL.memn(z, a), NL.memn(z, b)), NL.memn_app(z, a, b)) : {_ == False{} : Bool}
27	  %Equal.sym(Bool, NL.memn(z, a), False{}, ha) : {Bool.or(_, NL.memn(z, b)) == False{} : Bool}
28	  hb
29	
30	def nm_cons(+z: Nat, +i: Nat, +t: List<&2, Nat>, +hi: {Nat.is_eq(i, z) == False{} : Bool}, +ht: {NL.memn(z, t) == False{} : Bool}) -> {NL.memn(z, Con{i, t}) == False{} : Bool}:
31	  %Equal.sym(Bool, Nat.is_eq(i, z), False{}, hi) : {Bool.or(_, NL.memn(z, t)) == False{} : Bool}
32	  ht
33	
34	# the head of a list without repeats is not in its tail
35	def nd_head(+i: Nat, +t: List<&2, Nat>, +h: {NL.nodupn(Con{i, t}) == True{} : Bool}) -> {NL.memn(i, t) == False{} : Bool}:
36	  NL.not_t_f(NL.memn(i, t), L.and_left(Bool.not(NL.memn(i, t)), NL.nodupn(t), h))
37	
38	def nd_tail(+i: Nat, +t: List<&2, Nat>, +h: {NL.nodupn(Con{i, t}) == True{} : Bool}) -> {NL.nodupn(t) == True{} : Bool}:
39	  L.and_right(Bool.not(NL.memn(i, t)), NL.nodupn(t), h)
40	
41	# an id of the right part is not in the left one, and conversely
42	def dj_l(+a: List<&2, Nat>, +b: List<&2, Nat>, +h: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}, +z: Nat, +hz: {NL.memn(z, b) == True{} : Bool}) -> {NL.memn(z, a) == False{} : Bool}:
43	  NL.nd_dj(a, b, h, z, hz)
44	
45	def dj_r(+a: List<&2, Nat>, +b: List<&2, Nat>, +h: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}, +z: Nat, +hz: {NL.memn(z, a) == True{} : Bool}) -> {NL.memn(z, b) == False{} : Bool}:
46	  NL.nd_dj2(a, b, h, z, hz)
47	
48	def ndl(+a: List<&2, Nat>, +b: List<&2, Nat>, +h: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}) -> {NL.nodupn(a) == True{} : Bool}:
49	  NL.nd_l(a, b, h)
50	
51	def ndr(+a: List<&2, Nat>, +b: List<&2, Nat>, +h: {NL.nodupn(SC.append(Nat, a, b)) == True{} : Bool}) -> {NL.nodupn(b) == True{} : Bool}:
52	  NL.nd_r(a, b, h)
53	
54	def mem_l(+z: Nat, +a: List<&2, Nat>, +b: List<&2, Nat>, +h: {NL.memn(z, a) == True{} : Bool}) -> {NL.memn(z, SC.append(Nat, a, b)) == True{} : Bool}:
55	  NL.mem_app_l(z, a, b, h)
56	
57	def mem_r(+z: Nat, +a: List<&2, Nat>, +b: List<&2, Nat>, +h: {NL.memn(z, b) == True{} : Bool}) -> {NL.memn(z, SC.append(Nat, a, b)) == True{} : Bool}:
58	  NL.mem_app_r(z, a, b, h)
59	
60	def mem_hd(+i: Nat, +t: List<&2, Nat>) -> {NL.memn(i, Con{i, t}) == True{} : Bool}:
61	  P.mem_self(i, t)
62	
63	def mem_tl(+z: Nat, +i: Nat, +t: List<&2, Nat>, +h: {NL.memn(z, t) == True{} : Bool}) -> {NL.memn(z, Con{i, t}) == True{} : Bool}:
64	  P.mem_cons(z, i, t, h)
65	
66	# an absent id differs from a present one
67	def ne_nm(+a: Nat, +b: Nat, +xs: List<&2, Nat>, +ha: {NL.memn(a, xs) == False{} : Bool}, +hb: {NL.memn(b, xs) == True{} : Bool}) -> {Nat.is_eq(a, b) == False{} : Bool}:
68	  NL.not_t_f(Nat.is_eq(a, b), P.ne_mem(a, b, xs, ha, hb))