def spared_one

bendtorch-core@0.1.0.0 · src/autograd/tensor_backward_PROOF.bend:111

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

111# kept_others leaves no contribution to id.
112def spared_one(+id: Nat, +target: Nat, +shape: Shape.Shape, -gradient: Core.Dynamic, -rest: List<&1, Backward.Contribution>,
113  ih: {Laws.reaches(id, Backward.kept_others(id, rest)) == False{} : Bool},
114  decision: Shape.BoolCase<Nat.is_eq(id, target)>) ->
115  {Laws.reaches(id, Backward.kept_one(target, shape, gradient, Nat.is_eq(id, target), Backward.kept_others(id, rest))) == False{} : Bool}:
116  match decision:
117    case Shape.BTrue{equal}:
118      %equal : {Laws.reaches(id, Backward.kept_one(target, shape, gradient, _, Backward.kept_others(id, rest))) == False{} : Bool}
119      ih
120    case Shape.BFalse{+equal}:
121      %equal : {Laws.reaches(id, Backward.kept_one(target, shape, gradient, _, Backward.kept_others(id, rest))) == False{} : Bool}
122      %equal : {Bool.or(_, Laws.reaches(id, Backward.kept_others(id, rest))) == False{} : Bool}
123      %Equal.sym(Bool, Laws.reaches(id, Backward.kept_others(id, rest)), False{}, ih) : {Bool.or(False{}, _) == False{} : Bool}
124      {==}