PlanProofs.broadcast_checked_complete: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend as PlanProofs
Lines 178-191 of bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&start_line=178&end_line=191

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend as Unique
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws

def broadcast_checked_complete(+left: Shape.Shape, +right: Shape.Shape, +output: List<&2, U32>, +alignment: Shape.Broadcast<Shape.extents(left), Shape.extents(right), Shape.naturals(output)>, +rank_bound: Shape.LE(Shape.rank_dimensions(output), 4n), +capacity_bound: Shape.LE(Shape.logical_numel(output), 1048576n)) -> {Laws.broadcast_built(Shape.broadcast_checked(left, right)) == True{} : Bool}:
  match alignment:
    case Shape.BAlign{+left_padding, +right_padding, +minimal, +aligned}:
      +left_rank = Shape.rank_dimensions(Shape.dimensions(left))
      +right_rank = Shape.rank_dimensions(Shape.dimensions(right))
      +left_extra = Nat.sub(right_rank, left_rank)
      +right_extra = Nat.sub(left_rank, right_rank)
      +balanced = Equal.trans(Nat, Nat.add(left_padding, left_rank), Nat.add(left_padding, List.length(&2, Nat, Shape.extents(left))), Nat.add(right_padding, right_rank), Equal.cong(Nat, Nat, value => Nat.add(left_padding, value), left_rank, List.length(&2, Nat, Shape.extents(left)), Shape.rank_naturals(Shape.dimensions(left))), Equal.trans(Nat, Nat.add(left_padding, List.length(&2, Nat, Shape.extents(left))), Nat.add(right_padding, List.length(&2, Nat, Shape.extents(right))), Nat.add(right_padding, right_rank), Unique.balance(left_padding, right_padding, Shape.extents(left), Shape.extents(right), Shape.naturals(output), aligned), Equal.sym(Nat, Nat.add(right_padding, right_rank), Nat.add(right_padding, List.length(&2, Nat, Shape.extents(right))), Equal.cong(Nat, Nat, value => Nat.add(right_padding, value), right_rank, List.length(&2, Nat, Shape.extents(right)), Shape.rank_naturals(Shape.dimensions(right))))))
      +computed = sub_balance(left_rank, right_rank)
      +same_left = Unique.left_padding_equal(left_padding, right_padding, left_extra, right_extra, left_rank, right_rank, minimal, Shape.minimal(left_rank, right_rank), balanced, computed)
      +same_right = Unique.cancel_right(right_padding, right_extra, right_rank, Equal.trans(Nat, Nat.add(right_padding, right_rank), Nat.add(left_padding, left_rank), Nat.add(right_extra, right_rank), Equal.sym(Nat, Nat.add(left_padding, left_rank), Nat.add(right_padding, right_rank), balanced), Equal.trans(Nat, Nat.add(left_padding, left_rank), Nat.add(left_extra, left_rank), Nat.add(right_extra, right_rank), Equal.cong(Nat, Nat, value => Nat.add(value, left_rank), left_padding, left_extra, same_left), computed)))
      +retyped = Unique.retype(left_extra, left_padding, right_extra, right_padding, Shape.extents(left), Shape.extents(right), Shape.naturals(output), Equal.sym(Nat, left_padding, left_extra, same_left), Equal.sym(Nat, right_padding, right_extra, same_right), aligned)
      +seen = align_complete(Shape.pad_words(left_extra, Shape.dimensions(left)), Shape.pad_words(right_extra, Shape.dimensions(right)), Shape.naturals(output), padded_words(left_extra, right_extra, Shape.dimensions(left), Shape.dimensions(right), Shape.naturals(output), retyped))
      complete_align(left, right, left_extra, right_extra, Shape.minimal(left_rank, right_rank), Shape.align(Shape.pad_words(left_extra, Shape.dimensions(left)), Shape.pad_words(right_extra, Shape.dimensions(right))), Shape.naturals(output), seen, Nats.le_rewrite(List.length(&2, Nat, Shape.naturals(output)), Shape.rank_dimensions(output), 4n, Shape.rank_naturals(output), rank_bound), capacity_bound)

Uses (33):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=broadcast_built
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Broadcast
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=LE
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=align
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=broadcast_checked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=extents
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=minimal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=pad_words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=le_rewrite
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=align_complete
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=complete_align
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=padded_words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/plan_proofs.bend&name=sub_balance
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=balance
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=cancel_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=left_padding_equal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend&name=retype