def ssh1

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqc.bend:290

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

290def ssh1(+x: F.F64, +s: Bool, +e: Nat, +f: WU.U64, +t: Bool) -> {F.sq_cls(x, s, e, f, t) == simpl(s, t, X.is_zero(f), Nat.is_eq(e, 0n), x, F.sq_n(F.norm_e(e, f), F.norm_f(e, f), Nat.is_eq(Nat.mod(F.norm_e(e, f), 2n), 1n))) : F.F64}:
291  match t:
292    case True{}:
293      FL.non(x, Bool.or(Bool.not(X.is_zero(f)), s))
294    case False{}:
295      ssh2(x, s, e, f, Bool.and(Nat.is_eq(e, 0n), X.is_zero(f)))