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

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

# LAW (attn_par_fwd_full): the same tree law for FullAttention's forward leaf: fpar_full at any depth gives exactly
# what fleaf_full gives running the sequences one after another, so a full-attention forward does not depend on the
# depth or the thread count either.
law attn_par_fwd_full:
  for d: Nat
  for gs: T.Halves<T.FS>
  for +n: Nat
  for +h: Nat
  for +dm: T.Dm
  {T.fpar_full(d, gs, n, h, dm) == T.fleaf_full(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_f
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=treef
  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_full
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=fpar_full
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=hcat