def par_fin_f

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

532# the law: the treef gives what fleaf, the loop over the sequences one after another, gives
533def par_fin_f(-d: Nat, -gs: T.Halves<T.FS>, -n: Nat, +h: Nat, +dm: T.Dm, -ys: List<&1, T.FS>, +sy: {ys == T.hcat(T.FS, gs) : List<&1, T.FS>}, f: {T.fpar_full(d, gs, n, h, dm) == ffmap(h, dm, T.hcat(T.FS, gs)) : List<&1, Array<F32>>}, r: L1RF<h, dm, ys, Nil{}>) -> {T.fpar_full(d, gs, n, h, dm) == T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}) : List<&1, Array<F32>>}:
534  match r:
535    case L1RF{ys2, s2, fl}:
536      Equal.trans(List<&1, Array<F32>>, T.fpar_full(d, gs, n, h, dm), ffmap(h, dm, T.hcat(T.FS, gs)), T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}), f,
537        Equal.sym(List<&1, Array<F32>>, T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}), ffmap(h, dm, T.hcat(T.FS, gs)),
538          Equal.trans(List<&1, Array<F32>>, T.fleaf_full(T.hcat(T.FS, gs), h, dm, Nil{}), T.fleaf_full(ys, h, dm, Nil{}), ffmap(h, dm, T.hcat(T.FS, gs)), Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => T.fleaf_full(z, h, dm, Nil{}), T.hcat(T.FS, gs), ys, Equal.sym(List<&1, T.FS>, ys, T.hcat(T.FS, gs), sy)),
539            Equal.trans(List<&1, Array<F32>>, T.fleaf_full(ys, h, dm, Nil{}), ffmap(h, dm, ys), ffmap(h, dm, T.hcat(T.FS, gs)), fl, Equal.cong(List<&1, T.FS>, List<&1, Array<F32>>, z => ffmap(h, dm, z), ys, T.hcat(T.FS, gs), sy)))))
Uses (15)

Used by (1)

bendtorch@1.3.0.0/PROOF:par_mid_f