LAWS.attn_par_fwd: law of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/LAWS.bend as LAWS
Lines 189-199 of bendtorch@1.3.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/LAWS.bend&start_line=189&end_line=199

import Base
import bendtorch@1.3.0.0/main.bend as T

# LAW (attn_par_fwd): T.Attention runs its sequences in a tree of parallel lets (T.fpar: the sequences cut in halves,
# each half cut again, d levels deep, the leaves' outputs appended). Whatever the depth and however the sequences are
# split between the two halves, the tree gives exactly what T.fleaf gives running them one after another, in order: the
# parallel forward pass is the sequential one, and its output does not depend on d or on the thread count.
law attn_par_fwd:
  for d: Nat
  for gs: T.Halves<T.FS>
  for +n: Nat
  for +h: Nat
  for +dm: T.Dm
  {T.fpar(d, gs, n, h, dm) == T.fleaf(T.hcat(T.FS, gs), h, dm, Nil{}) : List<&1, Array<F32>>}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=par_mid
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=tree
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=Dm
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=FS
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=Halves
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=fleaf
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=fpar
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=hcat