~/jendhub

proofs/math/typed/f64addp.bend

bend-collections-laws-math@1.0.0.0 · 97 lines · 9 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
4import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
5import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
6import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
7import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
8import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
9import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A
10import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
11import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
14
15# The sticky bit under addition and subtraction of an even term: SoftFloat's
16# addMagsF64/subMagsF64 add or subtract the jammed smaller operand, which is
17# the jam of the exact sum or difference (the bits below the guard bits
18# never meet the even larger operand).
19
20def jam_add(+t: Nat, +h: Nat, +l: Nat) -> {SW.jam(Nat.add(h, Nat.double(t)), l) == Nat.add(SW.jam(h, l), Nat.double(t)) : Nat}:
21  +mn = Nat.min(l, 1n)
22  +q = Nat.add(h, Nat.double(t))
23  Equal.trans(Nat, SW.jam(q, l), Nat.add(Nat.max(C.bit(q), mn), Nat.double(C.half(q))), Nat.add(SW.jam(h, l), Nat.double(t)), FR.jam_form(q, l), Equal.trans(Nat, Nat.add(Nat.max(C.bit(q), mn), Nat.double(C.half(q))), Nat.add(Nat.max(C.bit(h), mn), Nat.double(C.half(q))), Nat.add(SW.jam(h, l), Nat.double(t)), Equal.cong(Nat, Nat, z => Nat.add(Nat.max(z, mn), Nat.double(C.half(q))), C.bit(q), C.bit(h), WW.bit_dbl(h, t)), Equal.trans(Nat, Nat.add(Nat.max(C.bit(h), mn), Nat.double(C.half(q))), Nat.add(Nat.max(C.bit(h), mn), Nat.double(Nat.add(C.half(h), t))), Nat.add(SW.jam(h, l), Nat.double(t)), Equal.cong(Nat, Nat, z => Nat.add(Nat.max(C.bit(h), mn), Nat.double(z)), C.half(q), Nat.add(C.half(h), t), WW.half_dbl(h, t)), Equal.trans(Nat, Nat.add(Nat.max(C.bit(h), mn), Nat.double(Nat.add(C.half(h), t))), Nat.add(Nat.max(C.bit(h), mn), Nat.add(Nat.double(C.half(h)), Nat.double(t))), Nat.add(SW.jam(h, l), Nat.double(t)), Equal.cong(Nat, Nat, z => Nat.add(Nat.max(C.bit(h), mn), z), Nat.double(Nat.add(C.half(h), t)), Nat.add(Nat.double(C.half(h)), Nat.double(t)), NA.double_add(C.half(h), t)), Equal.trans(Nat, Nat.add(Nat.max(C.bit(h), mn), Nat.add(Nat.double(C.half(h)), Nat.double(t))), Nat.add(Nat.add(Nat.max(C.bit(h), mn), Nat.double(C.half(h))), Nat.double(t)), Nat.add(SW.jam(h, l), Nat.double(t)), Equal.sym(Nat, Nat.add(Nat.add(Nat.max(C.bit(h), mn), Nat.double(C.half(h))), Nat.double(t)), Nat.add(Nat.max(C.bit(h), mn), Nat.add(Nat.double(C.half(h)), Nat.double(t))), NA.add_assoc(Nat.max(C.bit(h), mn), Nat.double(C.half(h)), Nat.double(t))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.double(t)), Nat.add(Nat.max(C.bit(h), mn), Nat.double(C.half(h))), SW.jam(h, l), Equal.sym(Nat, SW.jam(h, l), Nat.add(Nat.max(C.bit(h), mn), Nat.double(C.half(h))), FR.jam_form(h, l))))))))
24
25def jam_z(+h: Nat) -> {SW.jam(h, 0n) == h : Nat}:
26  SH.jam0_m(h, Nat.mod(h, 2n), {==}, NR.dm_lt(1n, h))
27
28def jam_nz(+h: Nat, +l: Nat, +hl: {Nat.is_eq(l, 0n) == False{} : Bool}) -> {SW.jam(h, l) == 1n+Nat.double(C.half(h)) : Nat}:
29  match l:
30    case 0n:
31      Empty.absurd({SW.jam(h, 0n) == 1n+Nat.double(C.half(h)) : Nat}, LW.true_ne_false(hl))
32    case 1n+ +lp:
33      SH.jam1_m(h, lp)
34
35def sub_shift(+d: Nat, +a: Nat, +b: Nat, +h: {Nat.is_le(b, a) == True{} : Bool}) -> {Nat.sub(C.shift(d, a), C.shift(d, b)) == C.shift(d, Nat.sub(a, b)) : Nat}:
36  +ea = N.sub_add(a, b, h)
37  Equal.trans(Nat, Nat.sub(C.shift(d, a), C.shift(d, b)), Nat.sub(C.shift(d, Nat.add(b, Nat.sub(a, b))), C.shift(d, b)), C.shift(d, Nat.sub(a, b)), Equal.cong(Nat, Nat, z => Nat.sub(C.shift(d, z), C.shift(d, b)), a, Nat.add(b, Nat.sub(a, b)), Equal.sym(Nat, Nat.add(b, Nat.sub(a, b)), a, ea)), Equal.trans(Nat, Nat.sub(C.shift(d, Nat.add(b, Nat.sub(a, b))), C.shift(d, b)), Nat.sub(Nat.add(C.shift(d, b), C.shift(d, Nat.sub(a, b))), C.shift(d, b)), C.shift(d, Nat.sub(a, b)), Equal.cong(Nat, Nat, z => Nat.sub(z, C.shift(d, b)), C.shift(d, Nat.add(b, Nat.sub(a, b))), Nat.add(C.shift(d, b), C.shift(d, Nat.sub(a, b))), WW.shift_add(d, b, Nat.sub(a, b))), N.add_sub_cancel(C.shift(d, b), C.shift(d, Nat.sub(a, b)))))
38
39def half_lt(+k: Nat, +t: Nat, +h: {Nat.is_lt(Nat.double(k), Nat.double(t)) == True{} : Bool}) -> {Nat.is_lt(k, t) == True{} : Bool}:
40  Equal.trans(Bool, Nat.is_lt(k, t), Nat.is_lt(Nat.double(k), Nat.double(t)), True{}, Equal.cong(Cmp, Bool, c => Cmp.is_lt(c), Nat.cmp(k, t), Nat.cmp(Nat.double(k), Nat.double(t)), Equal.sym(Cmp, Nat.cmp(Nat.double(k), Nat.double(t)), Nat.cmp(k, t), NC.cmp_dbl(k, t))), h)
41
42def lt_add_l(+l: Nat, +r: Nat, +hl: {Nat.is_eq(l, 0n) == False{} : Bool}) -> {Nat.is_lt(r, Nat.add(l, r)) == True{} : Bool}:
43  match l:
44    case 0n:
45      Empty.absurd({Nat.is_lt(r, Nat.add(0n, r)) == True{} : Bool}, LW.true_ne_false(hl))
46    case 1n+ +lp:
47      N.le_lt_succ(r, Nat.add(lp, r), L.subst(Nat, z => {Nat.is_le(r, z) == True{} : Bool}, Nat.add(r, lp), Nat.add(lp, r), NA.add_comm(r, lp), N.le_add_right(r, lp)))
48
49def rnz_c(+l: Nat, +R: Nat, +S: Nat, +e: {Nat.add(l, R) == S : Nat}, +hl: {Nat.is_lt(l, S) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(R, 0n) == c : Bool}) -> {c == False{} : Bool}:
50  match c:
51    case True{}:
52      +e0 = N.eq_from_is_eq(R, 0n, hc)
53      +el = Equal.trans(Nat, l, Nat.add(l, 0n), S, Equal.sym(Nat, Nat.add(l, 0n), l, N.add_zero(l)), Equal.trans(Nat, Nat.add(l, 0n), Nat.add(l, R), S, Equal.cong(Nat, Nat, z => Nat.add(l, z), 0n, R, Equal.sym(Nat, R, 0n, e0)), e))
54      Empty.absurd({True{} == False{} : Bool}, LW.true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(l, S), False{}, Equal.sym(Bool, Nat.is_lt(l, S), True{}, hl), L.subst(Nat, z => {Nat.is_lt(l, z) == False{} : Bool}, l, S, el, N.lt_irrefl(l)))))
55    case False{}:
56      {==}
57
58def hg_c(+u: Nat, +g: Nat, +b: Nat, +e: {Nat.add(b, 1n+g) == 2n+Nat.double(u) : Nat}, +hb: {Nat.is_le(b, 1n) == True{} : Bool}) -> {C.half(g) == u : Nat}:
59  match b:
60    case 0n:
61      +eg = N.succ_inj(g, 1n+Nat.double(u), e)
62      Equal.trans(Nat, C.half(g), C.half(1n+Nat.double(u)), u, Equal.cong(Nat, Nat, z => C.half(z), g, 1n+Nat.double(u), eg), WW.half_dbl(1n, u))
63    case 1n:
64      +eg = N.succ_inj(g, Nat.double(u), N.succ_inj(1n+g, 1n+Nat.double(u), e))
65      Equal.trans(Nat, C.half(g), C.half(Nat.double(u)), u, Equal.cong(Nat, Nat, z => C.half(z), g, Nat.double(u), eg), WW.half_dbl(0n, u))
66    case 2n+ +q:
67      NC.absurd_tf({C.half(g) == u : Nat}, hb)
68
69# T - jam(h, l) is the jam of T * 2^d - (l + h * 2^d) when 0 < l < 2^d, h < T, T even
70def jsub(+t: Nat, +d: Nat, +h: Nat, +l: Nat, +hl0: {Nat.is_eq(l, 0n) == False{} : Bool}, +hld: {C.fits(d, l) == True{} : Bool}, +hh: {Nat.is_lt(h, Nat.double(t)) == True{} : Bool}) -> {Nat.sub(Nat.double(t), SW.jam(h, l)) == SW.jam(C.high(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))) : Nat}:
71  +hTh = N.lt_le(h, Nat.double(t), hh)
72  +h1 = FR.lt_sub_pos(h, Nat.double(t), hh)
73  +eg1 = N.sub_add(Nat.sub(Nat.double(t), h), 1n, h1)
74  +ehg = Equal.trans(Nat, Nat.add(h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.add(h, Nat.sub(Nat.double(t), h)), Nat.double(t), Equal.cong(Nat, Nat, z => Nat.add(h, z), 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n), Nat.sub(Nat.double(t), h), eg1), N.sub_add(Nat.double(t), h, hTh))
75  +hl1 = WW.lt_one(d, 1n, {==}, l, hld)
76  +er = N.sub_add(C.shift(d, 1n), l, N.lt_le(l, C.shift(d, 1n), hl1))
77  +hr = L.subst(Nat, z => {Nat.is_lt(Nat.sub(C.shift(d, 1n), l), z) == True{} : Bool}, Nat.add(l, Nat.sub(C.shift(d, 1n), l)), C.shift(d, 1n), er, lt_add_l(l, Nat.sub(C.shift(d, 1n), l), hl0))
78  +fr = WW.fits_one(d, 1n, {==}, Nat.sub(C.shift(d, 1n), l), hr)
79  +rnz = rnz_c(l, Nat.sub(C.shift(d, 1n), l), C.shift(d, 1n), er, hl1, Nat.is_eq(Nat.sub(C.shift(d, 1n), l), 0n), {==})
80  +sh = C.shift(d, h)
81  +sg = C.shift(d, Nat.sub(Nat.sub(Nat.double(t), h), 1n))
82  +eW0 = Equal.trans(Nat, C.shift(d, Nat.double(t)), C.shift(d, Nat.add(h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n))), Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Equal.cong(Nat, Nat, z => C.shift(d, z), Nat.double(t), Nat.add(h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Equal.sym(Nat, Nat.add(h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.double(t), ehg)), Equal.trans(Nat, C.shift(d, Nat.add(h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n))), Nat.add(sh, C.shift(d, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n))), Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), WW.shift_add(d, h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Equal.trans(Nat, Nat.add(sh, C.shift(d, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n))), Nat.add(sh, Nat.add(C.shift(d, 1n), sg)), Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Equal.cong(Nat, Nat, z => Nat.add(sh, z), C.shift(d, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.add(C.shift(d, 1n), sg), WW.shift_add(d, 1n, Nat.sub(Nat.sub(Nat.double(t), h), 1n))), Equal.trans(Nat, Nat.add(sh, Nat.add(C.shift(d, 1n), sg)), Nat.add(sh, Nat.add(Nat.add(l, Nat.sub(C.shift(d, 1n), l)), sg)), Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Equal.cong(Nat, Nat, z => Nat.add(sh, Nat.add(z, sg)), C.shift(d, 1n), Nat.add(l, Nat.sub(C.shift(d, 1n), l)), Equal.sym(Nat, Nat.add(l, Nat.sub(C.shift(d, 1n), l)), C.shift(d, 1n), er)), Equal.trans(Nat, Nat.add(sh, Nat.add(Nat.add(l, Nat.sub(C.shift(d, 1n), l)), sg)), Nat.add(sh, Nat.add(l, Nat.add(Nat.sub(C.shift(d, 1n), l), sg))), Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Equal.cong(Nat, Nat, z => Nat.add(sh, z), Nat.add(Nat.add(l, Nat.sub(C.shift(d, 1n), l)), sg), Nat.add(l, Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), NA.add_assoc(l, Nat.sub(C.shift(d, 1n), l), sg)), Equal.trans(Nat, Nat.add(sh, Nat.add(l, Nat.add(Nat.sub(C.shift(d, 1n), l), sg))), Nat.add(Nat.add(sh, l), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Equal.sym(Nat, Nat.add(Nat.add(sh, l), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Nat.add(sh, Nat.add(l, Nat.add(Nat.sub(C.shift(d, 1n), l), sg))), NA.add_assoc(sh, l, Nat.add(Nat.sub(C.shift(d, 1n), l), sg))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Nat.add(sh, l), Nat.add(l, sh), NA.add_comm(sh, l))))))))
83  +eW = Equal.trans(Nat, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))), Nat.sub(Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Nat.add(l, sh)), Nat.add(Nat.sub(C.shift(d, 1n), l), sg), Equal.cong(Nat, Nat, z => Nat.sub(z, Nat.add(l, sh)), C.shift(d, Nat.double(t)), Nat.add(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), eW0), N.add_sub_cancel(Nat.add(l, sh), Nat.add(Nat.sub(C.shift(d, 1n), l), sg)))
84  +eH = Equal.trans(Nat, C.high(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), C.high(d, Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Nat.sub(Nat.sub(Nat.double(t), h), 1n), Equal.cong(Nat, Nat, z => C.high(d, z), Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))), Nat.add(Nat.sub(C.shift(d, 1n), l), sg), eW), WW.high_u(d, Nat.sub(C.shift(d, 1n), l), Nat.sub(Nat.sub(Nat.double(t), h), 1n), fr))
85  +eL = Equal.trans(Nat, C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), C.low(d, Nat.add(Nat.sub(C.shift(d, 1n), l), sg)), Nat.sub(C.shift(d, 1n), l), Equal.cong(Nat, Nat, z => C.low(d, z), Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))), Nat.add(Nat.sub(C.shift(d, 1n), l), sg), eW), WW.low_u(d, Nat.sub(C.shift(d, 1n), l), Nat.sub(Nat.sub(Nat.double(t), h), 1n), fr))
86  +rhs = Equal.trans(Nat, SW.jam(C.high(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))), SW.jam(Nat.sub(Nat.sub(Nat.double(t), h), 1n), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))), 1n+Nat.double(C.half(Nat.sub(Nat.sub(Nat.double(t), h), 1n))), Equal.cong(Nat, Nat, z => SW.jam(z, C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))), C.high(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), Nat.sub(Nat.sub(Nat.double(t), h), 1n), eH), Equal.trans(Nat, SW.jam(Nat.sub(Nat.sub(Nat.double(t), h), 1n), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))), SW.jam(Nat.sub(Nat.sub(Nat.double(t), h), 1n), Nat.sub(C.shift(d, 1n), l)), 1n+Nat.double(C.half(Nat.sub(Nat.sub(Nat.double(t), h), 1n))), Equal.cong(Nat, Nat, z => SW.jam(Nat.sub(Nat.sub(Nat.double(t), h), 1n), z), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), Nat.sub(C.shift(d, 1n), l), eL), jam_nz(Nat.sub(Nat.sub(Nat.double(t), h), 1n), Nat.sub(C.shift(d, 1n), l), rnz)))
87  +ehk = WW.hb(h)
88  +hdk = N.le_lt_trans(Nat.double(C.half(h)), h, Nat.double(t), L.subst(Nat, z => {Nat.is_le(Nat.double(C.half(h)), z) == True{} : Bool}, Nat.add(Nat.double(C.half(h)), C.bit(h)), h, Equal.trans(Nat, Nat.add(Nat.double(C.half(h)), C.bit(h)), Nat.add(C.bit(h), Nat.double(C.half(h))), h, NA.add_comm(Nat.double(C.half(h)), C.bit(h)), Equal.sym(Nat, h, Nat.add(C.bit(h), Nat.double(C.half(h))), ehk)), N.le_add_right(Nat.double(C.half(h)), C.bit(h))), hh)
89  +hk = half_lt(C.half(h), t, hdk)
90  +et = N.sub_add(t, 1n+C.half(h), N.lt_succ_le_succ(C.half(h), t, hk))
91  +eT = Equal.trans(Nat, Nat.double(t), Nat.double(Nat.add(1n+C.half(h), Nat.sub(t, 1n+C.half(h)))), Nat.add(1n+Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Equal.cong(Nat, Nat, z => Nat.double(z), t, Nat.add(1n+C.half(h), Nat.sub(t, 1n+C.half(h))), Equal.sym(Nat, Nat.add(1n+C.half(h), Nat.sub(t, 1n+C.half(h))), t, et)), Equal.trans(Nat, Nat.double(Nat.add(1n+C.half(h), Nat.sub(t, 1n+C.half(h)))), Nat.add(2n+Nat.double(C.half(h)), Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.add(1n+Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), NA.double_add(1n+C.half(h), Nat.sub(t, 1n+C.half(h))), Equal.cong(Nat, Nat, z => 1n+z, 1n+Nat.add(Nat.double(C.half(h)), Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.add(Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Equal.sym(Nat, Nat.add(Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), 1n+Nat.add(Nat.double(C.half(h)), Nat.double(Nat.sub(t, 1n+C.half(h)))), N.add_succ(Nat.double(C.half(h)), Nat.double(Nat.sub(t, 1n+C.half(h))))))))
92  +lhs = Equal.trans(Nat, Nat.sub(Nat.double(t), SW.jam(h, l)), Nat.sub(Nat.double(t), 1n+Nat.double(C.half(h))), 1n+Nat.double(Nat.sub(t, 1n+C.half(h))), Equal.cong(Nat, Nat, z => Nat.sub(Nat.double(t), z), SW.jam(h, l), 1n+Nat.double(C.half(h)), jam_nz(h, l, hl0)), Equal.trans(Nat, Nat.sub(Nat.double(t), 1n+Nat.double(C.half(h))), Nat.sub(Nat.add(1n+Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), 1n+Nat.double(C.half(h))), 1n+Nat.double(Nat.sub(t, 1n+C.half(h))), Equal.cong(Nat, Nat, z => Nat.sub(z, 1n+Nat.double(C.half(h))), Nat.double(t), Nat.add(1n+Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), eT), N.add_sub_cancel(1n+Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h))))))
93  +b = C.bit(h)
94  +e1 = Equal.trans(Nat, Nat.add(Nat.add(b, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.double(C.half(h))), Nat.add(Nat.add(b, Nat.double(C.half(h))), 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.add(Nat.add(1n, 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.double(C.half(h))), A.add_rot(b, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n), Nat.double(C.half(h))), Equal.trans(Nat, Nat.add(Nat.add(b, Nat.double(C.half(h))), 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.add(h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.add(Nat.add(1n, 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.double(C.half(h))), Equal.cong(Nat, Nat, z => Nat.add(z, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.add(b, Nat.double(C.half(h))), h, Equal.sym(Nat, h, Nat.add(b, Nat.double(C.half(h))), ehk)), Equal.trans(Nat, Nat.add(h, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.double(t), Nat.add(Nat.add(1n, 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.double(C.half(h))), ehg, Equal.trans(Nat, Nat.double(t), Nat.add(1n+Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.add(Nat.add(1n, 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.double(C.half(h))), eT, Equal.cong(Nat, Nat, z => 1n+z, Nat.add(Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.add(1n+Nat.double(Nat.sub(t, 1n+C.half(h))), Nat.double(C.half(h))), NA.add_comm(Nat.double(C.half(h)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))))))))
95  +e2 = A.add_cancel_r(Nat.add(b, 1n+Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.add(1n, 1n+Nat.double(Nat.sub(t, 1n+C.half(h)))), Nat.double(C.half(h)), e1)
96  +ehalf = hg_c(Nat.sub(t, 1n+C.half(h)), Nat.sub(Nat.sub(Nat.double(t), h), 1n), b, e2, WW.bit_le1(h))
97  Equal.trans(Nat, Nat.sub(Nat.double(t), SW.jam(h, l)), 1n+Nat.double(Nat.sub(t, 1n+C.half(h))), SW.jam(C.high(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))), lhs, Equal.sym(Nat, SW.jam(C.high(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))), 1n+Nat.double(Nat.sub(t, 1n+C.half(h))), Equal.trans(Nat, SW.jam(C.high(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h)))), C.low(d, Nat.sub(C.shift(d, Nat.double(t)), Nat.add(l, C.shift(d, h))))), 1n+Nat.double(C.half(Nat.sub(Nat.sub(Nat.double(t), h), 1n))), 1n+Nat.double(Nat.sub(t, 1n+C.half(h))), rhs, Equal.cong(Nat, Nat, z => 1n+Nat.double(z), C.half(Nat.sub(Nat.sub(Nat.double(t), h), 1n)), Nat.sub(t, 1n+C.half(h)), ehalf))))