def un.dmu

bend-osdev-u32@0.1.0.0 · PROOF.bend:1075

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

1075def un.dmu(+b: Nat, +q1: Nat, +r1: Nat, +q2: Nat, +r2: Nat, e: {Nat.add(Nat.mul(q1, b), r1) == Nat.add(Nat.mul(q2, b), r2) : Nat}, h1: {Nat.is_lt(r1, b) == True{} : Bool}, h2: {Nat.is_lt(r2, b) == True{} : Bool}) -> {q1 == q2 : Nat} & {r1 == r2 : Nat}:
1076  match q1 q2:
1077    case 0n 0n:
1078      ({==}, e)
1079    case 0n 1n+s:
1080      Empty.absurd({0n == 1n+s : Nat} & {r1 == r2 : Nat}, Laws.nat_succ_add_absurd(Nat.add(Nat.sub(b, 1n+r1), Nat.add(Nat.mul(s, b), r2)), b, Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(b, 1n+r1), Nat.add(Nat.mul(s, b), r2)), 1n+b), Nat.add(Nat.sub(b, 1n+r1), 1n+r1), b, Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(b, 1n+r1), Nat.add(Nat.mul(s, b), r2)), 1n+b), Nat.add(Nat.sub(b, 1n+r1), 1n+Nat.add(Nat.mul(0n, b), r1)), Nat.add(Nat.sub(b, 1n+r1), 1n+r1), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(b, 1n+r1), Nat.add(Nat.mul(s, b), r2)), 1n+b), Nat.add(Nat.sub(b, 1n+r1), 1n+Nat.add(Nat.mul(1n+s, b), r2)), Nat.add(Nat.sub(b, 1n+r1), 1n+Nat.add(Nat.mul(0n, b), r1)), ur.r0(Nat.sub(b, 1n+r1), s, b, r2), Equal.cong(Nat, Nat, zz => Nat.add(Nat.sub(b, 1n+r1), 1n+zz), Nat.add(Nat.mul(1n+s, b), r2), Nat.add(Nat.mul(0n, b), r1), Equal.sym(Nat, Nat.add(Nat.mul(0n, b), r1), Nat.add(Nat.mul(1n+s, b), r2), e))), {==}), Laws.nat_lt_witness(r1, b, h1))))
1081    case 1n+s 1n+t:
1082      un.dmu.s(s, t, r1, r2, un.dmu(b, s, r1, t, r2, Laws.nat_add_cancel(b, Nat.add(Nat.mul(s, b), r1), Nat.add(Nat.mul(t, b), r2), Equal.trans(Nat, Nat.add(b, Nat.add(Nat.mul(s, b), r1)), Nat.add(Nat.mul(1n+t, b), r2), Nat.add(b, Nat.add(Nat.mul(t, b), r2)), Equal.trans(Nat, Nat.add(b, Nat.add(Nat.mul(s, b), r1)), Nat.add(Nat.mul(1n+s, b), r1), Nat.add(Nat.mul(1n+t, b), r2), ur.r1(b, s, r1), e), ur.r2(t, b, r2))), h1, h2))
1083    case 1n+s 0n:
1084      Empty.absurd({1n+s == 0n : Nat} & {r1 == r2 : Nat}, Laws.nat_succ_add_absurd(Nat.add(Nat.sub(b, 1n+r2), Nat.add(Nat.mul(s, b), r1)), b, Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(b, 1n+r2), Nat.add(Nat.mul(s, b), r1)), 1n+b), Nat.add(Nat.sub(b, 1n+r2), 1n+r2), b, Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(b, 1n+r2), Nat.add(Nat.mul(s, b), r1)), 1n+b), Nat.add(Nat.sub(b, 1n+r2), 1n+Nat.add(Nat.mul(0n, b), r2)), Nat.add(Nat.sub(b, 1n+r2), 1n+r2), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(b, 1n+r2), Nat.add(Nat.mul(s, b), r1)), 1n+b), Nat.add(Nat.sub(b, 1n+r2), 1n+Nat.add(Nat.mul(1n+s, b), r1)), Nat.add(Nat.sub(b, 1n+r2), 1n+Nat.add(Nat.mul(0n, b), r2)), ur.r0(Nat.sub(b, 1n+r2), s, b, r1), Equal.cong(Nat, Nat, zz => Nat.add(Nat.sub(b, 1n+r2), 1n+zz), Nat.add(Nat.mul(1n+s, b), r1), Nat.add(Nat.mul(0n, b), r2), e)), {==}), Laws.nat_lt_witness(r2, b, h2))))