def loop_continue_certificate

bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:934

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

934def 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}