TensorBackwardPROOF.spared_one: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend as TensorBackwardPROOF
Lines 111-124 of bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend&start_line=111&end_line=124

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/autograd/tensor_backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward_LAWS.bend as Laws

# kept_others leaves no contribution to id.
def spared_one(+id: Nat, +target: Nat, +shape: Shape.Shape, -gradient: Core.Dynamic, -rest: List<&1, Backward.Contribution>,
  ih: {Laws.reaches(id, Backward.kept_others(id, rest)) == False{} : Bool},
  decision: Shape.BoolCase<Nat.is_eq(id, target)>) ->
  {Laws.reaches(id, Backward.kept_one(target, shape, gradient, Nat.is_eq(id, target), Backward.kept_others(id, rest))) == False{} : Bool}:
  match decision:
    case Shape.BTrue{equal}:
      %equal : {Laws.reaches(id, Backward.kept_one(target, shape, gradient, _, Backward.kept_others(id, rest))) == False{} : Bool}
      ih
    case Shape.BFalse{+equal}:
      %equal : {Laws.reaches(id, Backward.kept_one(target, shape, gradient, _, Backward.kept_others(id, rest))) == False{} : Bool}
      %equal : {Bool.or(_, Laws.reaches(id, Backward.kept_others(id, rest))) == False{} : Bool}
      %Equal.sym(Bool, Laws.reaches(id, Backward.kept_others(id, rest)), False{}, ih) : {Bool.or(False{}, _) == False{} : Bool}
      {==}

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=Contribution
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=kept_one
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=kept_others
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward_LAWS.bend&name=reaches
  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/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic