def took_miss

bendtorch-core@0.1.0.0 · src/autograd/tensor_chain_PROOF.bend:110

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

110def took_miss(+below: Nat, +target: Nat, +shape: Shape.Shape, -gradient: Core.Dynamic, -log: Laws.Log(), -w: Gradient.Slot,
111  -x: Gradient.Slot, -left: Laws.Log(), took: {Laws.take(log, below, w) == (Done{x}, left) : Laws.Taken()},
112  decided: {Nat.is_eq(below, target) == False{} : Bool}) ->
113  {Laws.take(Backward.Contribution{target, shape, gradient} <> log, below, w) == (Done{x}, Backward.Contribution{target, shape, gradient} <> left) : Laws.Taken()}:
114  %Equal.sym(Bool, Nat.is_eq(below, target), False{}, decided) :
115    {Laws.sorted(target, shape, gradient, _, Laws.take(log, below, w)) == (Done{x}, Backward.Contribution{target, shape, gradient} <> left) : Laws.Taken()}
116  %Equal.sym(Laws.Taken(), Laws.take(log, below, w), (Done{x}, left), took) :
117    {Laws.sorted(target, shape, gradient, False{}, _) == (Done{x}, Backward.Contribution{target, shape, gradient} <> left) : Laws.Taken()}
118  {==}