ProofWord.or_split.s: def of lawful-words@0.1.0.0
Import: import lawful-words@0.1.0.0/proof_word.bend as ProofWord
Lines 1125-1149 of lawful-words@0.1.0.0/proof_word.bend: https://jend.leeeet.dev/read.txt?path=lawful-words@0.1.0.0/proof_word.bend&start_line=1125&end_line=1149

import Base
import lawful-words@0.1.0.0/proof_nat.bend as N

def or_split.s(+p: Nat, +x: Bool, +y: Bool, +at: Word(p), +bt: Word(p), +j: Nat,
  ha: {Nat.mod(Word.to_nat(1n+p, WCon{x, at}), Nat.pow(2n, 1n+j)) == 0n : Nat},
  hb: {Nat.is_lt(Word.to_nat(1n+p, WCon{y, bt}), Nat.pow(2n, 1n+j)) == True{} : Bool},
  ih: {Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)) == 0n : Nat} -> {Nat.is_lt(Word.to_nat(p, bt), Nat.pow(2n, j)) == True{} : Bool} ->
    {Word.to_nat(p, Word.or(p, at, bt)) == Nat.add(Word.to_nat(p, at), Word.to_nat(p, bt)) : Nat}) ->
  {Word.to_nat(1n+p, Word.or(1n+p, WCon{x, at}, WCon{y, bt})) == Nat.add(Word.to_nat(1n+p, WCon{x, at}), Word.to_nat(1n+p, WCon{y, bt})) : Nat}:
  match x y:
    case True{} _:
      Empty.absurd({Word.to_nat(1n+p, Word.or(1n+p, WCon{True{}, at}, WCon{y, bt})) == Nat.add(Word.to_nat(1n+p, WCon{True{}, at}), Word.to_nat(1n+p, WCon{y, bt})) : Nat},
        N.succ_ne_zero(Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))),
          Equal.trans(Nat, 1n+Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{True{}, at}), Nat.pow(2n, 1n+j)), 0n,
            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{True{}, at}), Nat.pow(2n, 1n+j)), 1n+Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, True{}, at, j)),
            ha)))
    case False{} False{}:
      split_step(False{}, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.or(p, at, bt)),
        ih(N.dbl_zero(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)),
          Equal.trans(Nat, Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), 0n,
            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, False{}, at, j)),
            ha)))(lt_w(p, False{}, bt, j, hb)))
    case False{} True{}:
      split_step(True{}, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.or(p, at, bt)),
        ih(N.dbl_zero(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)),
          Equal.trans(Nat, Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), 0n,
            Equal.sym(Nat, Nat.mod(Word.to_nat(1n+p, WCon{False{}, at}), Nat.pow(2n, 1n+j)), Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))), moddbl_w(p, False{}, at, j)),
            ha)))(lt_w(p, True{}, bt, j, hb)))

Uses (19):
  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.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=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow
  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.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=dbl_zero
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_nat.bend&name=succ_ne_zero
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_word.bend&name=lt_w
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_word.bend&name=moddbl_w
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/proof_word.bend&name=split_step