Route.shr_cap: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/route.bend as Route
Lines 95-176 of bendtorch-core@0.1.0.0/src/storage/route.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/route.bend&start_line=95&end_line=176

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

def shr_cap(+d: Nat, +h: {Nat.is_le(1n+d, 20n) == True{} : Bool}) -> {Size.capacity(d) == U32.shr(Size.capacity(1n+d)) : U32}:
  match d:
    case 0n:
      {==}
    case 1n+d1:
      match d1:
        case 0n:
          {==}
        case 1n+d2:
          match d2:
            case 0n:
              {==}
            case 1n+d3:
              match d3:
                case 0n:
                  {==}
                case 1n+d4:
                  match d4:
                    case 0n:
                      {==}
                    case 1n+d5:
                      match d5:
                        case 0n:
                          {==}
                        case 1n+d6:
                          match d6:
                            case 0n:
                              {==}
                            case 1n+d7:
                              match d7:
                                case 0n:
                                  {==}
                                case 1n+d8:
                                  match d8:
                                    case 0n:
                                      {==}
                                    case 1n+d9:
                                      match d9:
                                        case 0n:
                                          {==}
                                        case 1n+d10:
                                          match d10:
                                            case 0n:
                                              {==}
                                            case 1n+d11:
                                              match d11:
                                                case 0n:
                                                  {==}
                                                case 1n+d12:
                                                  match d12:
                                                    case 0n:
                                                      {==}
                                                    case 1n+d13:
                                                      match d13:
                                                        case 0n:
                                                          {==}
                                                        case 1n+d14:
                                                          match d14:
                                                            case 0n:
                                                              {==}
                                                            case 1n+d15:
                                                              match d15:
                                                                case 0n:
                                                                  {==}
                                                                case 1n+d16:
                                                                  match d16:
                                                                    case 0n:
                                                                      {==}
                                                                    case 1n+d17:
                                                                      match d17:
                                                                        case 0n:
                                                                          {==}
                                                                        case 1n+d18:
                                                                          match d18:
                                                                            case 0n:
                                                                              {==}
                                                                            case 1n+d19:
                                                                              match d19:
                                                                                case 0n:
                                                                                  {==}
                                                                                case 1n+d20:
                                                                                  Empty.absurd({Size.capacity(20n+d20) == U32.shr(Size.capacity(1n+20n+d20)) : U32}, Arith.clash(h))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shr
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/size.bend&name=capacity