PROOFText.wsh.step: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
Lines 401-408 of bend-osdev-word64@0.1.1.0/PROOF_text.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&start_line=401&end_line=408

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

def wsh.step(+p: Nat, +a: W.W64, +acc: String, z: Bool, +ez: {W.W64.is_zero(a) == z : Bool}, +i0: {Nat.read.go(W.W64.show.go(p, wsh.q(a), acc), 0n) == Nat.read.go(acc, W.W64.to_nat(wsh.q(a))) : Maybe<&2, Nat>}, +i1: {Nat.read.go(W.W64.show.go(p, wsh.q(a), SCon{W.W64.digit(wsh.r(a)), acc}), 0n) == Nat.read.go(SCon{W.W64.digit(wsh.r(a)), acc}, W.W64.to_nat(wsh.q(a))) : Maybe<&2, Nat>}) -> {Nat.read.go(W.W64.show.go(p, wsh.q(a), W.W64.show.push(z, acc, wsh.r(a))), 0n) == Nat.read.go(acc, W.W64.to_nat(a)) : Maybe<&2, Nat>}:
  match z:
    case True{}:
      +a0 = wsh.zv(a, ez)
      +q0 = wsh.m0(W.W64.to_nat(wsh.q(a)), U32.to_nat(wsh.r(a)), Equal.trans(Nat, Nat.add(Nat.mul(W.W64.to_nat(wsh.q(a)), 10n), U32.to_nat(wsh.r(a))), W.W64.to_nat(a), 0n, wsd.e(a, wsd.sd(a)), a0))
      Equal.trans(Maybe<&2, Nat>, Nat.read.go(W.W64.show.go(p, wsh.q(a), acc), 0n), Nat.read.go(acc, W.W64.to_nat(wsh.q(a))), Nat.read.go(acc, W.W64.to_nat(a)), i0, Equal.cong(Nat, Maybe<&2, Nat>, zz => Nat.read.go(acc, zz), W.W64.to_nat(wsh.q(a)), W.W64.to_nat(a), Equal.trans(Nat, W.W64.to_nat(wsh.q(a)), 0n, W.W64.to_nat(a), q0, Equal.sym(Nat, W.W64.to_nat(a), 0n, a0))))
    case False{}:
      Equal.trans(Maybe<&2, Nat>, Nat.read.go(W.W64.show.go(p, wsh.q(a), SCon{W.W64.digit(wsh.r(a)), acc}), 0n), Nat.read.go(SCon{W.W64.digit(wsh.r(a)), acc}, W.W64.to_nat(wsh.q(a))), Nat.read.go(acc, W.W64.to_nat(a)), i1, Equal.trans(Maybe<&2, Nat>, Nat.read.go(SCon{W.W64.digit(wsh.r(a)), acc}, W.W64.to_nat(wsh.q(a))), Nat.read.go(acc, Nat.add(Nat.mul(W.W64.to_nat(wsh.q(a)), 10n), U32.to_nat(wsh.r(a)))), Nat.read.go(acc, W.W64.to_nat(a)), wsh.rd(wsh.r(a), acc, W.W64.to_nat(wsh.q(a)), wsd.l(a, wsd.sd(a))), Equal.cong(Nat, Maybe<&2, Nat>, zz => Nat.read.go(acc, zz), Nat.add(Nat.mul(W.W64.to_nat(wsh.q(a)), 10n), U32.to_nat(wsh.r(a))), W.W64.to_nat(a), wsd.e(a, wsd.sd(a)))))

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.read.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsd.e
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsd.l
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsd.sd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.m0
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.q
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.r
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.rd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wsh.zv
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.digit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.is_zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.show.go
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.show.push
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/word64.bend&name=W64.to_nat