1	import Base
2	import ../../../spec/containers/intrusive_doubly_linked_list/model.bend as G
3	
4	
5	# The graph is a proof shadow. These are pointwise map laws, proved here,
6	# not postconditions assumed of the list operation.
7	
8	def next_sn(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +x: N) -> {G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x) == G.choose(~Maybe<&2,N>,eq(n,x),v,G.next(~N, ~R, ~P, ~eq,g,x)) : Maybe<&2,N>}:
9	  match g:
10	    case G.Graph{ns,ps,rs,f}: {==}
11	
12	def prev_sn(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +x: N) -> {G.prev(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x) == G.prev(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}:
13	  match g:
14	    case G.Graph{ns,ps,rs,f}: {==}
15	
16	def next_sp(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +x: N) -> {G.next(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),x) == G.next(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}:
17	  match g:
18	    case G.Graph{ns,ps,rs,f}: {==}
19	
20	def prev_sp(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +x: N) -> {G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),x) == G.choose(~Maybe<&2,N>,eq(n,x),v,G.prev(~N, ~R, ~P, ~eq,g,x)) : Maybe<&2,N>}:
21	  match g:
22	    case G.Graph{ns,ps,rs,f}: {==}
23	
24	def next_sh(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +v: Maybe<&2,N>, +x: N) -> {G.next(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,g,r,v),x) == G.next(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}:
25	  match g:
26	    case G.Graph{ns,ps,rs,f}: {==}
27	
28	def prev_sh(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +v: Maybe<&2,N>, +x: N) -> {G.prev(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,g,r,v),x) == G.prev(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}:
29	  match g:
30	    case G.Graph{ns,ps,rs,f}: {==}
31	
32	def next_sn_other(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +x: N, neq: {eq(n,x) == False{} : Bool}) -> {G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x) == G.next(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}:
33	  %Equal.sym(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x),G.choose(~Maybe<&2,N>,eq(n,x),v,G.next(~N, ~R, ~P, ~eq,g,x)),next_sn(~N, ~R, ~P, ~eq,g,n,v,x)) : {_ == G.next(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}
34	  %Equal.sym(Bool,eq(n,x),False{},neq) : {G.choose(~Maybe<&2,N>,_,v,G.next(~N, ~R, ~P, ~eq,g,x)) == G.next(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}
35	  {==}
36	
37	def prev_sp_other(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +x: N, neq: {eq(n,x) == False{} : Bool}) -> {G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),x) == G.prev(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}:
38	  %Equal.sym(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),x),G.choose(~Maybe<&2,N>,eq(n,x),v,G.prev(~N, ~R, ~P, ~eq,g,x)),prev_sp(~N, ~R, ~P, ~eq,g,n,v,x)) : {_ == G.prev(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}
39	  %Equal.sym(Bool,eq(n,x),False{},neq) : {G.choose(~Maybe<&2,N>,_,v,G.prev(~N, ~R, ~P, ~eq,g,x)) == G.prev(~N, ~R, ~P, ~eq,g,x) : Maybe<&2,N>}
40	  {==}
41	
42	def next_sn_self(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, same: {eq(n,n) == True{} : Bool}) -> {G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),n) == v : Maybe<&2,N>}:
43	  %Equal.sym(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),n),G.choose(~Maybe<&2,N>,eq(n,n),v,G.next(~N, ~R, ~P, ~eq,g,n)),next_sn(~N, ~R, ~P, ~eq,g,n,v,n)) : {_ == v : Maybe<&2,N>}
44	  %Equal.sym(Bool,eq(n,n),True{},same) : {G.choose(~Maybe<&2,N>,_,v,G.next(~N, ~R, ~P, ~eq,g,n)) == v : Maybe<&2,N>}
45	  {==}
46	
47	def prev_sp_self(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, same: {eq(n,n) == True{} : Bool}) -> {G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),n) == v : Maybe<&2,N>}:
48	  %Equal.sym(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),n),G.choose(~Maybe<&2,N>,eq(n,n),v,G.prev(~N, ~R, ~P, ~eq,g,n)),prev_sp(~N, ~R, ~P, ~eq,g,n,v,n)) : {_ == v : Maybe<&2,N>}
49	  %Equal.sym(Bool,eq(n,n),True{},same) : {G.choose(~Maybe<&2,N>,_,v,G.prev(~N, ~R, ~P, ~eq,g,n)) == v : Maybe<&2,N>}
50	  {==}
51	
52	def segment_sn_frame(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +xs: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, away: G.away(~N,~eq,n,xs), good: G.segment(~N, ~R, ~P, ~eq,g,p,xs,q)) -> G.segment(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),p,xs,q):
53	  match xs away good:
54	    case Nil{} _ _: Unit{}
55	    case Con{+x,+rest} Tuple{Tuple{neq,rev},ar} Tuple{hp,Tuple{hn,ht}}:
56	      (Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x),G.prev(~N, ~R, ~P, ~eq,g,x),p,prev_sn(~N, ~R, ~P, ~eq,g,n,v,x),hp),
57	       (Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x),G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,rest,q),next_sn_other(~N, ~R, ~P, ~eq,g,n,v,x,neq),hn),
58	        segment_sn_frame(~N, ~R, ~P, ~eq,g,n,v,rest,Some{x},q,ar,ht)))
59	
60	def segment_sp_frame(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +xs: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, away: G.away(~N,~eq,n,xs), good: G.segment(~N, ~R, ~P, ~eq,g,p,xs,q)) -> G.segment(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),p,xs,q):
61	  match xs away good:
62	    case Nil{} _ _: Unit{}
63	    case Con{+x,+rest} Tuple{Tuple{neq,rev},ar} Tuple{hp,Tuple{hn,ht}}:
64	      (Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),x),G.prev(~N, ~R, ~P, ~eq,g,x),p,prev_sp_other(~N, ~R, ~P, ~eq,g,n,v,x,neq),hp),
65	       (Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,n,v),x),G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,rest,q),next_sp(~N, ~R, ~P, ~eq,g,n,v,x),hn),
66	        segment_sp_frame(~N, ~R, ~P, ~eq,g,n,v,rest,Some{x},q,ar,ht)))
67	
68	def segment_sh_frame(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +r: R, +v: Maybe<&2,N>, +xs: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, good: G.segment(~N, ~R, ~P, ~eq,g,p,xs,q)) -> G.segment(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,g,r,v),p,xs,q):
69	  match xs good:
70	    case Nil{} _: Unit{}
71	    case Con{+x,+rest} Tuple{hp,Tuple{hn,ht}}:
72	      (Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,g,r,v),x),G.prev(~N, ~R, ~P, ~eq,g,x),p,prev_sh(~N, ~R, ~P, ~eq,g,r,v,x),hp),
73	       (Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,g,r,v),x),G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,rest,q),next_sh(~N, ~R, ~P, ~eq,g,r,v,x),hn),
74	        segment_sh_frame(~N, ~R, ~P, ~eq,g,r,v,rest,Some{x},q,ht)))
75	
76	# Changing a segment's first predecessor preserves its entire suffix.
77	def segment_first_prev(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +x: N, +rest: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, +v: Maybe<&2,N>, same: {eq(x,x) == True{} : Bool}, away: G.away(~N,~eq,x,rest), good: G.segment(~N, ~R, ~P, ~eq,g,p,Con{x,rest},q)) -> G.segment(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,x,v),v,Con{x,rest},q):
78	  match good:
79	    case Tuple{hp,Tuple{hn,ht}}:
80	      (prev_sp_self(~N, ~R, ~P, ~eq,g,x,v,same),
81	       (Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,g,x,v),x),G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,rest,q),next_sp(~N, ~R, ~P, ~eq,g,x,v,x),hn),
82	        segment_sp_frame(~N, ~R, ~P, ~eq,g,x,v,rest,Some{x},q,away,ht)))
83	
84	def away_at(~N: Data, ~eq: N -> N -> Bool, +prefix: List<&2,N>, +n: N, +suffix: List<&2,N>, +x: N, h: G.away(~N,~eq,x,G.append(~N,prefix,Con{n,suffix}))) -> G.both({eq(x,n) == False{} : Bool}, {eq(n,x) == False{} : Bool}):
85	  match prefix h:
86	    case Nil{} Tuple{hn,ht}: hn
87	    case Con{a,rest} Tuple{ha,ht}: away_at(~N,~eq,rest,n,suffix,x,ht)
88	
89	def away_delete(~N: Data, ~eq: N -> N -> Bool, +prefix: List<&2,N>, +n: N, +suffix: List<&2,N>, +x: N, h: G.away(~N,~eq,x,G.append(~N,prefix,Con{n,suffix}))) -> G.away(~N,~eq,x,G.append(~N,prefix,suffix)):
90	  match prefix h:
91	    case Nil{} Tuple{hn,ht}: ht
92	    case Con{a,rest} Tuple{ha,ht}: (ha,away_delete(~N,~eq,rest,n,suffix,x,ht))
93	
94	def unique_delete(~N: Data, ~eq: N -> N -> Bool, +prefix: List<&2,N>, +n: N, +suffix: List<&2,N>, h: G.unique(~N,~eq,G.append(~N,prefix,Con{n,suffix}))) -> G.unique(~N,~eq,G.append(~N,prefix,suffix)):
95	  match prefix h:
96	    case Nil{} Tuple{hn,ht}: ht
97	    case Con{+a,+rest} Tuple{ha,ht}: (away_delete(~N,~eq,rest,n,suffix,a,ha),unique_delete(~N,~eq,rest,n,suffix,ht))
98	
99	def swapped(~N: Data, ~eq: N -> N -> Bool, +a: N, +b: N, h: G.both({eq(a,b) == False{} : Bool}, {eq(b,a) == False{} : Bool})) -> G.both({eq(b,a) == False{} : Bool}, {eq(a,b) == False{} : Bool}):
100	  match h:
101	    case Tuple{ab,ba}: (ba,ab)
102	
103	def deleted_away(~N: Data, ~eq: N -> N -> Bool, +prefix: List<&2,N>, +n: N, +suffix: List<&2,N>, h: G.unique(~N,~eq,G.append(~N,prefix,Con{n,suffix}))) -> G.away(~N,~eq,n,G.append(~N,prefix,suffix)):
104	  match prefix h:
105	    case Nil{} Tuple{hn,ht}: hn
106	    case Con{+a,+rest} Tuple{ha,ht}: (swapped(~N,~eq,a,n,away_at(~N,~eq,rest,n,suffix,a,ha)),deleted_away(~N,~eq,rest,n,suffix,ht))
107	
108	def first_append(~N: Data, +a: List<&2,N>, +b: List<&2,N>, +q: Maybe<&2,N>) -> {G.first(~N,G.append(~N,a,b),q) == G.first(~N,a,G.first(~N,b,q)) : Maybe<&2,N>}:
109	  match a:
110	    case Nil{}: {==}
111	    case Con{x,rest}: {==}
112	
113	def first_end(~N: Data, +a: List<&2,N>, +n: N, +q: Maybe<&2,N>, +v: Maybe<&2,N>) -> {G.first(~N,G.append(~N,a,Con{n,Nil{}}),q) == G.first(~N,G.append(~N,a,Con{n,Nil{}}),v) : Maybe<&2,N>}:
114	  match a:
115	    case Nil{}: {==}
116	    case Con{x,rest}: {==}
117	
118	def segment_last_next(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +prefix: List<&2,N>, +n: N, +p: Maybe<&2,N>, +q: Maybe<&2,N>, +v: Maybe<&2,N>, +same: {eq(n,n) == True{} : Bool}, unique: G.unique(~N,~eq,G.append(~N,prefix,Con{n,Nil{}})), good: G.segment(~N, ~R, ~P, ~eq,g,p,G.append(~N,prefix,Con{n,Nil{}}),q)) -> G.segment(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),p,G.append(~N,prefix,Con{n,Nil{}}),v):
119	  match prefix unique good:
120	    case Nil{} _ Tuple{hp,Tuple{hn,ht}}:
121	      (Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),n),G.prev(~N, ~R, ~P, ~eq,g,n),p,prev_sn(~N, ~R, ~P, ~eq,g,n,v,n),hp),(next_sn_self(~N, ~R, ~P, ~eq,g,n,v,same),Unit{}))
122	    case Con{+x,+rest} Tuple{away,un} Tuple{hp,Tuple{hn,ht}}:
123	      (Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x),G.prev(~N, ~R, ~P, ~eq,g,x),p,prev_sn(~N, ~R, ~P, ~eq,g,n,v,x),hp),
124	       (Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,v),x),G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,G.append(~N,rest,Con{n,Nil{}}),v),next_sn_other(~N, ~R, ~P, ~eq,g,n,v,x,G.right({eq(x,n) == False{} : Bool},{eq(n,x) == False{} : Bool},away_at(~N,~eq,rest,n,Nil{},x,away))),Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,G.append(~N,rest,Con{n,Nil{}}),q),G.first(~N,G.append(~N,rest,Con{n,Nil{}}),v),hn,first_end(~N,rest,n,q,v))),
125	        segment_last_next(~N, ~R, ~P, ~eq,g,rest,n,Some{x},q,v,same,un,ht)))
126	
127	def segment_join(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +g: G.Graph<N,R,P>, +b: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, ga: G.segment(~N, ~R, ~P, ~eq,g,p,a,G.first(~N,b,q)), gb: G.segment(~N, ~R, ~P, ~eq,g,G.last(~N,a,p),b,q)) -> G.segment(~N, ~R, ~P, ~eq,g,p,G.append(~N,a,b),q):
128	  match a ga:
129	    case Nil{} _: gb
130	    case Con{+x,+rest} Tuple{hp,Tuple{hn,ht}}:
131	      (hp,(Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,rest,G.first(~N,b,q)),G.first(~N,G.append(~N,rest,b),q),hn,Equal.sym(Maybe<&2,N>,G.first(~N,G.append(~N,rest,b),q),G.first(~N,rest,G.first(~N,b,q)),first_append(~N,rest,b,q))),segment_join(~N, ~R, ~P, ~eq,rest,g,b,Some{x},q,ht,gb)))
132	
133	def away_join(~N: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +b: List<&2,N>, +n: N, ga: G.away(~N,~eq,n,a), gb: G.away(~N,~eq,n,b)) -> G.away(~N,~eq,n,G.append(~N,a,b)):
134	  match a ga:
135	    case Nil{} _: gb
136	    case Con{x,rest} Tuple{hx,ht}: (hx,away_join(~N,~eq,rest,b,n,ht,gb))
137	
138	def unique_join(~N: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +b: List<&2,N>, ua: G.unique(~N,~eq,a), +ub: G.unique(~N,~eq,b), dis: G.disjoint(~N,~eq,a,b)) -> G.unique(~N,~eq,G.append(~N,a,b)):
139	  match a ua dis:
140	    case Nil{} _ _: ub
141	    case Con{+x,+rest} Tuple{away,ut} Tuple{ab,dt}: (away_join(~N,~eq,rest,b,x,away,ab),unique_join(~N,~eq,rest,b,ut,ub,dt))
142	
143	def disjoint_last(~N: Data, ~eq: N -> N -> Bool, +prefix: List<&2,N>, +n: N, +suffix: List<&2,N>, dis: G.disjoint(~N,~eq,G.append(~N,prefix,Con{n,Nil{}}),suffix)) -> G.away(~N,~eq,n,suffix):
144	  match prefix dis:
145	    case Nil{} Tuple{a,d}: a
146	    case Con{x,rest} Tuple{a,d}: disjoint_last(~N,~eq,rest,n,suffix,d)
147	
148	def disjoint_head(~N: Data, ~eq: N -> N -> Bool, +prefix: List<&2,N>, +n: N, +suffix: List<&2,N>, dis: G.disjoint(~N,~eq,prefix,Con{n,suffix})) -> G.away(~N,~eq,n,prefix):
149	  match prefix dis:
150	    case Nil{} _: Unit{}
151	    case Con{+x,+rest} Tuple{Tuple{hn,ht},dt}: (swapped(~N,~eq,x,n,hn),disjoint_head(~N,~eq,rest,n,suffix,dt))
152	
153	def last_end(~N: Data, +a: List<&2,N>, +n: N, +p: Maybe<&2,N>) -> {G.last(~N,G.append(~N,a,Con{n,Nil{}}),p) == Some{n} : Maybe<&2,N>}:
154	  match a:
155	    case Nil{}: {==}
156	    case Con{x,rest}: last_end(~N,rest,n,Some{x})
157	
158	# A prefix/suffix split is the ordinary witness for removing a known member.
159	# The following lemmas extract the representation facts from the whole chain.
160	def first_middle(~N: Data, +a: List<&2,N>, +n: N, +b: List<&2,N>, +q: Maybe<&2,N>) -> {G.first(~N,G.append(~N,a,Con{n,b}),q) == G.first(~N,a,Some{n}) : Maybe<&2,N>}:
161	  match a:
162	    case Nil{}: {==}
163	    case Con{x,rest}: {==}
164	
165	def prefix_segment(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +g: G.Graph<N,R,P>, +n: N, +b: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, good: G.segment(~N, ~R, ~P, ~eq,g,p,G.append(~N,a,Con{n,b}),q)) -> G.segment(~N, ~R, ~P, ~eq,g,p,a,Some{n}):
166	  match a good:
167	    case Nil{} _: Unit{}
168	    case Con{+x,+rest} Tuple{hp,Tuple{hn,ht}}:
169	      (hp,(Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,g,x),G.first(~N,G.append(~N,rest,Con{n,b}),q),G.first(~N,rest,Some{n}),hn,first_middle(~N,rest,n,b,q)),prefix_segment(~N, ~R, ~P, ~eq,rest,g,n,b,Some{x},q,ht)))
170	
171	def member_prev(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +g: G.Graph<N,R,P>, +n: N, +b: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, good: G.segment(~N, ~R, ~P, ~eq,g,p,G.append(~N,a,Con{n,b}),q)) -> {G.prev(~N, ~R, ~P, ~eq,g,n) == G.last(~N,a,p) : Maybe<&2,N>}:
172	  match a good:
173	    case Nil{} Tuple{hp,tail}: hp
174	    case Con{x,rest} Tuple{hp,Tuple{hn,ht}}: member_prev(~N, ~R, ~P, ~eq,rest,g,n,b,Some{x},q,ht)
175	
176	def member_next(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +g: G.Graph<N,R,P>, +n: N, +b: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, good: G.segment(~N, ~R, ~P, ~eq,g,p,G.append(~N,a,Con{n,b}),q)) -> {G.next(~N, ~R, ~P, ~eq,g,n) == G.first(~N,b,q) : Maybe<&2,N>}:
177	  match a good:
178	    case Nil{} Tuple{hp,Tuple{hn,ht}}: hn
179	    case Con{x,rest} Tuple{hp,Tuple{hn,ht}}: member_next(~N, ~R, ~P, ~eq,rest,g,n,b,Some{x},q,ht)
180	
181	def suffix_segment(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +g: G.Graph<N,R,P>, +n: N, +b: List<&2,N>, +p: Maybe<&2,N>, +q: Maybe<&2,N>, good: G.segment(~N, ~R, ~P, ~eq,g,p,G.append(~N,a,Con{n,b}),q)) -> G.segment(~N, ~R, ~P, ~eq,g,Some{n},b,q):
182	  match a good:
183	    case Nil{} Tuple{hp,Tuple{hn,ht}}: ht
184	    case Con{x,rest} Tuple{hp,Tuple{hn,ht}}: suffix_segment(~N, ~R, ~P, ~eq,rest,g,n,b,Some{x},q,ht)
185	
186	def head_sn(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +r: R) -> {G.head(~N, ~R, ~P,~req,G.sn(~N, ~R, ~P,g,n,v),r) == G.head(~N, ~R, ~P,~req,g,r) : Maybe<&2,N>}:
187	  match g:
188	    case G.Graph{ns,ps,rs,f}: {==}
189	
190	def head_sp(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>, +r: R) -> {G.head(~N, ~R, ~P,~req,G.sp(~N, ~R, ~P,g,n,v),r) == G.head(~N, ~R, ~P,~req,g,r) : Maybe<&2,N>}:
191	  match g:
192	    case G.Graph{ns,ps,rs,f}: {==}
193	
194	def frame_sn(~N: Data, ~R: Data, ~P: Data, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>) -> {G.frame(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,v)) == G.frame(~N, ~R, ~P,g) : P}:
195	  match g:
196	    case G.Graph{ns,ps,rs,f}: {==}
197	
198	def frame_sp(~N: Data, ~R: Data, ~P: Data, +g: G.Graph<N,R,P>, +n: N, +v: Maybe<&2,N>) -> {G.frame(~N, ~R, ~P,G.sp(~N, ~R, ~P,g,n,v)) == G.frame(~N, ~R, ~P,g) : P}:
199	  match g:
200	    case G.Graph{ns,ps,rs,f}: {==}
201	
202	def frame_sh(~N: Data, ~R: Data, ~P: Data, +g: G.Graph<N,R,P>, +r: R, +v: Maybe<&2,N>) -> {G.frame(~N, ~R, ~P,G.sh(~N, ~R, ~P,g,r,v)) == G.frame(~N, ~R, ~P,g) : P}:
203	  match g:
204	    case G.Graph{ns,ps,rs,f}: {==}
205	
206	def head_sh(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +v: Maybe<&2,N>, +x: R) -> {G.head(~N, ~R, ~P,~req,G.sh(~N, ~R, ~P,g,r,v),x) == G.choose(~Maybe<&2,N>,req(r,x),v,G.head(~N, ~R, ~P,~req,g,x)) : Maybe<&2,N>}:
207	  match g:
208	    case G.Graph{ns,ps,rs,f}: {==}
209	
210	def head_sh_self(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +v: Maybe<&2,N>, same: {req(r,r) == True{} : Bool}) -> {G.head(~N, ~R, ~P,~req,G.sh(~N, ~R, ~P,g,r,v),r) == v : Maybe<&2,N>}:
211	  %Equal.sym(Maybe<&2,N>,G.head(~N, ~R, ~P,~req,G.sh(~N, ~R, ~P,g,r,v),r),G.choose(~Maybe<&2,N>,req(r,r),v,G.head(~N, ~R, ~P,~req,g,r)),head_sh(~N, ~R, ~P,~req,g,r,v,r)) : {_ == v : Maybe<&2,N>}
212	  %Equal.sym(Bool,req(r,r),True{},same) : {G.choose(~Maybe<&2,N>,_,v,G.head(~N, ~R, ~P,~req,g,r)) == v : Maybe<&2,N>}
213	  {==}
214	
215	def head_sh_other(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +v: Maybe<&2,N>, +x: R, neq: {req(r,x) == False{} : Bool}) -> {G.head(~N, ~R, ~P,~req,G.sh(~N, ~R, ~P,g,r,v),x) == G.head(~N, ~R, ~P,~req,g,x) : Maybe<&2,N>}:
216	  %Equal.sym(Maybe<&2,N>,G.head(~N, ~R, ~P,~req,G.sh(~N, ~R, ~P,g,r,v),x),G.choose(~Maybe<&2,N>,req(r,x),v,G.head(~N, ~R, ~P,~req,g,x)),head_sh(~N, ~R, ~P,~req,g,r,v,x)) : {_ == G.head(~N, ~R, ~P,~req,g,x) : Maybe<&2,N>}
217	  %Equal.sym(Bool,req(r,x),False{},neq) : {G.choose(~Maybe<&2,N>,_,v,G.head(~N, ~R, ~P,~req,g,x)) == G.head(~N, ~R, ~P,~req,g,x) : Maybe<&2,N>}
218	  {==}
219	
220	def away_left(~N: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +b: List<&2,N>, +n: N, h: G.away(~N,~eq,n,G.append(~N,a,b))) -> G.away(~N,~eq,n,a):
221	  match a h:
222	    case Nil{} _: Unit{}
223	    case Con{x,rest} Tuple{hx,ht}: (hx,away_left(~N,~eq,rest,b,n,ht))
224	
225	def away_right(~N: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +b: List<&2,N>, +n: N, h: G.away(~N,~eq,n,G.append(~N,a,b))) -> G.away(~N,~eq,n,b):
226	  match a h:
227	    case Nil{} _: h
228	    case Con{x,rest} Tuple{hx,ht}: away_right(~N,~eq,rest,b,n,ht)
229	
230	def unique_left(~N: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +b: List<&2,N>, h: G.unique(~N,~eq,G.append(~N,a,b))) -> G.unique(~N,~eq,a):
231	  match a h:
232	    case Nil{} _: Unit{}
233	    case Con{+x,+rest} Tuple{ax,ut}: (away_left(~N,~eq,rest,b,x,ax),unique_left(~N,~eq,rest,b,ut))
234	
235	def unique_right(~N: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +b: List<&2,N>, h: G.unique(~N,~eq,G.append(~N,a,b))) -> G.unique(~N,~eq,b):
236	  match a h:
237	    case Nil{} _: h
238	    case Con{x,rest} Tuple{ax,ut}: unique_right(~N,~eq,rest,b,ut)
239	
240	def disjoint_unique(~N: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +b: List<&2,N>, h: G.unique(~N,~eq,G.append(~N,a,b))) -> G.disjoint(~N,~eq,a,b):
241	  match a h:
242	    case Nil{} _: Unit{}
243	    case Con{+x,+rest} Tuple{ax,ut}: (away_right(~N,~eq,rest,b,x,ax),disjoint_unique(~N,~eq,rest,b,ut))