ProofShift.ws.or_dis: def of bend-osdev-word64@0.1.1.0 Import: import bend-osdev-word64@0.1.1.0/proof_shift.bend as ProofShift Lines 345-367 of bend-osdev-word64@0.1.1.0/proof_shift.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&start_line=345&end_line=367 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 # x's value a multiple of 2^k and y's below 2^k: or(x, y) is x + y def ws.or_dis(n: Nat, k: Nat, +x: Word(n), +y: Word(n), +q: Nat, ex: {Word.to_nat(n, x) == U.U32Nat.dbl(k, q) : Nat}, hy: {Nat.is_lt(Word.to_nat(n, y), U.U32Nat.dbl(k, 1n)) == True{} : Bool}) -> {Word.to_nat(n, Word.or(n, x, y)) == Nat.add(Word.to_nat(n, x), Word.to_nat(n, y)) : Nat}: match n: case 0n: match x y: case WNil{} WNil{}: {==} case 1n+ +p: match k: case 0n: +y0 = ns.lt_one(Word.to_nat(1n+p, y), hy) +ey = UL.word_value_eq(1n+p, y, Word.zero(1n+p), Equal.trans(Nat, Word.to_nat(1n+p, y), 0n, Word.to_nat(1n+p, Word.zero(1n+p)), y0, Equal.sym(Nat, Word.to_nat(1n+p, Word.zero(1n+p)), 0n, UL.word_zero_value(1n+p)))) Equal.trans(Nat, Word.to_nat(1n+p, Word.or(1n+p, x, y)), Word.to_nat(1n+p, Word.or(1n+p, x, Word.zero(1n+p))), Nat.add(Word.to_nat(1n+p, x), Word.to_nat(1n+p, y)), Equal.cong(Word(1n+p), Nat, v => Word.to_nat(1n+p, Word.or(1n+p, x, v)), y, Word.zero(1n+p), ey), Equal.trans(Nat, Word.to_nat(1n+p, Word.or(1n+p, x, Word.zero(1n+p))), Word.to_nat(1n+p, x), Nat.add(Word.to_nat(1n+p, x), Word.to_nat(1n+p, y)), Equal.cong(Word(1n+p), Nat, v => Word.to_nat(1n+p, v), Word.or(1n+p, x, Word.zero(1n+p)), x, ws.or_zero(1n+p, x)), Equal.trans(Nat, Word.to_nat(1n+p, x), Nat.add(Word.to_nat(1n+p, x), 0n), Nat.add(Word.to_nat(1n+p, x), Word.to_nat(1n+p, y)), Equal.sym(Nat, Nat.add(Word.to_nat(1n+p, x), 0n), Word.to_nat(1n+p, x), UL.nat_add_zero(Word.to_nat(1n+p, x))), Equal.cong(Nat, Nat, v => Nat.add(Word.to_nat(1n+p, x), v), 0n, Word.to_nat(1n+p, y), Equal.sym(Nat, Word.to_nat(1n+p, y), 0n, y0))))) case 1n+ +j: match x y: case WCon{False{}, +xt} WCon{False{}, +yt}: Equal.trans(Nat, Nat.double(Word.to_nat(p, Word.or(p, xt, yt))), Nat.double(Nat.add(Word.to_nat(p, xt), Word.to_nat(p, yt))), Nat.add(Nat.double(Word.to_nat(p, xt)), Nat.double(Word.to_nat(p, yt))), Equal.cong(Nat, Nat, v => Nat.double(v), Word.to_nat(p, Word.or(p, xt, yt)), Nat.add(Word.to_nat(p, xt), Word.to_nat(p, yt)), ws.or_dis(p, j, xt, yt, q, ns.double_inj(Word.to_nat(p, xt), U.U32Nat.dbl(j, q), ex), Equal.trans(Bool, Nat.is_lt(Word.to_nat(p, yt), U.U32Nat.dbl(j, 1n)), Nat.is_lt(Nat.double(Word.to_nat(p, yt)), Nat.double(U.U32Nat.dbl(j, 1n))), True{}, Equal.sym(Bool, Nat.is_lt(Nat.double(Word.to_nat(p, yt)), Nat.double(U.U32Nat.dbl(j, 1n))), Nat.is_lt(Word.to_nat(p, yt), U.U32Nat.dbl(j, 1n)), ns.lt_dbl(Word.to_nat(p, yt), U.U32Nat.dbl(j, 1n))), hy))), ns.double_add(Word.to_nat(p, xt), Word.to_nat(p, yt))) case WCon{False{}, +xt} WCon{True{}, +yt}: Equal.trans(Nat, 1n+Nat.double(Word.to_nat(p, Word.or(p, xt, yt))), 1n+Nat.add(Nat.double(Word.to_nat(p, xt)), Nat.double(Word.to_nat(p, yt))), Nat.add(Nat.double(Word.to_nat(p, xt)), 1n+Nat.double(Word.to_nat(p, yt))), P.wn.succ_cong(Nat.double(Word.to_nat(p, Word.or(p, xt, yt))), Nat.add(Nat.double(Word.to_nat(p, xt)), Nat.double(Word.to_nat(p, yt))), Equal.trans(Nat, Nat.double(Word.to_nat(p, Word.or(p, xt, yt))), Nat.double(Nat.add(Word.to_nat(p, xt), Word.to_nat(p, yt))), Nat.add(Nat.double(Word.to_nat(p, xt)), Nat.double(Word.to_nat(p, yt))), Equal.cong(Nat, Nat, v => Nat.double(v), Word.to_nat(p, Word.or(p, xt, yt)), Nat.add(Word.to_nat(p, xt), Word.to_nat(p, yt)), ws.or_dis(p, j, xt, yt, q, ns.double_inj(Word.to_nat(p, xt), U.U32Nat.dbl(j, q), ex), Equal.trans(Bool, Nat.is_lt(Word.to_nat(p, yt), U.U32Nat.dbl(j, 1n)), Nat.is_lt(1n+Nat.double(Word.to_nat(p, yt)), Nat.double(U.U32Nat.dbl(j, 1n))), True{}, Equal.sym(Bool, Nat.is_lt(1n+Nat.double(Word.to_nat(p, yt)), Nat.double(U.U32Nat.dbl(j, 1n))), Nat.is_lt(Word.to_nat(p, yt), U.U32Nat.dbl(j, 1n)), ns.lt_dbl1(Word.to_nat(p, yt), U.U32Nat.dbl(j, 1n))), hy))), ns.double_add(Word.to_nat(p, xt), Word.to_nat(p, yt)))), Equal.sym(Nat, Nat.add(Nat.double(Word.to_nat(p, xt)), 1n+Nat.double(Word.to_nat(p, yt))), 1n+Nat.add(Nat.double(Word.to_nat(p, xt)), Nat.double(Word.to_nat(p, yt))), UL.nat_add_succ(Nat.double(Word.to_nat(p, xt)), Nat.double(Word.to_nat(p, yt))))) case WCon{True{}, +xt} WCon{False{}, +yt}: Empty.absurd({Word.to_nat(1n+p, Word.or(1n+p, WCon{True{}, xt}, WCon{False{}, yt})) == Nat.add(Word.to_nat(1n+p, WCon{True{}, xt}), Word.to_nat(1n+p, WCon{False{}, yt})) : Nat}, ns.odd_even(Word.to_nat(p, xt), U.U32Nat.dbl(j, q), ex)) case WCon{True{}, +xt} WCon{True{}, +yt}: Empty.absurd({Word.to_nat(1n+p, Word.or(1n+p, WCon{True{}, xt}, WCon{True{}, yt})) == Nat.add(Word.to_nat(1n+p, WCon{True{}, xt}), Word.to_nat(1n+p, WCon{True{}, yt})) : Nat}, ns.odd_even(Word.to_nat(p, xt), U.U32Nat.dbl(j, q), ex)) Uses (28): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd 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.sym 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.double https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.or https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_succ https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_zero https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_value_eq https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_zero_value 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-word64@0.1.1.0/proof_shift.bend&name=ns.double_add https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ns.double_inj https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ns.lt_dbl https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ns.lt_dbl1 https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ns.lt_one https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ns.odd_even https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_shift.bend&name=ws.or_zero https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.succ_cong