def rot3

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/f64bits.bend:181

import Base

181def rot3(+a: Bool, +b: Bool, +c: Bool) -> {Bool.and(a, Bool.and(b, c)) == Bool.and(c, Bool.and(a, b)) : Bool}:
182  match a b c:
183    case True{} True{} True{}:
184      {==}
185    case True{} True{} False{}:
186      {==}
187    case True{} False{} True{}:
188      {==}
189    case True{} False{} False{}:
190      {==}
191    case False{} True{} True{}:
192      {==}
193    case False{} True{} False{}:
194      {==}
195    case False{} False{} True{}:
196      {==}
197    case False{} False{} False{}:
198      {==}