GatherPROOF.halves_facts: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend as GatherPROOF
Lines 309-329 of bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&start_line=309&end_line=329

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather
import bendtorch-core@0.1.0.0/src/storage/clone.bend as Clone
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic

def halves_facts(+da: Nat, -A: Array<F32>, +di: Nat, -I: Array<U32>, lp: Array<F32> & Array<F32>, rp: Array<U32> & Array<U32>,
  -le: {lp == Array.clone(F32, A) : Array<F32> & Array<F32>}, -re: {rp == Array.clone(U32, I) : Array<U32> & Array<U32>},
  -valid: Model.Balanced(F32, da, A), -index_valid: Model.Balanced(U32, di, I)) ->
  Generic.Fact<({Pair.fst(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.halves(lp, rp)) == (A, I) : Array<F32> & Array<U32>} & {Pair.snd(Array<F32> & Array<U32>, Array<F32> & Array<U32>, Gather.halves(lp, rp)) == (A, I) : Array<F32> & Array<U32>})>:
  (l1, l2) = lp
  (r1, r2) = rp
  Generic.Fact{(
    both(l1, r1, A, I,
      Equal.trans(Array<F32>, l1, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, A)), A,
        Equal.cong(Array<F32> & Array<F32>, Array<F32>, p => Pair.fst(Array<F32>, Array<F32>, p), (l1, l2), Array.clone(F32, A), le),
        Clone.first_equal(F32, da, A, Clone.certify(F32, da, A, valid))),
      Equal.trans(Array<U32>, r1, Pair.fst(Array<U32>, Array<U32>, Array.clone(U32, I)), I,
        Equal.cong(Array<U32> & Array<U32>, Array<U32>, p => Pair.fst(Array<U32>, Array<U32>, p), (r1, r2), Array.clone(U32, I), re),
        Clone.first_equal(U32, di, I, Clone.certify(U32, di, I, index_valid)))),
    both(l2, r2, A, I,
      Equal.trans(Array<F32>, l2, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, A)), A,
        Equal.cong(Array<F32> & Array<F32>, Array<F32>, p => Pair.snd(Array<F32>, Array<F32>, p), (l1, l2), Array.clone(F32, A), le),
        Clone.second_equal(F32, da, A, Clone.certify(F32, da, A, valid))),
      Equal.trans(Array<U32>, r2, Pair.snd(Array<U32>, Array<U32>, Array.clone(U32, I)), I,
        Equal.cong(Array<U32> & Array<U32>, Array<U32>, p => Pair.snd(Array<U32>, Array<U32>, p), (r1, r2), Array.clone(U32, I), re),
        Clone.second_equal(U32, di, I, Clone.certify(U32, di, I, index_valid)))))}

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.clone
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/clone.bend&name=certify
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/clone.bend&name=first_equal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/clone.bend&name=second_equal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=halves
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=both
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact