1	# Finite list writes preserve earlier addresses and read back every list item.
2	# Allocation bounds come from the real public count, never example shapes.
3	import Base
4	import ./storage_tree_model.bend as Tree
5	import ./storage_shape.bend as Shape
6	import ./storage_readback.bend as Readback
7	import ./u32_full_range.bend as FullRange
8	import ./u32_comparison.bend as Comparison
9	import ./natural_addition.bend as Addition
10	import ./nat_order.bend as Order
11	import ./nat_to_u32_bounds.bend as Bounds
12	import ./word_encoding.bend as Words
13	import ./nat_interval.bend as Interval
14	import ./nat_division.bend as Division
15	import ./loop_projection.bend as Projection
16	import ./bounded_u32_arithmetic.bend as NativeArithmetic
17	
18	def end_position(~Element: Data,values: List<&2,Element>,offset: U32) -> U32:
19	  match values:
20	    case Nil{}: offset
21	    case head <> rest: end_position(~Element,rest,(offset + 1 : U32))
22	
23	def end_position_length(~Element: Data,values: List<&2,Element>,+offset: U32) ->
24	  {end_position(~Element,values,offset) == (offset + U32.from_nat(List.length(&2,Element,values)) : U32) : U32}:
25	  match values:
26	    case Nil{}: Equal.sym(U32,(offset + 0 : U32),offset,NativeArithmetic.add_zero(offset))
27	    case head <> +rest:
28	      Equal.trans(U32,end_position(~Element,rest,(offset + 1 : U32)),((offset + 1 : U32) + U32.from_nat(List.length(&2,Element,rest)) : U32),
29	        (offset + U32.from_nat(1n+List.length(&2,Element,rest)) : U32),end_position_length(~Element,rest,(offset + 1 : U32)),
30	        Equal.sym(U32,(offset + U32.from_nat(1n+List.length(&2,Element,rest)) : U32),((offset + 1 : U32) + U32.from_nat(List.length(&2,Element,rest)) : U32),
31	          Projection.indexed_successor(offset,List.length(&2,Element,rest))))
32	
33	def append_length(~Element: Data,left: List<&2,Element>,+right: List<&2,Element>) ->
34	  {List.length(&2,Element,List.append(&2,Element,left,right)) == Nat.add(List.length(&2,Element,left),List.length(&2,Element,right)) : Nat}:
35	  match left:
36	    case Nil{}: {==}
37	    case head <> +rest:
38	      %append_length(~Element,rest,right) : {1n+List.length(&2,Element,List.append(&2,Element,rest,right)) == 1n+_ : Nat}
39	      {==}
40	
41	def concatenated(~Element: Data,+first: List<&2,Element>,+second: List<&2,Element>,+offset: U32,+tree: Tree.Tree<Element>) ->
42	  {Tree.write_sequence(~Element,List.append(&2,Element,first,second),offset,tree) ==
43	    Tree.write_sequence(~Element,second,end_position(~Element,first,offset),Tree.write_sequence(~Element,first,offset,tree)) : Tree.Tree<Element>}:
44	  match first:
45	    case Nil{}: {==}
46	    case +head <> +rest: concatenated(~Element,rest,second,(offset + 1 : U32),Tree.write(Element,tree,offset,head))
47	
48	def at(~Element: Data,+fallback: Element,index: Nat,values: List<&2,Element>) -> Element:
49	  match index values:
50	    case 0n Nil{}: fallback
51	    case 0n head <> tail: head
52	    case 1n+rest Nil{}: fallback
53	    case 1n+rest head <> tail: at(~Element,fallback,rest,tail)
54	
55	# Generic ordered enumeration; the parameter bridge keeps its F32 wrappers.
56	def enumerate(~Element: Data,~Context: Data,~value: Context -> Nat -> Element,remaining: Nat,+first: Nat,+context: Context) -> List<&2,Element>:
57	  match remaining:
58	    case 0n: []
59	    case 1n+rest: value(context,first) <> enumerate(~Element,~Context,~value,rest,1n+first,context)
60	
61	def enumerate_length(~Element: Data,~Context: Data,~value: Context -> Nat -> Element,remaining: Nat,+first: Nat,+context: Context) -> {List.length(&2,Element,enumerate(~Element,~Context,~value,remaining,first,context)) == remaining : Nat}:
62	  match remaining:
63	    case 0n: {==}
64	    case 1n+ +rest:
65	      %enumerate_length(~Element,~Context,~value,rest,1n+first,context) : {1n+List.length(&2,Element,enumerate(~Element,~Context,~value,rest,1n+first,context)) == 1n+_ : Nat}
66	      {==}
67	
68	def enumerate_at(~Element: Data,~Context: Data,~value: Context -> Nat -> Element,+fallback: Element,remaining: Nat,index: Nat,+first: Nat,+context: Context,within: {Nat.is_lt(index,remaining) == True{} : Bool}) ->
69	  {at(~Element,fallback,index,enumerate(~Element,~Context,~value,remaining,first,context)) == value(context,Nat.add(first,index)) : Element}:
70	  match remaining index:
71	    case 0n 0n: Empty.absurd({fallback == value(context,Nat.add(first,0n)) : Element},Words.false_true(within))
72	    case 0n 1n+index: Empty.absurd({fallback == value(context,Nat.add(first,1n+index)) : Element},Words.false_true(within))
73	    case 1n+rest 0n:
74	      %Equal.sym(Nat,Nat.add(first,0n),first,Addition.zero_right(first)) : {value(context,first) == value(context,_) : Element}
75	      {==}
76	    case 1n+ +rest 1n+ +previous:
77	      %Equal.sym(Nat,Nat.add(first,1n+previous),1n+Nat.add(first,previous),Addition.successor_right(first,previous)) : {at(~Element,fallback,previous,enumerate(~Element,~Context,~value,rest,1n+first,context)) == value(context,_) : Element}
78	      enumerate_at(~Element,~Context,~value,fallback,rest,previous,1n+first,context,within)
79	
80	def inside(+index: Nat,+capacity: U32,+bound: {Nat.is_lt(index,U32.to_nat(capacity)) == True{} : Bool}) -> {U32.is_lt(U32.from_nat(index),capacity) == True{} : Bool}:
81	  %Equal.sym(Bool,U32.is_lt(U32.from_nat(index),capacity),Nat.is_lt(U32.to_nat(U32.from_nat(index)),U32.to_nat(capacity)),Comparison.lt(U32.from_nat(index),capacity)) : {_ == True{} : Bool}
82	  %Equal.sym(Nat,U32.to_nat(U32.from_nat(index)),index,FullRange.roundtrip(index,capacity,Bounds.strict_le(index,U32.to_nat(capacity),bound))) : {Nat.is_lt(_,U32.to_nat(capacity)) == True{} : Bool}
83	  bound
84	
85	def distinct(+first: Nat,+second: Nat,+capacity: U32,+first_bound: {Nat.is_lt(first,U32.to_nat(capacity)) == True{} : Bool},+second_bound: {Nat.is_lt(second,U32.to_nat(capacity)) == True{} : Bool},ordered: {Nat.is_lt(second,first) == True{} : Bool}) -> {U32.is_eq(U32.from_nat(first),U32.from_nat(second)) == False{} : Bool}:
86	  %Equal.sym(Bool,U32.is_eq(U32.from_nat(first),U32.from_nat(second)),Nat.is_eq(U32.to_nat(U32.from_nat(first)),U32.to_nat(U32.from_nat(second))),Comparison.eq(U32.from_nat(first),U32.from_nat(second))) : {_ == False{} : Bool}
87	  %Equal.sym(Nat,U32.to_nat(U32.from_nat(first)),first,FullRange.roundtrip(first,capacity,Bounds.strict_le(first,U32.to_nat(capacity),first_bound))) : {Nat.is_eq(_,U32.to_nat(U32.from_nat(second))) == False{} : Bool}
88	  %Equal.sym(Nat,U32.to_nat(U32.from_nat(second)),second,FullRange.roundtrip(second,capacity,Bounds.strict_le(second,U32.to_nat(capacity),second_bound))) : {Nat.is_eq(first,_) == False{} : Bool}
89	  %Equal.sym(Bool,Nat.is_eq(first,second),Nat.is_eq(second,first),Order.equal_symmetric(first,second)) : {_ == False{} : Bool}
90	  Order.less_not_equal(second,first,ordered)
91	
92	def preserved(~Element: Data,values: List<&2,Element>,+offset: Nat,+query: Nat,+depth: Nat,+tree: Tree.Tree<Element>,+balanced: Shape.Balanced(Element,depth,tree),+limit: {Nat.is_le(depth,30n) == True{} : Bool},
93	  +room: {Nat.is_le(Nat.add(offset,List.length(&2,Element,values)),U32.to_nat(Tree.capacity(Element,tree))) == True{} : Bool},
94	  +query_inside: {Nat.is_lt(query,U32.to_nat(Tree.capacity(Element,tree))) == True{} : Bool},+before: {Nat.is_lt(query,offset) == True{} : Bool}) ->
95	  {Tree.read(Element,Tree.write_sequence(~Element,values,U32.from_nat(offset),tree),U32.from_nat(query)) == Tree.read(Element,tree,U32.from_nat(query)) : Element}:
96	  match values:
97	    case []: {==}
98	    case +head <> +rest:
99	      +index_inside = Order.room_index(offset,List.length(&2,Element,rest),U32.to_nat(Tree.capacity(Element,tree)),room)
100	      +written = Tree.write(Element,tree,U32.from_nat(offset),head)
101	      +capacity = Readback.write_capacity(~Element,tree,U32.from_nat(offset),head)
102	      %Equal.sym(U32,(U32.from_nat(offset) + 1 : U32),U32.from_nat(1n+offset),Bounds.increment_encoded(offset)) :
103	        {Tree.read(Element,Tree.write_sequence(~Element,rest,_,written),U32.from_nat(query)) == Tree.read(Element,tree,U32.from_nat(query)) : Element}
104	      Equal.trans(Element,Tree.read(Element,Tree.write_sequence(~Element,rest,U32.from_nat(1n+offset),written),U32.from_nat(query)),Tree.read(Element,written,U32.from_nat(query)),Tree.read(Element,tree,U32.from_nat(query)),
105	        preserved(~Element,rest,1n+offset,query,depth,written,Shape.write(Element,depth,tree,U32.from_nat(offset),head,balanced),limit,
106	          %Equal.sym(U32,Tree.capacity(Element,written),Tree.capacity(Element,tree),capacity) : {Nat.is_le(Nat.add(1n+offset,List.length(&2,Element,rest)),U32.to_nat(_)) == True{} : Bool}
107	          Order.advance_room(offset,List.length(&2,Element,rest),U32.to_nat(Tree.capacity(Element,tree)),room),
108	          %Equal.sym(U32,Tree.capacity(Element,written),Tree.capacity(Element,tree),capacity) : {Nat.is_lt(query,U32.to_nat(_)) == True{} : Bool} query_inside,
109	          Order.lt_succ(query,offset,Bounds.strict_le(query,offset,before))),
110	        Readback.read_preserved(~Element,depth,tree,U32.from_nat(offset),U32.from_nat(query),head,balanced,limit,inside(offset,Tree.capacity(Element,tree),index_inside),inside(query,Tree.capacity(Element,tree),query_inside),distinct(offset,query,Tree.capacity(Element,tree),index_inside,query_inside,before)))
111	
112	def outside(~Element: Data,values: List<&2,Element>,+offset: Nat,+query: Nat,+depth: Nat,+tree: Tree.Tree<Element>,+balanced: Shape.Balanced(Element,depth,tree),+limit: {Nat.is_le(depth,30n) == True{} : Bool},
113	  +room: {Nat.is_le(Nat.add(offset,List.length(&2,Element,values)),U32.to_nat(Tree.capacity(Element,tree))) == True{} : Bool},
114	  +query_inside: {Nat.is_lt(query,U32.to_nat(Tree.capacity(Element,tree))) == True{} : Bool},
115	  +separate: Interval.Outside<offset,List.length(&2,Element,values),query>) ->
116	  {Tree.read(Element,Tree.write_sequence(~Element,values,U32.from_nat(offset),tree),U32.from_nat(query)) == Tree.read(Element,tree,U32.from_nat(query)) : Element}:
117	  match values:
118	    case Nil{}: {==}
119	    case +head <> +rest:
120	      +capacity = Tree.capacity(Element,tree)
121	      +index_inside = Order.room_index(offset,List.length(&2,Element,rest),U32.to_nat(capacity),room)
122	      +written = Tree.write(Element,tree,U32.from_nat(offset),head)
123	      +same_capacity = Readback.write_capacity(~Element,tree,U32.from_nat(offset),head)
124	      +different = {
125	        %Equal.sym(Bool,U32.is_eq(U32.from_nat(offset),U32.from_nat(query)),Nat.is_eq(U32.to_nat(U32.from_nat(offset)),U32.to_nat(U32.from_nat(query))),Comparison.eq(U32.from_nat(offset),U32.from_nat(query))) : {_ == False{} : Bool}
126	        %Equal.sym(Nat,U32.to_nat(U32.from_nat(offset)),offset,FullRange.roundtrip(offset,capacity,Bounds.strict_le(offset,U32.to_nat(capacity),index_inside))) : {Nat.is_eq(_,U32.to_nat(U32.from_nat(query))) == False{} : Bool}
127	        %Equal.sym(Nat,U32.to_nat(U32.from_nat(query)),query,FullRange.roundtrip(query,capacity,Bounds.strict_le(query,U32.to_nat(capacity),query_inside))) : {Nat.is_eq(offset,_) == False{} : Bool}
128	        %Order.equal_symmetric(query,offset) : {_ == False{} : Bool}
129	        Interval.outside_head(offset,List.length(&2,Element,rest),query,separate) : {U32.is_eq(U32.from_nat(offset),U32.from_nat(query)) == False{} : Bool}}
130	      %Equal.sym(U32,(U32.from_nat(offset) + 1 : U32),U32.from_nat(1n+offset),Bounds.increment_encoded(offset)) :
131	        {Tree.read(Element,Tree.write_sequence(~Element,rest,_,written),U32.from_nat(query)) == Tree.read(Element,tree,U32.from_nat(query)) : Element}
132	      Equal.trans(Element,Tree.read(Element,Tree.write_sequence(~Element,rest,U32.from_nat(1n+offset),written),U32.from_nat(query)),Tree.read(Element,written,U32.from_nat(query)),Tree.read(Element,tree,U32.from_nat(query)),
133	        outside(~Element,rest,1n+offset,query,depth,written,Shape.write(Element,depth,tree,U32.from_nat(offset),head,balanced),limit,
134	          %Equal.sym(U32,Tree.capacity(Element,written),capacity,same_capacity) : {Nat.is_le(Nat.add(1n+offset,List.length(&2,Element,rest)),U32.to_nat(_)) == True{} : Bool}
135	          Order.advance_room(offset,List.length(&2,Element,rest),U32.to_nat(capacity),room),
136	          %Equal.sym(U32,Tree.capacity(Element,written),capacity,same_capacity) : {Nat.is_lt(query,U32.to_nat(_)) == True{} : Bool} query_inside,
137	          Interval.outside_tail(offset,List.length(&2,Element,rest),query,separate)),
138	        Readback.read_preserved(~Element,depth,tree,U32.from_nat(offset),U32.from_nat(query),head,balanced,limit,inside(offset,capacity,index_inside),inside(query,capacity,query_inside),different))
139	
140	def listed(~Element: Data,+values: List<&2,Element>,index: Nat,+offset: Nat,+depth: Nat,+tree: Tree.Tree<Element>,+fallback: Element,+balanced: Shape.Balanced(Element,depth,tree),+limit: {Nat.is_le(depth,30n) == True{} : Bool},
141	  +room: {Nat.is_le(Nat.add(offset,List.length(&2,Element,values)),U32.to_nat(Tree.capacity(Element,tree))) == True{} : Bool},
142	  within: {Nat.is_lt(index,List.length(&2,Element,values)) == True{} : Bool}) ->
143	  {Tree.read(Element,Tree.write_sequence(~Element,values,U32.from_nat(offset),tree),U32.from_nat(Nat.add(offset,index))) == at(~Element,fallback,index,values) : Element}:
144	  match values index:
145	    case [] 0n: Empty.absurd({Tree.read(Element,tree,U32.from_nat(Nat.add(offset,0n))) == fallback : Element},Words.false_true(within))
146	    case [] 1n+rest: Empty.absurd({Tree.read(Element,tree,U32.from_nat(Nat.add(offset,1n+rest))) == fallback : Element},Words.false_true(within))
147	    case +head <> +rest 0n:
148	      +written = Tree.write(Element,tree,U32.from_nat(offset),head)
149	      +capacity = Readback.write_capacity(~Element,tree,U32.from_nat(offset),head)
150	      %Equal.sym(Nat,Nat.add(offset,0n),offset,Addition.zero_right(offset)) : {Tree.read(Element,Tree.write_sequence(~Element,rest,(U32.from_nat(offset) + 1 : U32),written),U32.from_nat(_)) == head : Element}
151	      %Equal.sym(U32,(U32.from_nat(offset) + 1 : U32),U32.from_nat(1n+offset),Bounds.increment_encoded(offset)) : {Tree.read(Element,Tree.write_sequence(~Element,rest,_,written),U32.from_nat(offset)) == head : Element}
152	      Equal.trans(Element,Tree.read(Element,Tree.write_sequence(~Element,rest,U32.from_nat(1n+offset),written),U32.from_nat(offset)),Tree.read(Element,written,U32.from_nat(offset)),head,
153	        preserved(~Element,rest,1n+offset,offset,depth,written,Shape.write(Element,depth,tree,U32.from_nat(offset),head,balanced),limit,
154	          %Equal.sym(U32,Tree.capacity(Element,written),Tree.capacity(Element,tree),capacity) : {Nat.is_le(Nat.add(1n+offset,List.length(&2,Element,rest)),U32.to_nat(_)) == True{} : Bool}
155	          Order.advance_room(offset,List.length(&2,Element,rest),U32.to_nat(Tree.capacity(Element,tree)),room),
156	          %Equal.sym(U32,Tree.capacity(Element,written),Tree.capacity(Element,tree),capacity) : {Nat.is_lt(offset,U32.to_nat(_)) == True{} : Bool}
157	          Order.room_index(offset,List.length(&2,Element,rest),U32.to_nat(Tree.capacity(Element,tree)),room),Order.lt_succ(offset,offset,Order.reflexive(offset))),
158	        Readback.read_written(~Element,tree,U32.from_nat(offset),head))
159	    case +head <> +rest 1n+ +previous:
160	      +written = Tree.write(Element,tree,U32.from_nat(offset),head)
161	      +capacity = Readback.write_capacity(~Element,tree,U32.from_nat(offset),head)
162	      %Equal.sym(U32,(U32.from_nat(offset) + 1 : U32),U32.from_nat(1n+offset),Bounds.increment_encoded(offset)) : {Tree.read(Element,Tree.write_sequence(~Element,rest,_,written),U32.from_nat(Nat.add(offset,1n+previous))) == at(~Element,fallback,previous,rest) : Element}
163	      %Equal.sym(Nat,Nat.add(offset,1n+previous),1n+Nat.add(offset,previous),Addition.successor_right(offset,previous)) : {Tree.read(Element,Tree.write_sequence(~Element,rest,U32.from_nat(1n+offset),written),U32.from_nat(_)) == at(~Element,fallback,previous,rest) : Element}
164	      listed(~Element,rest,previous,1n+offset,depth,written,fallback,Shape.write(Element,depth,tree,U32.from_nat(offset),head,balanced),limit,
165	        %Equal.sym(U32,Tree.capacity(Element,written),Tree.capacity(Element,tree),capacity) : {Nat.is_le(Nat.add(1n+offset,List.length(&2,Element,rest)),U32.to_nat(_)) == True{} : Bool}
166	        Order.advance_room(offset,List.length(&2,Element,rest),U32.to_nat(Tree.capacity(Element,tree)),room),within)
167	
168	# Readback from concatenated lists preserves each rectangular row's order.
169	def appended_before(~Element: Data,+fallback: Element,+left: List<&2,Element>,+right: List<&2,Element>,index: Nat,
170	  inside: {Nat.is_lt(index,List.length(&2,Element,left)) == True{} : Bool}) ->
171	  {at(~Element,fallback,index,List.append(&2,Element,left,right)) == at(~Element,fallback,index,left) : Element}:
172	  match left index:
173	    case Nil{} index:
174	      Empty.absurd({at(~Element,fallback,index,right) == at(~Element,fallback,index,[]) : Element},
175	        Words.false_true(Equal.trans(Bool,False{},Nat.is_lt(index,0n),True{},Equal.sym(Bool,Nat.is_lt(index,0n),False{},Division.lt_zero(index)),inside)))
176	    case head <> rest 0n: {==}
177	    case head <> +rest 1n+ +previous: appended_before(~Element,fallback,rest,right,previous,inside)
178	
179	def appended_after(~Element: Data,+fallback: Element,left: List<&2,Element>,+right: List<&2,Element>,+index: Nat) ->
180	  {at(~Element,fallback,Nat.add(List.length(&2,Element,left),index),List.append(&2,Element,left,right)) == at(~Element,fallback,index,right) : Element}:
181	  match left:
182	    case Nil{}: {==}
183	    case head <> rest: appended_after(~Element,fallback,rest,right,index)
184	
185	def concat_enumerate_at(~Element: Data,~Context: Data,~row: Context -> Nat -> List<&2,Element>,~width: Context -> Nat,
186	  ~row_length: @+context: Context -> @+index: Nat -> {List.length(&2,Element,row(context,index)) == width(context) : Nat},
187	  +fallback: Element,+rows: Nat,+first: Nat,+row_index: Nat,+column_index: Nat,+context: Context,
188	  row_inside: {Nat.is_lt(row_index,rows) == True{} : Bool},+column_inside: {Nat.is_lt(column_index,width(context)) == True{} : Bool}) ->
189	  {at(~Element,fallback,Nat.add(Nat.mul(row_index,width(context)),column_index),List.concat(&2,Element,enumerate(~List<&2,Element>,~Context,~row,rows,first,context))) ==
190	    at(~Element,fallback,column_index,row(context,Nat.add(first,row_index))) : Element}:
191	  match rows row_index:
192	    case 0n row_index:
193	      Empty.absurd({at(~Element,fallback,Nat.add(Nat.mul(row_index,width(context)),column_index),[]) == at(~Element,fallback,column_index,row(context,Nat.add(first,row_index))) : Element},
194	        Words.false_true(Equal.trans(Bool,False{},Nat.is_lt(row_index,0n),True{},Equal.sym(Bool,Nat.is_lt(row_index,0n),False{},Division.lt_zero(row_index)),row_inside)))
195	    case 1n+ +rest 0n:
196	      %Equal.sym(Nat,Nat.add(first,0n),first,Addition.zero_right(first)) :
197	        {at(~Element,fallback,column_index,List.append(&2,Element,row(context,first),List.concat(&2,Element,enumerate(~List<&2,Element>,~Context,~row,rest,1n+first,context)))) == at(~Element,fallback,column_index,row(context,_)) : Element}
198	      appended_before(~Element,fallback,row(context,first),List.concat(&2,Element,enumerate(~List<&2,Element>,~Context,~row,rest,1n+first,context)),column_index,
199	        %Equal.sym(Nat,List.length(&2,Element,row(context,first)),width(context),row_length(context,first)) : {Nat.is_lt(column_index,_) == True{} : Bool} column_inside)
200	    case 1n+ +rest 1n+ +previous:
201	      +tail_index = Nat.add(Nat.mul(previous,width(context)),column_index)
202	      +tail = List.concat(&2,Element,enumerate(~List<&2,Element>,~Context,~row,rest,1n+first,context))
203	      %Equal.sym(Nat,Nat.add(first,1n+previous),1n+Nat.add(first,previous),Addition.successor_right(first,previous)) :
204	        {at(~Element,fallback,Nat.add(Nat.mul(1n+previous,width(context)),column_index),List.append(&2,Element,row(context,first),tail)) == at(~Element,fallback,column_index,row(context,_)) : Element}
205	      %Equal.sym(Nat,Nat.add(Nat.add(width(context),Nat.mul(previous,width(context))),column_index),Nat.add(width(context),tail_index),Addition.associative(width(context),Nat.mul(previous,width(context)),column_index)) :
206	        {at(~Element,fallback,_,List.append(&2,Element,row(context,first),tail)) == at(~Element,fallback,column_index,row(context,1n+Nat.add(first,previous))) : Element}
207	      %row_length(context,first) :
208	        {at(~Element,fallback,Nat.add(_,tail_index),List.append(&2,Element,row(context,first),tail)) == at(~Element,fallback,column_index,row(context,1n+Nat.add(first,previous))) : Element}
209	      Equal.trans(Element,at(~Element,fallback,Nat.add(List.length(&2,Element,row(context,first)),tail_index),List.append(&2,Element,row(context,first),tail)),at(~Element,fallback,tail_index,tail),
210	        at(~Element,fallback,column_index,row(context,1n+Nat.add(first,previous))),appended_after(~Element,fallback,row(context,first),tail,tail_index),
211	        concat_enumerate_at(~Element,~Context,~row,~width,~row_length,fallback,rest,1n+first,previous,column_index,context,row_inside,column_inside))
212	
213	def concat_enumerate_length(~Element: Data,~Context: Data,~row: Context -> Nat -> List<&2,Element>,~width: Context -> Nat,
214	  ~row_length: @+context: Context -> @+index: Nat -> {List.length(&2,Element,row(context,index)) == width(context) : Nat},
215	  rows: Nat,+first: Nat,+context: Context) ->
216	  {List.length(&2,Element,List.concat(&2,Element,enumerate(~List<&2,Element>,~Context,~row,rows,first,context))) == Nat.mul(rows,width(context)) : Nat}:
217	  match rows:
218	    case 0n: {==}
219	    case 1n+ +rest:
220	      +head = row(context,first)
221	      +tail = List.concat(&2,Element,enumerate(~List<&2,Element>,~Context,~row,rest,1n+first,context))
222	      %Equal.sym(Nat,List.length(&2,Element,List.append(&2,Element,head,tail)),Nat.add(List.length(&2,Element,head),List.length(&2,Element,tail)),append_length(~Element,head,tail)) :
223	        {_ == Nat.add(width(context),Nat.mul(rest,width(context))) : Nat}
224	      %Equal.sym(Nat,List.length(&2,Element,head),width(context),row_length(context,first)) :
225	        {Nat.add(_,List.length(&2,Element,tail)) == Nat.add(width(context),Nat.mul(rest,width(context))) : Nat}
226	      %Equal.sym(Nat,List.length(&2,Element,tail),Nat.mul(rest,width(context)),concat_enumerate_length(~Element,~Context,~row,~width,~row_length,rest,1n+first,context)) :
227	        {Nat.add(width(context),_) == Nat.add(width(context),Nat.mul(rest,width(context))) : Nat}
228	      {==}