def times_scaled

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:317

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/signed.bend as Signed
import bendtorch-core@0.1.0.0/src/tensor/signed_LAWS.bend as Laws

317def times_scaled(+bound: Nat, +less: Nat, +rest: Nat, decision: Shape.BoolCase<Nat.is_lt(bound, 1n+less)>) ->
318  {Signed.scaled(bound, 1n+less, 1n+rest, Nat.is_lt(bound, 1n+less)) == Laws.classify(bound, Nat.mul(1n+less, 1n+rest)) : Signed.Product}:
319  match decision:
320    case Shape.BTrue{+equal}:
321      %equal : {Signed.scaled(bound, 1n+less, 1n+rest, _) == Laws.classify(bound, Nat.mul(1n+less, 1n+rest)) : Signed.Product}
322      %Equal.sym(Bool, Nat.is_le(Nat.mul(1n+less, 1n+rest), bound), False{},
323        past_bound(bound, less, rest, Equal.sym(Bool, True{}, Nat.is_lt(bound, 1n+less), equal))) :
324        {Signed.Beyond{} == Laws.classified(Nat.mul(1n+less, 1n+rest), _) : Signed.Product}
325      {==}
326    case Shape.BFalse{equal}:
327      %equal : {Signed.scaled(bound, 1n+less, 1n+rest, _) == Laws.classify(bound, Nat.mul(1n+less, 1n+rest)) : Signed.Product}
328      bounded_classified(Nat.mul(1n+less, 1n+rest), Nat.is_le(Nat.mul(1n+less, 1n+rest), bound))