def halves_facts

bendtorch-core@0.1.0.0 · src/tensor/gather_PROOF.bend:309

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

309def halves_facts(+da: Nat, -A: Array<F32>, +di: Nat, -I: Array<U32>, lp: Array<F32> & Array<F32>, rp: Array<U32> & Array<U32>,
310  -le: {lp == Array.clone(F32, A) : Array<F32> & Array<F32>}, -re: {rp == Array.clone(U32, I) : Array<U32> & Array<U32>},
311  -valid: Model.Balanced(F32, da, A), -index_valid: Model.Balanced(U32, di, I)) ->
312  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>})>:
313  (l1, l2) = lp
314  (r1, r2) = rp
315  Generic.Fact{(
316    both(l1, r1, A, I,
317      Equal.trans(Array<F32>, l1, Pair.fst(Array<F32>, Array<F32>, Array.clone(F32, A)), A,
318        Equal.cong(Array<F32> & Array<F32>, Array<F32>, p => Pair.fst(Array<F32>, Array<F32>, p), (l1, l2), Array.clone(F32, A), le),
319        Clone.first_equal(F32, da, A, Clone.certify(F32, da, A, valid))),
320      Equal.trans(Array<U32>, r1, Pair.fst(Array<U32>, Array<U32>, Array.clone(U32, I)), I,
321        Equal.cong(Array<U32> & Array<U32>, Array<U32>, p => Pair.fst(Array<U32>, Array<U32>, p), (r1, r2), Array.clone(U32, I), re),
322        Clone.first_equal(U32, di, I, Clone.certify(U32, di, I, index_valid)))),
323    both(l2, r2, A, I,
324      Equal.trans(Array<F32>, l2, Pair.snd(Array<F32>, Array<F32>, Array.clone(F32, A)), A,
325        Equal.cong(Array<F32> & Array<F32>, Array<F32>, p => Pair.snd(Array<F32>, Array<F32>, p), (l1, l2), Array.clone(F32, A), le),
326        Clone.second_equal(F32, da, A, Clone.certify(F32, da, A, valid))),
327      Equal.trans(Array<U32>, r2, Pair.snd(Array<U32>, Array<U32>, Array.clone(U32, I)), I,
328        Equal.cong(Array<U32> & Array<U32>, Array<U32>, p => Pair.snd(Array<U32>, Array<U32>, p), (r1, r2), Array.clone(U32, I), re),
329        Clone.second_equal(U32, di, I, Clone.certify(U32, di, I, index_valid)))))}