PROOF.outcome_steps: def of bend-osdev-acpi@0.1.1.0
Import: import bend-osdev-acpi@0.1.1.0/PROOF.bend as PROOF
Lines 2538-2548 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=2538&end_line=2548

import Base
import bend-osdev-acpi@0.1.1.0/aml_host.bend as Hs
import bend-osdev-acpi@0.1.1.0/aml_interp.bend as I
import bend-osdev-acpi@0.1.1.0/aml.bend as A

# an outcome counts the steps of its run
def outcome_steps(+r: I.AmlRun<Hs.AmlMemHost>) -> {I.AmlRun.steps(Hs.AmlMemHost, r) == A.AmlOutcome.steps(Hs.AmlMemHost, A.AmlOutcome.of_run(Hs.AmlMemHost, r)) : Nat}:
  match r:
    case I.AmlRun{m, s}:
      match m:
        case I.AmlMachine{md, c, fs, w}:
          match w:
            case I.AmlWorld{ctx, ns, h, e}:
              match e:
                case I.AmlEnv{wd, o, nts, d, cl}:
                  {==}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml.bend&name=AmlOutcome.of_run
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml.bend&name=AmlOutcome.steps
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_host.bend&name=AmlMemHost
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_interp.bend&name=AmlEnv
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_interp.bend&name=AmlMachine
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_interp.bend&name=AmlRun
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_interp.bend&name=AmlRun.steps
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.1.0/aml_interp.bend&name=AmlWorld