def hits_true

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:899

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice

899# start <= start + k * step, k < length and start + k * step is itself.
900def hits_true(+start: Nat, +step: Nat, +length: Nat, +k: Nat, +k_below: {Nat.is_lt(k, length) == True{} : Bool}) ->
901  {Slice.hits(start, step, length, Nat.add(start, Nat.mul(k, step)), k) == True{} : Bool}:
902  %Equal.sym(Bool, Nat.is_le(start, Nat.add(start, Nat.mul(k, step))), True{}, Api.le_add_right(start, Nat.mul(k, step))) :
903    {Bool.and(_, Bool.and(Nat.is_lt(k, length), Nat.is_eq(Nat.add(start, Nat.mul(k, step)), Nat.add(start, Nat.mul(k, step))))) == True{} : Bool}
904  %Equal.sym(Bool, Nat.is_lt(k, length), True{}, k_below) :
905    {Bool.and(True{}, Bool.and(_, Nat.is_eq(Nat.add(start, Nat.mul(k, step)), Nat.add(start, Nat.mul(k, step))))) == True{} : Bool}
906  %Equal.sym(Bool, Nat.is_eq(Nat.add(start, Nat.mul(k, step)), Nat.add(start, Nat.mul(k, step))), True{},
907    Arith.eq_refl(Nat.add(start, Nat.mul(k, step)))) :
908    {Bool.and(True{}, Bool.and(True{}, _)) == True{} : Bool}
909  {==}