PROOF.dec_rt: def of bend-osdev-acpi@0.1.1.0
Import: import bend-osdev-acpi@0.1.1.0/PROOF.bend as PROOF
Lines 2253-2276 of bend-osdev-acpi@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&start_line=2253&end_line=2276

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-acpi@0.1.1.0/error.bend as E
import bend-osdev-acpi@0.1.1.0/aml_name.bend as N

def dec_rt(+n: N.AmlName, +R: List<&2, U32>, +ok: {N.AmlName.valid(n) == True{} : Bool}) -> {Done{N.AmlNameL{n, R}} == N.nm.dec(B.append(B.mask(N.nm.enc(n)), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}:
  match n:
    case N.AmlName{r, u, ss}:
      match r:
        case True{}:
          match u:
            case 0n:
              %mask_app([92], N.nm.path(ss)) : {Done{N.AmlNameL{N.AmlName{True{}, 0n, ss}, R}} == N.nm.dec(B.append(_, R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
              %pth_dpath(ss, R, and_l(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok), and_r(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok)) : {Done{N.AmlNameL{N.AmlName{True{}, 0n, ss}, R}} == N.nm.named(True{}, 0n, _) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
              {==}
            case 1n+p:
              Empty.absurd({Done{N.AmlNameL{N.AmlName{True{}, 1n+p, ss}, R}} == N.nm.dec(B.append(B.mask(N.nm.enc(N.AmlName{True{}, 1n+p, ss})), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}, ft_absurd(ok))
        case False{}:
          match u:
            case 0n:
              %mask_app(N.nm.carets(0n), N.nm.path(ss)) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, ss}, R}} == N.nm.dec(B.append(_, R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
              %mask_carets(0n) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, ss}, R}} == N.nm.dec(B.append(B.append(_, B.mask(N.nm.path(ss))), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
              %app_assoc(N.nm.carets(0n), B.mask(N.nm.path(ss)), R) : {Done{N.AmlNameL{N.AmlName{False{}, 0n, ss}, R}} == N.nm.dec(_) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
              pth_dec(ss, R, and_l(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok), and_r(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok))
            case 1n+p:
              %mask_app(N.nm.carets(1n+p), N.nm.path(ss)) : {Done{N.AmlNameL{N.AmlName{False{}, 1n+p, ss}, R}} == N.nm.dec(B.append(_, R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
              %mask_carets(1n+p) : {Done{N.AmlNameL{N.AmlName{False{}, 1n+p, ss}, R}} == N.nm.dec(B.append(B.append(_, B.mask(N.nm.path(ss))), R)) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
              %app_assoc(N.nm.carets(1n+p), B.mask(N.nm.path(ss)), R) : {Done{N.AmlNameL{N.AmlName{False{}, 1n+p, ss}, R}} == N.nm.dec(_) : Result<&2, &2, E.AcpiError, N.AmlNameL>}
              ups_rt(1n+p, ss, R, and_l(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok), and_r(N.AmlName.segs_ok(ss), Nat.is_lt(N.nm.len(ss), 256n), ok))

Uses (29):
  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=List
  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_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=and_l
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=and_r
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=app_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=ft_absurd
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=mask_app
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=mask_carets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=pth_dec
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=pth_dpath
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/PROOF.bend&name=ups_rt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=AmlName
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=AmlName.segs_ok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=AmlName.valid
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=AmlNameL
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=nm.carets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=nm.dec
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=nm.enc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=nm.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=nm.named
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_name.bend&name=nm.path
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/error.bend&name=AcpiError
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=mask