def ws.uniq

bend-osdev-word64@0.1.1.0 · proof_shift.bend:299

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
import bend-osdev-word64@0.1.1.0/proof_value.bend as P
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO

299# x, y < 2^n and x + 2^n p = y + 2^n q: x = y
300def ws.uniq(+n: Nat, p: Nat, q: Nat, +x: Nat, +y: Nat, e: {Nat.add(x, U.U32Nat.dbl(n, p)) == Nat.add(y, U.U32Nat.dbl(n, q)) : Nat}, hx: {Nat.is_lt(x, U.U32Nat.dbl(n, 1n)) == True{} : Bool}, hy: {Nat.is_lt(y, U.U32Nat.dbl(n, 1n)) == True{} : Bool}) -> {x == y : Nat}:
301  match p q:
302    case 0n 0n:
303      Equal.trans(Nat, x, Nat.add(x, U.U32Nat.dbl(n, 0n)), y, Equal.sym(Nat, Nat.add(x, U.U32Nat.dbl(n, 0n)), x, ns.d0(n, x)), Equal.trans(Nat, Nat.add(x, U.U32Nat.dbl(n, 0n)), Nat.add(y, U.U32Nat.dbl(n, 0n)), y, e, ns.d0(n, y)))
304    case 0n 1n+ +q:
305      Empty.absurd({x == y : Nat}, P.wn.lt_irrefl(x, P.wn.lt_rw2(x, Nat.add(y, U.U32Nat.dbl(n, 1n+q)), x, Equal.trans(Nat, Nat.add(y, U.U32Nat.dbl(n, 1n+q)), Nat.add(x, U.U32Nat.dbl(n, 0n)), x, Equal.sym(Nat, Nat.add(x, U.U32Nat.dbl(n, 0n)), Nat.add(y, U.U32Nat.dbl(n, 1n+q)), e), ns.d0(n, x)), UO.nat_lt_le_trans(x, U.U32Nat.dbl(n, 1n+q), Nat.add(y, U.U32Nat.dbl(n, 1n+q)), UO.nat_lt_le_trans(x, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n+q), hx, Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n+q)), Nat.is_le(1n, 1n+q), True{}, UL.dbl_le(n, 1n, 1n+q), P.wn.le_zero(q))), UL.nat_le_add(U.U32Nat.dbl(n, 1n+q), y)))))
306    case 1n+ +p 0n:
307      Empty.absurd({x == y : Nat}, P.wn.lt_irrefl(y, P.wn.lt_rw2(y, Nat.add(x, U.U32Nat.dbl(n, 1n+p)), y, Equal.trans(Nat, Nat.add(x, U.U32Nat.dbl(n, 1n+p)), Nat.add(y, U.U32Nat.dbl(n, 0n)), y, e, ns.d0(n, y)), UO.nat_lt_le_trans(y, U.U32Nat.dbl(n, 1n+p), Nat.add(x, U.U32Nat.dbl(n, 1n+p)), UO.nat_lt_le_trans(y, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n+p), hy, Equal.trans(Bool, Nat.is_le(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, 1n+p)), Nat.is_le(1n, 1n+p), True{}, UL.dbl_le(n, 1n, 1n+p), P.wn.le_zero(p))), UL.nat_le_add(U.U32Nat.dbl(n, 1n+p), x)))))
308    case 1n+ +p 1n+ +q:
309      ws.uniq(n, p, q, x, y, UL.nat_add_cancel(U.U32Nat.dbl(n, 1n), Nat.add(x, U.U32Nat.dbl(n, p)), Nat.add(y, U.U32Nat.dbl(n, q)), Equal.trans(Nat, Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(x, U.U32Nat.dbl(n, p))), Nat.add(x, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(y, U.U32Nat.dbl(n, q))), UL.nat_add_left_comm(U.U32Nat.dbl(n, 1n), x, U.U32Nat.dbl(n, p)), Equal.trans(Nat, Nat.add(x, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p))), Nat.add(x, U.U32Nat.dbl(n, 1n+p)), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(y, U.U32Nat.dbl(n, q))), Equal.cong(Nat, Nat, v => Nat.add(x, v), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p)), U.U32Nat.dbl(n, 1n+p), Equal.sym(Nat, U.U32Nat.dbl(n, 1n+p), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, p)), UL.dbl_add(n, 1n, p))), Equal.trans(Nat, Nat.add(x, U.U32Nat.dbl(n, 1n+p)), Nat.add(y, U.U32Nat.dbl(n, 1n+q)), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(y, U.U32Nat.dbl(n, q))), e, Equal.trans(Nat, Nat.add(y, U.U32Nat.dbl(n, 1n+q)), Nat.add(y, Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q))), Nat.add(U.U32Nat.dbl(n, 1n), Nat.add(y, U.U32Nat.dbl(n, q))), Equal.cong(Nat, Nat, v => Nat.add(y, v), U.U32Nat.dbl(n, 1n+q), Nat.add(U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q)), UL.dbl_add(n, 1n, q)), UL.nat_add_left_comm(y, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(n, q))))))), hx, hy)