def or_split.s

lawful-words@0.1.0.0 · proof_word.bend:1125

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

1125def or_split.s(+p: Nat, +x: Bool, +y: Bool, +at: Word(p), +bt: Word(p), +j: Nat,
1126  ha: {Nat.mod(Word.to_nat(1n+p, WCon{x, at}), Nat.pow(2n, 1n+j)) == 0n : Nat},
1127  hb: {Nat.is_lt(Word.to_nat(1n+p, WCon{y, bt}), Nat.pow(2n, 1n+j)) == True{} : Bool},
1128  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} ->
1129    {Word.to_nat(p, Word.or(p, at, bt)) == Nat.add(Word.to_nat(p, at), Word.to_nat(p, bt)) : Nat}) ->
1130  {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}:
1131  match x y:
1132    case True{} _:
1133      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},
1134        N.succ_ne_zero(Nat.double(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j))),
1135          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,
1136            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)),
1137            ha)))
1138    case False{} False{}:
1139      split_step(False{}, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.or(p, at, bt)),
1140        ih(N.dbl_zero(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)),
1141          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,
1142            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)),
1143            ha)))(lt_w(p, False{}, bt, j, hb)))
1144    case False{} True{}:
1145      split_step(True{}, Word.to_nat(p, at), Word.to_nat(p, bt), Word.to_nat(p, Word.or(p, at, bt)),
1146        ih(N.dbl_zero(Nat.mod(Word.to_nat(p, at), Nat.pow(2n, j)),
1147          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,
1148            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)),
1149            ha)))(lt_w(p, True{}, bt, j, hb)))