GradientPROOF.written_true: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend as GradientPROOF
Lines 247-292 of bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&start_line=247&end_line=292

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_LAWS.bend as Laws

def written_true(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat,
  -before: Core.Tensor<shape>, -written: Core.Tensor<shape>, +index: U32, +accumulated: F32, +value: F32,
  +other: U32, -equal: {True{} == Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) : Bool},
  -inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
  -exact: {U32.to_nat(index) == cursor : Nat},
  -inv: Inv(shape, original, contribution, cursor, before),
  -read: {Core.checked_observe(shape, before, index) == Some{accumulated} : Maybe<&2, F32>},
  -stored: {Core.checked_observe(shape, written, index) == Some{F32.add(accumulated, value)} : Maybe<&2, F32>},
  -word: {Core.checked_observe_dynamic(contribution, index) == Some{value} : Maybe<&2, F32>}) ->
  Holds<{Core.checked_observe(shape, written, other) ==
    partial(Nat.is_lt(U32.to_nat(other), 1n+cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)) : Maybe<&2, F32>}>:
  Holds{
    %{\{Holds: proof => proof} : Holds<{index == other : U32}> -> {index == other : U32}}(word_exact(index, other, equal)) :
      {Core.checked_observe(shape, written, _) ==
        partial(Nat.is_lt(U32.to_nat(_), 1n+cursor), Core.checked_observe(shape, original, _), Core.checked_observe_dynamic(contribution, _)) : Maybe<&2, F32>}
    Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, written, index), Some{F32.add(accumulated, value)},
      partial(Nat.is_lt(U32.to_nat(index), 1n+cursor), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)),
      stored,
      %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), 1n+cursor), True{},
        %Equal.sym(Nat, U32.to_nat(index), cursor, exact) : {Nat.is_lt(_, 1n+cursor) == True{} : Bool}
        lt_succ_self(cursor)) :
        {Some{F32.add(accumulated, value)} == partial(_, Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
      %Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, original, index), Some{accumulated},
        Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, original, index),
          partial(Nat.is_lt(U32.to_nat(index), cursor), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)),
          Some{accumulated},
          %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), cursor), False{},
            %Equal.sym(Nat, U32.to_nat(index), cursor, exact) : {Nat.is_lt(_, cursor) == False{} : Bool}
            lt_self(cursor)) :
            {Core.checked_observe(shape, original, index) ==
              partial(_, Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
          {==},
          Equal.trans(Maybe<&2, F32>,
            partial(Nat.is_lt(U32.to_nat(index), cursor), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)),
            Core.checked_observe(shape, before, index), Some{accumulated},
            Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, before, index),
              partial(Nat.is_lt(U32.to_nat(index), cursor), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)),
              inv(index)(
                %Equal.sym(U32, index, other, {\{Holds: proof => proof} : Holds<{index == other : U32}> -> {index == other : U32}}(word_exact(index, other, equal))) :
                  {Nat.is_lt(U32.to_nat(_), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
                inside)),
            read))) :
        {Some{F32.add(accumulated, value)} == Laws.add_word(_, Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
      %Equal.sym(Maybe<&2, F32>, Core.checked_observe_dynamic(contribution, index), Some{value}, word) :
        {Some{F32.add(accumulated, value)} == Laws.add_word(Some{accumulated}, _) : Maybe<&2, F32>}
      {==})}

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend&name=add_word
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=Holds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=Inv
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=lt_self
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=lt_succ_self
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=partial
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient_PROOF.bend&name=word_exact
  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/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=checked_observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=checked_observe_dynamic