def frozen_nt_spared

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

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

195def frozen_nt_spared(+id: Nat, +a: Nat, +b: Nat, +left: Shape.Shape, +right: Shape.Shape, saved: Backward.Saved, g: Core.Dynamic,
196  decision: Shape.BoolCase<Bool.and(Nat.is_eq(id, a), Bool.not(Nat.is_eq(id, b)))>) ->
197  {Laws.sends_to(id, Backward.nt_frozen(id, a, b, left, right, saved, g, Bool.and(Nat.is_eq(id, a), Bool.not(Nat.is_eq(id, b))))) == False{} : Bool}:
198  match decision:
199    case Shape.BTrue{+equal}:
200      %equal : {Laws.sends_to(id, Backward.nt_frozen(id, a, b, left, right, saved, g, _)) == False{} : Bool}
201      right_alone_spared(id, b, right, saved, g,
202        other_operand(Nat.is_eq(id, a), Nat.is_eq(id, b), Equal.sym(Bool, True{}, Bool.and(Nat.is_eq(id, a), Bool.not(Nat.is_eq(id, b))), equal)))
203    case Shape.BFalse{equal}:
204      %equal : {Laws.sends_to(id, Backward.nt_frozen(id, a, b, left, right, saved, g, _)) == False{} : Bool}
205      unsent_spared(id, Backward.vjp_matmul_nt(a, b, left, right, saved, g))