MlbendGenerative.ddim_length: law of mlbend-generative@0.1.1.0
Import: import mlbend-generative@0.1.1.0/main.bend as MlbendGenerative
Lines 406-412 of mlbend-generative@0.1.1.0/main.bend: https://jend.leeeet.dev/read.txt?path=mlbend-generative@0.1.1.0/main.bend&start_line=406&end_line=412

import Base

# LAW 6 (ddim_length): a step over n elements is n elements.
law ddim_length:
  for +co: Step
  for +x: List<&2, F32>
  for +eps: List<&2, F32>
  for +z: List<&2, F32>
  {List.length(&2, F32, ddim(co, x, eps, z)) == List.length(&2, F32, x) : Nat}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=mlbend-generative@0.1.1.0/main.bend&name=Step
  https://jend.leeeet.dev/definition.txt?path=mlbend-generative@0.1.1.0/main.bend&name=ddim
  https://jend.leeeet.dev/definition.txt?path=mlbend-generative@0.1.1.0/main.bend&name=tail_or_nil