~/jendhub

proofs/math/typed/f64mexp.bend

bend-collections-laws-math@1.0.0.0 · 91 lines · 11 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
3import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
4import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
5import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
6import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
7import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
8import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
9import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
10import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
11import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as CLZ
15import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as UH
16import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as A
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
20import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend as NM
21
22# Mul.value of spec/math/f64.bend: SoftFloat's f64_mul multiplies the two
23# normalized 53-bit significands (shifted by 10 and 11) into 128 bits, jams
24# the low half into bit 0 and rounds with rp62; the spec rounds the exact
25# product of the significands. round_jam and round_shift bridge the two.
26
27
28# ---- exponent bookkeeping ----
29
30def sa_le(+ea: Nat, +fa: WU.U64) -> {Nat.is_le(NM.sa(ea, fa), 53n) == True{} : Bool}:
31  match ea:
32    case 0n:
33      +hc = L.subst(Nat, z => {Nat.is_le(z, 64n) == True{} : Bool}, Nat.sub(64n, M.bit_length(SW.value(fa))), X.clz(fa), Equal.sym(Nat, X.clz(fa), Nat.sub(64n, M.bit_length(SW.value(fa))), CLZ.clz_value(fa)), UH.sub_le(64n, M.bit_length(SW.value(fa))))
34      NF.sub_mono_l(X.clz(fa), 64n, 11n, hc)
35    case 1n+ +p:
36      {==}
37
38def e_ge1(+E: Nat, +h: {Nat.is_eq(E, 0n) == False{} : Bool}) -> {Nat.is_le(1926n, Nat.add(1925n, E)) == True{} : Bool}:
39  match E:
40    case 0n:
41      Empty.absurd({Nat.is_le(1926n, Nat.add(1925n, 0n)) == True{} : Bool}, LW.true_ne_false(h))
42    case 1n+ +p:
43      N.zero_le(p)
44
45def xg_c(+E: Nat, +c: Bool, +hc: {Nat.is_eq(E, 0n) == c : Bool}) -> {Nat.is_le(1926n, SF.pick(Nat, c, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n))) == True{} : Bool}:
46  match c:
47    case True{}:
48      {==}
49    case False{}:
50      L.subst(Nat, z => {Nat.is_le(1926n, z) == True{} : Bool}, Nat.add(1925n, E), Nat.sub(Nat.add(E, SF.zb()), 1075n), Equal.sym(Nat, Nat.sub(Nat.add(E, SF.zb()), 1075n), Nat.add(1925n, E), FC.esub(E)), e_ge1(E, hc))
51
52def xexp_ge(+E: Nat) -> {Nat.is_le(1926n, SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n))) == True{} : Bool}:
53  xg_c(E, Nat.is_eq(E, 0n), {==})
54
55def eg(+ea: Nat, +sa: Nat, +Xx: Nat, +n2: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +hs: {Nat.is_le(sa, 53n) == True{} : Bool}, +hX: {Nat.is_le(1926n, Xx) == True{} : Bool}) -> {Nat.is_le(4044n, ea) == True{} : Bool}:
56  +h1 = L.subst(Nat, z => {Nat.is_le(4097n, z) == True{} : Bool}, Nat.add(Xx, 2171n), Nat.add(ea, sa), Equal.sym(Nat, Nat.add(ea, sa), Nat.add(Xx, 2171n), n2), Equal.trans(Bool, Nat.is_le(Nat.add(1926n, 2171n), Nat.add(Xx, 2171n)), Nat.is_le(1926n, Xx), True{}, FR.le_cancel_r(1926n, Xx, 2171n), hX))
57  +h2 = N.le_trans(4097n, Nat.add(ea, sa), Nat.add(ea, 53n), h1, N.le_add_left(sa, 53n, ea, hs))
58  Equal.trans(Bool, Nat.is_le(4044n, ea), Nat.is_le(Nat.add(4044n, 53n), Nat.add(ea, 53n)), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(4044n, 53n), Nat.add(ea, 53n)), Nat.is_le(4044n, ea), FR.le_cancel_r(4044n, ea, 53n)), h2)
59
60def s_ge(+ea: Nat, +eb: Nat, +sa: Nat, +sb: Nat, +Xx: Nat, +Xy: Nat, +n2x: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +n2y: {Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hsb: {Nat.is_le(sb, 53n) == True{} : Bool}, +hXx: {Nat.is_le(1926n, Xx) == True{} : Bool}, +hXy: {Nat.is_le(1926n, Xy) == True{} : Bool}) -> {Nat.is_le(8088n, Nat.add(ea, eb)) == True{} : Bool}:
61  +ha = eg(ea, sa, Xx, n2x, hsa, hXx)
62  +hb = eg(eb, sb, Xy, n2y, hsb, hXy)
63  N.le_trans(8088n, Nat.add(4044n, eb), Nat.add(ea, eb), N.le_add_left(4044n, eb, 4044n, hb), Equal.trans(Bool, Nat.is_le(Nat.add(4044n, eb), Nat.add(ea, eb)), Nat.is_le(4044n, ea), True{}, FR.le_cancel_r(4044n, ea, eb), ha))
64
65def e0_ge(+ea: Nat, +eb: Nat, +sa: Nat, +sb: Nat, +Xx: Nat, +Xy: Nat, +n2x: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +n2y: {Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hsb: {Nat.is_le(sb, 53n) == True{} : Bool}, +hXx: {Nat.is_le(1926n, Xx) == True{} : Bool}, +hXy: {Nat.is_le(1926n, Xy) == True{} : Bool}) -> {Nat.is_le(2244n, Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n))) == True{} : Bool}:
66  RT.le_sub(2244n, 5119n, Nat.add(ea, eb), N.le_trans(Nat.add(2244n, 5119n), 8088n, Nat.add(ea, eb), {==}, s_ge(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy)))
67
68def x_eq(+ea: Nat, +eb: Nat, +sa: Nat, +sb: Nat, +Xx: Nat, +Xy: Nat, +n2x: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +n2y: {Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hsb: {Nat.is_le(sb, 53n) == True{} : Bool}, +hXx: {Nat.is_le(1926n, Xx) == True{} : Bool}, +hXy: {Nat.is_le(1926n, Xy) == True{} : Bool}) -> {Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n) == Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)) : Nat}:
69  +h = N.le_trans(2180n, 2244n, Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), {==}, e0_ge(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy))
70  Equal.trans(Nat, Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), Nat.add(2180n, Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n)), Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), NA.add_comm(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), N.sub_add(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n, h))
71
72def x_ge(+ea: Nat, +eb: Nat, +sa: Nat, +sb: Nat, +Xx: Nat, +Xy: Nat, +n2x: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +n2y: {Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hsb: {Nat.is_le(sb, 53n) == True{} : Bool}, +hXx: {Nat.is_le(1926n, Xx) == True{} : Bool}, +hXy: {Nat.is_le(1926n, Xy) == True{} : Bool}) -> {Nat.is_le(64n, Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n)) == True{} : Bool}:
73  RT.le_sub(64n, 2180n, Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), e0_ge(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy))
74
75def x0_eq(+ea: Nat, +eb: Nat, +sa: Nat, +sb: Nat, +Xx: Nat, +Xy: Nat, +n2x: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +n2y: {Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hsb: {Nat.is_le(sb, 53n) == True{} : Bool}, +hXx: {Nat.is_le(1926n, Xx) == True{} : Bool}, +hXy: {Nat.is_le(1926n, Xy) == True{} : Bool}) -> {Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n) == Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n) : Nat}:
76  Equal.trans(Nat, Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), Nat.add(64n, Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n)), Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), NA.add_comm(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), N.sub_add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n, x_ge(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy)))
77
78# x0 + 21 + sa + sb is the spec's product exponent
79def mexp(+ea: Nat, +eb: Nat, +sa: Nat, +sb: Nat, +Xx: Nat, +Xy: Nat, +n2x: {Nat.add(ea, sa) == Nat.add(Xx, 2171n) : Nat}, +n2y: {Nat.add(eb, sb) == Nat.add(Xy, 2171n) : Nat}, +hsa: {Nat.is_le(sa, 53n) == True{} : Bool}, +hsb: {Nat.is_le(sb, 53n) == True{} : Bool}, +hXx: {Nat.is_le(1926n, Xx) == True{} : Bool}, +hXy: {Nat.is_le(1926n, Xy) == True{} : Bool}) -> {Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(sa, sb)) == Nat.sub(Nat.add(Xx, Xy), SF.zb()) : Nat}:
80  +ex0 = x0_eq(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy)
81  +exx = x_eq(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy)
82  +eS0 = Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), Nat.add(5119n, Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n))), Nat.add(ea, eb), NA.add_comm(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), N.sub_add(Nat.add(ea, eb), 5119n, N.le_trans(5119n, 8088n, Nat.add(ea, eb), {==}, s_ge(ea, eb, sa, sb, Xx, Xy, n2x, n2y, hsa, hsb, hXx, hXy))))
83  +eS = Equal.trans(Nat, Nat.add(ea, eb), Nat.add(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), Nat.add(ea, eb), eS0), Equal.trans(Nat, Nat.add(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 5119n), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), 5119n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), Equal.cong(Nat, Nat, z => Nat.add(z, 5119n), Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), exx)), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 2180n), 5119n), Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), 2180n), 5119n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(z, 2180n), 5119n), Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), Equal.sym(Nat, Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), ex0)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), 2180n), 5119n), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), 7299n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), NA.add_assoc(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n), 2180n, 5119n), NA.add_assoc(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 64n, 7299n)))))
84  +e1 = Equal.trans(Nat, Nat.add(Nat.add(ea, sa), Nat.add(eb, sb)), Nat.add(Nat.add(Xx, 2171n), Nat.add(eb, sb)), Nat.add(Nat.add(Xx, 2171n), Nat.add(Xy, 2171n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(eb, sb)), Nat.add(ea, sa), Nat.add(Xx, 2171n), n2x), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Xx, 2171n), z), Nat.add(eb, sb), Nat.add(Xy, 2171n), n2y))
85  +e2 = W64M.add4(ea, sa, eb, sb)
86  +e3 = W64M.add4(Xx, 2171n, Xy, 2171n)
87  +T2 = Nat.add(sa, sb)
88  +W = Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), T2)
89  +e4 = Equal.trans(Nat, Nat.add(Nat.add(W, 3000n), 4342n), Nat.add(W, 7342n), Nat.add(Nat.add(Xx, Xy), 4342n), NA.add_assoc(W, 3000n, 4342n), Equal.trans(Nat, Nat.add(W, 7342n), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(T2, 7342n)), Nat.add(Nat.add(Xx, Xy), 4342n), NA.add_assoc(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), T2, 7342n), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(T2, 7342n)), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(7342n, T2)), Nat.add(Nat.add(Xx, Xy), 4342n), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), z), Nat.add(T2, 7342n), Nat.add(7342n, T2), NA.add_comm(T2, 7342n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(7342n, T2)), Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), 7342n), T2), Nat.add(Nat.add(Xx, Xy), 4342n), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), 7342n), T2), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), Nat.add(7342n, T2)), NA.add_assoc(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), 7342n, T2)), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), 7342n), T2), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), T2), Nat.add(Nat.add(Xx, Xy), 4342n), Equal.cong(Nat, Nat, z => Nat.add(z, T2), Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n), 7342n), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), NA.add_assoc(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 21n, 7342n)), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), T2), Nat.add(Nat.add(ea, eb), T2), Nat.add(Nat.add(Xx, Xy), 4342n), Equal.cong(Nat, Nat, z => Nat.add(z, T2), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), Nat.add(ea, eb), Equal.sym(Nat, Nat.add(ea, eb), Nat.add(Nat.sub(Nat.sub(Nat.sub(Nat.add(ea, eb), Nat.add(F.off(), 1023n)), 2180n), 64n), 7363n), eS)), Equal.trans(Nat, Nat.add(Nat.add(ea, eb), T2), Nat.add(Nat.add(ea, sa), Nat.add(eb, sb)), Nat.add(Nat.add(Xx, Xy), 4342n), Equal.sym(Nat, Nat.add(Nat.add(ea, sa), Nat.add(eb, sb)), Nat.add(Nat.add(ea, eb), T2), e2), Equal.trans(Nat, Nat.add(Nat.add(ea, sa), Nat.add(eb, sb)), Nat.add(Nat.add(Xx, 2171n), Nat.add(Xy, 2171n)), Nat.add(Nat.add(Xx, Xy), 4342n), e1, e3))))))))
90  +e5 = A.add_cancel_r(Nat.add(W, 3000n), Nat.add(Xx, Xy), 4342n, e4)
91  Equal.sym(Nat, Nat.sub(Nat.add(Xx, Xy), SF.zb()), W, Equal.trans(Nat, Nat.sub(Nat.add(Xx, Xy), 3000n), Nat.sub(Nat.add(W, 3000n), 3000n), W, Equal.cong(Nat, Nat, z => Nat.sub(z, 3000n), Nat.add(Xx, Xy), Nat.add(W, 3000n), Equal.sym(Nat, Nat.add(W, 3000n), Nat.add(Xx, Xy), e5)), FR.sub_add_l(W, 3000n)))