def strans.step

bend-kit-collections@0.1.4.1 · PROOF.bend:4076

import Base
import bend-kit-collections@0.1.4.1/order.bend as Order

4076# One step of transitivity on the heads a < b < c, with the tails' result as ih.
4077def strans.step(
4078  +a: U32, +b: U32, +c: U32, -s: String, -t: String, -u: String, c1: Cmp, c2: Cmp,
4079  h1: {U32.cmp(a, b) == c1 : Cmp}, h2: {U32.cmp(b, c) == c2 : Cmp},
4080  e1: {Order.string.fin(c1, Order.string(s, t)) == LT{} : Cmp},
4081  e2: {Order.string.fin(c2, Order.string(t, u)) == LT{} : Cmp},
4082  ih: {Order.string(s, t) == LT{} : Cmp} -> {Order.string(t, u) == LT{} : Cmp} -> {Order.string(s, u) == LT{} : Cmp}
4083) -> {Order.string.fin(U32.cmp(a, c), Order.string(s, u)) == LT{} : Cmp}:
4084  match c1 c2:
4085    case LT{} LT{}:
4086      %Equal.sym(Cmp, U32.cmp(a, c), LT{}, ucmp_trans(a, b, c, h1, h2)) : {Order.string.fin(_, Order.string(s, u)) == LT{} : Cmp}
4087      {==}
4088    case LT{} EQ{}:
4089      +ebc = ucmp_eq(b, c, h2)
4090      +eac = rw(U32, w => {U32.cmp(a, w) == LT{} : Cmp}, c, b, Equal.sym(U32, b, c, ebc), h1)
4091      %Equal.sym(Cmp, U32.cmp(a, c), LT{}, eac) : {Order.string.fin(_, Order.string(s, u)) == LT{} : Cmp}
4092      {==}
4093    case EQ{} LT{}:
4094      +eab = ucmp_eq(a, b, h1)
4095      +eac = rw(U32, w => {U32.cmp(w, c) == LT{} : Cmp}, a, b, eab, h2)
4096      %Equal.sym(Cmp, U32.cmp(a, c), LT{}, eac) : {Order.string.fin(_, Order.string(s, u)) == LT{} : Cmp}
4097      {==}
4098    case EQ{} EQ{}:
4099      +eca = Equal.sym(U32, a, c, Equal.trans(U32, a, b, c, ucmp_eq(a, b, h1), ucmp_eq(b, c, h2)))
4100      +eac = rw(U32, w => {U32.cmp(a, w) == EQ{} : Cmp}, c, a, eca, ucmp_refl(a))
4101      %Equal.sym(Cmp, U32.cmp(a, c), EQ{}, eac) : {Order.string.fin(_, Order.string(s, u)) == LT{} : Cmp}
4102      ih(e1, e2)
4103    case GT{} _:
4104      lt_absurd({Order.string.fin(U32.cmp(a, c), Order.string(s, u)) == LT{} : Cmp}, GT{}, {==}, e1)
4105    case _ GT{}:
4106      lt_absurd({Order.string.fin(U32.cmp(a, c), Order.string(s, u)) == LT{} : Cmp}, GT{}, {==}, e2)