def ud.dm_sum
bend-osdev-u32@0.1.0.0 · PROOF_div.bend:74
import bend-osdev-u32@0.1.0.0/PROOF_div.bend as PROOFDiv
import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
74def ud.dm_sum(+n: Nat, +m: Nat, +d: Nat, +r: Nat, +bp: Nat) -> {Nat.add(m, r) == bp : Nat} -> {ud.dm_lhs(n, m, d, r, bp) == Nat.add(n, Nat.add(Nat.mul(d, 1n+bp), r)) : Nat}:
75 match n m:
76 case 0n _:
77 h => {==}
78 case 1n+np 0n:
79 +h =>
80 +dd = Nat.mul(d, 1n+bp)
81 +x = Nat.add(Nat.add(bp, dd), 0n)
82 %Equal.sym(Nat, r, bp, h) : {ud.dm_lhs(1n+np, 0n, d, r, bp) == 1n+Nat.add(np, Nat.add(dd, _)) : Nat}
83 %UL.nat_add_comm(bp, dd) : {ud.dm_lhs(1n+np, 0n, d, r, bp) == 1n+Nat.add(np, _) : Nat}
84 %UL.nat_add_zero(Nat.add(bp, dd)) : {ud.dm_lhs(1n+np, 0n, d, r, bp) == 1n+Nat.add(np, _) : Nat}
85 %UL.nat_add_succ(np, x) : {ud.dm_lhs(1n+np, 0n, d, r, bp) == _ : Nat}
86 ud.dm_sum(np, r, 1n+d, 0n, bp, Equal.trans(Nat, Nat.add(r, 0n), r, bp, UL.nat_add_zero(r), h))
87 case 1n+np 1n+mp:
88 h =>
89 +dd = Nat.mul(d, 1n+bp)
90 %UL.nat_add_succ(np, Nat.add(dd, r)) : {ud.dm_lhs(1n+np, 1n+mp, d, r, bp) == _ : Nat}
91 %UL.nat_add_succ(dd, r) : {ud.dm_lhs(1n+np, 1n+mp, d, r, bp) == Nat.add(np, _) : Nat}
92 ud.dm_sum(np, mp, d, 1n+r, bp, Equal.trans(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), bp, UL.nat_add_succ(mp, r), h))