def wsh.step

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

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

401def 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>}:
402  match z:
403    case True{}:
404      +a0 = wsh.zv(a, ez)
405      +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))
406      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))))
407    case False{}:
408      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)))))