import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/u32.bend as U
import ./words.bend as LW
import ../../math/hash/hash.bend as HH
import ../../math/natural/arith.bend as NR
import ../../../src/crypto/argon2/phc.bend as PH
# Generated by tools/generators/argon2_phc_gen.py; do not edit by hand.

# The PHC string of an Argon2id hash parses back to its fields: base64 and
# decimal round trips, and the '$'-separated fields. Every finite fact
# (a crumb, a base64 digit, a decimal digit) is checked value by value.

# Every byte is below 256.
def ok(bs: List<&2, U32>) -> Bool:
  match bs:
    case Nil{}:
      True{}
    case x <> r:
      Bool.and(Nat.is_lt(U32.to_nat(x), 256n), ok(r))

def ok_head(+x: U32, +r: List<&2, U32>, +h: {ok(x <> r) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}:
  L.and_left(Nat.is_lt(U32.to_nat(x), 256n), ok(r), h)

def ok_tail(+x: U32, +r: List<&2, U32>, +h: {ok(x <> r) == True{} : Bool}) -> {ok(r) == True{} : Bool}:
  L.and_right(Nat.is_lt(U32.to_nat(x), 256n), ok(r), h)

def u(+n: Nat) -> U32:
  U32.from_nat(n)

# ---------------------------------------------------------------- base64 digits

def dv_n(+n: Nat, +h: {Nat.is_lt(n, 64n) == True{} : Bool}) -> {PH.value(PH.digit(u(n))) == Some{u(n)} : Maybe<&2, U32>}:
  match n:
    case 0n:
      {==}
    case 1n:
      {==}
    case 2n:
      {==}
    case 3n:
      {==}
    case 4n:
      {==}
    case 5n:
      {==}
    case 6n:
      {==}
    case 7n:
      {==}
    case 8n:
      {==}
    case 9n:
      {==}
    case 10n:
      {==}
    case 11n:
      {==}
    case 12n:
      {==}
    case 13n:
      {==}
    case 14n:
      {==}
    case 15n:
      {==}
    case 16n:
      {==}
    case 17n:
      {==}
    case 18n:
      {==}
    case 19n:
      {==}
    case 20n:
      {==}
    case 21n:
      {==}
    case 22n:
      {==}
    case 23n:
      {==}
    case 24n:
      {==}
    case 25n:
      {==}
    case 26n:
      {==}
    case 27n:
      {==}
    case 28n:
      {==}
    case 29n:
      {==}
    case 30n:
      {==}
    case 31n:
      {==}
    case 32n:
      {==}
    case 33n:
      {==}
    case 34n:
      {==}
    case 35n:
      {==}
    case 36n:
      {==}
    case 37n:
      {==}
    case 38n:
      {==}
    case 39n:
      {==}
    case 40n:
      {==}
    case 41n:
      {==}
    case 42n:
      {==}
    case 43n:
      {==}
    case 44n:
      {==}
    case 45n:
      {==}
    case 46n:
      {==}
    case 47n:
      {==}
    case 48n:
      {==}
    case 49n:
      {==}
    case 50n:
      {==}
    case 51n:
      {==}
    case 52n:
      {==}
    case 53n:
      {==}
    case 54n:
      {==}
    case 55n:
      {==}
    case 56n:
      {==}
    case 57n:
      {==}
    case 58n:
      {==}
    case 59n:
      {==}
    case 60n:
      {==}
    case 61n:
      {==}
    case 62n:
      {==}
    case 63n:
      {==}
    case 64n+r:
      Empty.absurd({PH.value(PH.digit(u(64n+r))) == Some{u(64n+r)} : Maybe<&2, U32>}, N.lt_zero_absurd(r, h))

def digit_value(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 64n) == True{} : Bool}) -> {PH.value(PH.digit(x)) == Some{x} : Maybe<&2, U32>}:
  %LW.rt(x) : {PH.value(PH.digit(_)) == Some{_} : Maybe<&2, U32>}
  dv_n(U32.to_nat(x), h)

def nd_n(+n: Nat, +h: {Nat.is_lt(n, 64n) == True{} : Bool}) -> {PH.dollar(SCon{PH.digit(u(n)), SNil{}}) == False{} : Bool}:
  match n:
    case 0n:
      {==}
    case 1n:
      {==}
    case 2n:
      {==}
    case 3n:
      {==}
    case 4n:
      {==}
    case 5n:
      {==}
    case 6n:
      {==}
    case 7n:
      {==}
    case 8n:
      {==}
    case 9n:
      {==}
    case 10n:
      {==}
    case 11n:
      {==}
    case 12n:
      {==}
    case 13n:
      {==}
    case 14n:
      {==}
    case 15n:
      {==}
    case 16n:
      {==}
    case 17n:
      {==}
    case 18n:
      {==}
    case 19n:
      {==}
    case 20n:
      {==}
    case 21n:
      {==}
    case 22n:
      {==}
    case 23n:
      {==}
    case 24n:
      {==}
    case 25n:
      {==}
    case 26n:
      {==}
    case 27n:
      {==}
    case 28n:
      {==}
    case 29n:
      {==}
    case 30n:
      {==}
    case 31n:
      {==}
    case 32n:
      {==}
    case 33n:
      {==}
    case 34n:
      {==}
    case 35n:
      {==}
    case 36n:
      {==}
    case 37n:
      {==}
    case 38n:
      {==}
    case 39n:
      {==}
    case 40n:
      {==}
    case 41n:
      {==}
    case 42n:
      {==}
    case 43n:
      {==}
    case 44n:
      {==}
    case 45n:
      {==}
    case 46n:
      {==}
    case 47n:
      {==}
    case 48n:
      {==}
    case 49n:
      {==}
    case 50n:
      {==}
    case 51n:
      {==}
    case 52n:
      {==}
    case 53n:
      {==}
    case 54n:
      {==}
    case 55n:
      {==}
    case 56n:
      {==}
    case 57n:
      {==}
    case 58n:
      {==}
    case 59n:
      {==}
    case 60n:
      {==}
    case 61n:
      {==}
    case 62n:
      {==}
    case 63n:
      {==}
    case 64n+r:
      Empty.absurd({PH.dollar(SCon{PH.digit(u(64n+r)), SNil{}}) == False{} : Bool}, N.lt_zero_absurd(r, h))

def no_dollar(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 64n) == True{} : Bool}) -> {PH.dollar(SCon{PH.digit(x), SNil{}}) == False{} : Bool}:
  %LW.rt(x) : {PH.dollar(SCon{PH.digit(_), SNil{}}) == False{} : Bool}
  nd_n(U32.to_nat(x), h)

# ---------------------------------------------------------------- crumbs

# A value below 4 round-trips through U32.
def tn(+i: Nat, +h: {Nat.is_lt(i, 4n) == True{} : Bool}) -> {U32.to_nat(U32.from_nat(i)) == i : Nat}:
  U.to_nat_from_nat(i, 2n, {==}, h)

# m < K * 4 gives m / 4 < K.
def div4_lt(+m: Nat, +k: Nat, +h: {Nat.is_lt(m, Nat.mul(k, 4n)) == True{} : Bool}) -> {Nat.is_lt(Nat.div(m, 4n), k) == True{} : Bool}:
  N.not_le_lt(k, Nat.div(m, 4n), Equal.trans(Bool, Nat.is_le(k, Nat.div(m, 4n)), Nat.is_le(Nat.mul(k, 4n), m), False{}, NR.le_div(3n, k, m), N.lt_not_le(m, Nat.mul(k, 4n), h)))

def c0_lt(+x: U32) -> {Nat.is_lt(U32.to_nat(PH.c0(x)), 4n) == True{} : Bool}:
  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(U32.to_nat(x), 4n))), Nat.mod(U32.to_nat(x), 4n), tn(Nat.mod(U32.to_nat(x), 4n), NR.dm_lt(3n, U32.to_nat(x)))) : {Nat.is_lt(_, 4n) == True{} : Bool}
  NR.dm_lt(3n, U32.to_nat(x))

def c1_lt(+x: U32) -> {Nat.is_lt(U32.to_nat(PH.c1(x)), 4n) == True{} : Bool}:
  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n))), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), tn(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), NR.dm_lt(3n, Nat.div(U32.to_nat(x), 4n)))) : {Nat.is_lt(_, 4n) == True{} : Bool}
  NR.dm_lt(3n, Nat.div(U32.to_nat(x), 4n))

def c2_lt(+x: U32) -> {Nat.is_lt(U32.to_nat(PH.c2(x)), 4n) == True{} : Bool}:
  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), NR.dm_lt(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n)))) : {Nat.is_lt(_, 4n) == True{} : Bool}
  NR.dm_lt(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n))

def t3_lt(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}) -> {Nat.is_lt(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n) == True{} : Bool}:
  div4_lt(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n, div4_lt(Nat.div(U32.to_nat(x), 4n), 16n, div4_lt(U32.to_nat(x), 64n, h)))

def c3_lt(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(PH.c3(x)), 4n) == True{} : Bool}:
  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), t3_lt(x, h))) : {Nat.is_lt(_, 4n) == True{} : Bool}
  t3_lt(x, h)

# A byte is the byte of its crumbs.
def byte_rt(+x: U32, +h: {Nat.is_lt(U32.to_nat(x), 256n) == True{} : Bool}) -> {PH.byte_of(PH.c3(x), PH.c2(x), PH.c1(x), PH.c0(x)) == x : U32}:
  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), t3_lt(x, h))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(_, 4n), U32.to_nat(PH.c2(x))), 4n), U32.to_nat(PH.c1(x))), 4n), U32.to_nat(PH.c0(x)))) == x : U32}
  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n))), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), tn(Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), NR.dm_lt(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n)))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n), _), 4n), U32.to_nat(PH.c1(x))), 4n), U32.to_nat(PH.c0(x)))) == x : U32}
  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n))), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), tn(Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n), NR.dm_lt(3n, Nat.div(U32.to_nat(x), 4n)))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n)), 4n), _), 4n), U32.to_nat(PH.c0(x)))) == x : U32}
  %Equal.sym(Nat, U32.to_nat(U32.from_nat(Nat.mod(U32.to_nat(x), 4n))), Nat.mod(U32.to_nat(x), 4n), tn(Nat.mod(U32.to_nat(x), 4n), NR.dm_lt(3n, U32.to_nat(x)))) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.add(Nat.mul(Nat.div(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n), 4n), Nat.mod(Nat.div(Nat.div(U32.to_nat(x), 4n), 4n), 4n)), 4n), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n)), 4n), _)) == x : U32}
  %NR.dm_eq(3n, Nat.div(Nat.div(U32.to_nat(x), 4n), 4n)) : {U32.from_nat(Nat.add(Nat.mul(Nat.add(Nat.mul(_, 4n), Nat.mod(Nat.div(U32.to_nat(x), 4n), 4n)), 4n), Nat.mod(U32.to_nat(x), 4n))) == x : U32}
  %NR.dm_eq(3n, Nat.div(U32.to_nat(x), 4n)) : {U32.from_nat(Nat.add(Nat.mul(_, 4n), Nat.mod(U32.to_nat(x), 4n))) == x : U32}
  %NR.dm_eq(3n, U32.to_nat(x)) : {U32.from_nat(_) == x : U32}
  LW.rt(x)

# ---------------------------------------------------------------- digit values of crumbs

def su_eq_n(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_lt(a, 4n) == True{} : Bool}, +hb: {Nat.is_lt(b, 4n) == True{} : Bool}, +hc: {Nat.is_lt(c, 4n) == True{} : Bool}) -> {PH.su(PH.sext(u(a), u(b), u(c))) == u(a) : U32}:
  match a b c:
    case 0n 0n 0n:
      {==}
    case 0n 0n 1n:
      {==}
    case 0n 0n 2n:
      {==}
    case 0n 0n 3n:
      {==}
    case 0n 1n 0n:
      {==}
    case 0n 1n 1n:
      {==}
    case 0n 1n 2n:
      {==}
    case 0n 1n 3n:
      {==}
    case 0n 2n 0n:
      {==}
    case 0n 2n 1n:
      {==}
    case 0n 2n 2n:
      {==}
    case 0n 2n 3n:
      {==}
    case 0n 3n 0n:
      {==}
    case 0n 3n 1n:
      {==}
    case 0n 3n 2n:
      {==}
    case 0n 3n 3n:
      {==}
    case 1n 0n 0n:
      {==}
    case 1n 0n 1n:
      {==}
    case 1n 0n 2n:
      {==}
    case 1n 0n 3n:
      {==}
    case 1n 1n 0n:
      {==}
    case 1n 1n 1n:
      {==}
    case 1n 1n 2n:
      {==}
    case 1n 1n 3n:
      {==}
    case 1n 2n 0n:
      {==}
    case 1n 2n 1n:
      {==}
    case 1n 2n 2n:
      {==}
    case 1n 2n 3n:
      {==}
    case 1n 3n 0n:
      {==}
    case 1n 3n 1n:
      {==}
    case 1n 3n 2n:
      {==}
    case 1n 3n 3n:
      {==}
    case 2n 0n 0n:
      {==}
    case 2n 0n 1n:
      {==}
    case 2n 0n 2n:
      {==}
    case 2n 0n 3n:
      {==}
    case 2n 1n 0n:
      {==}
    case 2n 1n 1n:
      {==}
    case 2n 1n 2n:
      {==}
    case 2n 1n 3n:
      {==}
    case 2n 2n 0n:
      {==}
    case 2n 2n 1n:
      {==}
    case 2n 2n 2n:
      {==}
    case 2n 2n 3n:
      {==}
    case 2n 3n 0n:
      {==}
    case 2n 3n 1n:
      {==}
    case 2n 3n 2n:
      {==}
    case 2n 3n 3n:
      {==}
    case 3n 0n 0n:
      {==}
    case 3n 0n 1n:
      {==}
    case 3n 0n 2n:
      {==}
    case 3n 0n 3n:
      {==}
    case 3n 1n 0n:
      {==}
    case 3n 1n 1n:
      {==}
    case 3n 1n 2n:
      {==}
    case 3n 1n 3n:
      {==}
    case 3n 2n 0n:
      {==}
    case 3n 2n 1n:
      {==}
    case 3n 2n 2n:
      {==}
    case 3n 2n 3n:
      {==}
    case 3n 3n 0n:
      {==}
    case 3n 3n 1n:
      {==}
    case 3n 3n 2n:
      {==}
    case 3n 3n 3n:
      {==}
    case 4n+r _ _:
      Empty.absurd({PH.su(PH.sext(u(4n+r), u(b), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, ha))
    case 0n 4n+r _:
      Empty.absurd({PH.su(PH.sext(u(0n), u(4n+r), u(c))) == u(0n) : U32}, N.lt_zero_absurd(r, hb))
    case 0n 0n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(0n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
    case 0n 1n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(0n), u(1n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
    case 0n 2n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(0n), u(2n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
    case 0n 3n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(0n), u(3n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
    case 1n 4n+r _:
      Empty.absurd({PH.su(PH.sext(u(1n), u(4n+r), u(c))) == u(1n) : U32}, N.lt_zero_absurd(r, hb))
    case 1n 0n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(1n), u(0n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
    case 1n 1n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(1n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
    case 1n 2n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(1n), u(2n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
    case 1n 3n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(1n), u(3n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
    case 2n 4n+r _:
      Empty.absurd({PH.su(PH.sext(u(2n), u(4n+r), u(c))) == u(2n) : U32}, N.lt_zero_absurd(r, hb))
    case 2n 0n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(2n), u(0n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
    case 2n 1n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(2n), u(1n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
    case 2n 2n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(2n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
    case 2n 3n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(2n), u(3n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
    case 3n 4n+r _:
      Empty.absurd({PH.su(PH.sext(u(3n), u(4n+r), u(c))) == u(3n) : U32}, N.lt_zero_absurd(r, hb))
    case 3n 0n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(3n), u(0n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
    case 3n 1n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(3n), u(1n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
    case 3n 2n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(3n), u(2n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
    case 3n 3n 4n+r:
      Empty.absurd({PH.su(PH.sext(u(3n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))

def su_eq(+x: U32, +y: U32, +z: U32, +hx: {Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool}, +hy: {Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool}, +hz: {Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool}) -> {PH.su(PH.sext(x, y, z)) == x : U32}:
  %LW.rt(x) : {PH.su(PH.sext(_, y, z)) == _ : U32}
  %LW.rt(y) : {PH.su(PH.sext(u(U32.to_nat(x)), _, z)) == u(U32.to_nat(x)) : U32}
  %LW.rt(z) : {PH.su(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)) == u(U32.to_nat(x)) : U32}
  su_eq_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)

def sv_eq_n(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_lt(a, 4n) == True{} : Bool}, +hb: {Nat.is_lt(b, 4n) == True{} : Bool}, +hc: {Nat.is_lt(c, 4n) == True{} : Bool}) -> {PH.sv(PH.sext(u(a), u(b), u(c))) == u(b) : U32}:
  match a b c:
    case 0n 0n 0n:
      {==}
    case 0n 0n 1n:
      {==}
    case 0n 0n 2n:
      {==}
    case 0n 0n 3n:
      {==}
    case 0n 1n 0n:
      {==}
    case 0n 1n 1n:
      {==}
    case 0n 1n 2n:
      {==}
    case 0n 1n 3n:
      {==}
    case 0n 2n 0n:
      {==}
    case 0n 2n 1n:
      {==}
    case 0n 2n 2n:
      {==}
    case 0n 2n 3n:
      {==}
    case 0n 3n 0n:
      {==}
    case 0n 3n 1n:
      {==}
    case 0n 3n 2n:
      {==}
    case 0n 3n 3n:
      {==}
    case 1n 0n 0n:
      {==}
    case 1n 0n 1n:
      {==}
    case 1n 0n 2n:
      {==}
    case 1n 0n 3n:
      {==}
    case 1n 1n 0n:
      {==}
    case 1n 1n 1n:
      {==}
    case 1n 1n 2n:
      {==}
    case 1n 1n 3n:
      {==}
    case 1n 2n 0n:
      {==}
    case 1n 2n 1n:
      {==}
    case 1n 2n 2n:
      {==}
    case 1n 2n 3n:
      {==}
    case 1n 3n 0n:
      {==}
    case 1n 3n 1n:
      {==}
    case 1n 3n 2n:
      {==}
    case 1n 3n 3n:
      {==}
    case 2n 0n 0n:
      {==}
    case 2n 0n 1n:
      {==}
    case 2n 0n 2n:
      {==}
    case 2n 0n 3n:
      {==}
    case 2n 1n 0n:
      {==}
    case 2n 1n 1n:
      {==}
    case 2n 1n 2n:
      {==}
    case 2n 1n 3n:
      {==}
    case 2n 2n 0n:
      {==}
    case 2n 2n 1n:
      {==}
    case 2n 2n 2n:
      {==}
    case 2n 2n 3n:
      {==}
    case 2n 3n 0n:
      {==}
    case 2n 3n 1n:
      {==}
    case 2n 3n 2n:
      {==}
    case 2n 3n 3n:
      {==}
    case 3n 0n 0n:
      {==}
    case 3n 0n 1n:
      {==}
    case 3n 0n 2n:
      {==}
    case 3n 0n 3n:
      {==}
    case 3n 1n 0n:
      {==}
    case 3n 1n 1n:
      {==}
    case 3n 1n 2n:
      {==}
    case 3n 1n 3n:
      {==}
    case 3n 2n 0n:
      {==}
    case 3n 2n 1n:
      {==}
    case 3n 2n 2n:
      {==}
    case 3n 2n 3n:
      {==}
    case 3n 3n 0n:
      {==}
    case 3n 3n 1n:
      {==}
    case 3n 3n 2n:
      {==}
    case 3n 3n 3n:
      {==}
    case 4n+r _ _:
      Empty.absurd({PH.sv(PH.sext(u(4n+r), u(b), u(c))) == u(b) : U32}, N.lt_zero_absurd(r, ha))
    case 0n 4n+r _:
      Empty.absurd({PH.sv(PH.sext(u(0n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
    case 0n 0n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(0n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
    case 0n 1n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(0n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
    case 0n 2n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(0n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
    case 0n 3n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(0n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
    case 1n 4n+r _:
      Empty.absurd({PH.sv(PH.sext(u(1n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
    case 1n 0n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(1n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
    case 1n 1n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(1n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
    case 1n 2n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(1n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
    case 1n 3n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(1n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
    case 2n 4n+r _:
      Empty.absurd({PH.sv(PH.sext(u(2n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
    case 2n 0n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(2n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
    case 2n 1n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(2n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
    case 2n 2n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(2n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
    case 2n 3n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(2n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))
    case 3n 4n+r _:
      Empty.absurd({PH.sv(PH.sext(u(3n), u(4n+r), u(c))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hb))
    case 3n 0n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(3n), u(0n), u(4n+r))) == u(0n) : U32}, N.lt_zero_absurd(r, hc))
    case 3n 1n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(3n), u(1n), u(4n+r))) == u(1n) : U32}, N.lt_zero_absurd(r, hc))
    case 3n 2n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(3n), u(2n), u(4n+r))) == u(2n) : U32}, N.lt_zero_absurd(r, hc))
    case 3n 3n 4n+r:
      Empty.absurd({PH.sv(PH.sext(u(3n), u(3n), u(4n+r))) == u(3n) : U32}, N.lt_zero_absurd(r, hc))

def sv_eq(+x: U32, +y: U32, +z: U32, +hx: {Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool}, +hy: {Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool}, +hz: {Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool}) -> {PH.sv(PH.sext(x, y, z)) == y : U32}:
  %LW.rt(x) : {PH.sv(PH.sext(_, y, z)) == y : U32}
  %LW.rt(y) : {PH.sv(PH.sext(u(U32.to_nat(x)), _, z)) == _ : U32}
  %LW.rt(z) : {PH.sv(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)) == u(U32.to_nat(y)) : U32}
  sv_eq_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)

def sw_eq_n(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_lt(a, 4n) == True{} : Bool}, +hb: {Nat.is_lt(b, 4n) == True{} : Bool}, +hc: {Nat.is_lt(c, 4n) == True{} : Bool}) -> {PH.sw(PH.sext(u(a), u(b), u(c))) == u(c) : U32}:
  match a b c:
    case 0n 0n 0n:
      {==}
    case 0n 0n 1n:
      {==}
    case 0n 0n 2n:
      {==}
    case 0n 0n 3n:
      {==}
    case 0n 1n 0n:
      {==}
    case 0n 1n 1n:
      {==}
    case 0n 1n 2n:
      {==}
    case 0n 1n 3n:
      {==}
    case 0n 2n 0n:
      {==}
    case 0n 2n 1n:
      {==}
    case 0n 2n 2n:
      {==}
    case 0n 2n 3n:
      {==}
    case 0n 3n 0n:
      {==}
    case 0n 3n 1n:
      {==}
    case 0n 3n 2n:
      {==}
    case 0n 3n 3n:
      {==}
    case 1n 0n 0n:
      {==}
    case 1n 0n 1n:
      {==}
    case 1n 0n 2n:
      {==}
    case 1n 0n 3n:
      {==}
    case 1n 1n 0n:
      {==}
    case 1n 1n 1n:
      {==}
    case 1n 1n 2n:
      {==}
    case 1n 1n 3n:
      {==}
    case 1n 2n 0n:
      {==}
    case 1n 2n 1n:
      {==}
    case 1n 2n 2n:
      {==}
    case 1n 2n 3n:
      {==}
    case 1n 3n 0n:
      {==}
    case 1n 3n 1n:
      {==}
    case 1n 3n 2n:
      {==}
    case 1n 3n 3n:
      {==}
    case 2n 0n 0n:
      {==}
    case 2n 0n 1n:
      {==}
    case 2n 0n 2n:
      {==}
    case 2n 0n 3n:
      {==}
    case 2n 1n 0n:
      {==}
    case 2n 1n 1n:
      {==}
    case 2n 1n 2n:
      {==}
    case 2n 1n 3n:
      {==}
    case 2n 2n 0n:
      {==}
    case 2n 2n 1n:
      {==}
    case 2n 2n 2n:
      {==}
    case 2n 2n 3n:
      {==}
    case 2n 3n 0n:
      {==}
    case 2n 3n 1n:
      {==}
    case 2n 3n 2n:
      {==}
    case 2n 3n 3n:
      {==}
    case 3n 0n 0n:
      {==}
    case 3n 0n 1n:
      {==}
    case 3n 0n 2n:
      {==}
    case 3n 0n 3n:
      {==}
    case 3n 1n 0n:
      {==}
    case 3n 1n 1n:
      {==}
    case 3n 1n 2n:
      {==}
    case 3n 1n 3n:
      {==}
    case 3n 2n 0n:
      {==}
    case 3n 2n 1n:
      {==}
    case 3n 2n 2n:
      {==}
    case 3n 2n 3n:
      {==}
    case 3n 3n 0n:
      {==}
    case 3n 3n 1n:
      {==}
    case 3n 3n 2n:
      {==}
    case 3n 3n 3n:
      {==}
    case 4n+r _ _:
      Empty.absurd({PH.sw(PH.sext(u(4n+r), u(b), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, ha))
    case 0n 4n+r _:
      Empty.absurd({PH.sw(PH.sext(u(0n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb))
    case 0n 0n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(0n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 0n 1n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(0n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 0n 2n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(0n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 0n 3n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(0n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 1n 4n+r _:
      Empty.absurd({PH.sw(PH.sext(u(1n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb))
    case 1n 0n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(1n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 1n 1n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(1n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 1n 2n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(1n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 1n 3n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(1n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 2n 4n+r _:
      Empty.absurd({PH.sw(PH.sext(u(2n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb))
    case 2n 0n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(2n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 2n 1n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(2n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 2n 2n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(2n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 2n 3n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(2n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 3n 4n+r _:
      Empty.absurd({PH.sw(PH.sext(u(3n), u(4n+r), u(c))) == u(c) : U32}, N.lt_zero_absurd(r, hb))
    case 3n 0n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(3n), u(0n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 3n 1n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(3n), u(1n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 3n 2n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(3n), u(2n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))
    case 3n 3n 4n+r:
      Empty.absurd({PH.sw(PH.sext(u(3n), u(3n), u(4n+r))) == u(4n+r) : U32}, N.lt_zero_absurd(r, hc))

def sw_eq(+x: U32, +y: U32, +z: U32, +hx: {Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool}, +hy: {Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool}, +hz: {Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool}) -> {PH.sw(PH.sext(x, y, z)) == z : U32}:
  %LW.rt(x) : {PH.sw(PH.sext(_, y, z)) == z : U32}
  %LW.rt(y) : {PH.sw(PH.sext(u(U32.to_nat(x)), _, z)) == z : U32}
  %LW.rt(z) : {PH.sw(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)) == _ : U32}
  sw_eq_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)

def sx_lt_n(+a: Nat, +b: Nat, +c: Nat, +ha: {Nat.is_lt(a, 4n) == True{} : Bool}, +hb: {Nat.is_lt(b, 4n) == True{} : Bool}, +hc: {Nat.is_lt(c, 4n) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(PH.sext(u(a), u(b), u(c))), 64n) == True{} : Bool}:
  match a b c:
    case 0n 0n 0n:
      {==}
    case 0n 0n 1n:
      {==}
    case 0n 0n 2n:
      {==}
    case 0n 0n 3n:
      {==}
    case 0n 1n 0n:
      {==}
    case 0n 1n 1n:
      {==}
    case 0n 1n 2n:
      {==}
    case 0n 1n 3n:
      {==}
    case 0n 2n 0n:
      {==}
    case 0n 2n 1n:
      {==}
    case 0n 2n 2n:
      {==}
    case 0n 2n 3n:
      {==}
    case 0n 3n 0n:
      {==}
    case 0n 3n 1n:
      {==}
    case 0n 3n 2n:
      {==}
    case 0n 3n 3n:
      {==}
    case 1n 0n 0n:
      {==}
    case 1n 0n 1n:
      {==}
    case 1n 0n 2n:
      {==}
    case 1n 0n 3n:
      {==}
    case 1n 1n 0n:
      {==}
    case 1n 1n 1n:
      {==}
    case 1n 1n 2n:
      {==}
    case 1n 1n 3n:
      {==}
    case 1n 2n 0n:
      {==}
    case 1n 2n 1n:
      {==}
    case 1n 2n 2n:
      {==}
    case 1n 2n 3n:
      {==}
    case 1n 3n 0n:
      {==}
    case 1n 3n 1n:
      {==}
    case 1n 3n 2n:
      {==}
    case 1n 3n 3n:
      {==}
    case 2n 0n 0n:
      {==}
    case 2n 0n 1n:
      {==}
    case 2n 0n 2n:
      {==}
    case 2n 0n 3n:
      {==}
    case 2n 1n 0n:
      {==}
    case 2n 1n 1n:
      {==}
    case 2n 1n 2n:
      {==}
    case 2n 1n 3n:
      {==}
    case 2n 2n 0n:
      {==}
    case 2n 2n 1n:
      {==}
    case 2n 2n 2n:
      {==}
    case 2n 2n 3n:
      {==}
    case 2n 3n 0n:
      {==}
    case 2n 3n 1n:
      {==}
    case 2n 3n 2n:
      {==}
    case 2n 3n 3n:
      {==}
    case 3n 0n 0n:
      {==}
    case 3n 0n 1n:
      {==}
    case 3n 0n 2n:
      {==}
    case 3n 0n 3n:
      {==}
    case 3n 1n 0n:
      {==}
    case 3n 1n 1n:
      {==}
    case 3n 1n 2n:
      {==}
    case 3n 1n 3n:
      {==}
    case 3n 2n 0n:
      {==}
    case 3n 2n 1n:
      {==}
    case 3n 2n 2n:
      {==}
    case 3n 2n 3n:
      {==}
    case 3n 3n 0n:
      {==}
    case 3n 3n 1n:
      {==}
    case 3n 3n 2n:
      {==}
    case 3n 3n 3n:
      {==}
    case 4n+r _ _:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(4n+r), u(b), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, ha))
    case 0n 4n+r _:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb))
    case 0n 0n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 0n 1n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 0n 2n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 0n 3n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(0n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 1n 4n+r _:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb))
    case 1n 0n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 1n 1n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 1n 2n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 1n 3n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(1n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 2n 4n+r _:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb))
    case 2n 0n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 2n 1n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 2n 2n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 2n 3n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(2n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 3n 4n+r _:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(4n+r), u(c))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hb))
    case 3n 0n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(0n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 3n 1n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(1n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 3n 2n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(2n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))
    case 3n 3n 4n+r:
      Empty.absurd({Nat.is_lt(U32.to_nat(PH.sext(u(3n), u(3n), u(4n+r))), 64n) == True{} : Bool}, N.lt_zero_absurd(r, hc))

def sx_lt(+x: U32, +y: U32, +z: U32, +hx: {Nat.is_lt(U32.to_nat(x), 4n) == True{} : Bool}, +hy: {Nat.is_lt(U32.to_nat(y), 4n) == True{} : Bool}, +hz: {Nat.is_lt(U32.to_nat(z), 4n) == True{} : Bool}) -> {Nat.is_lt(U32.to_nat(PH.sext(x, y, z)), 64n) == True{} : Bool}:
  %LW.rt(x) : {Nat.is_lt(U32.to_nat(PH.sext(_, y, z)), 64n) == True{} : Bool}
  %LW.rt(y) : {Nat.is_lt(U32.to_nat(PH.sext(u(U32.to_nat(x)), _, z)), 64n) == True{} : Bool}
  %LW.rt(z) : {Nat.is_lt(U32.to_nat(PH.sext(u(U32.to_nat(x)), u(U32.to_nat(y)), _)), 64n) == True{} : Bool}
  sx_lt_n(U32.to_nat(x), U32.to_nat(y), U32.to_nat(z), hx, hy, hz)

# ---------------------------------------------------------------- base64

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>>}
      {==}

# ---------------------------------------------------------------- the '$' separator

# No character is '$'.
def nd(s: String) -> Bool:
  match s:
    case SNil{}:
      True{}
    case SCon{c, r}:
      Bool.and(Bool.not(PH.dollar(SCon{c, SNil{}})), nd(r))

def dollar_cons(+c: Char, +r: String, +r2: String) -> {PH.dollar(SCon{c, r}) == PH.dollar(SCon{c, r2}) : Bool}:
  match c:
    case Chr{x}:
      {==}

def nd_head(+c: Char, +r: String, +h: {nd(SCon{c, r}) == True{} : Bool}) -> {PH.dollar(SCon{c, SNil{}}) == False{} : Bool}:
  +e = L.and_left(Bool.not(PH.dollar(SCon{c, SNil{}})), nd(r), h)
  L.not_true(PH.dollar(SCon{c, SNil{}}), e)

def nd_tail(+c: Char, +r: String, +h: {nd(SCon{c, r}) == True{} : Bool}) -> {nd(r) == True{} : Bool}:
  L.and_right(Bool.not(PH.dollar(SCon{c, SNil{}})), nd(r), h)

# A string without '$', then '$': the field before it and the rest.
def field_nd(+cs: String, +r: String, +h: {nd(cs) == True{} : Bool}) -> {PH.field_go(String.append(cs, SCon{Chr{36}, r}), PH.dollar(String.append(cs, SCon{Chr{36}, r}))) == Some{PH.Cut{cs, r}} : Maybe<&2, PH.Cut>}:
  match cs:
    case SNil{}:
      {==}
    case SCon{Chr{+x}, +t}:
      +hd = Equal.trans(Bool, PH.dollar(SCon{Chr{x}, String.append(t, SCon{Chr{36}, r})}), PH.dollar(SCon{Chr{x}, SNil{}}), False{}, dollar_cons(Chr{x}, String.append(t, SCon{Chr{36}, r}), SNil{}), nd_head(Chr{x}, t, h))
      %Equal.sym(Bool, PH.dollar(SCon{Chr{x}, String.append(t, SCon{Chr{36}, r})}), False{}, hd) : {PH.field_go(SCon{Chr{x}, String.append(t, SCon{Chr{36}, r})}, _) == Some{PH.Cut{SCon{Chr{x}, t}, r}} : Maybe<&2, PH.Cut>}
      %Equal.sym(Maybe<&2, PH.Cut>, PH.field_go(String.append(t, SCon{Chr{36}, r}), PH.dollar(String.append(t, SCon{Chr{36}, r}))), Some{PH.Cut{t, r}}, field_nd(t, r, nd_tail(Chr{x}, t, h))) : {PH.field_cons(x, _) == Some{PH.Cut{SCon{Chr{x}, t}, r}} : Maybe<&2, PH.Cut>}
      {==}

def b64_nd(+bs: List<&2, U32>, +h: {ok(bs) == True{} : Bool}) -> {nd(PH.b64(bs)) == True{} : Bool}:
  match bs:
    case Nil{}:
      {==}
    case +a <> Nil{}:
      +ha = ok_head(a, Nil{}, h)
      +ta = ok_tail(a, Nil{}, h)
      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), SNil{}}), False{}, no_dollar(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)))) : {Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), 0, 0)), SNil{}})), True{})) == True{} : Bool}
      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), 0, 0)), SNil{}}), False{}, no_dollar(PH.sext(PH.c0(a), 0, 0), sx_lt(PH.c0(a), 0, 0, c0_lt(a), {==}, {==}))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), True{})) == True{} : Bool}
      {==}
    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(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), SNil{}}), False{}, no_dollar(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)))) : {Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)), SNil{}})), True{}))) == True{} : Bool}
      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}}), False{}, no_dollar(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)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)), SNil{}})), True{}))) == True{} : Bool}
      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), 0)), SNil{}}), False{}, no_dollar(PH.sext(PH.c1(b), PH.c0(b), 0), sx_lt(PH.c1(b), PH.c0(b), 0, c1_lt(b), c0_lt(b), {==}))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), True{}))) == True{} : Bool}
      {==}
    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(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c3(a), PH.c2(a), PH.c1(a))), SNil{}}), False{}, no_dollar(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)))) : {Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}})), nd(PH.b64(rest)))))) == True{} : Bool}
      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c0(a), PH.c3(b), PH.c2(b))), SNil{}}), False{}, no_dollar(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)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), SNil{}})), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}})), nd(PH.b64(rest)))))) == True{} : Bool}
      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c1(b), PH.c0(b), PH.c3(c))), SNil{}}), False{}, no_dollar(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)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), Bool.and(Bool.not(PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}})), nd(PH.b64(rest)))))) == True{} : Bool}
      %Equal.sym(Bool, PH.dollar(SCon{PH.digit(PH.sext(PH.c2(c), PH.c1(c), PH.c0(c))), SNil{}}), False{}, no_dollar(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)))) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(_), nd(PH.b64(rest)))))) == True{} : Bool}
      %Equal.sym(Bool, nd(PH.b64(rest)), True{}, b64_nd(rest, tc)) : {Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), Bool.and(Bool.not(False{}), _)))) == True{} : Bool}
      {==}

def field_b64(+bs: List<&2, U32>, +r: String, +h: {ok(bs) == True{} : Bool}) -> {PH.field(String.append(PH.b64(bs), SCon{Chr{36}, r})) == Some{PH.Cut{PH.b64(bs), r}} : Maybe<&2, PH.Cut>}:
  field_nd(PH.b64(bs), r, b64_nd(bs, h))

# ---------------------------------------------------------------- decimal

def dd_n(+n: Nat, +h: {Nat.is_lt(n, 10n) == True{} : Bool}) -> {U32.to_nat(U32.sub(U32.add(48, U32.from_nat(n)), 48)) == n : Nat}:
  match n:
    case 0n:
      {==}
    case 1n:
      {==}
    case 2n:
      {==}
    case 3n:
      {==}
    case 4n:
      {==}
    case 5n:
      {==}
    case 6n:
      {==}
    case 7n:
      {==}
    case 8n:
      {==}
    case 9n:
      {==}
    case 10n+r:
      Empty.absurd({U32.to_nat(U32.sub(U32.add(48, U32.from_nat(10n+r)), 48)) == 10n+r : Nat}, N.lt_zero_absurd(r, h))

def di_n(+n: Nat, +h: {Nat.is_lt(n, 10n) == True{} : Bool}) -> {PH.is_digit(U32.add(48, U32.from_nat(n))) == True{} : Bool}:
  match n:
    case 0n:
      {==}
    case 1n:
      {==}
    case 2n:
      {==}
    case 3n:
      {==}
    case 4n:
      {==}
    case 5n:
      {==}
    case 6n:
      {==}
    case 7n:
      {==}
    case 8n:
      {==}
    case 9n:
      {==}
    case 10n+r:
      Empty.absurd({PH.is_digit(U32.add(48, U32.from_nat(10n+r))) == True{} : Bool}, N.lt_zero_absurd(r, h))

def mul10_ge(+k: Nat) -> {Nat.is_le(k, Nat.mul(k, 10n)) == True{} : Bool}:
  match k:
    case 0n:
      {==}
    case 1n+ +j:
      +x = Nat.mul(j, 10n)
      +h1 = N.le_trans(j, x, Nat.add(x, 9n), mul10_ge(j), N.le_add_right(x, 9n))
      L.subst(Nat, z => {Nat.is_le(j, z) == True{} : Bool}, Nat.add(x, 9n), Nat.add(9n, x), N.add_comm(x, 9n), h1)

# m < 9 + 10 m
def lt9(+m: Nat) -> {Nat.is_lt(m, Nat.add(9n, Nat.mul(m, 10n))) == True{} : Bool}:
  +x = Nat.mul(m, 10n)
  +h0 = L.subst(Nat, z => {Nat.is_lt(z, Nat.add(x, 9n)) == True{} : Bool}, Nat.add(x, 0n), x, N.add_zero(x), N.lt_add_left(0n, 9n, x, {==}))
  +h1 = N.le_lt_trans(m, x, Nat.add(x, 9n), mul10_ge(m), h0)
  L.subst(Nat, z => {Nat.is_lt(m, z) == True{} : Bool}, Nat.add(x, 9n), Nat.add(9n, x), N.add_comm(x, 9n), h1)

# n / 10 < n for n >= 1.
def div10_lt(+n: Nat, +h: {Nat.is_le(1n, n) == True{} : Bool}) -> {Nat.is_lt(Nat.div(n, 10n), n) == True{} : Bool}:
  match n:
    case 0n:
      Empty.absurd({Nat.is_lt(Nat.div(0n, 10n), 0n) == True{} : Bool}, L.false_true(h))
    case 1n+ +m:
      +e = NR.le_div(9n, 1n+m, 1n+m)
      +f = N.lt_not_le(m, Nat.add(9n, Nat.mul(m, 10n)), lt9(m))
      N.not_le_lt(1n+m, Nat.div(1n+m, 10n), Equal.trans(Bool, Nat.is_le(1n+m, Nat.div(1n+m, 10n)), Nat.is_le(Nat.mul(1n+m, 10n), 1n+m), False{}, e, f))

def ge10_pos(+n: Nat, +h: {Nat.is_lt(n, 10n) == False{} : Bool}) -> {Nat.is_le(1n, n) == True{} : Bool}:
  match n:
    case 0n:
      Empty.absurd({Nat.is_le(1n, 0n) == True{} : Bool}, L.true_false(h))
    case 1n+ +m:
      N.zero_le(m)

def sd_dec(+f: Nat, +n: Nat, +acc: String, +Y: String, +last: Bool, +el: {Nat.is_lt(n, 10n) == last : Bool}, +hf: {Nat.is_lt(n, f) == True{} : Bool}) -> {PH.starts_digit(String.append(PH.dec_go(f, n, acc, last), Y)) == True{} : Bool}:
  match f last:
    case 0n _:
      Empty.absurd({PH.starts_digit(String.append(acc, Y)) == True{} : Bool}, N.lt_zero_absurd(n, hf))
    case 1n+ +g True{}:
      di_n(n, el)
    case 1n+ +g False{}:
      +q = Nat.div(n, 10n)
      sd_dec(g, q, SCon{PH.dchar(Nat.mod(n, 10n)), acc}, Y, Nat.is_lt(q, 10n), {==}, N.lt_le_trans(q, n, g, div10_lt(n, ge10_pos(n, el)), N.lt_succ_le(n, g, hf)))

def dec_step(+n: Nat, +ay: String, +hr: {Nat.is_lt(Nat.mod(n, 10n), 10n) == True{} : Bool}) -> {PH.read_go(SCon{PH.dchar(Nat.mod(n, 10n)), ay}, Nat.div(n, 10n), PH.starts_digit(SCon{PH.dchar(Nat.mod(n, 10n)), ay})) == PH.read_go(ay, n, PH.starts_digit(ay)) : PH.Got}:
  +q = Nat.div(n, 10n)
  +r = Nat.mod(n, 10n)
  -rhs = PH.read_go(ay, n, PH.starts_digit(ay))
  %Equal.sym(Bool, PH.is_digit(U32.add(48, U32.from_nat(r))), True{}, di_n(r, hr)) : {PH.read_go(SCon{PH.dchar(r), ay}, q, _) == rhs : PH.Got}
  %Equal.sym(Nat, U32.to_nat(U32.sub(U32.add(48, U32.from_nat(r)), 48)), r, dd_n(r, hr)) : {PH.read_go(ay, Nat.add(Nat.mul(q, 10n), _), PH.starts_digit(ay)) == rhs : PH.Got}
  %NR.dm_eq(9n, n) : {PH.read_go(ay, _, PH.starts_digit(ay)) == rhs : PH.Got}
  {==}

# Reading the decimal digits of n before acc gives n and acc.
def dec_go_rt(+f: Nat, +n: Nat, +acc: String, +Y: String, +last: Bool, +el: {Nat.is_lt(n, 10n) == last : Bool}, +hf: {Nat.is_lt(n, f) == True{} : Bool}) -> {PH.read_go(String.append(PH.dec_go(f, n, acc, last), Y), 0n, True{}) == PH.read_go(String.append(acc, Y), n, PH.starts_digit(String.append(acc, Y))) : PH.Got}:
  match f last:
    case 0n _:
      Empty.absurd({PH.read_go(String.append(acc, Y), 0n, True{}) == PH.read_go(String.append(acc, Y), n, PH.starts_digit(String.append(acc, Y))) : PH.Got}, N.lt_zero_absurd(n, hf))
    case 1n+ +g True{}:
      %Equal.sym(Nat, U32.to_nat(U32.sub(U32.add(48, U32.from_nat(n)), 48)), n, dd_n(n, el)) : {PH.read_go(String.append(acc, Y), _, PH.starts_digit(String.append(acc, Y))) == PH.read_go(String.append(acc, Y), n, PH.starts_digit(String.append(acc, Y))) : PH.Got}
      {==}
    case 1n+ +g False{}:
      +q = Nat.div(n, 10n)
      +r = Nat.mod(n, 10n)
      +ay = String.append(acc, Y)
      +hr = NR.dm_lt(9n, n)
      +hq = N.lt_le_trans(q, n, g, div10_lt(n, ge10_pos(n, el)), N.lt_succ_le(n, g, hf))
      -rhs = PH.read_go(ay, n, PH.starts_digit(ay))
      Equal.trans(PH.Got, PH.read_go(String.append(PH.dec_go(g, q, SCon{PH.dchar(r), acc}, Nat.is_lt(q, 10n)), Y), 0n, True{}), PH.read_go(SCon{PH.dchar(r), ay}, q, PH.starts_digit(SCon{PH.dchar(r), ay})), rhs,
        dec_go_rt(g, q, SCon{PH.dchar(r), acc}, Y, Nat.is_lt(q, 10n), {==}, hq),
        dec_step(n, ay, hr))

def got_nd(+n: Nat, +c: Char, +Y: String) -> {Some{PH.read_go(SCon{c, Y}, n, False{})} == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}:
  match c:
    case Chr{x}:
      {==}

# A decimal number followed by a non-digit is read back.
def dec_rt(+n: Nat, +c: Char, +Y: String, +hc: {PH.starts_digit(SCon{c, Y}) == False{} : Bool}) -> {PH.read(String.append(PH.decimal(n), SCon{c, Y})) == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}:
  +s = String.append(PH.dec_go(1n+n, n, SNil{}, Nat.is_lt(n, 10n)), SCon{c, Y})
  %Equal.sym(Bool, PH.starts_digit(s), True{}, sd_dec(1n+n, n, SNil{}, SCon{c, Y}, Nat.is_lt(n, 10n), {==}, N.lt_succ(n))) : {PH.read_check(s, _) == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}
  %Equal.sym(PH.Got, PH.read_go(s, 0n, True{}), PH.read_go(SCon{c, Y}, n, PH.starts_digit(SCon{c, Y})), dec_go_rt(1n+n, n, SNil{}, SCon{c, Y}, Nat.is_lt(n, 10n), {==}, N.lt_succ(n))) : {Some{_} == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}
  %Equal.sym(Bool, PH.starts_digit(SCon{c, Y}), False{}, hc) : {Some{PH.read_go(SCon{c, Y}, n, _)} == Some{PH.Got{n, SCon{c, Y}}} : Maybe<&2, PH.Got>}
  got_nd(n, c, Y)


# ---------------------------------------------------------------- the PHC string

def append_nil(+x: String) -> {String.append(x, SNil{}) == x : String}:
  match x:
    case SNil{}:
      {==}
    case SCon{+h, +t}:
      Equal.cong(String, String, z => SCon{h, z}, String.append(t, SNil{}), t, append_nil(t))

# parse(format(x)) == Some{x}, for byte lists of bytes below 256.
def parse_format(+m: Nat, +t: Nat, +p: Nat, +salt: List<&2, U32>, +hash: List<&2, U32>, +hs: {ok(salt) == True{} : Bool}, +hh: {ok(hash) == True{} : Bool}) -> {PH.parse(PH.format(PH.Phc{m, t, p, salt, hash})) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}:
  %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(m), SCon{Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))})), Some{PH.Got{m, SCon{Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))}}}, dec_rt(m, Chr{44}, String.append("t=", String.concat([PH.decimal(t), ",p=", PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)])), {==})) : {PH.parse_m(_) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
  %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(t), SCon{Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))})), Some{PH.Got{t, SCon{Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)]))}}}, dec_rt(t, Chr{44}, String.append("p=", String.concat([PH.decimal(p), "$", PH.b64(salt), "$", PH.b64(hash)])), {==})) : {PH.parse_t(m, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
  %Equal.sym(Maybe<&2, PH.Got>, PH.read(String.append(PH.decimal(p), SCon{Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)])})), Some{PH.Got{p, SCon{Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)])}}}, dec_rt(p, Chr{36}, String.concat([PH.b64(salt), "$", PH.b64(hash)]), {==})) : {PH.parse_p(m, t, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
  %Equal.sym(Maybe<&2, PH.Cut>, PH.field(String.append(PH.b64(salt), SCon{Chr{36}, String.concat([PH.b64(hash)])})), Some{PH.Cut{PH.b64(salt), String.concat([PH.b64(hash)])}}, field_b64(salt, String.concat([PH.b64(hash)]), hs)) : {PH.parse_salt(m, t, p, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
  %Equal.sym(String, String.append(PH.b64(hash), SNil{}), PH.b64(hash), append_nil(PH.b64(hash))) : {PH.parse_hash(m, t, p, PH.unb64(PH.b64(salt)), PH.unb64(_)) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
  %Equal.sym(Maybe<&2, List<&2, U32>>, PH.unb64(PH.b64(salt)), Some{salt}, b64_rt(salt, hs)) : {PH.parse_hash(m, t, p, _, PH.unb64(PH.b64(hash))) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
  %Equal.sym(Maybe<&2, List<&2, U32>>, PH.unb64(PH.b64(hash)), Some{hash}, b64_rt(hash, hh)) : {PH.parse_hash(m, t, p, Some{salt}, _) == Some{PH.Phc{m, t, p, salt, hash}} : Maybe<&2, PH.Phc>}
  {==}