PROOFWhole.ckw.gfix: def of bend-osdev-acpi@0.1.2.0
Import: import bend-osdev-acpi@0.1.2.0/PROOF_whole.bend as PROOFWhole
Lines 141-154 of bend-osdev-acpi@0.1.2.0/PROOF_whole.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_whole.bend&start_line=141&end_line=154

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-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-acpi@0.1.2.0/checksum.bend as C

def ckw.gfix(+i: Nat, +p: B.Octets, +q: U32, +rest: B.Octets, +hp: {B.Octets.len(p) == i : Nat}) -> {C.AcpiChecksum.fix(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}:
  %Equal.sym(Bool, Nat.is_lt(i, B.Octets.len(B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))), True{}, ckw.glt(i, p, q, rest, hp)) : {C.ck.fix.pick(_, i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), [B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]}), B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.concat([B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))])), BL.octets_concat_cons(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), [B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))])) : {_ == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), [B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]}), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.concat([B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))])), BL.octets_concat_cons(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), [B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))])) : {B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), _) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.concat(Con{B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), Nil{}}), B.Octets.append(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.concat(Nil{})), BL.octets_concat_cons(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), Nil{})) : {B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), _)) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.concat(Nil{}), B.Octets.empty(), BL.octets_concat_nil()) : {B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.append(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), _))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.append(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.empty()), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), BL.octets_append_empty_r(B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))))) : {B.Octets.append(B.Octets.take(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), _)) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
  %hp : {B.Octets.append(B.Octets.take(_, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.take(B.Octets.len(p), B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), p, BL.octets_take_append(p, B.Octets.append(B.Octets.of_list([q]), rest))) : {B.Octets.append(_, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(1n+i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
  %Equal.trans(Nat, Nat.add(B.Octets.len(p), 1n), Nat.add(i, 1n), Nat.add(1n, i), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), B.Octets.len(p), i, hp), UL.nat_add_comm(i, 1n)) : {B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(_, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.drop(Nat.add(B.Octets.len(p), 1n), B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), B.Octets.drop(1n, B.Octets.append(B.Octets.of_list([q]), rest)), BL.octets_drop_append_add(p, 1n, B.Octets.append(B.Octets.of_list([q]), rest))) : {B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), _)) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
  %BL.octets_len_of_list([q]) : {B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), B.Octets.drop(_, B.Octets.append(B.Octets.of_list([q]), rest)))) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
  %Equal.sym(B.Octets, B.Octets.drop(B.Octets.len(B.Octets.of_list([q])), B.Octets.append(B.Octets.of_list([q]), rest)), rest, BL.octets_drop_append(B.Octets.of_list([q]), rest)) : {B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), _)) == B.Octets.append(p, B.Octets.append(B.Octets.of_list([C.AcpiChecksum.byte_for(i, B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))]), rest)) : B.Octets}
  {==}

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=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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.add
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/PROOF_whole.bend&name=ckw.glt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/checksum.bend&name=AcpiChecksum.byte_for
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/checksum.bend&name=AcpiChecksum.fix
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-acpi@0.1.2.0/checksum.bend&name=ck.fix.pick
  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/LAWS.bend&name=octets_drop_append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/LAWS.bend&name=octets_drop_append_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/LAWS.bend&name=octets_len_of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/LAWS.bend&name=octets_take_append
  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.drop
  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.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.take
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_comm