def output_nats

bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_PROOF.bend:693

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend as Batched
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend as Laws

693def output_nats(+rank: Nat, +o1: U32, +o2: U32, +first: Nat, +second: Nat,
694  +e1: {U32.to_nat(o1) == first : Nat}, +e2: {U32.to_nat(o2) == second : Nat}, +rows: U32, +lv: Bool, +columns: U32, +rv: Bool) ->
695  {Shape.naturals(List.append(&2, U32, Batched.batch_dims(rank, o1, o2), Batched.matrix_dims(rows, lv, columns, rv))) ==
696    List.append(&2, Nat, batch_nats(rank, first, second),
697      List.append(&2, Nat, Laws.kept(lv, U32.to_nat(rows)), Laws.kept(rv, U32.to_nat(columns)))) : List<&2, Nat>}:
698  %Equal.sym(List<&2, Nat>, Shape.naturals(List.append(&2, U32, Batched.batch_dims(rank, o1, o2), Batched.matrix_dims(rows, lv, columns, rv))),
699    List.append(&2, Nat, Shape.naturals(Batched.batch_dims(rank, o1, o2)), Shape.naturals(Batched.matrix_dims(rows, lv, columns, rv))),
700    naturals_append(Batched.batch_dims(rank, o1, o2), Batched.matrix_dims(rows, lv, columns, rv))) :
701    {_ == List.append(&2, Nat, batch_nats(rank, first, second),
702      List.append(&2, Nat, Laws.kept(lv, U32.to_nat(rows)), Laws.kept(rv, U32.to_nat(columns)))) : List<&2, Nat>}
703  %Equal.sym(List<&2, Nat>, Shape.naturals(Batched.batch_dims(rank, o1, o2)), batch_nats(rank, first, second), batch_part(rank, o1, o2, first, second, e1, e2)) :
704    {List.append(&2, Nat, _, Shape.naturals(Batched.matrix_dims(rows, lv, columns, rv))) == List.append(&2, Nat, batch_nats(rank, first, second),
705      List.append(&2, Nat, Laws.kept(lv, U32.to_nat(rows)), Laws.kept(rv, U32.to_nat(columns)))) : List<&2, Nat>}
706  %Equal.sym(List<&2, Nat>, Shape.naturals(Batched.matrix_dims(rows, lv, columns, rv)),
707    List.append(&2, Nat, Laws.kept(lv, U32.to_nat(rows)), Laws.kept(rv, U32.to_nat(columns))), matrix_part(rows, lv, columns, rv)) :
708    {List.append(&2, Nat, batch_nats(rank, first, second), _) == List.append(&2, Nat, batch_nats(rank, first, second),
709      List.append(&2, Nat, Laws.kept(lv, U32.to_nat(rows)), Laws.kept(rv, U32.to_nat(columns)))) : List<&2, Nat>}
710  {==}