LAWS.count_par4_step: law of bend-prot@0.1.0.0
Import: import bend-prot@0.1.0.0/LAWS.bend as LAWS
Lines 438-447 of bend-prot@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-prot@0.1.0.0/LAWS.bend&start_line=438&end_line=447

import Base
import bend-prot@0.1.0.0/geom.bend as G
import bend-prot@0.1.0.0/protein.bend as P
import bend-prot@0.1.0.0/topology.bend as T
import bend-prot@0.1.0.0/par.bend as Par

# A full unrolled step splits four parallel hits plus the tail.
law count_par4_step:
  for h1: P.Atom
  for h2: P.Atom
  for h3: P.Atom
  for h4: P.Atom
  for t: List<&2, P.Atom>
  for qp: G.Vec3
  for c2: F32
  {Par.count_par4(h1 <> h2 <> h3 <> h4 <> t, qp, c2) == Nat.add(Nat.add(T.head_hit_nat(h1, qp, c2), T.head_hit_nat(h2, qp, c2)), Nat.add(T.head_hit_nat(h3, qp, c2), Nat.add(T.head_hit_nat(h4, qp, c2), Par.count_par4(t, qp, c2)))) : Nat}

Uses (8):
  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=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/geom.bend&name=Vec3
  https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/par.bend&name=count_par4
  https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/protein.bend&name=Atom
  https://jend.leeeet.dev/definition.txt?path=bend-prot@0.1.0.0/topology.bend&name=head_hit_nat