PROOFText.wsd.alg: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_text.bend as PROOFText
Lines 306-307 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=306&end_line=307

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

def wsd.alg(+H: Nat, +L: Nat, +Z: Nat, +C1: Nat, +C2: Nat, +C3: Nat, +C4: Nat, +D1: Nat, +D2: Nat, +D3: Nat, +D4: Nat, +M1: Nat, +M2: Nat, +M3: Nat, +M4: Nat, +Q1: Nat, +Q2: Nat, +Q3: Nat, +Q4: Nat, +ez: {Z == 0n : Nat}, +eq1: {Q1 == Nat.add(U.U32Nat.dbl(16n, Z), D1) : Nat}, +eq2: {Q2 == Nat.add(U.U32Nat.dbl(16n, Q1), D2) : Nat}, +eq3: {Q3 == Nat.add(U.U32Nat.dbl(16n, Z), D3) : Nat}, +eq4: {Q4 == Nat.add(U.U32Nat.dbl(16n, Q3), D4) : Nat}, +ed1: {Nat.add(Nat.mul(D1, 10n), M1) == Nat.add(U.U32Nat.dbl(16n, Z), C1) : Nat}, +ed2: {Nat.add(Nat.mul(D2, 10n), M2) == Nat.add(U.U32Nat.dbl(16n, M1), C2) : Nat}, +ed3: {Nat.add(Nat.mul(D3, 10n), M3) == Nat.add(U.U32Nat.dbl(16n, M2), C3) : Nat}, +ed4: {Nat.add(Nat.mul(D4, 10n), M4) == Nat.add(U.U32Nat.dbl(16n, M3), C4) : Nat}, +ec1: {C1 == U.U32Nat.high(16n, H) : Nat}, +ec2: {C2 == U.U32Nat.low(16n, H) : Nat}, +ec3: {C3 == U.U32Nat.high(16n, L) : Nat}, +ec4: {C4 == U.U32Nat.low(16n, L) : Nat}) -> {Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4) == Nat.add(L, U.U32Nat.dbl(32n, H)) : Nat}:
  Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(L, U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(16n, H), U.U32Nat.dbl(16n, U.U32Nat.high(16n, H))))), Nat.add(L, U.U32Nat.dbl(32n, H)), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(L, U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(16n, H), U.U32Nat.dbl(16n, C1)))), Nat.add(L, U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(16n, H), U.U32Nat.dbl(16n, U.U32Nat.high(16n, H))))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(L, U.U32Nat.dbl(32n, Nat.add(C2, U.U32Nat.dbl(16n, C1)))), Nat.add(L, U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(16n, H), U.U32Nat.dbl(16n, C1)))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.add(U.U32Nat.low(16n, L), U.U32Nat.dbl(16n, U.U32Nat.high(16n, L))), U.U32Nat.dbl(32n, Nat.add(C2, U.U32Nat.dbl(16n, C1)))), Nat.add(L, U.U32Nat.dbl(32n, Nat.add(C2, U.U32Nat.dbl(16n, C1)))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.add(U.U32Nat.low(16n, L), U.U32Nat.dbl(16n, C3)), U.U32Nat.dbl(32n, Nat.add(C2, U.U32Nat.dbl(16n, C1)))), Nat.add(Nat.add(U.U32Nat.low(16n, L), U.U32Nat.dbl(16n, U.U32Nat.high(16n, L))), U.U32Nat.dbl(32n, Nat.add(C2, U.U32Nat.dbl(16n, C1)))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.add(C4, U.U32Nat.dbl(16n, C3)), U.U32Nat.dbl(32n, Nat.add(C2, U.U32Nat.dbl(16n, C1)))), Nat.add(Nat.add(U.U32Nat.low(16n, L), U.U32Nat.dbl(16n, C3)), U.U32Nat.dbl(32n, Nat.add(C2, U.U32Nat.dbl(16n, C1)))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.add(U.U32Nat.dbl(16n, C3), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, 0n), C1)), C2))), Nat.add(Nat.add(C4, U.U32Nat.dbl(16n, C3)), U.U32Nat.dbl(32n, Nat.add(C2, U.U32Nat.dbl(16n, C1)))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.add(U.U32Nat.dbl(16n, C3), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, Z), C1)), C2))), Nat.add(Nat.add(U.U32Nat.dbl(16n, C3), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, 0n), C1)), C2))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.add(U.U32Nat.dbl(16n, C3), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.add(Nat.mul(D1, 10n), M1)), C2))), Nat.add(Nat.add(U.U32Nat.dbl(16n, C3), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, Z), C1)), C2))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.add(U.U32Nat.dbl(16n, C3), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.add(U.U32Nat.dbl(16n, M1), C2)))), Nat.add(Nat.add(U.U32Nat.dbl(16n, C3), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.add(Nat.mul(D1, 10n), M1)), C2))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.add(U.U32Nat.dbl(16n, C3), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.add(Nat.mul(D2, 10n), M2)))), Nat.add(Nat.add(U.U32Nat.dbl(16n, C3), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.add(U.U32Nat.dbl(16n, M1), C2)))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, M2), C3)), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.mul(D2, 10n)))), Nat.add(Nat.add(U.U32Nat.dbl(16n, C3), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.add(Nat.mul(D2, 10n), M2)))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(Nat.mul(D3, 10n), M3)), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.mul(D2, 10n)))), Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, M2), C3)), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.mul(D2, 10n)))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.mul(D3, 10n)), Nat.add(U.U32Nat.dbl(16n, M3), C4)), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.mul(D2, 10n)))), Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(Nat.mul(D3, 10n), M3)), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.mul(D2, 10n)))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.mul(D3, 10n)), Nat.add(Nat.mul(D4, 10n), M4)), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.mul(D2, 10n)))), Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.mul(D3, 10n)), Nat.add(U.U32Nat.dbl(16n, M3), C4)), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.mul(D2, 10n)))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.mul(Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, 0n), D3)), D4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, 0n), D1)), D2))), 10n), M4), Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.mul(D3, 10n)), Nat.add(Nat.mul(D4, 10n), M4)), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.mul(D2, 10n)))), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.mul(Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, Z), D3)), D4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, Z), D1)), D2))), 10n), M4), Nat.add(Nat.mul(Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, 0n), D3)), D4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, 0n), D1)), D2))), 10n), M4), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.mul(Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, Z), D3)), D4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Q1), D2))), 10n), M4), Nat.add(Nat.mul(Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, Z), D3)), D4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, Z), D1)), D2))), 10n), M4), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.mul(Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, Z), D3)), D4), U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.mul(Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, Z), D3)), D4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Q1), D2))), 10n), M4), Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(Q4, U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.mul(Nat.add(Nat.add(U.U32Nat.dbl(16n, Q3), D4), U.U32Nat.dbl(32n, Q2)), 10n), M4), Nat.add(Nat.mul(Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, Z), D3)), D4), U.U32Nat.dbl(32n, Q2)), 10n), M4), Equal.cong(Nat, Nat, zz => Nat.add(Nat.mul(Nat.add(zz, U.U32Nat.dbl(32n, Q2)), 10n), M4), Q4, Nat.add(U.U32Nat.dbl(16n, Q3), D4), eq4), Equal.cong(Nat, Nat, zz => Nat.add(Nat.mul(Nat.add(Nat.add(U.U32Nat.dbl(16n, zz), D4), U.U32Nat.dbl(32n, Q2)), 10n), M4), Q3, Nat.add(U.U32Nat.dbl(16n, Z), D3), eq3)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.mul(Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, Z), D3)), D4), U.U32Nat.dbl(32n, zz)), 10n), M4), Q2, Nat.add(U.U32Nat.dbl(16n, Q1), D2), eq2)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.mul(Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, Z), D3)), D4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, zz), D2))), 10n), M4), Q1, Nat.add(U.U32Nat.dbl(16n, Z), D1), eq1)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.mul(Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, zz), D3)), D4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, zz), D1)), D2))), 10n), M4), Z, 0n, ez)), wr.t6(D3, D4, D1, D2, M4)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.dbl(16n, Nat.mul(D3, 10n)), zz), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.mul(D2, 10n)))), Nat.add(Nat.mul(D4, 10n), M4), Nat.add(U.U32Nat.dbl(16n, M3), C4), ed4)), Equal.cong(Nat, Nat, zz => Nat.add(zz, U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.mul(D2, 10n)))), Nat.add(U.U32Nat.dbl(16n, Nat.mul(D3, 10n)), Nat.add(U.U32Nat.dbl(16n, M3), C4)), Nat.add(U.U32Nat.dbl(16n, Nat.add(Nat.mul(D3, 10n), M3)), C4), wr.t7(D3, M3, C4))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.dbl(16n, zz), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.mul(D2, 10n)))), Nat.add(Nat.mul(D3, 10n), M3), Nat.add(U.U32Nat.dbl(16n, M2), C3), ed3)), wr.t8(M2, C3, C4, D1, D2)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.dbl(16n, C3), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), zz))), Nat.add(Nat.mul(D2, 10n), M2), Nat.add(U.U32Nat.dbl(16n, M1), C2), ed2)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.dbl(16n, C3), C4), U.U32Nat.dbl(32n, zz)), Nat.add(U.U32Nat.dbl(16n, Nat.mul(D1, 10n)), Nat.add(U.U32Nat.dbl(16n, M1), C2)), Nat.add(U.U32Nat.dbl(16n, Nat.add(Nat.mul(D1, 10n), M1)), C2), wr.t7(D1, M1, C2))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.dbl(16n, C3), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, zz), C2))), Nat.add(Nat.mul(D1, 10n), M1), Nat.add(U.U32Nat.dbl(16n, Z), C1), ed1)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.dbl(16n, C3), C4), U.U32Nat.dbl(32n, Nat.add(U.U32Nat.dbl(16n, Nat.add(U.U32Nat.dbl(16n, zz), C1)), C2))), Z, 0n, ez)), wr.t9(C3, C4, C1, C2)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(zz, U.U32Nat.dbl(16n, C3)), U.U32Nat.dbl(32n, Nat.add(C2, U.U32Nat.dbl(16n, C1)))), C4, U.U32Nat.low(16n, L), ec4)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(U.U32Nat.low(16n, L), U.U32Nat.dbl(16n, zz)), U.U32Nat.dbl(32n, Nat.add(C2, U.U32Nat.dbl(16n, C1)))), C3, U.U32Nat.high(16n, L), ec3)), Equal.cong(Nat, Nat, zz => Nat.add(zz, U.U32Nat.dbl(32n, Nat.add(C2, U.U32Nat.dbl(16n, C1)))), Nat.add(U.U32Nat.low(16n, L), U.U32Nat.dbl(16n, U.U32Nat.high(16n, L))), L, UL.low_high(16n, L))), Equal.cong(Nat, Nat, zz => Nat.add(L, U.U32Nat.dbl(32n, Nat.add(zz, U.U32Nat.dbl(16n, C1)))), C2, U.U32Nat.low(16n, H), ec2)), Equal.cong(Nat, Nat, zz => Nat.add(L, U.U32Nat.dbl(32n, Nat.add(U.U32Nat.low(16n, H), U.U32Nat.dbl(16n, zz)))), C1, U.U32Nat.high(16n, H), ec1)), Equal.cong(Nat, Nat, zz => Nat.add(L, U.U32Nat.dbl(32n, zz)), Nat.add(U.U32Nat.low(16n, H), U.U32Nat.dbl(16n, U.U32Nat.high(16n, H))), H, UL.low_high(16n, H)))

Uses (13):
  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.trans
  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=bend-osdev-u32@0.1.0.0/LAWS.bend&name=low_high
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.high
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.low
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wr.t6
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wr.t7
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wr.t8
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_text.bend&name=wr.t9