PROOF.pass_pair: def of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/PROOF.bend as PROOF
Lines 1023-1036 of bendtorch@1.3.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/PROOF.bend&start_line=1023&end_line=1036

import Base
import bendtorch@1.3.0.0/spec.bend as Spec
import bend-ml-nat-lemmas@0.1.2.0/main.bend as NL

# one pass over 2k blocks of 2^p cells gives the k blocks of 2^(p+1) cells: the pass adds blocks 2j and 2j+1, the two
# halves bal puts under one node. Induction on k; add_succ turns k + (k + 1) into 2 + (k + k), and add_assoc moves the
# next pair's start from (lo + 2^p) + 2^p to lo + 2^(p+1)
def pass_pair(+p: Nat, +k: Nat, +lo: Nat) -> {Spec.spass(Spec.blocks(p, Nat.add(k, k), lo)) == Spec.blocks(1n+p, k, lo) : List<&2, Spec.Sum>}:
  match k:
    case 0n:
      {==}
    case 1n+j:
      +a = Spec.pw(p)
      +nx = Nat.add(Nat.add(lo, a), a)
      %NL.add_succ(j, j) : {Spec.spass(Spec.blocks(p, 1n+_, lo)) == Spec.blocks(1n+p, 1n+j, lo) : List<&2, Spec.Sum>}
      %Equal.sym(Nat, Nat.add(lo, Nat.add(a, a)), nx, NL.add_assoc(lo, a, a)) : {Spec.spass(Spec.blocks(p, 1n+1n+Nat.add(j, j), lo)) == Spec.SAdd{Spec.bal(p, lo), Spec.bal(p, Nat.add(lo, a))} <> Spec.blocks(1n+p, j, _) : List<&2, Spec.Sum>}
      %pass_pair(p, j, nx) : {Spec.spass(Spec.blocks(p, 1n+1n+Nat.add(j, j), lo)) == Spec.SAdd{Spec.bal(p, lo), Spec.bal(p, Nat.add(lo, a))} <> _ : List<&2, Spec.Sum>}
      {==}

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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-ml-nat-lemmas@0.1.2.0/main.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/spec.bend&name=Sum
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/spec.bend&name=bal
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/spec.bend&name=blocks
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/spec.bend&name=pw
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/spec.bend&name=spass