def sswap

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

import Base
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F

304def sswap(+s1: Bool, +s2: Bool, +hs: {s1 == s2 : Bool}, +x: F.F64, +r: F.F64, +p1: Bool, +q1: Bool, +h0: {p1 == q1 : Bool}, +p2: Bool, +q2: Bool, +h1: {p2 == q2 : Bool}, +p3: Bool, +q3: Bool, +h2: {p3 == q3 : Bool}) -> {simpl(s1, p1, p2, p3, x, r) == simpl(s2, q1, q2, q3, x, r) : F.F64}:
305  Equal.trans(F.F64, simpl(s1, p1, p2, p3, x, r), simpl(s2, p1, p2, p3, x, r), simpl(s2, q1, q2, q3, x, r), Equal.cong(Bool, F.F64, w => simpl(w, p1, p2, p3, x, r), s1, s2, hs), Equal.trans(F.F64, simpl(s2, p1, p2, p3, x, r), simpl(s2, q1, p2, p3, x, r), simpl(s2, q1, q2, q3, x, r), Equal.cong(Bool, F.F64, w => simpl(s2, w, p2, p3, x, r), p1, q1, h0), Equal.trans(F.F64, simpl(s2, q1, p2, p3, x, r), simpl(s2, q1, q2, p3, x, r), simpl(s2, q1, q2, q3, x, r), Equal.cong(Bool, F.F64, w => simpl(s2, q1, w, p3, x, r), p2, q2, h1), Equal.cong(Bool, F.F64, w => simpl(s2, q1, q2, w, x, r), p3, q3, h2))))