SlicePROOF.viewed_view: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend as SlicePROOF
Lines 334-338 of bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&start_line=334&end_line=338

import Base
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice
import bendtorch-core@0.1.0.0/src/tensor/slice_LAWS.bend as Laws

def viewed_view(+given: Slice.View, +s: Nat, +t: Nat, +p: Nat) ->
  {Laws.view_part(Slice.viewed(given, s, t, p)) == view_pair(given) : Nat & Nat}:
  match given:
    case Slice.View{+o, +n, +i}:
      {==}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=View
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=viewed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_LAWS.bend&name=view_part
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=view_pair