1	# bend-mathlib/sort.bend: insertion and merge sort proved sorted over perm.bend's value defs (generic ~le).
2	import Base
3	import ./nat.bend as MNat
4	import ./list.bend as MList
5	import ./perm.bend as MPerm
6	
7	def internal_sorted_single(~A: Data, ~le: A -> A -> Bool, +x: A) -> MList.sorted_by(~A, ~le, x <> Nil{}):
8	  {==}
9	
10	def internal_sorted_cons_cons_intro(~A: Data, ~le: A -> A -> Bool, +x: A, +y: A, +t: List<&2, A>, hxy: {le(x, y) == True{} : Bool}, hyt: MList.sorted_by(~A, ~le, y <> t)) -> MList.sorted_by(~A, ~le, x <> y <> t):
11	  %Equal.sym(Bool, le(x, y), True{}, hxy) : {Bool.and(_, List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), List.zip(&2, A, &2, A, y <> t, t))) == True{} : Bool}
12	  hyt
13	
14	def internal_sorted_cons_cons_elim_le(~A: Data, ~le: A -> A -> Bool, +x: A, +y: A, +t: List<&2, A>, h: MList.sorted_by(~A, ~le, x <> y <> t)) -> {le(x, y) == True{} : Bool}:
15	  MList.internal_and_left(le(x, y), List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), List.zip(&2, A, &2, A, y <> t, t)), h)
16	
17	def internal_sorted_cons_cons_elim_tail(~A: Data, ~le: A -> A -> Bool, +x: A, +y: A, +t: List<&2, A>, h: MList.sorted_by(~A, ~le, x <> y <> t)) -> MList.sorted_by(~A, ~le, y <> t):
18	  MList.internal_and_right(le(x, y), List.all(~&1, ~(A & A), ~(p => le(Pair.fst(A, A, p), Pair.snd(A, A, p))), List.zip(&2, A, &2, A, y <> t, t)), h)
19	
20	def internal_sorted_tail(~A: Data, ~le: A -> A -> Bool, +x: A, +xs: List<&2, A>, h: MList.sorted_by(~A, ~le, x <> xs)) -> MList.sorted_by(~A, ~le, xs):
21	  match xs:
22	    case Nil{}:
23	      {==}
24	    case +y <> +t:
25	      internal_sorted_cons_cons_elim_tail(~A, ~le, x, y, t, h)
26	
27	def internal_le_flip_nat(x: Nat, y: Nat, e: {Nat.is_le(x, y) == False{} : Bool}) -> {Nat.is_le(y, x) == True{} : Bool}:
28	  match x y:
29	    case 0n 0n:
30	      Empty.absurd({True{} == True{} : Bool}, MNat.internal_false_ne_true(Equal.sym(Bool, True{}, False{}, e)))
31	    case 0n 1n+q:
32	      Empty.absurd({Nat.is_le(1n+q, 0n) == True{} : Bool}, MNat.internal_false_ne_true(Equal.sym(Bool, True{}, False{}, e)))
33	    case 1n+p 0n:
34	      {==}
35	    case 1n+p 1n+q:
36	      internal_le_flip_nat(p, q, e)
37	
38	def internal_le_trans_nat(x: Nat, y: Nat, z: Nat, xy: {Nat.is_le(x, y) == True{} : Bool}, yz: {Nat.is_le(y, z) == True{} : Bool}) -> {Nat.is_le(x, z) == True{} : Bool}:
39	  MNat.le_trans(x, y, z, xy, yz)
40	
41	def internal_cons_ins_step(~A: Data, ~le: A -> A -> Bool, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, b: Bool, +y: A, +x: A, +z: A, +u: List<&2, A>, e: {le(x, z) == b : Bool}, hyx: {le(y, x) == True{} : Bool}, +h: MList.sorted_by(~A, ~le, y <> z <> u), k: {le(z, x) == True{} : Bool} -> MList.sorted_by(~A, ~le, z <> MPerm.insert_by(~A, ~le, x, u))) -> MList.sorted_by(~A, ~le, y <> Bool.pick(List<&2, A>, b, x <> z <> u, z <> MPerm.insert_by(~A, ~le, x, u))):
42	  match b:
43	    case True{}:
44	      internal_sorted_cons_cons_intro(~A, ~le, y, x, z <> u, hyx, internal_sorted_cons_cons_intro(~A, ~le, x, z, u, e, internal_sorted_cons_cons_elim_tail(~A, ~le, y, z, u, h)))
45	    case False{}:
46	      internal_sorted_cons_cons_intro(~A, ~le, y, z, MPerm.insert_by(~A, ~le, x, u), internal_sorted_cons_cons_elim_le(~A, ~le, y, z, u, h), k(le_total(x, z, e)))
47	
48	def internal_sorted_cons_ins(~A: Data, ~le: A -> A -> Bool, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, +t: List<&2, A>, +y: A, +x: A, hyx: {le(y, x) == True{} : Bool}, +h: MList.sorted_by(~A, ~le, y <> t)) -> MList.sorted_by(~A, ~le, y <> MPerm.insert_by(~A, ~le, x, t)):
49	  match t:
50	    case Nil{}:
51	      internal_sorted_cons_cons_intro(~A, ~le, y, x, Nil{}, hyx, internal_sorted_single(~A, ~le, x))
52	    case +z <> +u:
53	      internal_cons_ins_step(~A, ~le, ~le_total, le(x, z), y, x, z, u, {==}, hyx, h, hzx => internal_sorted_cons_ins(~A, ~le, ~le_total, u, z, x, hzx, internal_sorted_cons_cons_elim_tail(~A, ~le, y, z, u, h)))
54	
55	def internal_insert_step(~A: Data, ~le: A -> A -> Bool, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, b: Bool, +x: A, +y: A, +t: List<&2, A>, e: {le(x, y) == b : Bool}, +h: MList.sorted_by(~A, ~le, y <> t)) -> MList.sorted_by(~A, ~le, Bool.pick(List<&2, A>, b, x <> y <> t, y <> MPerm.insert_by(~A, ~le, x, t))):
56	  match b:
57	    case True{}:
58	      internal_sorted_cons_cons_intro(~A, ~le, x, y, t, e, h)
59	    case False{}:
60	      internal_sorted_cons_ins(~A, ~le, ~le_total, t, y, x, le_total(x, y, e), h)
61	
62	def insert_by_sorted(~A: Data, ~le: A -> A -> Bool, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, +x: A, +xs: List<&2, A>, +h: MList.sorted_by(~A, ~le, xs)) -> MList.sorted_by(~A, ~le, MPerm.insert_by(~A, ~le, x, xs)):
63	  match xs:
64	    case Nil{}:
65	      internal_sorted_single(~A, ~le, x)
66	    case +y <> t:
67	      internal_insert_step(~A, ~le, ~le_total, le(x, y), x, y, t, {==}, h)
68	
69	# Insertion sort returns a sorted list.
70	def isort_by_sorted(~A: Data, ~le: A -> A -> Bool, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, +xs: List<&2, A>) -> MList.sorted_by(~A, ~le, MPerm.isort_by(~A, ~le, xs)):
71	  match xs:
72	    case Nil{}:
73	      {==}
74	    case +x <> t:
75	      insert_by_sorted(~A, ~le, ~le_total, x, MPerm.isort_by(~A, ~le, t), isort_by_sorted(~A, ~le, ~le_total, t))
76	
77	def isort_by_sorted_nat(+xs: List<&2, Nat>) -> MList.sorted_by(~Nat, ~Nat.is_le, MPerm.isort_by(~Nat, ~Nat.is_le, xs)):
78	  isort_by_sorted(~Nat, ~Nat.is_le, ~internal_le_flip_nat, xs)
79	
80	def internal_least(~A: Data, ~le: A -> A -> Bool, +lo: A, +xs: List<&2, A>) -> Data:
81	  {List.all(~&2, ~A, ~(y => le(lo, y)), xs) == True{} : Bool}
82	
83	def internal_least_intro(~A: Data, ~le: A -> A -> Bool, +lo: A, +h: A, +t: List<&2, A>, hh: {le(lo, h) == True{} : Bool}, ht: internal_least(~A, ~le, lo, t)) -> internal_least(~A, ~le, lo, h <> t):
84	  %Equal.sym(Bool, le(lo, h), True{}, hh) : {Bool.and(_, List.all(~&2, ~A, ~(y => le(lo, y)), t)) == True{} : Bool}
85	  ht
86	
87	def internal_least_cons_le(~A: Data, ~le: A -> A -> Bool, +lo: A, +h: A, +t: List<&2, A>, hh: internal_least(~A, ~le, lo, h <> t)) -> {le(lo, h) == True{} : Bool}:
88	  MList.internal_and_left(le(lo, h), List.all(~&2, ~A, ~(y => le(lo, y)), t), hh)
89	
90	def internal_least_cons_tail(~A: Data, ~le: A -> A -> Bool, +lo: A, +h: A, +t: List<&2, A>, hh: internal_least(~A, ~le, lo, h <> t)) -> internal_least(~A, ~le, lo, t):
91	  MList.internal_and_right(le(lo, h), List.all(~&2, ~A, ~(y => le(lo, y)), t), hh)
92	
93	def internal_least_trans(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, +a: A, +b: A, +xs: List<&2, A>, +hab: {le(a, b) == True{} : Bool}, +hb: internal_least(~A, ~le, b, xs)) -> internal_least(~A, ~le, a, xs):
94	  match xs:
95	    case Nil{}:
96	      {==}
97	    case +h <> +t:
98	      internal_least_intro(~A, ~le, a, h, t, le_trans(a, b, h, hab, internal_least_cons_le(~A, ~le, b, h, t, hb)), internal_least_trans(~A, ~le, ~le_trans, a, b, t, hab, internal_least_cons_tail(~A, ~le, b, h, t, hb)))
99	
100	def internal_sorted_least_head(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, +xs: List<&2, A>, +x: A, +h: MList.sorted_by(~A, ~le, x <> xs)) -> internal_least(~A, ~le, x, xs):
101	  match xs:
102	    case Nil{}:
103	      {==}
104	    case +y <> +t:
105	      internal_least_intro(~A, ~le, x, y, t, internal_sorted_cons_cons_elim_le(~A, ~le, x, y, t, h), internal_least_trans(~A, ~le, ~le_trans, x, y, t, internal_sorted_cons_cons_elim_le(~A, ~le, x, y, t, h), internal_sorted_least_head(~A, ~le, ~le_trans, t, y, internal_sorted_cons_cons_elim_tail(~A, ~le, x, y, t, h))))
106	
107	def internal_sorted_cons_of_least(~A: Data, ~le: A -> A -> Bool, +lo: A, +m: List<&2, A>, hl: internal_least(~A, ~le, lo, m), hm: MList.sorted_by(~A, ~le, m)) -> MList.sorted_by(~A, ~le, lo <> m):
108	  match m:
109	    case Nil{}:
110	      {==}
111	    case +z <> +t:
112	      internal_sorted_cons_cons_intro(~A, ~le, lo, z, t, internal_least_cons_le(~A, ~le, lo, z, t, hl), hm)
113	
114	def internal_least_merge_pick(~A: Data, ~le: A -> A -> Bool, +lo: A, b: Bool, +x: A, +xt: List<&2, A>, +y: A, +yt: List<&2, A>, hx: internal_least(~A, ~le, lo, x <> xt), hy: internal_least(~A, ~le, lo, y <> yt), hm1: internal_least(~A, ~le, lo, MPerm.merge_by(~A, ~le, xt, y <> yt)), hm2: internal_least(~A, ~le, lo, MPerm.merge_by(~A, ~le, x <> xt, yt))) -> internal_least(~A, ~le, lo, Bool.pick(List<&2, A>, b, x <> MPerm.merge_by(~A, ~le, xt, y <> yt), y <> MPerm.merge_by(~A, ~le, x <> xt, yt))):
115	  match b:
116	    case True{}:
117	      internal_least_intro(~A, ~le, lo, x, MPerm.merge_by(~A, ~le, xt, y <> yt), internal_least_cons_le(~A, ~le, lo, x, xt, hx), hm1)
118	    case False{}:
119	      internal_least_intro(~A, ~le, lo, y, MPerm.merge_by(~A, ~le, x <> xt, yt), internal_least_cons_le(~A, ~le, lo, y, yt, hy), hm2)
120	
121	def internal_least_merge(~A: Data, ~le: A -> A -> Bool, +lo: A, +xs: List<&2, A>, +ys: List<&2, A>, +hx: internal_least(~A, ~le, lo, xs), +hy: internal_least(~A, ~le, lo, ys)) -> internal_least(~A, ~le, lo, MPerm.merge_by(~A, ~le, xs, ys)):
122	  match xs ys:
123	    case Nil{} _:
124	      hy
125	    case +x <> +xt Nil{}:
126	      hx
127	    case +x <> +xt +y <> +yt:
128	      internal_least_merge_pick(~A, ~le, lo, le(x, y), x, xt, y, yt, hx, hy, internal_least_merge(~A, ~le, lo, xt, y <> yt, internal_least_cons_tail(~A, ~le, lo, x, xt, hx), hy), internal_least_merge(~A, ~le, lo, x <> xt, yt, hx, internal_least_cons_tail(~A, ~le, lo, y, yt, hy)))
129	
130	def internal_merge_sorted_pick(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, b: Bool, +x: A, +xt: List<&2, A>, +y: A, +yt: List<&2, A>, +e: {le(x, y) == b : Bool}, hx: MList.sorted_by(~A, ~le, x <> xt), hy: MList.sorted_by(~A, ~le, y <> yt), hm1: MList.sorted_by(~A, ~le, MPerm.merge_by(~A, ~le, xt, y <> yt)), hm2: MList.sorted_by(~A, ~le, MPerm.merge_by(~A, ~le, x <> xt, yt))) -> MList.sorted_by(~A, ~le, Bool.pick(List<&2, A>, b, x <> MPerm.merge_by(~A, ~le, xt, y <> yt), y <> MPerm.merge_by(~A, ~le, x <> xt, yt))):
131	  match b:
132	    case True{}:
133	      internal_sorted_cons_of_least(~A, ~le, x, MPerm.merge_by(~A, ~le, xt, y <> yt), internal_least_merge(~A, ~le, x, xt, y <> yt, internal_sorted_least_head(~A, ~le, ~le_trans, xt, x, hx), internal_least_intro(~A, ~le, x, y, yt, e, internal_least_trans(~A, ~le, ~le_trans, x, y, yt, e, internal_sorted_least_head(~A, ~le, ~le_trans, yt, y, hy)))), hm1)
134	    case False{}:
135	      internal_sorted_cons_of_least(~A, ~le, y, MPerm.merge_by(~A, ~le, x <> xt, yt), internal_least_merge(~A, ~le, y, x <> xt, yt, internal_least_intro(~A, ~le, y, x, xt, le_total(x, y, e), internal_least_trans(~A, ~le, ~le_trans, y, x, xt, le_total(x, y, e), internal_sorted_least_head(~A, ~le, ~le_trans, xt, x, hx))), internal_sorted_least_head(~A, ~le, ~le_trans, yt, y, hy)), hm2)
136	
137	# Merging two sorted lists is sorted (needs transitivity, and totality for the un-taken branch).
138	def merge_by_sorted(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, +xs: List<&2, A>, +ys: List<&2, A>, +hx: MList.sorted_by(~A, ~le, xs), +hy: MList.sorted_by(~A, ~le, ys)) -> MList.sorted_by(~A, ~le, MPerm.merge_by(~A, ~le, xs, ys)):
139	  match xs ys:
140	    case Nil{} _:
141	      hy
142	    case +x <> +xt Nil{}:
143	      hx
144	    case +x <> +xt +y <> +yt:
145	      internal_merge_sorted_pick(~A, ~le, ~le_trans, ~le_total, le(x, y), x, xt, y, yt, {==}, hx, hy, merge_by_sorted(~A, ~le, ~le_trans, ~le_total, xt, y <> yt, internal_sorted_tail(~A, ~le, x, xt, hx), hy), merge_by_sorted(~A, ~le, ~le_trans, ~le_total, x <> xt, yt, hx, internal_sorted_tail(~A, ~le, y, yt, hy)))
146	
147	def merge_by_sorted_nat(+xs: List<&2, Nat>, +ys: List<&2, Nat>, hx: MList.sorted_by(~Nat, ~Nat.is_le, xs), hy: MList.sorted_by(~Nat, ~Nat.is_le, ys)) -> MList.sorted_by(~Nat, ~Nat.is_le, MPerm.merge_by(~Nat, ~Nat.is_le, xs, ys)):
148	  merge_by_sorted(~Nat, ~Nat.is_le, ~internal_le_trans_nat, ~internal_le_flip_nat, xs, ys, hx, hy)
149	
150	def internal_length_zero(~A: Data, +xs: List<&2, A>, e: {List.length(&2, A, xs) == 0n : Nat}) -> {xs == Nil{} : List<&2, A>}:
151	  match xs:
152	    case Nil{}:
153	      {==}
154	    case +x <> +t:
155	      Empty.absurd({x <> t == Nil{} : List<&2, A>}, MNat.zero_ne_succ(List.length(&2, A, t), Equal.sym(Nat, List.length(&2, A, x <> t), 0n, e)))
156	
157	def internal_sorted_short(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>, h: MNat.le(List.length(&2, A, xs), 1n)) -> MList.sorted_by(~A, ~le, xs):
158	  match xs:
159	    case Nil{}:
160	      {==}
161	    case +x <> +t:
162	      match t:
163	        case Nil{}:
164	          internal_sorted_single(~A, ~le, x)
165	        case +y <> +u:
166	          %Equal.sym(List<&2, A>, t, Nil{}, internal_length_zero(~A, t, MNat.le_zero_eq(List.length(&2, A, t), MNat.le_of_succ_le_succ(List.length(&2, A, t), 0n, h)))) : {MList.sorted_by(~A, ~le, x <> _) : Data}
167	          internal_sorted_single(~A, ~le, x)
168	
169	def internal_length_evens_le(~A: Data, +xs: List<&2, A>) -> {Nat.is_le(List.length(&2, A, MPerm.evens(A, xs)), List.length(&2, A, xs)) == True{} : Bool}:
170	  match xs:
171	    case Nil{}:
172	      {==}
173	    case +x <> +r:
174	      match r:
175	        case Nil{}:
176	          {==}
177	        case +y <> +t:
178	          MNat.succ_le_succ(List.length(&2, A, MPerm.evens(A, t)), 1n+List.length(&2, A, t), MNat.le_trans(List.length(&2, A, MPerm.evens(A, t)), List.length(&2, A, t), 1n+List.length(&2, A, t), internal_length_evens_le(~A, t), MNat.le_succ(List.length(&2, A, t))))
179	
180	def internal_length_odds_le(~A: Data, +xs: List<&2, A>) -> {Nat.is_le(List.length(&2, A, MPerm.odds(A, xs)), List.length(&2, A, xs)) == True{} : Bool}:
181	  match xs:
182	    case Nil{}:
183	      {==}
184	    case +x <> +r:
185	      match r:
186	        case Nil{}:
187	          {==}
188	        case +y <> +t:
189	          MNat.succ_le_succ(List.length(&2, A, MPerm.odds(A, t)), 1n+List.length(&2, A, t), MNat.le_trans(List.length(&2, A, MPerm.odds(A, t)), List.length(&2, A, t), 1n+List.length(&2, A, t), internal_length_odds_le(~A, t), MNat.le_succ(List.length(&2, A, t))))
190	
191	def internal_least_evens(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>, +lo: A, +h: internal_least(~A, ~le, lo, xs)) -> internal_least(~A, ~le, lo, MPerm.evens(A, xs)):
192	  match xs:
193	    case Nil{}:
194	      {==}
195	    case +x <> +r:
196	      match r:
197	        case Nil{}:
198	          h
199	        case +y <> +t:
200	          internal_least_intro(~A, ~le, lo, x, MPerm.evens(A, t), internal_least_cons_le(~A, ~le, lo, x, r, h), internal_least_evens(~A, ~le, t, lo, internal_least_cons_tail(~A, ~le, lo, y, t, internal_least_cons_tail(~A, ~le, lo, x, r, h))))
201	
202	def internal_least_odds(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>, +lo: A, +h: internal_least(~A, ~le, lo, xs)) -> internal_least(~A, ~le, lo, MPerm.odds(A, xs)):
203	  match xs:
204	    case Nil{}:
205	      {==}
206	    case +x <> +r:
207	      match r:
208	        case Nil{}:
209	          {==}
210	        case +y <> +t:
211	          internal_least_intro(~A, ~le, lo, y, MPerm.odds(A, t), internal_least_cons_le(~A, ~le, lo, y, t, internal_least_cons_tail(~A, ~le, lo, x, r, h)), internal_least_odds(~A, ~le, t, lo, internal_least_cons_tail(~A, ~le, lo, y, t, internal_least_cons_tail(~A, ~le, lo, x, r, h))))
212	
213	def internal_evens_sorted(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, +xs: List<&2, A>, +h: MList.sorted_by(~A, ~le, xs)) -> MList.sorted_by(~A, ~le, MPerm.evens(A, xs)):
214	  match xs:
215	    case Nil{}:
216	      {==}
217	    case +x <> +r:
218	      match r:
219	        case Nil{}:
220	          h
221	        case +y <> +t:
222	          internal_sorted_cons_of_least(~A, ~le, x, MPerm.evens(A, t), internal_least_evens(~A, ~le, t, x, internal_least_cons_tail(~A, ~le, x, y, t, internal_sorted_least_head(~A, ~le, ~le_trans, y <> t, x, h))), internal_evens_sorted(~A, ~le, ~le_trans, t, internal_sorted_tail(~A, ~le, y, t, internal_sorted_cons_cons_elim_tail(~A, ~le, x, y, t, h))))
223	
224	def internal_odds_sorted(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, +xs: List<&2, A>, +h: MList.sorted_by(~A, ~le, xs)) -> MList.sorted_by(~A, ~le, MPerm.odds(A, xs)):
225	  match xs:
226	    case Nil{}:
227	      {==}
228	    case +x <> +r:
229	      match r:
230	        case Nil{}:
231	          {==}
232	        case +y <> +t:
233	          internal_sorted_cons_of_least(~A, ~le, y, MPerm.odds(A, t), internal_least_odds(~A, ~le, t, y, internal_sorted_least_head(~A, ~le, ~le_trans, t, y, internal_sorted_cons_cons_elim_tail(~A, ~le, x, y, t, h))), internal_odds_sorted(~A, ~le, ~le_trans, t, internal_sorted_tail(~A, ~le, y, t, internal_sorted_cons_cons_elim_tail(~A, ~le, x, y, t, h))))
234	
235	# Merge sort returns a sorted list once the fuel reaches the input length (invariant: length <= fuel+1).
236	def msort_by_sorted(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, fuel: Nat, +xs: List<&2, A>, +h: {Nat.is_le(List.length(&2, A, xs), 1n+fuel) == True{} : Bool}) -> MList.sorted_by(~A, ~le, MPerm.msort_by(~A, ~le, fuel, xs)):
237	  match fuel:
238	    case 0n:
239	      internal_sorted_short(~A, ~le, xs, h)
240	    case 1n++f:
241	      match xs:
242	        case Nil{}:
243	          merge_by_sorted(~A, ~le, ~le_trans, ~le_total, MPerm.msort_by(~A, ~le, f, MPerm.evens(A, xs)), MPerm.msort_by(~A, ~le, f, MPerm.odds(A, xs)), msort_by_sorted(~A, ~le, ~le_trans, ~le_total, f, MPerm.evens(A, xs), MNat.zero_le(1n+f)), msort_by_sorted(~A, ~le, ~le_trans, ~le_total, f, MPerm.odds(A, xs), MNat.zero_le(1n+f)))
244	        case +x <> +r:
245	          match r:
246	            case Nil{}:
247	              merge_by_sorted(~A, ~le, ~le_trans, ~le_total, MPerm.msort_by(~A, ~le, f, MPerm.evens(A, x <> r)), MPerm.msort_by(~A, ~le, f, MPerm.odds(A, x <> r)), msort_by_sorted(~A, ~le, ~le_trans, ~le_total, f, MPerm.evens(A, x <> r), MNat.le_add_right(1n, f)), msort_by_sorted(~A, ~le, ~le_trans, ~le_total, f, MPerm.odds(A, x <> r), MNat.zero_le(1n+f)))
248	            case +y <> +t:
249	              merge_by_sorted(~A, ~le, ~le_trans, ~le_total, MPerm.msort_by(~A, ~le, f, MPerm.evens(A, x <> y <> t)), MPerm.msort_by(~A, ~le, f, MPerm.odds(A, x <> y <> t)), msort_by_sorted(~A, ~le, ~le_trans, ~le_total, f, MPerm.evens(A, x <> y <> t), MNat.succ_le_succ(List.length(&2, A, MPerm.evens(A, t)), f, MNat.le_trans(List.length(&2, A, MPerm.evens(A, t)), List.length(&2, A, t), f, internal_length_evens_le(~A, t), MNat.le_of_succ_le_succ(List.length(&2, A, t), f, MNat.le_of_succ_le_succ(1n+List.length(&2, A, t), 1n+f, h))))), msort_by_sorted(~A, ~le, ~le_trans, ~le_total, f, MPerm.odds(A, x <> y <> t), MNat.succ_le_succ(List.length(&2, A, MPerm.odds(A, t)), f, MNat.le_trans(List.length(&2, A, MPerm.odds(A, t)), List.length(&2, A, t), f, internal_length_odds_le(~A, t), MNat.le_of_succ_le_succ(List.length(&2, A, t), f, MNat.le_of_succ_le_succ(1n+List.length(&2, A, t), 1n+f, h))))))
250	
251	# Merge sort of the full-length fuel sorts its input.
252	def sort_by_sorted(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, +xs: List<&2, A>) -> MList.sorted_by(~A, ~le, MPerm.sort_by(~A, ~le, xs)):
253	  match xs:
254	    case Nil{}:
255	      {==}
256	    case +x <> +t:
257	      msort_by_sorted(~A, ~le, ~le_trans, ~le_total, 1n+List.length(&2, A, t), x <> t, MNat.le_succ(1n+List.length(&2, A, t)))
258	
259	def msort_by_sorted_nat(+xs: List<&2, Nat>, +h: {Nat.is_le(List.length(&2, Nat, xs), 1n+List.length(&2, Nat, xs)) == True{} : Bool}) -> MList.sorted_by(~Nat, ~Nat.is_le, MPerm.msort_by(~Nat, ~Nat.is_le, List.length(&2, Nat, xs), xs)):
260	  msort_by_sorted(~Nat, ~Nat.is_le, ~internal_le_trans_nat, ~internal_le_flip_nat, List.length(&2, Nat, xs), xs, h)
261	
262	def sort_by_sorted_nat(+xs: List<&2, Nat>) -> MList.sorted_by(~Nat, ~Nat.is_le, MPerm.sort_by(~Nat, ~Nat.is_le, xs)):
263	  sort_by_sorted(~Nat, ~Nat.is_le, ~internal_le_trans_nat, ~internal_le_flip_nat, xs)