proofs/math/typed/f64sqx.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqx.bend as F64sqx

4 imports

import Base
import ../../lib/nat.bend as N
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR

Definitions

def sqexp source · line 11 · raw

@+q:Nat -> @+p:Nat -> @+j:Nat -> @+x:Nat -> @+XX:Nat -> @+EN:Nat -> @+Ep:Nat -> @+sa:Nat -> @+ci:Nat -> @+cs:Nat -> @+hq:{Nat.add(Nat.add(q, q), cs) == XX : Nat} -> @+hp:{Nat.add(Nat.add(p, p), 1075n) == Nat.add(Ep, 4096n) : Nat} -> @+hE:{Nat.add(Ep, ci) == EN : Nat} -> @+hEN:{Nat.add(EN, sa) == Nat.add(XX, 2171n) : Nat} -> @+hj:{Nat.add(Nat.add(j, j), Nat.add(72n, Nat.add(sa, ci))) == Nat.add(200n, cs) : Nat} -> @+hx:{Nat.add(x, 2180n) == Nat.add(p, 1048n) : Nat} -> {Nat.add(Nat.add(q, 1399n), Nat.add(1n, j)) == x : Nat}