def internal_merge_sorted_pick

bend-mathlib@0.8.1.0 · sort.bend:154

import Base
import bend-mathlib@0.8.1.0/list.bend as MList
import bend-mathlib@0.8.1.0/perm.bend as MPerm

154def internal_merge_sorted_pick(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, b: Bool, +x: A, +xt: List<&2, A>, +y: A, +yt: List<&2, A>, +e: {le(x, y) == b : Bool}, hx: MList.sorted_by(~A, ~le, x <> xt), hy: MList.sorted_by(~A, ~le, y <> yt), hm1: MList.sorted_by(~A, ~le, MPerm.merge_by(~A, ~le, xt, y <> yt)), hm2: MList.sorted_by(~A, ~le, MPerm.merge_by(~A, ~le, x <> xt, yt))) -> MList.sorted_by(~A, ~le, Bool.pick(List<&2, A>, b, x <> MPerm.merge_by(~A, ~le, xt, y <> yt), y <> MPerm.merge_by(~A, ~le, x <> xt, yt))):
155  match b:
156    case True{}:
157      internal_sorted_cons_of_least(~A, ~le, x, MPerm.merge_by(~A, ~le, xt, y <> yt), internal_least_merge(~A, ~le, x, xt, y <> yt, internal_sorted_least_head(~A, ~le, ~le_trans, xt, x, hx), internal_least_intro(~A, ~le, x, y, yt, e, internal_least_trans(~A, ~le, ~le_trans, x, y, yt, e, internal_sorted_least_head(~A, ~le, ~le_trans, yt, y, hy)))), hm1)
158    case False{}:
159      internal_sorted_cons_of_least(~A, ~le, y, MPerm.merge_by(~A, ~le, x <> xt, yt), internal_least_merge(~A, ~le, y, x <> xt, yt, internal_least_intro(~A, ~le, y, x, xt, le_total(x, y, e), internal_least_trans(~A, ~le, ~le_trans, y, x, xt, le_total(x, y, e), internal_sorted_least_head(~A, ~le, ~le_trans, xt, x, hx))), internal_sorted_least_head(~A, ~le, ~le_trans, yt, y, hy)), hm2)