def bx_swap

bend-osdev-gf@0.1.1.0 · PROOF.bend:79

import Base

79def bx_swap(+a: Bool, +b: Bool, +c: Bool, +d: Bool) -> {Bool.xor(Bool.xor(a, b), Bool.xor(c, d)) == Bool.xor(Bool.xor(a, c), Bool.xor(b, d)) : Bool}:
80  match a:
81    case True{}:
82      match b:
83        case True{}:
84          match c:
85            case True{}:
86              match d:
87                case True{}:
88                  {==}
89                case False{}:
90                  {==}
91            case False{}:
92              match d:
93                case True{}:
94                  {==}
95                case False{}:
96                  {==}
97        case False{}:
98          match c:
99            case True{}:
100              match d:
101                case True{}:
102                  {==}
103                case False{}:
104                  {==}
105            case False{}:
106              match d:
107                case True{}:
108                  {==}
109                case False{}:
110                  {==}
111    case False{}:
112      match b:
113        case True{}:
114          match c:
115            case True{}:
116              match d:
117                case True{}:
118                  {==}
119                case False{}:
120                  {==}
121            case False{}:
122              match d:
123                case True{}:
124                  {==}
125                case False{}:
126                  {==}
127        case False{}:
128          match c:
129            case True{}:
130              match d:
131                case True{}:
132                  {==}
133                case False{}:
134                  {==}
135            case False{}:
136              match d:
137                case True{}:
138                  {==}
139                case False{}:
140                  {==}