def written_false

bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:294

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

294def written_false(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat,
295  -before: Core.Tensor<shape>, -read_owner: Core.Tensor<shape>, -written: Core.Tensor<shape>, +index: U32,
296  +other: U32, -equal: {False{} == Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) : Bool},
297  -inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
298  -exact: {U32.to_nat(index) == cursor : Nat},
299  -inv: Inv(shape, original, contribution, cursor, before),
300  -kept: {Core.checked_observe(shape, read_owner, other) == Core.checked_observe(shape, before, other) : Maybe<&2, F32>},
301  -frame: {Core.checked_observe(shape, written, other) == Core.checked_observe(shape, read_owner, other) : Maybe<&2, F32>}) ->
302  Holds<{Core.checked_observe(shape, written, other) ==
303    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>}>:
304  Holds{Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, written, other), Core.checked_observe(shape, read_owner, other),
305    partial(Nat.is_lt(U32.to_nat(other), 1n+cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)),
306    frame,
307    Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, read_owner, other), Core.checked_observe(shape, before, other),
308      partial(Nat.is_lt(U32.to_nat(other), 1n+cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)),
309      kept,
310      Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, before, other),
311        partial(Nat.is_lt(U32.to_nat(other), cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)),
312        partial(Nat.is_lt(U32.to_nat(other), 1n+cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)),
313        inv(other)(inside),
314        %lt_step(U32.to_nat(other), cursor,
315          %exact : {False{} == Nat.is_eq(_, U32.to_nat(other)) : Bool}
316          equal) :
317          {partial(Nat.is_lt(U32.to_nat(other), cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)) ==
318            partial(_, Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)) : Maybe<&2, F32>}
319        {==})))}