PROOF.dec: def of bend-osdev-gf@0.1.1.0
Import: import bend-osdev-gf@0.1.1.0/PROOF.bend as PROOF
Lines 586-1610 of bend-osdev-gf@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&start_line=586&end_line=1610

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G

# every byte is the sum of its bits times the basis (by cases)
def dec(+a: G.Gf8Bits) -> {ss(bl(a), basis()) == a : G.Gf8Bits}:
  match a:
    case G.Gf8Bits{b0, b1, b2, b3, b4, b5, b6, b7}:
      match b0:
        case True{}:
          match b1:
            case True{}:
              match b2:
                case True{}:
                  match b3:
                    case True{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                    case False{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                case False{}:
                  match b3:
                    case True{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                    case False{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
            case False{}:
              match b2:
                case True{}:
                  match b3:
                    case True{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                    case False{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                case False{}:
                  match b3:
                    case True{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                    case False{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
        case False{}:
          match b1:
            case True{}:
              match b2:
                case True{}:
                  match b3:
                    case True{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                    case False{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                case False{}:
                  match b3:
                    case True{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                    case False{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
            case False{}:
              match b2:
                case True{}:
                  match b3:
                    case True{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                    case False{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                case False{}:
                  match b3:
                    case True{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                    case False{}:
                      match b4:
                        case True{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                        case False{}:
                          match b5:
                            case True{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                            case False{}:
                              match b6:
                                case True{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}
                                case False{}:
                                  match b7:
                                    case True{}:
                                      {==}
                                    case False{}:
                                      {==}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=basis
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=bl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/PROOF.bend&name=ss
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8Bits