def shr_cap

bendtorch-core@0.1.0.0 · src/storage/route.bend:95

import Base
import bendtorch-core@0.1.0.0/src/storage/size.bend as Size
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

95def shr_cap(+d: Nat, +h: {Nat.is_le(1n+d, 20n) == True{} : Bool}) -> {Size.capacity(d) == U32.shr(Size.capacity(1n+d)) : U32}:
96  match d:
97    case 0n:
98      {==}
99    case 1n+d1:
100      match d1:
101        case 0n:
102          {==}
103        case 1n+d2:
104          match d2:
105            case 0n:
106              {==}
107            case 1n+d3:
108              match d3:
109                case 0n:
110                  {==}
111                case 1n+d4:
112                  match d4:
113                    case 0n:
114                      {==}
115                    case 1n+d5:
116                      match d5:
117                        case 0n:
118                          {==}
119                        case 1n+d6:
120                          match d6:
121                            case 0n:
122                              {==}
123                            case 1n+d7:
124                              match d7:
125                                case 0n:
126                                  {==}
127                                case 1n+d8:
128                                  match d8:
129                                    case 0n:
130                                      {==}
131                                    case 1n+d9:
132                                      match d9:
133                                        case 0n:
134                                          {==}
135                                        case 1n+d10:
136                                          match d10:
137                                            case 0n:
138                                              {==}
139                                            case 1n+d11:
140                                              match d11:
141                                                case 0n:
142                                                  {==}
143                                                case 1n+d12:
144                                                  match d12:
145                                                    case 0n:
146                                                      {==}
147                                                    case 1n+d13:
148                                                      match d13:
149                                                        case 0n:
150                                                          {==}
151                                                        case 1n+d14:
152                                                          match d14:
153                                                            case 0n:
154                                                              {==}
155                                                            case 1n+d15:
156                                                              match d15:
157                                                                case 0n:
158                                                                  {==}
159                                                                case 1n+d16:
160                                                                  match d16:
161                                                                    case 0n:
162                                                                      {==}
163                                                                    case 1n+d17:
164                                                                      match d17:
165                                                                        case 0n:
166                                                                          {==}
167                                                                        case 1n+d18:
168                                                                          match d18:
169                                                                            case 0n:
170                                                                              {==}
171                                                                            case 1n+d19:
172                                                                              match d19:
173                                                                                case 0n:
174                                                                                  {==}
175                                                                                case 1n+d20:
176                                                                                  Empty.absurd({Size.capacity(20n+d20) == U32.shr(Size.capacity(1n+20n+d20)) : U32}, Arith.clash(h))