Xbits.or_le: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as Xbits
Lines 122-132 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend&start_line=122&end_line=132

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as SN
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M

def or_le(+n: Nat, +x: Word(n), +m: Word(n)) -> {Nat.is_le(WD.uw(n, Word.or(n, x, m)), Nat.add(WD.uw(n, x), WD.uw(n, m))) == True{} : Bool}:
  match n x m:
    case 0n WNil{} WNil{}:
      {==}
    case 1n+ +p WCon{+a, +t1} WCon{+b, +t2}:
      +u1 = WD.uw(p, t1)
      +u2 = WD.uw(p, t2)
      +d1 = N.double_le(WD.uw(p, Word.or(p, t1, t2)), Nat.add(u1, u2), or_le(p, t1, t2))
      +d2 = L.subst(Nat, z => {Nat.is_le(Nat.double(WD.uw(p, Word.or(p, t1, t2))), z) == True{} : Bool}, Nat.double(Nat.add(u1, u2)), Nat.add(Nat.double(u1), Nat.double(u2)), NA.double_add(u1, u2), d1)
      +s = M.le_add2(SN.bit_value(Bool.or(a, b)), Nat.double(WD.uw(p, Word.or(p, t1, t2))), Nat.add(SN.bit_value(a), SN.bit_value(b)), Nat.add(Nat.double(u1), Nat.double(u2)), bit_or_le(a, b), d2)
      L.subst(Nat, z => {Nat.is_le(Nat.add(SN.bit_value(Bool.or(a, b)), Nat.double(WD.uw(p, Word.or(p, t1, t2)))), z) == True{} : Bool}, Nat.add(Nat.add(SN.bit_value(a), SN.bit_value(b)), Nat.add(Nat.double(u1), Nat.double(u2))), Nat.add(Nat.add(SN.bit_value(a), Nat.double(u1)), Nat.add(SN.bit_value(b), Nat.double(u2))), M.add4(SN.bit_value(a), SN.bit_value(b), Nat.double(u1), Nat.double(u2)), s)

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  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_le
  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=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=add4
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=le_add2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend&name=bit_or_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=double_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=bit_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=double_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=uw