1	# A finite half-open interval, represented as its consecutive positions.
2	import Base
3	import ./natural_addition.bend as Addition
4	import ../ordered_matrix.bend as OrderedMatrix
5	
6	def range(n: Nat,+start: Nat) -> List<&2,Nat>:
7	  match n:
8	    case 0n:
9	      []
10	    case 1n+rest:
11	      start <> range(rest,1n+start)
12	
13	def split(+a: Nat,+b: Nat,+start: Nat) -> {range(Nat.add(a,b),start) == OrderedMatrix.cat(Nat,range(a,start),range(b,Nat.add(start,
14	        a))) : List<&2,Nat>}:
15	  match a:
16	    case 0n:
17	      %Equal.sym(Nat,Nat.add(start,0n),start,Addition.zero_right(start)) : {range(b,start) == range(b,_) : List<&2,Nat>}
18	      {==}
19	    case 1n+ +p:
20	      %Equal.sym(Nat,Nat.add(start,1n+p),1n+Nat.add(start,p),Addition.successor_right(start,p)) : {start <> range(Nat.add(p,b),
21	          1n+start) == start <> OrderedMatrix.cat(Nat,range(p,1n+start),range(b,_)) : List<&2,Nat>}
22	      %split(p,b,1n+start) : {start <> range(Nat.add(p,b),1n+start) == start <> _ : List<&2,Nat>}
23	      {==}
24	
25	# [start, end) followed by [end, start + whole) is the whole interval.
26	def join(+start: Nat,+left: Nat,+right: Nat,+end: Nat,+whole: Nat,end_exact: {end == Nat.add(start,left) : Nat},size_exact: {Nat.add(left,
27	      right) == whole : Nat}) -> {OrderedMatrix.cat(Nat,range(left,start),range(right,end)) == range(whole,start) : List<&2,Nat>}:
28	  %size_exact : {OrderedMatrix.cat(Nat,range(left,start),range(right,end)) == range(_,start) : List<&2,Nat>}
29	  %Equal.sym(Nat,end,Nat.add(start,left),end_exact) : {OrderedMatrix.cat(Nat,range(left,start),range(right,_)) == range(Nat.add(left,right),
30	      start) : List<&2,Nat>}
31	  Equal.sym(List<&2,Nat>,range(Nat.add(left,right),start),OrderedMatrix.cat(Nat,range(left,start),range(right,Nat.add(start,left))),split(left,
32	      right,start))