def wsh.go

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:410

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W

410def wsh.go(n: Nat, +a: W.W64, +acc: String, +hf: {W.W64.is_zero(wsh.it(n, a)) == True{} : Bool}) -> {Nat.read.go(W.W64.show.go(n, a, acc), 0n) == Nat.read.go(acc, W.W64.to_nat(a)) : Maybe<&2, Nat>}:
411  match n:
412    case 0n:
413      Equal.cong(Nat, Maybe<&2, Nat>, zz => Nat.read.go(acc, zz), 0n, W.W64.to_nat(a), Equal.sym(Nat, W.W64.to_nat(a), 0n, wsh.zv(a, hf)))
414    case 1n+ +p:
415      wsh.step(p, a, acc, W.W64.is_zero(a), {==}, wsh.go(p, wsh.q(a), acc, hf), wsh.go(p, wsh.q(a), SCon{W.W64.digit(wsh.r(a)), acc}, hf))