def ud.k
bend-osdev-u32@0.1.0.0 · PROOF.bend:1682
import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
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 Laws
1682
1683def ud.k(+N: Nat, +S: Nat, +B: Nat, +R: Nat, +A: Nat, +R1: Nat, +T: Bool, +L: Bool, +g: Bool, +eput: {Nat.add(S, U.U32Nat.dbl(N, U.U32Nat.bit(T))) == Nat.add(A, Nat.double(R)) : Nat}, +eL: {Nat.is_lt(S, B) == L : Bool}, +eg: {Bool.or(T, Bool.not(L)) == g : Bool}, +er1: {Nat.add(R1, Nat.mul(U.U32Nat.bit(g), B)) == Nat.add(S, U.U32Nat.dbl(N, Nat.mul(U.U32Nat.bit(g), U.U32Nat.bit(L)))) : Nat}, +hA: {Nat.is_le(A, 1n) == True{} : Bool}, +hR: {Nat.is_lt(R, B) == True{} : Bool}, +hB: {Nat.is_lt(B, U.U32Nat.dbl(N, 1n)) == True{} : Bool}) -> {Nat.add(R1, Nat.mul(U.U32Nat.bit(g), B)) == Nat.add(A, Nat.double(R)) : Nat} & {Nat.is_lt(R1, B) == True{} : Bool}:
1684 match T L g:
1685 case True{} True{} True{}:
1686 (Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, 1n)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, Nat.mul(1n, 1n))), Nat.add(S, U.U32Nat.dbl(N, 1n)), er1, Equal.cong(Nat, Nat, zz => Nat.add(S, U.U32Nat.dbl(N, zz)), Nat.mul(1n, 1n), 1n, ur.r21())), eput), Equal.trans(Bool, Nat.is_lt(R1, B), Nat.is_lt(R1, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), True{}, Equal.sym(Bool, Nat.is_lt(R1, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.is_lt(R1, B), Equal.cong(Nat, Bool, zz => Nat.is_lt(R1, zz), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1), B, Laws.nat_add_cancel(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1), B, Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.double(B), Nat.add(B, B), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.double(Nat.add(Nat.sub(B, 1n+R), 1n+R)), Nat.double(B), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), 1n), Nat.double(Nat.add(Nat.sub(B, 1n+R), 1n+R)), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), Nat.add(Nat.sub(1n, A), A)), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), 1n), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), Nat.add(A, Nat.double(R))), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), Nat.add(Nat.sub(1n, A), A)), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), Nat.add(R1, Nat.mul(1n, B))), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), Nat.add(A, Nat.double(R))), ur.r29(B, Nat.sub(B, 1n+R), Nat.sub(1n, A), R1), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), zz), Nat.add(R1, Nat.mul(1n, B)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, 1n)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, Nat.mul(1n, 1n))), Nat.add(S, U.U32Nat.dbl(N, 1n)), er1, Equal.cong(Nat, Nat, zz => Nat.add(S, U.U32Nat.dbl(N, zz)), Nat.mul(1n, 1n), 1n, ur.r21())), eput))), ur.r30(Nat.sub(B, 1n+R), Nat.sub(1n, A), A, R)), Equal.cong(Nat, Nat, zz => Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), zz), Nat.add(Nat.sub(1n, A), A), 1n, Laws.nat_le_witness(A, 1n, hA))), ur.r7(Nat.sub(B, 1n+R), R)), Equal.cong(Nat, Nat, zz => Nat.double(zz), Nat.add(Nat.sub(B, 1n+R), 1n+R), B, Laws.nat_lt_witness(R, B, hR))), ur.r31(B))))), Laws.nat_lt_add(R1, Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)))))
1687 case True{} False{} True{}:
1688 Empty.absurd({Nat.add(R1, Nat.mul(U.U32Nat.bit(True{}), B)) == Nat.add(A, Nat.double(R)) : Nat} & {Nat.is_lt(R1, B) == True{} : Bool}, Laws.nat_succ_add_absurd(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), 1n+Nat.add(A, Nat.double(R))), Nat.add(S, U.U32Nat.dbl(N, 1n)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), 1n+Nat.add(A, Nat.double(R))), Nat.add(S, Nat.add(Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), 1n+B)), Nat.add(S, U.U32Nat.dbl(N, 1n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), 1n+Nat.add(A, Nat.double(R))), Nat.add(Nat.add(Nat.sub(S, B), B), Nat.add(Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), 1n+B)), Nat.add(S, Nat.add(Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), 1n+B)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), 1n+Nat.add(A, Nat.double(R))), Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 1n+Nat.double(B)), Nat.add(Nat.add(Nat.sub(S, B), B), Nat.add(Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), 1n+B)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), 1n+Nat.add(A, Nat.double(R))), Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), 1n+R))), Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 1n+Nat.double(B)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), 1n+Nat.add(A, Nat.double(R))), Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 2n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R))), 1n), Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), 1n+R))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A))), 1n+Nat.add(A, Nat.double(R))), Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 2n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R))), Nat.add(Nat.sub(1n, A), A)), Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 2n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R))), 1n), ur.r26(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), Nat.sub(B, 1n+R), Nat.sub(1n, A), A, R), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 2n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R))), zz), Nat.add(Nat.sub(1n, A), A), 1n, Laws.nat_le_witness(A, 1n, hA))), ur.r27(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), Nat.sub(B, 1n+R), R)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B)), 1n+Nat.double(zz)), Nat.add(Nat.sub(B, 1n+R), 1n+R), B, Laws.nat_lt_witness(R, B, hR))), ur.r28(Nat.sub(S, B), Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), B)), Equal.cong(Nat, Nat, zz => Nat.add(zz, Nat.add(Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), 1n+B)), Nat.add(Nat.sub(S, B), B), S, Laws.nat_le_witness(B, S, un.nlt_le(S, B, eL)))), Equal.cong(Nat, Nat, zz => Nat.add(S, zz), Nat.add(Nat.sub(U.U32Nat.dbl(N, 1n), 1n+B), 1n+B), U.U32Nat.dbl(N, 1n), Laws.nat_lt_witness(B, U.U32Nat.dbl(N, 1n), hB))), eput)))
1689 case False{} False{} True{}:
1690 (Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, 0n)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, Nat.mul(1n, 0n))), Nat.add(S, U.U32Nat.dbl(N, 0n)), er1, Equal.cong(Nat, Nat, zz => Nat.add(S, U.U32Nat.dbl(N, zz)), Nat.mul(1n, 0n), 0n, ur.r22())), eput), Equal.trans(Bool, Nat.is_lt(R1, B), Nat.is_lt(R1, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), True{}, Equal.sym(Bool, Nat.is_lt(R1, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.is_lt(R1, B), Equal.cong(Nat, Bool, zz => Nat.is_lt(R1, zz), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1), B, Laws.nat_add_cancel(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1), B, Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.double(B), Nat.add(B, B), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.double(Nat.add(Nat.sub(B, 1n+R), 1n+R)), Nat.double(B), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), 1n), Nat.double(Nat.add(Nat.sub(B, 1n+R), 1n+R)), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), Nat.add(Nat.sub(1n, A), A)), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), 1n), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), Nat.add(A, Nat.double(R))), Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), Nat.add(Nat.sub(1n, A), A)), Equal.trans(Nat, Nat.add(B, Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)), 1n+R1)), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), Nat.add(R1, Nat.mul(1n, B))), Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), Nat.add(A, Nat.double(R))), ur.r29(B, Nat.sub(B, 1n+R), Nat.sub(1n, A), R1), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(Nat.double(Nat.sub(B, 1n+R)), 1n+Nat.sub(1n, A)), zz), Nat.add(R1, Nat.mul(1n, B)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, 0n)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(R1, Nat.mul(1n, B)), Nat.add(S, U.U32Nat.dbl(N, Nat.mul(1n, 0n))), Nat.add(S, U.U32Nat.dbl(N, 0n)), er1, Equal.cong(Nat, Nat, zz => Nat.add(S, U.U32Nat.dbl(N, zz)), Nat.mul(1n, 0n), 0n, ur.r22())), eput))), ur.r30(Nat.sub(B, 1n+R), Nat.sub(1n, A), A, R)), Equal.cong(Nat, Nat, zz => Nat.add(1n+Nat.double(Nat.add(Nat.sub(B, 1n+R), R)), zz), Nat.add(Nat.sub(1n, A), A), 1n, Laws.nat_le_witness(A, 1n, hA))), ur.r7(Nat.sub(B, 1n+R), R)), Equal.cong(Nat, Nat, zz => Nat.double(zz), Nat.add(Nat.sub(B, 1n+R), 1n+R), B, Laws.nat_lt_witness(R, B, hR))), ur.r31(B))))), Laws.nat_lt_add(R1, Nat.add(Nat.double(Nat.sub(B, 1n+R)), Nat.sub(1n, A)))))
1691 case False{} True{} False{}:
1692 (Equal.trans(Nat, Nat.add(R1, Nat.mul(0n, B)), Nat.add(S, U.U32Nat.dbl(N, 0n)), Nat.add(A, Nat.double(R)), Equal.trans(Nat, Nat.add(R1, Nat.mul(0n, B)), Nat.add(S, U.U32Nat.dbl(N, Nat.mul(0n, 1n))), Nat.add(S, U.U32Nat.dbl(N, 0n)), er1, Equal.cong(Nat, Nat, zz => Nat.add(S, U.U32Nat.dbl(N, zz)), Nat.mul(0n, 1n), 0n, ur.r23())), eput), Equal.trans(Bool, Nat.is_lt(R1, B), Nat.is_lt(S, B), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(zz, B), R1, S, Equal.trans(Nat, R1, Nat.add(S, U.U32Nat.dbl(N, Nat.mul(0n, 1n))), S, Equal.trans(Nat, R1, Nat.add(R1, Nat.mul(0n, B)), Nat.add(S, U.U32Nat.dbl(N, Nat.mul(0n, 1n))), ur.r24(R1, B), er1), ur.r25(S, N))), eL))
1693 case True{} _ False{}:
1694 Empty.absurd({Nat.add(R1, Nat.mul(U.U32Nat.bit(False{}), B)) == Nat.add(A, Nat.double(R)) : Nat} & {Nat.is_lt(R1, B) == True{} : Bool}, un.tf(eg))
1695 case False{} False{} False{}:
1696 Empty.absurd({Nat.add(R1, Nat.mul(U.U32Nat.bit(False{}), B)) == Nat.add(A, Nat.double(R)) : Nat} & {Nat.is_lt(R1, B) == True{} : Bool}, un.tf(eg))
1697 case False{} True{} True{}:
1698 Empty.absurd({Nat.add(R1, Nat.mul(U.U32Nat.bit(True{}), B)) == Nat.add(A, Nat.double(R)) : Nat} & {Nat.is_lt(R1, B) == True{} : Bool}, un.ft(eg))