def left_inside

bendtorch-core@0.1.0.0 · src/tensor/contracts/dot_proof.bend:85

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend as Pointwise
import bendtorch-core@0.1.0.0/src/tensor/contracts/dot.bend as Dot

85def left_inside(+rows: Nat, +inner: Nat, +columns: Nat, +row: Nat, +column: Nat,
86  +row_below: {Nat.is_lt(row, rows) == True{} : Bool}, +left: Shape.Shape,
87  +left_extents: {Shape.extents(left) == [rows, inner] : List<&2, Nat>}, +count: Nat,
88  +room: {Nat.is_le(count, inner) == True{} : Bool}) ->
89  {Pointwise.inside(~Dot.Cell, ~Dot.left_index, Dot.Cell{row, column, inner, columns}, count, Shape.logical_numel(Shape.dimensions(left))) == True{} : Bool}:
90  match count:
91    case 0n:
92      {==}
93    case 1n+previous:
94      +cell : Dot.Cell = Dot.Cell{row, column, inner, columns}
95      +bound = Shape.logical_numel(Shape.dimensions(left))
96      %Equal.sym(Bool, Pointwise.inside(~Dot.Cell, ~Dot.left_index, cell, previous, bound), True{},
97        left_inside(rows, inner, columns, row, column, row_below, left, left_extents, previous,
98          Conversion.le_predecessor(previous, inner, room))) :
99        {Bool.and(_, Nat.is_lt(Dot.left_index(cell, previous), bound)) == True{} : Bool}
100      %Equal.sym(Bool, Nat.is_lt(Dot.left_index(cell, previous), bound), True{},
101        left_below(rows, inner, columns, row, column, row_below, left, left_extents, previous,
102          Conversion.le_successor_lt(previous, inner, room))) :
103        {Bool.and(True{}, _) == True{} : Bool}
104      {==}