def zc_t

bend-collections-laws-math@1.0.0.0 · proofs/math/number/fixprime.bend:35

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as SF
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

35def zc_t(+one: Nat, +h1: {one == 1n : Nat}, +r: Nat, +x: Nat, +e: {Nat.add(r, C.shift(32n, one)) == Nat.add(x, 1n) : Nat}, +hx: {C.fits(32n, x) == True{} : Bool}) -> {SF.bn(Nat.is_eq(r, 0n)) == one : Nat}:
36  match r:
37    case 0n:
38      Equal.sym(Nat, one, 1n, h1)
39    case 1n+ +rp:
40      +S = C.shift(32n, one)
41      +e1 = Equal.trans(Nat, 1n+Nat.add(rp, S), Nat.add(x, 1n), 1n+x, e, N.add_comm(x, 1n))
42      +e2 = N.succ_inj(Nat.add(rp, S), x, e1)
43      +hl = Equal.trans(Bool, Nat.is_lt(Nat.add(rp, S), S), Nat.is_lt(x, S), True{}, Equal.cong(Nat, Bool, t => Nat.is_lt(t, S), Nat.add(rp, S), x, e2), WW.lt_one(32n, one, h1, x, hx))
44      +hg = Equal.trans(Bool, Nat.is_le(S, Nat.add(rp, S)), Nat.is_le(S, Nat.add(S, rp)), True{}, Equal.cong(Nat, Bool, t => Nat.is_le(S, t), Nat.add(rp, S), Nat.add(S, rp), N.add_comm(rp, S)), N.le_add_right(S, rp))
45      Empty.absurd({SF.bn(Nat.is_eq(1n+rp, 0n)) == one : Nat}, L.true_false(Equal.trans(Bool, True{}, Nat.is_le(S, Nat.add(rp, S)), False{}, Equal.sym(Bool, Nat.is_le(S, Nat.add(rp, S)), True{}, hg), N.lt_not_le(Nat.add(rp, S), S, hl))))