def ckw.glt

bend-osdev-acpi@0.1.2.0 · PROOF_whole.bend:134

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

134def ckw.glt(+i: Nat, +p: B.Octets, +q: U32, +rest: B.Octets, +hp: {B.Octets.len(p) == i : Nat}) -> {Nat.is_lt(i, B.Octets.len(B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest)))) == True{} : Bool}:
135  %Equal.sym(Nat, B.Octets.len(B.Octets.append(p, B.Octets.append(B.Octets.of_list([q]), rest))), Nat.add(B.Octets.len(p), B.Octets.len(B.Octets.append(B.Octets.of_list([q]), rest))), BL.octets_len_append(p, B.Octets.append(B.Octets.of_list([q]), rest))) : {Nat.is_lt(i, _) == True{} : Bool}
136  %Equal.sym(Nat, B.Octets.len(p), i, hp) : {Nat.is_lt(i, Nat.add(_, B.Octets.len(B.Octets.append(B.Octets.of_list([q]), rest)))) == True{} : Bool}
137  %Equal.sym(Nat, B.Octets.len(B.Octets.append(B.Octets.of_list([q]), rest)), Nat.add(B.Octets.len(B.Octets.of_list([q])), B.Octets.len(rest)), BL.octets_len_append(B.Octets.of_list([q]), rest)) : {Nat.is_lt(i, Nat.add(i, _)) == True{} : Bool}
138  %Equal.sym(Nat, B.Octets.len(B.Octets.of_list([q])), B.len([q]), BL.octets_len_of_list([q])) : {Nat.is_lt(i, Nat.add(i, Nat.add(_, B.Octets.len(rest)))) == True{} : Bool}
139  ckw.ltadd(i, B.Octets.len(rest))