PROOFRsdp.ckr.vr: def of bend-osdev-acpi@0.1.2.0
Import: import bend-osdev-acpi@0.1.2.0/PROOF_rsdp.bend as PROOFRsdp
Lines 51-60 of bend-osdev-acpi@0.1.2.0/PROOF_rsdp.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_rsdp.bend&start_line=51&end_line=60

import Base
import bend-osdev-bytes@0.1.1.1/bytes.bend as B
import bend-osdev-bytes@0.1.1.1/LAWS.bend as BL
import bend-osdev-acpi@0.1.2.0/fields.bend as F
import bend-osdev-acpi@0.1.2.0/rsdp.bend as P

def ckr.vr(+oem: B.Octets, +oem6: {B.Octets.len(oem) == 6n : Nat}, +rev: U32, +rsdt: U32) -> {B.Octets.concat([P.AcpiRsdp.signature(), B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)]) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}:
  %Equal.sym(B.Octets, B.Octets.concat(Con{P.AcpiRsdp.signature(), [B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)]}), B.Octets.append(P.AcpiRsdp.signature(), B.Octets.concat([B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)])), BL.octets_concat_cons(P.AcpiRsdp.signature(), [B.Octets.of_list([0]), F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)])) : {_ == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.of_list([0]), [F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)]}), B.Octets.append(B.Octets.of_list([0]), B.Octets.concat([F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)])), BL.octets_concat_cons(B.Octets.of_list([0]), [F.AcpiF.fit(6n, oem), B.Octets.of_list([rev]), B.Octets.le32(rsdt)])) : {B.Octets.append(P.AcpiRsdp.signature(), _) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.concat(Con{F.AcpiF.fit(6n, oem), [B.Octets.of_list([rev]), B.Octets.le32(rsdt)]}), B.Octets.append(F.AcpiF.fit(6n, oem), B.Octets.concat([B.Octets.of_list([rev]), B.Octets.le32(rsdt)])), BL.octets_concat_cons(F.AcpiF.fit(6n, oem), [B.Octets.of_list([rev]), B.Octets.le32(rsdt)])) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), _)) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.of_list([rev]), [B.Octets.le32(rsdt)]}), B.Octets.append(B.Octets.of_list([rev]), B.Octets.concat([B.Octets.le32(rsdt)])), BL.octets_concat_cons(B.Octets.of_list([rev]), [B.Octets.le32(rsdt)])) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(F.AcpiF.fit(6n, oem), _))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.le32(rsdt), Nil{}}), B.Octets.append(B.Octets.le32(rsdt), B.Octets.concat(Nil{})), BL.octets_concat_cons(B.Octets.le32(rsdt), Nil{})) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(F.AcpiF.fit(6n, oem), B.Octets.append(B.Octets.of_list([rev]), _)))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.concat(Nil{}), B.Octets.empty(), BL.octets_concat_nil()) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(F.AcpiF.fit(6n, oem), B.Octets.append(B.Octets.of_list([rev]), B.Octets.append(B.Octets.le32(rsdt), _))))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.append(B.Octets.le32(rsdt), B.Octets.empty()), B.Octets.le32(rsdt), BL.octets_append_empty_r(B.Octets.le32(rsdt))) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(F.AcpiF.fit(6n, oem), B.Octets.append(B.Octets.of_list([rev]), _)))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
  %Equal.sym(B.Octets, F.AcpiF.fit(6n, oem), oem, ckr.fit(oem, oem6)) : {B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(_, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) == B.Octets.append(P.AcpiRsdp.signature(), B.Octets.append(B.Octets.of_list([0]), B.Octets.append(oem, B.Octets.append(B.Octets.of_list([rev]), B.Octets.le32(rsdt))))) : B.Octets}
  {==}

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_rsdp.bend&name=ckr.fit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/fields.bend&name=AcpiF.fit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/rsdp.bend&name=AcpiRsdp.signature
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/LAWS.bend&name=octets_append_empty_r
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/LAWS.bend&name=octets_concat_cons
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/LAWS.bend&name=octets_concat_nil
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.concat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.empty
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.le32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.of_list