1	import Base
2	import ../shape/core.bend as Shape
3	import ../storage/main.bend as Storage
4	import ../storage/model.bend as Model
5	import ../storage/refinement.bend as Refinement
6	import ../storage/route.bend as Route
7	import ../storage/clone.bend as Clone
8	import ../storage/PROOF.bend as StorageProof
9	import ../storage/LAWS.bend as StorageLaws
10	import ./core.bend as Core
11	import ./lifecycle.bend as Lifecycle
12	import ./word_injective.bend as Injective
13	import ./elementwise.bend as Elementwise
14	import ./core_LAWS.bend as Laws
15	import ./projection_LAWS.bend as Projection
16	import ./projection_PROOF.bend as ProjectionProof
17	import ./elementwise_parallel_proof.bend as Parallel
18	
19	def Laws.scalar_add(left, right):
20	  {==}
21	
22	def Laws.scalar_sub(left, right):
23	  {==}
24	
25	def Laws.scalar_mul(left, right):
26	  {==}
27	
28	def Laws.indexed_length(shape, tensor):
29	  Core.TTensor{storage, exact} = tensor
30	  Core.LengthValid{exact}
31	
32	def construction_values_dimensions(+dimensions: List<&2, U32>, +shape: Shape.Shape,
33	  preserved: {Shape.dimensions(shape) == dimensions : List<&2, U32>},
34	  result: Result<&2, &1, Core.Error, Core.Tensor<shape>>) ->
35	  Core.ConstructionDimensions(dimensions, Core.construct_values(shape, result)):
36	  match result:
37	    case Fail{error}:
38	      Unit{}
39	    case Done{tensor}:
40	      preserved
41	
42	def construction_shape_dimensions(+dimensions: List<&2, U32>, values: List<&2, F32>, result: Shape.ConstructResult<dimensions>) ->
43	  Core.ConstructionDimensions(dimensions, Core.construct_shape(dimensions, values, result)):
44	  match result:
45	    case Shape.SError{error}:
46	      Unit{}
47	    case Shape.SBuilt{+shape, preserved}:
48	      construction_values_dimensions(dimensions, shape, preserved, Core.from_values(shape, values))
49	
50	def Laws.successful_construction_dimensions(dimensions, values):
51	  construction_shape_dimensions(dimensions, values, Shape.construct(dimensions))
52	
53	def count_outcome(+shape: Shape.Shape, +values: List<&2, F32>,
54	  equal: {Shape.logical_numel(Shape.dimensions(shape)) == List.length(&2, F32, values) : Nat},
55	  result: Result<&2, &1, Core.Error, Core.Tensor<shape>>) -> Core.ValuesCount(shape, values, result):
56	  match result:
57	    case Fail{error}:
58	      Unit{}
59	    case Done{tensor}:
60	      equal
61	
62	def count_decision(+shape: Shape.Shape, +values: List<&2, F32>,
63	  decision: Shape.BoolCase<Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape))>) ->
64	  Core.ValuesCount(shape, values, Core.from_values_counted(shape, values, decision)):
65	  match decision:
66	    case Shape.BFalse{equal}:
67	      Unit{}
68	    case Shape.BTrue{equal}:
69	      count_outcome(shape, values,
70	        Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(shape)), Shape.elements(shape), List.length(&2, F32, values),
71	          Equal.sym(Nat, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Shape.elements_exact(shape)),
72	          Equal.sym(Nat, List.length(&2, F32, values), Shape.elements(shape),
73	            Lifecycle.natural_equal(List.length(&2, F32, values), Shape.elements(shape), equal))),
74	        Core.from_values_new(shape, values, Core.new(shape, 0.0)))
75	
76	def Laws.successful_value_count(shape, values):
77	  count_decision(shape, values, Shape.bool_case(Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape))))
78	
79	def Laws.checked_reader_pair(shape, original, index):
80	  Core.read_certificate(shape, original, index)
81	
82	def Laws.reader_certificate_value(shape, original, index, certificate):
83	  Core.Read{tensor, result, exact} = certificate
84	  %exact : {Core.read_value(shape, _) == Core.result_value(result) : Maybe<&2, F32>}
85	  {==}
86	
87	def Laws.checked_reader_source(shape, original, index):
88	  Core.source_read_model(shape, original, index)
89	
90	def Laws.checked_dynamic_reader_source(original, index):
91	  Core.dynamic_source_read_model(original, index)
92	
93	def Laws.checked_reader_retains_source(shape, original, index):
94	  Core.source_read_keeps(shape, original, index)
95	
96	def Laws.checked_dynamic_reader_retains_source(original, index):
97	  Core.dynamic_source_read_keeps(original, index)
98	
99	def Laws.primitive_read_retains_elements(depth, array, index, other, balanced):
100	  Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, depth, a, Refinement.route(depth, other)),
101	    Refinement.first(F32, Array.get(F32, array, index)), array,
102	    Refinement.law_get_retains(F32, depth, array, index, balanced))
103	
104	def Laws.storage_read_retains_length(storage, index):
105	  Lifecycle.get_length(storage, index)
106	
107	def Laws.storage_write_retains_length(storage, index, value):
108	  Lifecycle.set_length(storage, index, value)
109	
110	def Laws.storage_clone_first_length(storage):
111	  Lifecycle.clone_first_length(storage)
112	
113	def Laws.storage_clone_second_length(storage):
114	  Lifecycle.clone_second_length(storage)
115	
116	def Laws.primitive_clone_first_elements(depth, array, path, balanced):
117	  Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, depth, a, path),
118	    Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, array)), array,
119	    Clone.first_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced)))
120	
121	def Laws.primitive_clone_second_elements(depth, array, path, balanced):
122	  Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, depth, a, path),
123	    Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, array)), array,
124	    Clone.second_equal(F32, depth, array, Clone.certify(F32, depth, array, balanced)))
125	
126	def write_checked_mapping(-shape: Shape.Shape, +d: Nat, +n: Nat, array: Array<F32>, +i: U32, +value: F32,
127	  balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool},
128	  -exact: {n == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, allowed: Bool,
129	  -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
130	  -same: {Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid) ==
131	    Storage.set(Storage.Owned{d, n, array, balanced, valid}, i, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>},
132	  accepted: {allowed == True{} : Bool}) ->
133	  {Core.write_observe(shape, Core.write_result(shape, Storage.Owned{d, n, array, balanced, valid}, exact, i, value,
134	    Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid), same), i) == Some{value} : Maybe<&2, F32>}:
135	  match allowed:
136	    case False{}:
137	      Empty.absurd({Core.write_observe(shape, Core.write_result(shape, Storage.Owned{d, n, array, balanced, valid}, exact, i, value,
138	        Storage.set_checked(d, n, array, i, value, False{}, decision, balanced, valid), same), i) == Some{value} : Maybe<&2, F32>},
139	        Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, accepted)))
140	    case True{}:
141	      StorageLaws.primitive_write_read(F32, d, array, i, value, balanced)
142	
143	def Laws.tensor_write_mapping(shape, depth, length, array, index, value, balanced, valid, exact, allowed, matched):
144	  write_checked_mapping(shape, depth, length, array, index, value, balanced, valid, exact,
145	    Nat.is_lt(U32.to_nat(index), length), {==}, {==}, allowed)
146	
147	def step_checked_mapping(-shape: Shape.Shape, +d: Nat, +n: Nat, array: Array<F32>, +i: U32, +value: F32,
148	  -left: Core.Dynamic, -right: Core.Dynamic,
149	  balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool},
150	  -exact: {n == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, allowed: Bool,
151	  -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
152	  -same: {Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid) ==
153	    Storage.set(Storage.Owned{d, n, array, balanced, valid}, i, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>},
154	  accepted: {allowed == True{} : Bool}) ->
155	  {Elementwise.step_observe(shape, Elementwise.step_write(shape, left, right,
156	    Core.write_result(shape, Storage.Owned{d, n, array, balanced, valid}, exact, i, value,
157	      Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid), same)), i) == Some{value} : Maybe<&2, F32>}:
158	  match allowed:
159	    case False{}:
160	      Empty.absurd({Elementwise.step_observe(shape, Elementwise.step_write(shape, left, right,
161	        Core.write_result(shape, Storage.Owned{d, n, array, balanced, valid}, exact, i, value,
162	          Storage.set_checked(d, n, array, i, value, False{}, decision, balanced, valid), same)), i) == Some{value} : Maybe<&2, F32>},
163	        Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, accepted)))
164	    case True{}:
165	      StorageLaws.primitive_write_read(F32, d, array, i, value, balanced)
166	
167	def Laws.broadcast_step_mapping(operation, shape, depth, length, array, index, left, right,
168	  left_value, right_value, balanced, valid, exact, allowed, matched):
169	  step_checked_mapping(shape, depth, length, array, index, Elementwise.scalar(operation, left_value, right_value),
170	    left, right, balanced, valid, exact, Nat.is_lt(U32.to_nat(index), length), {==}, {==}, allowed)
171	
172	def and_true_left(+left: Bool, +right: Bool, equal: {Bool.and(left, right) == True{} : Bool}) -> {left == True{} : Bool}:
173	  match left:
174	    case False{}:
175	      Empty.absurd({False{} == True{} : Bool}, Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, equal)))
176	    case True{}:
177	      {==}
178	
179	def same_path_offset(+depth: Nat, +left: Model.Path(depth), +right: Model.Path(depth),
180	  equal: {Model.same(depth, left, right) == True{} : Bool}) -> {Model.offset(depth, left) == Model.offset(depth, right) : Nat}:
181	  match depth:
182	    case 0n:
183	      {==}
184	    case 1n++p:
185	      Model.Step{+lb, +lt} = left
186	      match lb:
187	        case False{}:
188	          Model.Step{+rb, +rt} = right
189	          match rb:
190	            case False{}:
191	              same_path_offset(p, lt, rt, equal)
192	            case True{}:
193	              Empty.absurd({Model.offset(p, lt) == Nat.add(Model.capacity(p), Model.offset(p, rt)) : Nat},
194	                Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, equal)))
195	        case True{}:
196	          Model.Step{+rb, +rt} = right
197	          match rb:
198	            case False{}:
199	              Empty.absurd({Nat.add(Model.capacity(p), Model.offset(p, lt)) == Model.offset(p, rt) : Nat},
200	                Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, equal)))
201	            case True{}:
202	              Equal.cong(Nat, Nat, n => Nat.add(Model.capacity(p), n), Model.offset(p, lt), Model.offset(p, rt),
203	                same_path_offset(p, lt, rt, equal))
204	
205	def checked_offset(+depth: Nat, +length: Nat, +index: U32,
206	  checked: {Storage.index_matches(depth, length, index) == True{} : Bool}) ->
207	  {Model.offset(depth, Refinement.route(depth, index)) == U32.to_nat(index) : Nat}:
208	  Lifecycle.natural_equal(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index),
209	    Equal.sym(Bool, Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)), True{},
210	      and_true_left(Nat.is_eq(Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index)),
211	        Nat.is_lt(Model.offset(depth, Refinement.route(depth, index)), length), checked)))
212	
213	def nat_equal_self(+n: Nat) -> {Nat.is_eq(n, n) == True{} : Bool}:
214	  match n:
215	    case 0n:
216	      {==}
217	    case 1n+p:
218	      nat_equal_self(p)
219	
220	def natural_clash(+left: Nat, +right: Nat, equal: {left == right : Nat},
221	  different: {Nat.is_eq(left, right) == False{} : Bool}) -> Empty:
222	  Lifecycle.false_true(Equal.trans(Bool, True{}, Nat.is_eq(left, right), False{},
223	    Equal.sym(Bool, Nat.is_eq(left, right), True{},
224	      %equal : {Nat.is_eq(left, _) == True{} : Bool}
225	      nat_equal_self(left)), different))
226	
227	def route_separation_decided(+depth: Nat, +length: Nat, +index: U32, +other: U32,
228	  index_checked: {Storage.index_matches(depth, length, index) == True{} : Bool},
229	  other_checked: {Storage.index_matches(depth, length, other) == True{} : Bool},
230	  different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool}, same: Bool,
231	  decision: {same == Model.same(depth, Refinement.route(depth, index), Refinement.route(depth, other)) : Bool}) -> {same == False{} : Bool}:
232	  match same:
233	    case False{}:
234	      {==}
235	    case True{}:
236	      Empty.absurd({True{} == False{} : Bool}, natural_clash(U32.to_nat(index), U32.to_nat(other),
237	        Equal.trans(Nat, U32.to_nat(index), Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(other),
238	          Equal.sym(Nat, Model.offset(depth, Refinement.route(depth, index)), U32.to_nat(index), checked_offset(depth, length, index, index_checked)),
239	          Equal.trans(Nat, Model.offset(depth, Refinement.route(depth, index)), Model.offset(depth, Refinement.route(depth, other)), U32.to_nat(other),
240	            same_path_offset(depth, Refinement.route(depth, index), Refinement.route(depth, other),
241	              Equal.sym(Bool, True{}, Model.same(depth, Refinement.route(depth, index), Refinement.route(depth, other)), decision)),
242	            checked_offset(depth, length, other, other_checked))), different))
243	
244	def Laws.checked_route_separation(depth, length, index, other, index_checked, other_checked, different):
245	  route_separation_decided(depth, length, index, other, index_checked, other_checked, different,
246	    Model.same(depth, Refinement.route(depth, index), Refinement.route(depth, other)), {==})
247	
248	def frame_checked_mapping(-shape: Shape.Shape, +d: Nat, +n: Nat, array: Array<F32>, +i: U32, +other: U32, +value: F32,
249	  balanced: Model.Balanced(F32, d, array), -valid: {Storage.bounds(d, n) == True{} : Bool},
250	  -exact: {n == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, allowed: Bool,
251	  -decision: {allowed == Nat.is_lt(U32.to_nat(i), n) : Bool},
252	  -same: {Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid) ==
253	    Storage.set(Storage.Owned{d, n, array, balanced, valid}, i, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>},
254	  accepted: {allowed == True{} : Bool},
255	  index_checked: {Storage.index_matches(d, n, i) == True{} : Bool},
256	  other_checked: {Storage.index_matches(d, n, other) == True{} : Bool},
257	  different: {Nat.is_eq(U32.to_nat(i), U32.to_nat(other)) == False{} : Bool}) ->
258	  {Core.write_observe(shape, Core.write_result(shape, Storage.Owned{d, n, array, balanced, valid}, exact, i, value,
259	    Storage.set_checked(d, n, array, i, value, allowed, decision, balanced, valid), same), other) ==
260	    Model.observe(F32, d, array, Refinement.route(d, other)) : Maybe<&2, F32>}:
261	  match allowed:
262	    case False{}:
263	      Empty.absurd({Core.write_observe(shape, Core.write_result(shape, Storage.Owned{d, n, array, balanced, valid}, exact, i, value,
264	        Storage.set_checked(d, n, array, i, value, False{}, decision, balanced, valid), same), other) ==
265	        Model.observe(F32, d, array, Refinement.route(d, other)) : Maybe<&2, F32>},
266	        Lifecycle.false_true(Equal.sym(Bool, False{}, True{}, accepted)))
267	    case True{}:
268	      %Laws.checked_route_separation(d, n, i, other, index_checked, other_checked, different) :
269	        {Model.observe(F32, d, Array.set(F32, array, i, value), Refinement.route(d, other)) ==
270	          Model.select(F32, _, value, Model.observe(F32, d, array, Refinement.route(d, other))) : Maybe<&2, F32>}
271	      StorageLaws.primitive_update_frame(F32, d, array, i, Refinement.route(d, other), value, balanced)
272	
273	def Laws.tensor_write_frame(shape, depth, length, array, index, other, value, balanced, valid, exact,
274	  allowed, index_checked, other_checked, different):
275	  frame_checked_mapping(shape, depth, length, array, index, other, value, balanced, valid, exact,
276	    Nat.is_lt(U32.to_nat(index), length), {==}, {==}, allowed, index_checked, other_checked, different)
277	
278	def Laws.checked_conversion_value(cursor, index, verdict):
279	  Lifecycle.natural_equal(U32.to_nat(index), cursor, verdict)
280	
281	def cursor_validity(-shape: Shape.Shape, +cursor: Nat, result: Elementwise.NaturalStep<shape, cursor>) ->
282	  Elementwise.CursorValidity(shape, cursor, result):
283	  match result:
284	    case Elementwise.NaturalStop{left, right, error}:
285	      Unit{}
286	    case Elementwise.NaturalContinue{state, index, exact}:
287	      Elementwise.CursorWitness{exact}
288	
289	def Laws.natural_cursor_step(operation, plan, cursor, state):
290	  cursor_validity(Shape.output_shape(plan), cursor, Elementwise.natural_step(operation, plan, cursor, state))
291	
292	def Laws.u32_natural_injective(left, right, equal):
293	  Injective.u32_natural_injective(left, right)(equal)
294	
295	type UpdateCheckedModel<-shape: Shape.Shape, -depth: Nat, -length: Nat, -array: Array<F32>, -index: U32, -value: F32,
296	  -allowed: Bool, -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
297	  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
298	  -length_exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
299	  -same: {Storage.set_checked(depth, length, array, index, value, allowed, decision, balanced, valid) ==
300	    Storage.set(Storage.Owned{depth, length, array, balanced, valid}, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}> is Data:
301	  UpdateCheckedModel{-meaning: Core.UpdateMeaning(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}, index, value,
302	    Core.write_result(shape, Storage.Owned{depth, length, array, balanced, valid}, length_exact, index, value,
303	      Storage.set_checked(depth, length, array, index, value, allowed, decision, balanced, valid), same))}
304	
305	def update_checked_model(-shape: Shape.Shape, +depth: Nat, +length: Nat, -array: Array<F32>, +index: U32, +value: F32,
306	  allowed: Bool, -decision: {allowed == Nat.is_lt(U32.to_nat(index), length) : Bool},
307	  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
308	  -length_exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
309	  -same: {Storage.set_checked(depth, length, array, index, value, allowed, decision, balanced, valid) ==
310	    Storage.set(Storage.Owned{depth, length, array, balanced, valid}, index, value) : Storage.Storage & Result<&2, &2, Storage.Error, Unit>}) ->
311	  UpdateCheckedModel<shape, depth, length, array, index, value, allowed, decision, balanced, valid, length_exact, same>:
312	  match allowed:
313	    case False{}:
314	      UpdateCheckedModel{Unit{}}
315	    case True{}:
316	      UpdateCheckedModel{(Route.index_matched(depth, length, index, valid, Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), length), decision)),
317	        (StorageLaws.primitive_write_read(F32, depth, array, index, value, balanced),
318	          other => checked => different => (checked,
319	            %Laws.checked_route_separation(depth, length, index, other,
320	              Route.index_matched(depth, length, index, valid, Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), length), decision)),
321	              checked, different) :
322	              {Model.observe(F32, depth, Array.set(F32, array, index, value), Refinement.route(depth, other)) ==
323	                Model.select(F32, _, value, Model.observe(F32, depth, array, Refinement.route(depth, other))) : Maybe<&2, F32>}
324	            StorageLaws.primitive_update_frame(F32, depth, array, index, Refinement.route(depth, other), value, balanced))))}
325	
326	def update_checked_tensor(-shape: Shape.Shape, +depth: Nat, +length: Nat, -array: Array<F32>, +index: U32, +value: F32,
327	  -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
328	  -length_exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat},
329	  certificate: UpdateCheckedModel<shape, depth, length, array, index, value, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid, length_exact, {==}>) ->
330	  Core.UpdateModel<shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}, index, value>:
331	  UpdateCheckedModel{meaning} = certificate
332	  Core.UpdateModel{meaning}
333	
334	def update_model(-shape: Shape.Shape, original: Core.Tensor<shape>, +index: U32, +value: F32) -> Core.UpdateModel<shape, original, index, value>:
335	  Core.TTensor{storage, length_exact} = original
336	  match storage:
337	    case Storage.Empty{}:
338	      Core.UpdateModel{Unit{}}
339	    case Storage.Owned{+depth, +length, array, balanced, valid}:
340	      update_checked_tensor(shape, depth, length, array, index, value, balanced, valid, length_exact,
341	        update_checked_model(shape, depth, length, array, index, value, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid, length_exact, {==}))
342	
343	type WriteInfo<-shape: Shape.Shape, -original: Core.Tensor<shape>, -index: U32, -value: F32> is Type:
344	  WriteInfo{owner: Core.Tensor<shape>, same: {owner == original : Core.Tensor<shape>}, model: Core.UpdateModel<shape, original, index, value>}
345	
346	def write_info(-shape: Shape.Shape, original: Core.Tensor<shape>, +index: U32, +value: F32) -> WriteInfo<shape, original, index, value>:
347	  Core.TTensor{storage, length_exact} = original
348	  match storage:
349	    case Storage.Empty{}:
350	      WriteInfo{Core.TTensor{Storage.Empty{}, length_exact}, {==}, Core.UpdateModel{Unit{}}}
351	    case Storage.Owned{+depth, +length, array, balanced, valid}:
352	      WriteInfo{Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, length_exact}, {==},
353	        update_checked_tensor(shape, depth, length, array, index, value, balanced, valid, length_exact,
354	          update_checked_model(shape, depth, length, array, index, value, Nat.is_lt(U32.to_nat(index), length), {==}, balanced, valid, length_exact, {==}))}
355	
356	def read_original(-original: Core.Dynamic, -owner: Core.Dynamic, +index: U32, same: {owner == original : Core.Dynamic},
357	  certificate: Core.DynamicRead<owner, index>) -> Core.DynamicRead<original, index>:
358	  Core.DynamicRead{dynamic, result, exact} = certificate
359	  Core.DynamicRead{dynamic, result, Equal.trans(Core.Dynamic & Result<&2, &2, Core.Error, F32>, (dynamic, result),
360	    Core.read_dynamic(owner, index), Core.read_dynamic(original, index), exact,
361	    Equal.cong(Core.Dynamic, Core.Dynamic & Result<&2, &2, Core.Error, F32>, input => Core.read_dynamic(input, index), owner, original, same))}
362	
363	def write_original(-shape: Shape.Shape, -original: Core.Tensor<shape>, -owner: Core.Tensor<shape>, +index: U32, +value: F32,
364	  same: {owner == original : Core.Tensor<shape>}, certificate: Core.Write<shape, owner, index, value>) -> Core.Write<shape, original, index, value>:
365	  Core.Write{tensor, result, exact} = certificate
366	  Core.Write{tensor, result, Equal.trans(Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, (tensor, result),
367	    Core.write_flat(shape, owner, index, value), Core.write_flat(shape, original, index, value), exact,
368	    Equal.cong(Core.Tensor<shape>, Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, input => Core.write_flat(shape, input, index, value), owner, original, same))}
369	
370	type ReadValueModel<-original: Core.Dynamic, -index: U32, -value: F32> is Data:
371	  ReadValueModel{-equal: {Core.checked_observe_dynamic(original, index) == Some{value} : Maybe<&2, F32>}}
372	
373	def read_value_model(-original: Core.Dynamic, -retained: Core.Dynamic, +index: U32, +value: F32,
374	  -exact: {(retained, Done{value}) == Core.read_dynamic(original, index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>},
375	  certificate: Core.DynamicSourceRead<original, index>) -> ReadValueModel<original, index, value>:
376	  Core.DynamicSourceRead{meaning} = certificate
377	  ReadValueModel{Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(original, index),
378	    Core.dynamic_read_value(Core.read_dynamic(original, index)), Some{value},
379	    Equal.sym(Maybe<&2, F32>, Core.dynamic_read_value(Core.read_dynamic(original, index)), Core.checked_observe_dynamic(original, index), meaning),
380	    Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.dynamic_read_value(pair),
381	      Core.read_dynamic(original, index), (retained, Done{value}),
382	      Equal.sym(Core.Dynamic & Result<&2, &2, Core.Error, F32>, (retained, Done{value}), Core.read_dynamic(original, index), exact)))}
383	
384	type RetainedSourceModel<-original: Core.Dynamic, -retained: Core.Dynamic> is Data:
385	  RetainedSourceModel{-kept: Elementwise.SameSource(original, retained)}
386	
387	def retained_source_model(-original: Core.Dynamic, -retained: Core.Dynamic, +index: U32, -value: F32,
388	  -exact: {(retained, Done{value}) == Core.read_dynamic(original, index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>},
389	  certificate: Core.DynamicSourceReadKeeps<original, index>) -> RetainedSourceModel<original, retained>:
390	  Core.DynamicSourceReadKeeps{kept} = certificate
391	  RetainedSourceModel{other => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(retained, other),
392	    Core.retained_dynamic_observe(Core.read_dynamic(original, index), other), Core.checked_observe_dynamic(original, other),
393	    Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.retained_dynamic_observe(pair, other),
394	      (retained, Done{value}), Core.read_dynamic(original, index), exact), kept(other))}
395	
396	type ExpectedValue<-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -index: U32,
397	  -left: Core.Dynamic, -right: Core.Dynamic, -left_value: F32, -right_value: F32> is Data:
398	  ExpectedValue{-equal: {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}}
399	
400	def expected_value(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32, -left: Core.Dynamic, -right: Core.Dynamic,
401	  +left_index: U32, +right_index: U32, +left_value: F32, +right_value: F32,
402	  -indices_exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
403	  left_model: ReadValueModel<left, left_index, left_value>, right_model: ReadValueModel<right, right_index, right_value>) ->
404	  ExpectedValue<operation, plan, index, left, right, left_value, right_value>:
405	  ReadValueModel{left_equal} = left_model
406	  ReadValueModel{right_equal} = right_model
407	  ExpectedValue{
408	    %indices_exact : {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected_indices(operation, left, right, _) : Maybe<&2, F32>}
409	    %Equal.sym(Maybe<&2, F32>, Core.checked_observe_dynamic(left, left_index), Some{left_value}, left_equal) :
410	      {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected_left(operation, right, right_index, _) : Maybe<&2, F32>}
411	    %Equal.sym(Maybe<&2, F32>, Core.checked_observe_dynamic(right, right_index), Some{right_value}, right_equal) :
412	      {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected_right(operation, left_value, _) : Maybe<&2, F32>}
413	    {==}}
414	
415	type KnownUpdate<-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32, -value: F32, -unit: Unit> is Data:
416	  KnownUpdate{-meaning: Core.UpdateMeaning(shape, original, index, value, (output, Done{unit}))}
417	
418	def known_update(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, +index: U32, +value: F32, -unit: Unit,
419	  -exact: {(output, Done{unit}) == Core.write_flat(shape, original, index, value) : Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>},
420	  certificate: Core.UpdateModel<shape, original, index, value>) -> KnownUpdate<shape, original, output, index, value, unit>:
421	  Core.UpdateModel{meaning} = certificate
422	  KnownUpdate{
423	    %Equal.sym(Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, (output, Done{unit}), Core.write_flat(shape, original, index, value), exact) :
424	      Core.UpdateMeaning(shape, original, index, value, _)
425	    meaning}
426	
427	def update_route(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32, -value: F32, -unit: Unit,
428	  meaning: Core.UpdateMeaning(shape, original, index, value, (output, Done{unit}))) -> Core.ObservationChecked(Core.Packed{shape, output}, index):
429	  (checked, rest) = meaning
430	  checked
431	
432	def update_value(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32, -value: F32, -unit: Unit,
433	  meaning: Core.UpdateMeaning(shape, original, index, value, (output, Done{unit}))) -> {Core.observe(shape, output, index) == Some{value} : Maybe<&2, F32>}:
434	  (checked, rest) = meaning
435	  (observed, frame) = rest
436	  observed
437	
438	def update_frame(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -index: U32, -value: F32, -unit: Unit,
439	  meaning: Core.UpdateMeaning(shape, original, index, value, (output, Done{unit}))) ->
440	  @+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{shape, original}, other) ->
441	    @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
442	      Core.ObservationChecked(Core.Packed{shape, output}, other) &
443	        {Core.observe(shape, output, other) == Core.observe(shape, original, other) : Maybe<&2, F32>}:
444	  (checked, rest) = meaning
445	  (observed, frame) = rest
446	  frame
447	
448	type CheckedFrame<-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, -other: U32> is Data:
449	  CheckedFrame{-equal: {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}}
450	
451	def checked_frame(-shape: Shape.Shape, -original: Core.Tensor<shape>, -output: Core.Tensor<shape>, +other: U32,
452	  -before: Core.ObservationChecked(Core.Packed{shape, original}, other),
453	  -after: Core.ObservationChecked(Core.Packed{shape, output}, other),
454	  -physical: {Core.observe(shape, output, other) == Core.observe(shape, original, other) : Maybe<&2, F32>}) -> CheckedFrame<shape, original, output, other>:
455	  CheckedFrame{
456	    {\{Core.ObservationModel: after_equal =>
457	      {\{Core.ObservationModel: before_equal =>
458	        Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, output, other), Core.observe(shape, output, other), Core.checked_observe(shape, original, other),
459	          after_equal, Equal.trans(Maybe<&2, F32>, Core.observe(shape, output, other), Core.observe(shape, original, other), Core.checked_observe(shape, original, other),
460	            physical, Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, original, other), Core.observe(shape, original, other), before_equal)))
461	      } : Core.ObservationModel<shape, original, other, before> -> {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}}(Core.observation_model(shape, original, other, before))
462	    } : Core.ObservationModel<shape, output, other, after> -> {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}}(Core.observation_model(shape, output, other, after))}
463	
464	type CheckedUpdatePair<-shape: Shape.Shape, -original: Core.Tensor<shape>, -index: U32, -value: F32,
465	  -pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>> is Data:
466	  CheckedUpdatePair{-meaning: Core.CheckedUpdateMeaning(shape, original, index, value, pair)}
467	
468	def checked_update_pair(-shape: Shape.Shape, -original: Core.Tensor<shape>, +index: U32, +value: F32,
469	  pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, -meaning: Core.UpdateMeaning(shape, original, index, value, pair)) ->
470	  CheckedUpdatePair<shape, original, index, value, pair>:
471	  (output, result) = pair
472	  match result:
473	    case Fail{error}:
474	      CheckedUpdatePair{Unit{}}
475	    case Done{unit}:
476	      CheckedUpdatePair{(update_route(shape, original, output, index, value, unit, meaning),
477	        (Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, output, index), Core.observe(shape, output, index), Some{value},
478	          {\{Core.ObservationModel: equal => equal} :
479	            Core.ObservationModel<shape, output, index, update_route(shape, original, output, index, value, unit, meaning)> ->
480	              {Core.checked_observe(shape, output, index) == Core.observe(shape, output, index) : Maybe<&2, F32>}}(Core.observation_model(shape, output, index, update_route(shape, original, output, index, value, unit, meaning))),
481	          update_value(shape, original, output, index, value, unit, meaning)),
482	          other => checked => different =>
483	            {\{Tuple: after => physical => (after,
484	              {\{CheckedFrame: equal => equal} : CheckedFrame<shape, original, output, other> ->
485	                {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}}(checked_frame(shape, original, output, other, checked, after, physical)))
486	            } :
487	              (Core.ObservationChecked(Core.Packed{shape, output}, other) &
488	                {Core.observe(shape, output, other) == Core.observe(shape, original, other) : Maybe<&2, F32>}) ->
489	              (Core.ObservationChecked(Core.Packed{shape, output}, other) &
490	                {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})}(update_frame(shape, original, output, index, value, unit, meaning)(other)(checked)(different))))}
491	
492	def checked_update_model(-shape: Shape.Shape, original: Core.Tensor<shape>, +index: U32, +value: F32) -> Core.CheckedUpdateModel<shape, original, index, value>:
493	  Core.CheckedUpdateModel{
494	    {\{Core.UpdateModel: meaning =>
495	      {\{CheckedUpdatePair: checked_meaning => checked_meaning} :
496	        CheckedUpdatePair<shape, original, index, value, Core.write_flat(shape, original, index, value)> ->
497	          Core.CheckedUpdateMeaning(shape, original, index, value, Core.write_flat(shape, original, index, value))}(checked_update_pair(shape, original, index, value, Core.write_flat(shape, original, index, value), meaning))
498	    } : Core.UpdateModel<shape, original, index, value> ->
499	      Core.CheckedUpdateMeaning(shape, original, index, value, Core.write_flat(shape, original, index, value))}(update_model(shape, original, index, value))}
500	
501	def step_write_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
502	  -original_left: Core.Dynamic, -original_right: Core.Dynamic, -original_output: Core.Tensor<Shape.output_shape(plan)>,
503	  +left_index: U32, +right_index: U32, +left_value: F32, +right_value: F32,
504	  -indices_exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
505	  certificate: Core.Write<Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value)>,
506	  left: Core.Dynamic, right: Core.Dynamic,
507	  -left_exact: {(left, Done{left_value}) == Core.read_dynamic(original_left, left_index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>},
508	  -right_exact: {(right, Done{right_value}) == Core.read_dynamic(original_right, right_index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>},
509	  lift: @-result: Elementwise.Step<Shape.output_shape(plan)> ->
510	    {result == Elementwise.step_write(Shape.output_shape(plan), left, right,
511	      Core.write_flat(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value))) : Elementwise.Step<Shape.output_shape(plan)>} ->
512	    {result == Elementwise.step(operation, plan, index, Elementwise.State{original_left, original_right, original_output}) : Elementwise.Step<Shape.output_shape(plan)>}) ->
513	  Elementwise.StepCertificate<operation, plan, index, Elementwise.State{original_left, original_right, original_output}>:
514	  Core.Write{output, result, exact} = certificate
515	  match result:
516	    case Fail{error}:
517	      Elementwise.StepCertificate{Elementwise.Stop{left, right, error},
518	        lift(Elementwise.Stop{left, right, error},
519	          Equal.cong(Core.Tensor<Shape.output_shape(plan)> & Result<&2, &2, Core.Error, Unit>, Elementwise.Step<Shape.output_shape(plan)>,
520	            pair => Elementwise.step_write(Shape.output_shape(plan), left, right, pair),
521	            (output, Fail{error}), Core.write_flat(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value)), exact)), Unit{}}
522	    case Done{unit}:
523	      Elementwise.StepCertificate{Elementwise.Continue{Elementwise.State{left, right, output}},
524	        lift(Elementwise.Continue{Elementwise.State{left, right, output}},
525	          Equal.cong(Core.Tensor<Shape.output_shape(plan)> & Result<&2, &2, Core.Error, Unit>, Elementwise.Step<Shape.output_shape(plan)>,
526	            pair => Elementwise.step_write(Shape.output_shape(plan), left, right, pair),
527	            (output, Done{unit}), Core.write_flat(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value)), exact)),
528	        ({\{RetainedSourceModel: kept => kept} : RetainedSourceModel<original_left, left> -> Elementwise.SameSource(original_left, left)}(retained_source_model(original_left, left, left_index, left_value, left_exact, Core.dynamic_source_read_keeps(original_left, left_index))),
529	          ({\{RetainedSourceModel: kept => kept} : RetainedSourceModel<original_right, right> -> Elementwise.SameSource(original_right, right)}(retained_source_model(original_right, right, right_index, right_value, right_exact, Core.dynamic_source_read_keeps(original_right, right_index))),
530	            {\{KnownUpdate: meaning =>
531	              (update_route(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, meaning),
532	                (Equal.trans(Maybe<&2, F32>, Core.observe(Shape.output_shape(plan), output, index), Some{Elementwise.scalar(operation, left_value, right_value)},
533	                  Elementwise.expected(operation, plan, original_left, original_right, index),
534	                  update_value(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, meaning),
535	                  {\{ExpectedValue: equal => equal} : ExpectedValue<operation, plan, index, original_left, original_right, left_value, right_value> ->
536	                    {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>}}(expected_value(operation, plan, index, original_left, original_right, left_index, right_index, left_value, right_value, indices_exact,
537	                      read_value_model(original_left, left, left_index, left_value, left_exact, Core.dynamic_source_read_model(original_left, left_index)),
538	                      read_value_model(original_right, right, right_index, right_value, right_exact, Core.dynamic_source_read_model(original_right, right_index))))),
539	                  update_frame(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, meaning)))
540	            } : KnownUpdate<Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit> ->
541	              (Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), output}, index) &
542	                ({Core.observe(Shape.output_shape(plan), output, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>} &
543	                  (@+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), original_output}, other) ->
544	                    @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
545	                      Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), output}, other) &
546	                        {Core.observe(Shape.output_shape(plan), output, other) == Core.observe(Shape.output_shape(plan), original_output, other) : Maybe<&2, F32>})))}(known_update(Shape.output_shape(plan), original_output, output, index, Elementwise.scalar(operation, left_value, right_value), unit, exact,
547	                          update_model(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value))))))}
548	
549	def step_right_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
550	  -original_left: Core.Dynamic, -original_right: Core.Dynamic,
551	  +left_index: U32, +right_index: U32, +left_value: F32,
552	  -indices_exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
553	  certificate: Core.DynamicRead<original_right, right_index>,
554	  original_output: Core.Tensor<Shape.output_shape(plan)>,
555	  left: Core.Dynamic,
556	  -left_exact: {(left, Done{left_value}) == Core.read_dynamic(original_left, left_index) : Core.Dynamic & Result<&2, &2, Core.Error, F32>},
557	  lift: @-result: Elementwise.Step<Shape.output_shape(plan)> ->
558	    {result == Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value,
559	      Core.read_dynamic(original_right, right_index)) : Elementwise.Step<Shape.output_shape(plan)>} ->
560	    {result == Elementwise.step(operation, plan, index, Elementwise.State{original_left, original_right, original_output}) : Elementwise.Step<Shape.output_shape(plan)>}) ->
561	  Elementwise.StepCertificate<operation, plan, index, Elementwise.State{original_left, original_right, original_output}>:
562	  Core.DynamicRead{right, result, exact} = certificate
563	  match result:
564	    case Fail{error}:
565	      Elementwise.StepCertificate{Elementwise.Stop{left, right, error},
566	        lift(Elementwise.Stop{left, right, error}, Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Elementwise.Step<Shape.output_shape(plan)>,
567	          pair => Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value, pair),
568	          (right, Fail{error}), Core.read_dynamic(original_right, right_index), exact)), Unit{}}
569	    case Done{+right_value}:
570	      step_write_certificate(operation, plan, index, original_left, original_right, original_output,
571	        left_index, right_index, left_value, right_value, indices_exact,
572	        Core.write_certificate(Shape.output_shape(plan), original_output, index, Elementwise.scalar(operation, left_value, right_value)), left, right, left_exact, exact,
573	        result => equality => lift(result,
574	          Equal.trans(Elementwise.Step<Shape.output_shape(plan)>, result,
575	            Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value, (right, Done{right_value})),
576	            Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value, Core.read_dynamic(original_right, right_index)), equality,
577	            Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Elementwise.Step<Shape.output_shape(plan)>,
578	              pair => Elementwise.step_right(operation, Shape.output_shape(plan), index, left, original_output, left_value, pair),
579	              (right, Done{right_value}), Core.read_dynamic(original_right, right_index), exact))))
580	
581	def step_left_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
582	  -original_left: Core.Dynamic, original_right: Core.Dynamic, original_output: Core.Tensor<Shape.output_shape(plan)>,
583	  +left_index: U32, +right_index: U32,
584	  -indices_exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
585	  lift: @-result: Elementwise.Step<Shape.output_shape(plan)> ->
586	    {result == Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index,
587	      Core.read_dynamic(original_left, left_index)) : Elementwise.Step<Shape.output_shape(plan)>} ->
588	    {result == Elementwise.step(operation, plan, index, Elementwise.State{original_left, original_right, original_output}) : Elementwise.Step<Shape.output_shape(plan)>},
589	  certificate: Core.DynamicRead<original_left, left_index>) ->
590	  Elementwise.StepCertificate<operation, plan, index, Elementwise.State{original_left, original_right, original_output}>:
591	  Core.DynamicRead{left, result, exact} = certificate
592	  match result:
593	    case Fail{error}:
594	      Elementwise.StepCertificate{Elementwise.Stop{left, original_right, error},
595	        lift(Elementwise.Stop{left, original_right, error}, Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Elementwise.Step<Shape.output_shape(plan)>,
596	          pair => Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index, pair),
597	          (left, Fail{error}), Core.read_dynamic(original_left, left_index), exact)), Unit{}}
598	    case Done{+left_value}:
599	      step_right_certificate(operation, plan, index, original_left, original_right,
600	        left_index, right_index, left_value, indices_exact, Core.dynamic_read_certificate(original_right, right_index), original_output, left, exact,
601	        result => equality => lift(result,
602	          Equal.trans(Elementwise.Step<Shape.output_shape(plan)>, result,
603	            Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index, (left, Done{left_value})),
604	            Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index, Core.read_dynamic(original_left, left_index)), equality,
605	            Equal.cong(Core.Dynamic & Result<&2, &2, Core.Error, F32>, Elementwise.Step<Shape.output_shape(plan)>,
606	              pair => Elementwise.step_left(operation, Shape.output_shape(plan), index, original_right, original_output, right_index, pair),
607	              (left, Done{left_value}), Core.read_dynamic(original_left, left_index), exact))))
608	
609	def step_indices_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
610	  state: Elementwise.State<Shape.output_shape(plan)>, result: Result<&2, &1, Core.Error, U32 & U32>,
611	  exact: {result == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>}) -> Elementwise.StepCertificate<operation, plan, index, state>:
612	  Elementwise.State{left, right, output} = state
613	  match result:
614	    case Fail{error}:
615	      Elementwise.StepCertificate{Elementwise.Stop{left, right, error},
616	        Equal.cong(Result<&2, &1, Core.Error, U32 & U32>, Elementwise.Step<Shape.output_shape(plan)>,
617	          input => Elementwise.step_indices(operation, Shape.output_shape(plan), index, Elementwise.State{left, right, output}, input),
618	          Fail{error}, Elementwise.input_indices(plan, index), exact), Unit{}}
619	    case Done{indices}:
620	      (+left_index, +right_index) = indices
621	      step_left_certificate(operation, plan, index, left, right, output, left_index, right_index, exact,
622	        result => equality => Equal.trans(Elementwise.Step<Shape.output_shape(plan)>, result,
623	          Elementwise.step_indices(operation, Shape.output_shape(plan), index, Elementwise.State{left, right, output}, Done{(left_index, right_index)}),
624	          Elementwise.step(operation, plan, index, Elementwise.State{left, right, output}), equality,
625	          Equal.cong(Result<&2, &1, Core.Error, U32 & U32>, Elementwise.Step<Shape.output_shape(plan)>,
626	            input => Elementwise.step_indices(operation, Shape.output_shape(plan), index, Elementwise.State{left, right, output}, input),
627	            Done{(left_index, right_index)}, Elementwise.input_indices(plan, index), exact)),
628	        Core.dynamic_read_certificate(left, left_index))
629	
630	def step_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
631	  state: Elementwise.State<Shape.output_shape(plan)>) -> Elementwise.StepCertificate<operation, plan, index, state>:
632	  step_indices_certificate(operation, plan, index, state, Elementwise.input_indices(plan, index), {==})
633	
634	def converted_step_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat, +index: U32,
635	  +equal: {True{} == Nat.is_eq(U32.to_nat(index), cursor) : Bool}, -original: Elementwise.State<Shape.output_shape(plan)>,
636	  certificate: Elementwise.StepCertificate<operation, plan, index, original>) ->
637	  Elementwise.ConvertedCertificate<operation, plan, cursor, index, Shape.BTrue{equal}, original>:
638	  Elementwise.StepCertificate{result, exact, meaning} = certificate
639	  match result:
640	    case Elementwise.Stop{left, right, error}:
641	      Elementwise.ConvertedCertificate{Elementwise.NaturalStop{left, right, error},
642	        Equal.cong(Elementwise.Step<Shape.output_shape(plan)>, Elementwise.NaturalStep<Shape.output_shape(plan), cursor>,
643	          step => Elementwise.natural_step_result(Shape.output_shape(plan), cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal), step),
644	          Elementwise.Stop{left, right, error}, Elementwise.step(operation, plan, index, original), exact), Unit{}}
645	    case Elementwise.Continue{state}:
646	      Elementwise.ConvertedCertificate{Elementwise.NaturalContinue{state, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal)},
647	        Equal.cong(Elementwise.Step<Shape.output_shape(plan)>, Elementwise.NaturalStep<Shape.output_shape(plan), cursor>,
648	          step => Elementwise.natural_step_result(Shape.output_shape(plan), cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal), step),
649	          Elementwise.Continue{state}, Elementwise.step(operation, plan, index, original), exact), meaning}
650	
651	def natural_decision_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat, +index: U32,
652	  decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(index), cursor)>, state: Elementwise.State<Shape.output_shape(plan)>) ->
653	  Elementwise.ConvertedCertificate<operation, plan, cursor, index, decision, state>:
654	  match decision:
655	    case Shape.BFalse{equal}:
656	      Elementwise.State{left, right, output} = state
657	      Elementwise.ConvertedCertificate{Elementwise.NaturalStop{left, right, Core.StorageError{Storage.InvalidIndex{}}}, {==}, Unit{}}
658	    case Shape.BTrue{+equal}:
659	      converted_step_certificate(operation, plan, cursor, index, equal, state, step_certificate(operation, plan, index, state))
660	
661	def natural_converted_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
662	  -original: Elementwise.State<Shape.output_shape(plan)>,
663	  certificate: Elementwise.ConvertedCertificate<operation, plan, cursor, U32.from_nat(cursor), Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), original>) ->
664	  Elementwise.NaturalCertificate<operation, plan, cursor, original>:
665	  Elementwise.ConvertedCertificate{result, exact, meaning} = certificate
666	  Elementwise.NaturalCertificate{result, exact, meaning}
667	
668	def natural_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
669	  state: Elementwise.State<Shape.output_shape(plan)>) -> Elementwise.NaturalCertificate<operation, plan, cursor, state>:
670	  natural_converted_certificate(operation, plan, cursor, state,
671	    natural_decision_certificate(operation, plan, cursor, U32.from_nat(cursor), Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), state))
672	
673	def lt_zero(+number: Nat, proof: Shape.LT(number, 0n)) -> Empty:
674	  match number:
675	    case 0n:
676	      match proof:
677	    case 1n+p:
678	      match proof:
679	
680	def lt_previous_or_equal(+number: Nat, +cursor: Nat, proof: Shape.LT(number, 1n+cursor)) ->
681	  Either<Shape.LT(number, cursor), {number == cursor : Nat}>:
682	  match number cursor:
683	    case 0n 0n:
684	      Inr{{==}}
685	    case 0n 1n+p:
686	      Inl{Unit{}}
687	    case 1n+p 0n:
688	      Empty.absurd(Either<Shape.LT(1n+p, 0n), {1n+p == 0n : Nat}>, lt_zero(p, proof))
689	    case 1n+p 1n+q:
690	      {\{Inl: earlier => Inl{earlier}; Inr: equal => Inr{Equal.cong(Nat, Nat, n => 1n+n, p, q, equal)}} :
691	        Either<Shape.LT(p, q), {p == q : Nat}> -> Either<Shape.LT(1n+p, 1n+q), {1n+p == 1n+q : Nat}>}(lt_previous_or_equal(p, q, proof))
692	
693	def lt_big_small_different(+small: Nat, +big: Nat, proof: Shape.LT(small, big)) -> {Nat.is_eq(big, small) == False{} : Bool}:
694	  match small big:
695	    case 0n 0n:
696	      match proof:
697	    case 0n 1n+p:
698	      {==}
699	    case 1n+p 0n:
700	      match proof:
701	    case 1n+p 1n+q:
702	      lt_big_small_different(p, q, proof)
703	
704	def add_successor_right(+left: Nat, -right: Nat) -> {Nat.add(left, 1n+right) == 1n+Nat.add(left, right) : Nat}:
705	  match left:
706	    case 0n:
707	      {==}
708	    case 1n+p:
709	      Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 1n+right), 1n+Nat.add(p, right), add_successor_right(p, right))
710	
711	def expected_left_same(+operation: Elementwise.Operation, -current: Core.Dynamic, -original: Core.Dynamic, +index: U32,
712	  left: Maybe<&2, F32>, equal: {Core.checked_observe_dynamic(current, index) == Core.checked_observe_dynamic(original, index) : Maybe<&2, F32>}) ->
713	  {Elementwise.expected_left(operation, current, index, left) == Elementwise.expected_left(operation, original, index, left) : Maybe<&2, F32>}:
714	  match left:
715	    case None{}:
716	      {==}
717	    case Some{+value}:
718	      Equal.cong(Maybe<&2, F32>, Maybe<&2, F32>, right => Elementwise.expected_right(operation, value, right),
719	        Core.checked_observe_dynamic(current, index), Core.checked_observe_dynamic(original, index), equal)
720	
721	type ExpectedSame<-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -index: U32,
722	  -original_left: Core.Dynamic, -original_right: Core.Dynamic, -left: Core.Dynamic, -right: Core.Dynamic> is Data:
723	  ExpectedSame{-equal: {Elementwise.expected(operation, plan, left, right, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>}}
724	
725	def expected_same_indices(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
726	  -original_left: Core.Dynamic, -original_right: Core.Dynamic, -left: Core.Dynamic, -right: Core.Dynamic,
727	  -left_same: Elementwise.SameSource(original_left, left), -right_same: Elementwise.SameSource(original_right, right),
728	  result: Result<&2, &1, Core.Error, U32 & U32>,
729	  -exact: {result == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>}) ->
730	  ExpectedSame<operation, plan, index, original_left, original_right, left, right>:
731	  match result:
732	    case Fail{error}:
733	      ExpectedSame{
734	        %exact : {Elementwise.expected_indices(operation, left, right, _) == Elementwise.expected_indices(operation, original_left, original_right, _) : Maybe<&2, F32>}
735	        {==}}
736	    case Done{indices}:
737	      (+left_index, +right_index) = indices
738	      ExpectedSame{
739	        %exact : {Elementwise.expected_indices(operation, left, right, _) == Elementwise.expected_indices(operation, original_left, original_right, _) : Maybe<&2, F32>}
740	        Equal.trans(Maybe<&2, F32>, Elementwise.expected_left(operation, right, right_index, Core.checked_observe_dynamic(left, left_index)),
741	          Elementwise.expected_left(operation, right, right_index, Core.checked_observe_dynamic(original_left, left_index)),
742	          Elementwise.expected_left(operation, original_right, right_index, Core.checked_observe_dynamic(original_left, left_index)),
743	          Equal.cong(Maybe<&2, F32>, Maybe<&2, F32>, value => Elementwise.expected_left(operation, right, right_index, value),
744	            Core.checked_observe_dynamic(left, left_index), Core.checked_observe_dynamic(original_left, left_index), left_same(left_index)),
745	          expected_left_same(operation, right, original_right, right_index, Core.checked_observe_dynamic(original_left, left_index), right_same(right_index)))}
746	
747	def expected_same(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
748	  -original_left: Core.Dynamic, -original_right: Core.Dynamic, -left: Core.Dynamic, -right: Core.Dynamic,
749	  -left_same: Elementwise.SameSource(original_left, left), -right_same: Elementwise.SameSource(original_right, right)) ->
750	  ExpectedSame<operation, plan, index, original_left, original_right, left, right>:
751	  expected_same_indices(operation, plan, index, original_left, original_right, left, right, left_same, right_same, Elementwise.input_indices(plan, index), {==})
752	
753	type PrefixModel<-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -original_left: Core.Dynamic, -original_right: Core.Dynamic,
754	  -cursor: Nat, -output: Core.Tensor<Shape.output_shape(plan)>> is Data:
755	  PrefixModel{-prefix: Elementwise.PrefixInvariant(operation, plan, original_left, original_right, cursor, Core.Packed{Shape.output_shape(plan), output})}
756	
757	def prefix_previous(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
758	  -original_left: Core.Dynamic, -original_right: Core.Dynamic, +cursor: Nat, +index: U32,
759	  -before: Core.Tensor<Shape.output_shape(plan)>, -after: Core.Tensor<Shape.output_shape(plan)>,
760	  converted: {U32.to_nat(index) == cursor : Nat},
761	  prefix: Elementwise.PrefixInvariant(operation, plan, original_left, original_right, cursor, Core.Packed{Shape.output_shape(plan), before}),
762	  frame: @+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), before}, other) ->
763	    @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
764	      Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
765	        {Core.observe(Shape.output_shape(plan), after, other) == Core.observe(Shape.output_shape(plan), before, other) : Maybe<&2, F32>},
766	  +other: U32, +earlier: Shape.LT(U32.to_nat(other), cursor)) ->
767	  Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
768	    {Core.observe(Shape.output_shape(plan), after, other) == Elementwise.expected(operation, plan, original_left, original_right, other) : Maybe<&2, F32>}:
769	  {\{Tuple: before_checked => before_equal =>
770	    {\{Tuple: after_checked => after_equal => (after_checked,
771	      Equal.trans(Maybe<&2, F32>, Core.observe(Shape.output_shape(plan), after, other), Core.observe(Shape.output_shape(plan), before, other),
772	        Elementwise.expected(operation, plan, original_left, original_right, other), after_equal, before_equal))} :
773	      (Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
774	        {Core.observe(Shape.output_shape(plan), after, other) == Core.observe(Shape.output_shape(plan), before, other) : Maybe<&2, F32>}) ->
775	      (Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
776	        {Core.observe(Shape.output_shape(plan), after, other) == Elementwise.expected(operation, plan, original_left, original_right, other) : Maybe<&2, F32>})}(frame(other)(before_checked)(
777	          %Equal.sym(Nat, U32.to_nat(index), cursor, converted) : {Nat.is_eq(_, U32.to_nat(other)) == False{} : Bool}
778	          lt_big_small_different(U32.to_nat(other), cursor, earlier)))
779	  } :
780	    (Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), before}, other) &
781	      {Core.observe(Shape.output_shape(plan), before, other) == Elementwise.expected(operation, plan, original_left, original_right, other) : Maybe<&2, F32>}) ->
782	    (Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
783	      {Core.observe(Shape.output_shape(plan), after, other) == Elementwise.expected(operation, plan, original_left, original_right, other) : Maybe<&2, F32>})}(prefix(other)(earlier))
784	
785	def prefix_equal(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
786	  -original_left: Core.Dynamic, -original_right: Core.Dynamic, +cursor: Nat, +index: U32,
787	  -after: Core.Tensor<Shape.output_shape(plan)>, converted: {U32.to_nat(index) == cursor : Nat},
788	  checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, index),
789	  observed: {Core.observe(Shape.output_shape(plan), after, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>},
790	  +other: U32, equal: {U32.to_nat(other) == cursor : Nat}) ->
791	  Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
792	    {Core.observe(Shape.output_shape(plan), after, other) == Elementwise.expected(operation, plan, original_left, original_right, other) : Maybe<&2, F32>}:
793	  %Injective.u32_natural_injective(index, other)(Equal.trans(Nat, U32.to_nat(index), cursor, U32.to_nat(other), converted,
794	    Equal.sym(Nat, U32.to_nat(other), cursor, equal))) :
795	    Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, _) &
796	      {Core.observe(Shape.output_shape(plan), after, _) == Elementwise.expected(operation, plan, original_left, original_right, _) : Maybe<&2, F32>}
797	  (checked, observed)
798	
799	def prefix_extend(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
800	  -original_left: Core.Dynamic, -original_right: Core.Dynamic, +cursor: Nat, +index: U32,
801	  -before: Core.Tensor<Shape.output_shape(plan)>, -after: Core.Tensor<Shape.output_shape(plan)>,
802	  -converted: {U32.to_nat(index) == cursor : Nat},
803	  -prefix: Elementwise.PrefixInvariant(operation, plan, original_left, original_right, cursor, Core.Packed{Shape.output_shape(plan), before}),
804	  -checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, index),
805	  -observed: {Core.observe(Shape.output_shape(plan), after, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>},
806	  -frame: @+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), before}, other) ->
807	    @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
808	      Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
809	        {Core.observe(Shape.output_shape(plan), after, other) == Core.observe(Shape.output_shape(plan), before, other) : Maybe<&2, F32>}) ->
810	  PrefixModel<operation, plan, original_left, original_right, 1n+cursor, after>:
811	  PrefixModel{other => bound =>
812	    {\{Inl: earlier => prefix_previous(operation, plan, original_left, original_right, cursor, index, before, after, converted, prefix, frame, other, earlier);
813	      Inr: equal => prefix_equal(operation, plan, original_left, original_right, cursor, index, after, converted, checked, observed, other, equal)} :
814	      Either<Shape.LT(U32.to_nat(other), cursor), {U32.to_nat(other) == cursor : Nat}> ->
815	        (Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
816	          {Core.observe(Shape.output_shape(plan), after, other) == Elementwise.expected(operation, plan, original_left, original_right, other) : Maybe<&2, F32>})}(lt_previous_or_equal(U32.to_nat(other), cursor, bound))}
817	
818	def invariant_left(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -original_left: Core.Dynamic, -original_right: Core.Dynamic,
819	  -cursor: Nat, -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
820	  invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, Elementwise.State{left, right, output})) ->
821	  Elementwise.SameSource(original_left, left):
822	  (same, rest) = invariant
823	  same
824	
825	def invariant_right(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -original_left: Core.Dynamic, -original_right: Core.Dynamic,
826	  -cursor: Nat, -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
827	  invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, Elementwise.State{left, right, output})) ->
828	  Elementwise.SameSource(original_right, right):
829	  (same, rest) = invariant
830	  (right_same, prefix) = rest
831	  right_same
832	
833	def invariant_prefix(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -original_left: Core.Dynamic, -original_right: Core.Dynamic,
834	  -cursor: Nat, -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
835	  invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, Elementwise.State{left, right, output})) ->
836	  Elementwise.PrefixInvariant(operation, plan, original_left, original_right, cursor, Core.Packed{Shape.output_shape(plan), output}):
837	  (same, rest) = invariant
838	  (right_same, prefix) = rest
839	  prefix
840	
841	def step_same_left(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -index: U32,
842	  -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
843	  -after_left: Core.Dynamic, -after_right: Core.Dynamic, -after_output: Core.Tensor<Shape.output_shape(plan)>,
844	  meaning: Elementwise.StepMeaning(operation, plan, index, Elementwise.State{left, right, output}, Elementwise.Continue{Elementwise.State{after_left, after_right, after_output}})) ->
845	  Elementwise.SameSource(left, after_left):
846	  (same, rest) = meaning
847	  same
848	
849	def step_same_right(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -index: U32,
850	  -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
851	  -after_left: Core.Dynamic, -after_right: Core.Dynamic, -after_output: Core.Tensor<Shape.output_shape(plan)>,
852	  meaning: Elementwise.StepMeaning(operation, plan, index, Elementwise.State{left, right, output}, Elementwise.Continue{Elementwise.State{after_left, after_right, after_output}})) ->
853	  Elementwise.SameSource(right, after_right):
854	  (same, rest) = meaning
855	  (right_same, result) = rest
856	  right_same
857	
858	def step_checked(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -index: U32,
859	  -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
860	  -after_left: Core.Dynamic, -after_right: Core.Dynamic, -after_output: Core.Tensor<Shape.output_shape(plan)>,
861	  meaning: Elementwise.StepMeaning(operation, plan, index, Elementwise.State{left, right, output}, Elementwise.Continue{Elementwise.State{after_left, after_right, after_output}})) ->
862	  Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after_output}, index):
863	  (same, rest) = meaning
864	  (right_same, result) = rest
865	  (checked, values) = result
866	  checked
867	
868	def step_observed(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -index: U32,
869	  -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
870	  -after_left: Core.Dynamic, -after_right: Core.Dynamic, -after_output: Core.Tensor<Shape.output_shape(plan)>,
871	  meaning: Elementwise.StepMeaning(operation, plan, index, Elementwise.State{left, right, output}, Elementwise.Continue{Elementwise.State{after_left, after_right, after_output}})) ->
872	  {Core.observe(Shape.output_shape(plan), after_output, index) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}:
873	  (same, rest) = meaning
874	  (right_same, result) = rest
875	  (checked, values) = result
876	  (observed, frame) = values
877	  observed
878	
879	def step_frame(-operation: Elementwise.Operation, -plan: Shape.BroadcastPlan, -index: U32,
880	  -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
881	  -after_left: Core.Dynamic, -after_right: Core.Dynamic, -after_output: Core.Tensor<Shape.output_shape(plan)>,
882	  meaning: Elementwise.StepMeaning(operation, plan, index, Elementwise.State{left, right, output}, Elementwise.Continue{Elementwise.State{after_left, after_right, after_output}})) ->
883	  @+other: U32 -> @checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), output}, other) ->
884	    @different: {Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) == False{} : Bool} ->
885	      Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after_output}, other) &
886	        {Core.observe(Shape.output_shape(plan), after_output, other) == Core.observe(Shape.output_shape(plan), output, other) : Maybe<&2, F32>}:
887	  (same, rest) = meaning
888	  (right_same, result) = rest
889	  (checked, values) = result
890	  (observed, frame) = values
891	  frame
892	
893	def invariant_advance(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, -original_left: Core.Dynamic, -original_right: Core.Dynamic,
894	  +cursor: Nat, +index: U32, -converted: {U32.to_nat(index) == cursor : Nat},
895	  before: Elementwise.State<Shape.output_shape(plan)>, after: Elementwise.State<Shape.output_shape(plan)>,
896	  -invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, before),
897	  -meaning: Elementwise.StepMeaning(operation, plan, index, before, Elementwise.Continue{after})) ->
898	  Elementwise.InvariantModel<operation, plan, original_left, original_right, 1n+cursor, after>:
899	  Elementwise.State{left, right, output} = before
900	  Elementwise.State{after_left, after_right, after_output} = after
901	  Elementwise.InvariantModel{(other => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(after_left, other), Core.checked_observe_dynamic(left, other), Core.checked_observe_dynamic(original_left, other),
902	      step_same_left(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning)(other),
903	      invariant_left(operation, plan, original_left, original_right, cursor, left, right, output, invariant)(other)),
904	    (other => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(after_right, other), Core.checked_observe_dynamic(right, other), Core.checked_observe_dynamic(original_right, other),
905	      step_same_right(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning)(other),
906	      invariant_right(operation, plan, original_left, original_right, cursor, left, right, output, invariant)(other)),
907	      {\{PrefixModel: prefix => prefix} : PrefixModel<operation, plan, original_left, original_right, 1n+cursor, after_output> ->
908	        Elementwise.PrefixInvariant(operation, plan, original_left, original_right, 1n+cursor, Core.Packed{Shape.output_shape(plan), after_output})}(prefix_extend(operation, plan, original_left, original_right, cursor, index, output, after_output, converted,
909	          invariant_prefix(operation, plan, original_left, original_right, cursor, left, right, output, invariant),
910	          step_checked(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning),
911	          Equal.trans(Maybe<&2, F32>, Core.observe(Shape.output_shape(plan), after_output, index), Elementwise.expected(operation, plan, left, right, index),
912	            Elementwise.expected(operation, plan, original_left, original_right, index),
913	            step_observed(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning),
914	            {\{ExpectedSame: equal => equal} : ExpectedSame<operation, plan, index, original_left, original_right, left, right> ->
915	              {Elementwise.expected(operation, plan, left, right, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>}}(expected_same(operation, plan, index, original_left, original_right, left, right,
916	                invariant_left(operation, plan, original_left, original_right, cursor, left, right, output, invariant),
917	                invariant_right(operation, plan, original_left, original_right, cursor, left, right, output, invariant)))),
918	          step_frame(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning)))))}
919	
920	def initial_invariant(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
921	  -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>) ->
922	  Elementwise.InvariantModel<operation, plan, left, right, 0n, Elementwise.State{left, right, output}>:
923	  Elementwise.InvariantModel{(other => {==}, (other => {==}, other => bound =>
924	    Empty.absurd(Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), output}, other) &
925	      {Core.observe(Shape.output_shape(plan), output, other) == Elementwise.expected(operation, plan, left, right, other) : Maybe<&2, F32>}, lt_zero(U32.to_nat(other), bound))))}
926	
927	def add_zero_right(+number: Nat) -> {Nat.add(number, 0n) == number : Nat}:
928	  match number:
929	    case 0n:
930	      {==}
931	    case 1n+p:
932	      Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 0n), p, add_zero_right(p))
933	
934	def loop_continue_certificate(+remaining: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
935	  -original_left: Core.Dynamic, -original_right: Core.Dynamic, -original: Elementwise.State<Shape.output_shape(plan)>,
936	  -after: Elementwise.State<Shape.output_shape(plan)>, -index: U32, -converted: {U32.to_nat(index) == cursor : Nat},
937	  natural_exact: {Elementwise.NaturalContinue{after, index, converted} == Elementwise.natural_step(operation, plan, cursor, original) : Elementwise.NaturalStep<Shape.output_shape(plan), cursor>},
938	  certificate: Elementwise.LoopCertificate<remaining, operation, plan, 1n+cursor, original_left, original_right, after>) ->
939	  Elementwise.LoopCertificate<1n+remaining, operation, plan, cursor, original_left, original_right, original>:
940	  Elementwise.LoopCertificate{result, exact, meaning} = certificate
941	  Elementwise.LoopCertificate{result,
942	    Equal.trans((Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>, result,
943	      Elementwise.loop(remaining, operation, plan, 1n+cursor, after), Elementwise.loop(1n+remaining, operation, plan, cursor, original), exact,
944	      Equal.cong(Elementwise.NaturalStep<Shape.output_shape(plan), cursor>, (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
945	        step => Elementwise.finish_step(Shape.output_shape(plan), cursor, state => Elementwise.loop(remaining, operation, plan, 1n+cursor, state), step),
946	        Elementwise.NaturalContinue{after, index, converted}, Elementwise.natural_step(operation, plan, cursor, original), natural_exact)),
947	    %Equal.sym(Nat, Nat.add(cursor, 1n+remaining), Nat.add(1n+cursor, remaining), add_successor_right(cursor, remaining)) :
948	      Elementwise.LoopMeaning(operation, plan, original_left, original_right, _, result)
949	    meaning}
950	
951	def loop_after_certificate(+remaining: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
952	  -original_left: Core.Dynamic, -original_right: Core.Dynamic, -original: Elementwise.State<Shape.output_shape(plan)>,
953	  -invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, original),
954	  certificate: Elementwise.NaturalCertificate<operation, plan, cursor, original>,
955	  rec: @state: Elementwise.State<Shape.output_shape(plan)> ->
956	    @-invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, 1n+cursor, state) ->
957	      Elementwise.LoopCertificate<remaining, operation, plan, 1n+cursor, original_left, original_right, state>) ->
958	  Elementwise.LoopCertificate<1n+remaining, operation, plan, cursor, original_left, original_right, original>:
959	  Elementwise.NaturalCertificate{result, exact, meaning} = certificate
960	  match result:
961	    case Elementwise.NaturalStop{left, right, error}:
962	      Elementwise.LoopCertificate{((left, right), Fail{error}),
963	        Equal.cong(Elementwise.NaturalStep<Shape.output_shape(plan), cursor>, (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
964	          step => Elementwise.finish_step(Shape.output_shape(plan), cursor, state => Elementwise.loop(remaining, operation, plan, 1n+cursor, state), step),
965	          Elementwise.NaturalStop{left, right, error}, Elementwise.natural_step(operation, plan, cursor, original), exact), Unit{}}
966	    case Elementwise.NaturalContinue{state, index, converted}:
967	      loop_continue_certificate(remaining, operation, plan, cursor, original_left, original_right, original, state, index, converted, exact,
968	        rec(state,
969	          {\{Elementwise.InvariantModel: invariant => invariant} :
970	            Elementwise.InvariantModel<operation, plan, original_left, original_right, 1n+cursor, state> ->
971	              Elementwise.StateInvariant(operation, plan, original_left, original_right, 1n+cursor, state)}(invariant_advance(operation, plan, original_left, original_right, cursor, index, converted,
972	                original, state, invariant, meaning))))
973	
974	def loop_certificate(fuel: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
975	  -original_left: Core.Dynamic, -original_right: Core.Dynamic, state: Elementwise.State<Shape.output_shape(plan)>,
976	  -invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, state)) ->
977	  Elementwise.LoopCertificate<fuel, operation, plan, cursor, original_left, original_right, state>:
978	  match fuel:
979	    case 0n:
980	      Elementwise.State{left, right, output} = state
981	      Elementwise.LoopCertificate{((left, right), Done{Core.Packed{Shape.output_shape(plan), output}}), {==},
982	        %Equal.sym(Nat, Nat.add(cursor, 0n), cursor, add_zero_right(cursor)) :
983	          Elementwise.PrefixInvariant(operation, plan, original_left, original_right, _, Core.Packed{Shape.output_shape(plan), output})
984	        invariant_prefix(operation, plan, original_left, original_right, cursor, left, right, output, invariant)}
985	    case 1n++remaining:
986	      loop_after_certificate(remaining, operation, plan, cursor, original_left, original_right, state, invariant,
987	        natural_certificate(operation, plan, cursor, state),
988	        state => invariant => loop_certificate(remaining, operation, plan, 1n+cursor, original_left, original_right, state, invariant))
989	
990	def successful_pair_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, -left: Core.Dynamic, -right: Core.Dynamic,
991	  result: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
992	  -meaning: Elementwise.LoopMeaning(operation, plan, left, right, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), result)) ->
993	  Elementwise.MappingModel<operation, plan, left, right, result>:
994	  (inputs, outcome) = result
995	  match outcome:
996	    case Fail{error}:
997	      Elementwise.MappingModel{Unit{}}
998	    case Done{output}:
999	      Elementwise.MappingModel{index => bound => Pair.snd(Core.ObservationChecked(output, index),
1000	        {Core.observe_dynamic(output, index) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}, meaning(index)(bound))}
1001	
1002	def successful_loop_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
1003	  -left: Core.Dynamic, -right: Core.Dynamic, -output: Core.Tensor<Shape.output_shape(plan)>,
1004	  certificate: Elementwise.LoopCertificate<Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, 0n, left, right, Elementwise.State{left, right, output}>) ->
1005	  Elementwise.MappingModel<operation, plan, left, right,
1006	    Elementwise.loop(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, 0n, Elementwise.State{left, right, output})>:
1007	  Elementwise.LoopCertificate{result, exact, meaning} = certificate
1008	  Elementwise.MappingModel{
1009	    %exact : Elementwise.SuccessfulMapping(operation, plan, left, right, _)
1010	    {\{Elementwise.MappingModel: mapping => mapping} : Elementwise.MappingModel<operation, plan, left, right, result> ->
1011	      Elementwise.SuccessfulMapping(operation, plan, left, right, result)}(successful_pair_mapping(operation, plan, left, right, result, meaning))}
1012	
1013	def successful_loop_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
1014	  left: Core.Dynamic, right: Core.Dynamic, output: Core.Tensor<Shape.output_shape(plan)>) ->
1015	  Elementwise.MappingModel<operation, plan, left, right,
1016	    Elementwise.loop(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, 0n, Elementwise.State{left, right, output})>:
1017	  successful_loop_certificate(operation, plan, left, right, output,
1018	    loop_certificate(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, 0n, left, right, Elementwise.State{left, right, output},
1019	      {\{Elementwise.InvariantModel: invariant => invariant} : Elementwise.InvariantModel<operation, plan, left, right, 0n, Elementwise.State{left, right, output}> ->
1020	        Elementwise.StateInvariant(operation, plan, left, right, 0n, Elementwise.State{left, right, output})}(initial_invariant(operation, plan, left, right, output))))
1021	
1022	def Laws.checked_writer_pair(shape, original, index, value):
1023	  Core.write_certificate(shape, original, index, value)
1024	
1025	def Laws.checked_writer_source(shape, original, index, value):
1026	  checked_update_model(shape, original, index, value)
1027	
1028	def Laws.actual_elementwise_step(operation, plan, index, original):
1029	  step_certificate(operation, plan, index, original)
1030	
1031	def Laws.successful_elementwise_loop(operation, plan, left, right, output):
1032	  successful_loop_mapping(operation, plan, left, right, output)
1033	
1034	def successful_cached_loop_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
1035	  left: Core.Dynamic, right: Core.Dynamic, output: Core.Tensor<Shape.output_shape(plan)>) ->
1036	  Elementwise.MappingModel<operation, plan, left, right,
1037	    Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output})>:
1038	  Elementwise.MappingModel{
1039	    %Equal.sym(Nat, Shape.elements(Shape.output_shape(plan)), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), Shape.elements_exact(Shape.output_shape(plan))) :
1040	      Elementwise.SuccessfulMapping(operation, plan, left, right, Elementwise.loop(_, operation, plan, 0n, Elementwise.State{left, right, output}))
1041	    {\{Elementwise.MappingModel: mapping => mapping} :
1042	      Elementwise.MappingModel<operation, plan, left, right,
1043	        Elementwise.loop(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, 0n, Elementwise.State{left, right, output})> ->
1044	      Elementwise.SuccessfulMapping(operation, plan, left, right,
1045	        Elementwise.loop(Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), operation, plan, 0n, Elementwise.State{left, right, output}))}(successful_loop_mapping(operation, plan, left, right, output))}
1046	
1047	def allocated_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
1048	  result: Result<&2, &1, Core.Error, Core.Tensor<Shape.output_shape(plan)>>, left: Core.Dynamic, right: Core.Dynamic) ->
1049	  Elementwise.MappingModel<operation, plan, left, right, Elementwise.allocated(operation, plan, left, right, result)>:
1050	  match result:
1051	    case Fail{error}:
1052	      Elementwise.MappingModel{Unit{}}
1053	    case Done{output}:
1054	      successful_cached_loop_mapping(operation, plan, left, right, output)
1055	
1056	def successful_allocated_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, left: Core.Dynamic, right: Core.Dynamic) ->
1057	  Elementwise.MappingModel<operation, plan, left, right, Elementwise.allocated(operation, plan, left, right, Core.new(Shape.output_shape(plan), 0.0))>:
1058	  Elementwise.MappingModel{
1059	    {\{Elementwise.MappingModel: mapping => mapping} :
1060	      Elementwise.MappingModel<operation, plan, left, right, Elementwise.allocated(operation, plan, left, right, Core.new(Shape.output_shape(plan), 0.0))> ->
1061	      Elementwise.SuccessfulMapping(operation, plan, left, right, Elementwise.allocated(operation, plan, left, right, Core.new(Shape.output_shape(plan), 0.0)))}(allocated_mapping(operation, plan, Core.new(Shape.output_shape(plan), 0.0), left, right))}
1062	
1063	def successful_binary_mapping(+operation: Elementwise.Operation, left: Core.Dynamic, right: Core.Dynamic) ->
1064	  Elementwise.BinaryModel<operation, left, right, Elementwise.binary(operation, left, right)>:
1065	  Parallel.binary_mapping(operation, left, right)
1066	
1067	def Laws.successful_elementwise_cached_loop(operation, plan, left, right, output):
1068	  successful_cached_loop_mapping(operation, plan, left, right, output)
1069	
1070	def Laws.successful_elementwise_allocated(operation, plan, left, right):
1071	  successful_allocated_mapping(operation, plan, left, right)
1072	
1073	def Laws.successful_elementwise_binary(operation, left, right):
1074	  successful_binary_mapping(operation, left, right)
1075	
1076	def independent_pair_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, -left: Core.Dynamic, -right: Core.Dynamic,
1077	  result: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
1078	  -shared: Elementwise.SuccessfulMapping(operation, plan, left, right, result)) -> Laws.IndependentModel<operation, plan, left, right, result>:
1079	  (inputs, outcome) = result
1080	  match outcome:
1081	    case Fail{error}:
1082	      Laws.IndependentModel{Unit{}}
1083	    case Done{output}:
1084	      Laws.IndependentModel{index => inside => Equal.trans(Maybe<&2, F32>, Core.observe_dynamic(output, index), Elementwise.expected(operation, plan, left, right, index),
1085	        Projection.specified_expected(operation, left, right, Projection.offset_spec(plan, U32.to_nat(index))), shared(index)(inside),
1086	        Projection.expected_projection_refines(operation, plan, left, right, index))}
1087	
1088	def independent_loop_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
1089	  left: Core.Dynamic, right: Core.Dynamic, output: Core.Tensor<Shape.output_shape(plan)>) ->
1090	  Laws.IndependentModel<operation, plan, left, right,
1091	    Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output})>:
1092	  Laws.IndependentModel{
1093	    {\{Elementwise.MappingModel: mapping =>
1094	      {\{Laws.IndependentModel: independent => independent} :
1095	        Laws.IndependentModel<operation, plan, left, right, Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output})> ->
1096	          Laws.IndependentMapping(operation, plan, left, right, Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output}))}(independent_pair_mapping(operation, plan, left, right,
1097	            Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output}), mapping))
1098	    } : Elementwise.MappingModel<operation, plan, left, right, Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output})> ->
1099	      Laws.IndependentMapping(operation, plan, left, right, Elementwise.loop(Shape.elements(Shape.output_shape(plan)), operation, plan, 0n, Elementwise.State{left, right, output}))}(successful_cached_loop_mapping(operation, plan, left, right, output))}
1100	
1101	type IndependentPlannedModel<-operation: Elementwise.Operation, -left: Core.Dynamic, -right: Core.Dynamic,
1102	  -result: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
1103	  -plan: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>> is Data:
1104	  IndependentPlannedModel{-mapping: Laws.IndependentPlanned(operation, left, right, result, plan)}
1105	
1106	def independent_planned_pair(+operation: Elementwise.Operation, -left: Core.Dynamic, -right: Core.Dynamic,
1107	  result: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
1108	  plan: Result<&2, &2, Shape.Error, Shape.BroadcastPlan>, -shared: Elementwise.PlannedMeaning(operation, left, right, result, plan)) ->
1109	  IndependentPlannedModel<operation, left, right, result, plan>:
1110	  match plan:
1111	    case Fail{error}:
1112	      IndependentPlannedModel{Unit{}}
1113	    case Done{+plan}:
1114	      IndependentPlannedModel{{\{Laws.IndependentModel: independent => independent} : Laws.IndependentModel<operation, plan, left, right, result> -> Laws.IndependentMapping(operation, plan, left, right, result)}(independent_pair_mapping(operation, plan, left, right, result, shared))}
1115	
1116	def independent_binary_reasoning(+operation: Elementwise.Operation, -left: Core.Dynamic, -right: Core.Dynamic) ->
1117	  Laws.IndependentBinaryModel<operation, left, right, Elementwise.binary(operation, left, right)>:
1118	  Laws.IndependentBinaryModel{
1119	    {\{Elementwise.BinaryModel: mapping =>
1120	      {\{IndependentPlannedModel: independent => independent} :
1121	        IndependentPlannedModel<operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right)> ->
1122	          Laws.IndependentPlanned(operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right))}(independent_planned_pair(operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right), mapping))
1123	    } : Elementwise.BinaryModel<operation, left, right, Elementwise.binary(operation, left, right)> ->
1124	      Laws.IndependentPlanned(operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right))}(successful_binary_mapping(operation, left, right))}
1125	
1126	def independent_binary_mapping(+operation: Elementwise.Operation, left: Core.Dynamic, right: Core.Dynamic) ->
1127	  Laws.IndependentBinaryModel<operation, left, right, Elementwise.binary(operation, left, right)>:
1128	  Laws.IndependentBinaryModel{
1129	    {\{Laws.IndependentBinaryModel: mapping => mapping} :
1130	      Laws.IndependentBinaryModel<operation, left, right, Elementwise.binary(operation, left, right)> ->
1131	        Laws.IndependentPlanned(operation, left, right, Elementwise.binary(operation, left, right), Elementwise.plan_for(left, right))}(independent_binary_reasoning(operation, left, right))}
1132	
1133	def Laws.independent_elementwise_loop(operation, plan, left, right, output):
1134	  independent_loop_mapping(operation, plan, left, right, output)
1135	
1136	def Laws.independent_elementwise_binary(operation, left, right):
1137	  independent_binary_mapping(operation, left, right)
1138	
1139	def Laws.public_add_dispatch(left, right):
1140	  {==}
1141	
1142	def Laws.public_sub_dispatch(left, right):
1143	  {==}
1144	
1145	def Laws.public_mul_dispatch(left, right):
1146	  {==}