CorePROOF.invariant_advance: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF Lines 893-918 of bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&start_line=893&end_line=918 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/tensor/elementwise.bend as Elementwise def invariant_advance(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, -original_left: Core.Dynamic, -original_right: Core.Dynamic, +cursor: Nat, +index: U32, -converted: {U32.to_nat(index) == cursor : Nat}, before: Elementwise.State, after: Elementwise.State, -invariant: Elementwise.StateInvariant(operation, plan, original_left, original_right, cursor, before), -meaning: Elementwise.StepMeaning(operation, plan, index, before, Elementwise.Continue{after})) -> Elementwise.InvariantModel: Elementwise.State{left, right, output} = before Elementwise.State{after_left, after_right, after_output} = after Elementwise.InvariantModel{(other => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(after_left, other), Core.checked_observe_dynamic(left, other), Core.checked_observe_dynamic(original_left, other), step_same_left(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning)(other), invariant_left(operation, plan, original_left, original_right, cursor, left, right, output, invariant)(other)), (other => Equal.trans(Maybe<&2, F32>, Core.checked_observe_dynamic(after_right, other), Core.checked_observe_dynamic(right, other), Core.checked_observe_dynamic(original_right, other), step_same_right(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning)(other), invariant_right(operation, plan, original_left, original_right, cursor, left, right, output, invariant)(other)), {\{PrefixModel: prefix => prefix} : PrefixModel -> Elementwise.PrefixInvariant(operation, plan, original_left, original_right, 1n+cursor, Core.Packed{Shape.output_shape(plan), after_output})}(prefix_extend(operation, plan, original_left, original_right, cursor, index, output, after_output, converted, invariant_prefix(operation, plan, original_left, original_right, cursor, left, right, output, invariant), step_checked(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning), Equal.trans(Maybe<&2, F32>, Core.observe(Shape.output_shape(plan), after_output, index), Elementwise.expected(operation, plan, left, right, index), Elementwise.expected(operation, plan, original_left, original_right, index), step_observed(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning), {\{ExpectedSame: equal => equal} : ExpectedSame -> {Elementwise.expected(operation, plan, left, right, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>}}(expected_same(operation, plan, index, original_left, original_right, left, right, invariant_left(operation, plan, original_left, original_right, cursor, left, right, output, invariant), invariant_right(operation, plan, original_left, original_right, cursor, left, right, output, invariant)))), step_frame(operation, plan, index, left, right, output, after_left, after_right, after_output, meaning)))))} Uses (32): 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=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma 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/shape/core.bend&name=BroadcastPlan https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=output_shape 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=checked_observe_dynamic https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=observe https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=ExpectedSame https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=PrefixModel https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=expected_same https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=invariant_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=invariant_prefix https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=invariant_right https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=prefix_extend https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=step_checked https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=step_frame https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=step_observed https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=step_same_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=step_same_right https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=InvariantModel https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Operation https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=PrefixInvariant https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=State https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=StateInvariant https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Step https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=StepMeaning https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=expected