def or3

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64close.bend:22

import Base

22# three-way disjunction congruence over abstract Booleans (book-less: the
23# checker never unfolds the comparisons it is applied to)
24def or3(+x1: Bool, +x2: Bool, +x3: Bool, +y1: Bool, +y2: Bool, +y3: Bool, +h1: {x1 == y1 : Bool}, +h2: {x2 == y2 : Bool}, +h3: {x3 == y3 : Bool}) -> {Bool.or(Bool.or(x1, x2), x3) == Bool.or(Bool.or(y1, y2), y3) : Bool}:
25  +c1 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(t, x2), x3), x1, y1, h1)
26  +c2 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(y1, t), x3), x2, y2, h2)
27  +c3 = Equal.cong(Bool, Bool, t => Bool.or(Bool.or(y1, y2), t), x3, y3, h3)
28  Equal.trans(Bool, Bool.or(Bool.or(x1, x2), x3), Bool.or(Bool.or(y1, x2), x3), Bool.or(Bool.or(y1, y2), y3), c1, Equal.trans(Bool, Bool.or(Bool.or(y1, x2), x3), Bool.or(Bool.or(y1, y2), x3), Bool.or(Bool.or(y1, y2), y3), c2, c3))