PROOF.dbs.law: def of bend-osdev-apparmor@0.1.0.0
Import: import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
Lines 3788-3795 of bend-osdev-apparmor@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&start_line=3788&end_line=3795

import Base
import bend-osdev-apparmor@0.1.0.0/options.bend as O
import bend-osdev-apparmor@0.1.0.0/profile.bend as PR
import bend-osdev-apparmor@0.1.0.0/eval.bend as V
import bend-osdev-apparmor@0.1.0.0/rule_dbus.bend as RD

def dbs.law(+opts: O.AaOptions, +p: PR.AaProfile, +r: PR.AaRules, +q: RD.AaDbusQuery) -> {V.AaEval.dbus(opts, PR.AaProfile.include(PR.AaProfile.include(p, r), r), q) == V.AaEval.dbus(opts, PR.AaProfile.include(p, r), q) : V.AaDecision}:
  match p:
    case PR.AaProfile{n, a, f, r0, c, h}:
      match r0:
        case PR.AaRules{f0, c0, n0, s0, p0, m0, d0, x0}:
          match r:
            case PR.AaRules{f1, c1, n1, s1, p1, m1, d1, x1}:
              dbs.inc(opts, f, RD.AaDbusQuery.req(q), d0, d1, q)

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&name=dbs.inc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/eval.bend&name=AaDecision
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/eval.bend&name=AaEval.dbus
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/options.bend&name=AaOptions
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/profile.bend&name=AaProfile
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/profile.bend&name=AaProfile.include
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/profile.bend&name=AaRules
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/rule_dbus.bend&name=AaDbusQuery
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-apparmor@0.1.0.0/rule_dbus.bend&name=AaDbusQuery.req