ReduceFiberProof.mask_off_decided: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof
Lines 206-220 of bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&start_line=206&end_line=220

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/storage/arith.bend as Arith

def mask_off_decided(+size: Nat, +d: Nat, +w: Nat, +t: Nat, below: {Nat.is_lt(w, size) == True{} : Bool},
  differ: {Nat.is_eq(d, Nat.div(t, size)) == False{} : Bool},
  decision: Shape.BoolCase<Nat.is_eq(Nat.add(Nat.mul(size, d), w), t)>) ->
  {Nat.is_eq(Nat.add(Nat.mul(size, d), w), t) == False{} : Bool}:
  match decision:
    case Shape.BFalse{equal}:
      Equal.sym(Bool, False{}, Nat.is_eq(Nat.add(Nat.mul(size, d), w), t), equal)
    case Shape.BTrue{equal}:
      +hit = Arith.eq_true(Nat.add(Nat.mul(size, d), w), t, Equal.sym(Bool, True{}, Nat.is_eq(Nat.add(Nat.mul(size, d), w), t), equal))
      Empty.absurd({Nat.is_eq(Nat.add(Nat.mul(size, d), w), t) == False{} : Bool},
        ne_from(d, Nat.div(t, size),
          div_of(t, size, d, w, below,
            %Nats.mul_comm(size, d) : {Nat.add(_, w) == t : Nat}
            hit),
          differ))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=div_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=ne_from
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=eq_true