Phc.b64_rt: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend as Phc
Lines 1068-1132 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&start_line=1068&end_line=1132

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend as PH

def b64_rt(+bs: List<&2, U32>, +h: {ok(bs) == True{} : Bool}) -> {PH.unb64(PH.b64(bs)) == Some{bs} : Maybe<&2, List<&2, U32>>}:
  match bs:
    case Nil{}:
      {==}
    case +a <> Nil{}:
      +ha = ok_head(a, Nil{}, h)
      +ta = ok_tail(a, Nil{}, h)
      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)))), Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, digit_value(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {PH.dec2(_, PH.value(PH.digit(PH.sext(PH.c0(a), 0, 0)))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c0(a), 0, 0))), Some{PH.sext(PH.c0(a), 0, 0)}, digit_value(PH.sext(PH.c0(a), 0, 0), sx_lt(PH.c0(a), 0, 0, c0_lt(a), {==}, {==}))) : {PH.dec2(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, _) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.su(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c3(a), su_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec2_fin(PH.byte_of(_, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), 0, 0))), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c2(a), sv_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec2_fin(PH.byte_of(PH.c3(a), _, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), 0, 0))), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c1(a), sw_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), _, PH.su(PH.sext(PH.c0(a), 0, 0))), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.su(PH.sext(PH.c0(a), 0, 0)), PH.c0(a), su_eq(PH.c0(a), 0, 0, c0_lt(a), {==}, {==})) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), _), Bool.and(U32.is_eq(PH.sv(PH.sext(PH.c0(a), 0, 0)), 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sv(PH.sext(PH.c0(a), 0, 0)), 0, sv_eq(PH.c0(a), 0, 0, c0_lt(a), {==}, {==})) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), Bool.and(U32.is_eq(_, 0), U32.is_eq(PH.sw(PH.sext(PH.c0(a), 0, 0)), 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sw(PH.sext(PH.c0(a), 0, 0)), 0, sw_eq(PH.c0(a), 0, 0, c0_lt(a), {==}, {==})) : {PH.dec2_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), Bool.and(U32.is_eq(0, 0), U32.is_eq(_, 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), a, byte_rt(a, ha)) : {PH.dec2_fin(_, Bool.and(U32.is_eq(0, 0), U32.is_eq(0, 0))) == Some{a <> Nil{}} : Maybe<&2, List<&2, U32>>}
      {==}
    case +a <> +b <> Nil{}:
      +ha = ok_head(a, b <> Nil{}, h)
      +ta = ok_tail(a, b <> Nil{}, h)
      +hb = ok_head(b, Nil{}, ta)
      +tb = ok_tail(b, Nil{}, ta)
      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)))), Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, digit_value(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {PH.dec3(_, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)))) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, digit_value(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)), sx_lt(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b)))) : {PH.dec3(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, _, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)))) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0))), Some{PH.sext(PH.c1(b), PH.c0(b), 0)}, digit_value(PH.sext(PH.c1(b), PH.c0(b), 0), sx_lt(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==}))) : {PH.dec3(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, _) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.su(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c3(a), su_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec3_fin(PH.byte_of(_, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c2(a), sv_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), _, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c1(a), sw_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), _, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c0(a), su_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), _), PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c3(b), sv_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(_, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c2(b), sw_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), _, PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.su(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.c1(b), su_eq(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==})) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), PH.c2(b), _, PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0))), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sv(PH.sext(PH.c1(b), PH.c0(b), 0)), PH.c0(b), sv_eq(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==})) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), _), U32.is_eq(PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sw(PH.sext(PH.c1(b), PH.c0(b), 0)), 0, sw_eq(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==})) : {PH.dec3_fin(PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), U32.is_eq(_, 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), a, byte_rt(a, ha)) : {PH.dec3_fin(_, PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), U32.is_eq(0, 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), b, byte_rt(b, hb)) : {PH.dec3_fin(a, _, U32.is_eq(0, 0)) == Some{a <> b <> Nil{}} : Maybe<&2, List<&2, U32>>}
      {==}
    case +a <> +b <> +c <> +rest:
      +ha = ok_head(a, b <> c <> rest, h)
      +ta = ok_tail(a, b <> c <> rest, h)
      +hb = ok_head(b, c <> rest, ta)
      +tb = ok_tail(b, c <> rest, ta)
      +hc = ok_head(c, rest, tb)
      +tc = ok_tail(c, rest, tb)
      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)))), Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, digit_value(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a)), sx_lt(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a)))) : {PH.dec4(_, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))), PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))), Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, digit_value(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)), sx_lt(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b)))) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, _, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))), PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))), Some{PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))}, digit_value(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)), sx_lt(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc)))) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, _, PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(Maybe<&2, U32>, PH.value(PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))), Some{PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))}, digit_value(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)), sx_lt(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c)))) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, Some{PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))}, _, PH.unb64(PH.b64(rest))) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(Maybe<&2, List<&2, U32>>, PH.unb64(PH.b64(rest)), Some{rest}, b64_rt(rest, tc)) : {PH.dec4(Some{PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))}, Some{PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))}, Some{PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))}, Some{PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))}, _) == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.su(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c3(a), su_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {Some{PH.byte_of(_, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sv(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c2(a), sv_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {Some{PH.byte_of(PH.c3(a), _, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sw(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), PH.c1(a), sw_eq(PH.c3(a), PH.c2(a), PH.c1(a), c3_lt(a, ha), c2_lt(a), c1_lt(a))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), _, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b)))) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.su(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c0(a), su_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), _) <> PH.byte_of(PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sv(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c3(b), sv_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(_, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sw(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), PH.c2(b), sw_eq(PH.c0(a), PH.c3(b), PH.c2(b), c0_lt(a), c3_lt(b, hb), c2_lt(b))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), _, PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.su(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.c1(b), su_eq(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), _, PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c)))) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sv(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.c0(b), sv_eq(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), _) <> PH.byte_of(PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sw(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), PH.c3(c), sw_eq(PH.c1(b), PH.c0(b), PH.c3(c), c1_lt(b), c0_lt(b), c3_lt(c, hc))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(_, PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.su(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.c2(c), su_eq(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), _, PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sv(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.c1(c), sv_eq(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), PH.c2(c), _, PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c)))) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.sw(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), PH.c0(c), sw_eq(PH.c2(c), PH.c1(c), PH.c0(c), c2_lt(c), c1_lt(c), c0_lt(c))) : {Some{PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)) <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), _) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.byte_of(PH.c3(a), PH.c2(a), PH.c1(a), PH.c0(a)), a, byte_rt(a, ha)) : {Some{_ <> PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)) <> PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), PH.c0(c)) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.byte_of(PH.c3(b), PH.c2(b), PH.c1(b), PH.c0(b)), b, byte_rt(b, hb)) : {Some{a <> _ <> PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), PH.c0(c)) <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      %Equal.sym(U32, PH.byte_of(PH.c3(c), PH.c2(c), PH.c1(c), PH.c0(c)), c, byte_rt(c, hc)) : {Some{a <> b <> _ <> rest} == Some{a <> b <> c <> rest} : Maybe<&2, List<&2, U32>>}
      {==}

Uses (38):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=byte_rt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=c0_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=c1_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=c2_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=c3_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=digit_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=ok_head
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=ok_tail
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=su_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=sv_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=sw_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&name=sx_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=b64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=byte_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=c0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=c1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=c2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=c3
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=dec2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=dec2_fin
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=dec3
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=dec3_fin
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=dec4
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=digit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=sext
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=su
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=sv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=sw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=unb64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend&name=value