def inc.acc
bend-osdev-apparmor@0.1.0.0 · PROOF.bend:3493
import bend-osdev-apparmor@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-apparmor@0.1.0.0/perm.bend as P
import bend-osdev-apparmor@0.1.0.0/eval.bend as V
3493def inc.acc(+g0: List<&2, P.AaGrant>, +g1: List<&2, P.AaGrant>) -> {V.AaAcc.of(P.AaGrant.append(P.AaGrant.append(g0, g1), g1)) == V.AaAcc.of(P.AaGrant.append(g0, g1)) : V.AaAcc}:
3494 Equal.trans(V.AaAcc, V.AaAcc.from(P.AaGrant.append(P.AaGrant.append(g0, g1), g1), V.AaAcc.empty()), V.AaAcc.from(g1, V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty())), V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), from_app(P.AaGrant.append(g0, g1), g1, V.AaAcc.empty()), Equal.trans(V.AaAcc, V.AaAcc.from(g1, V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty())), V.AaAcc.from(g1, V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty()))), V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), Equal.cong(V.AaAcc, V.AaAcc, x => V.AaAcc.from(g1, x), V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty())), from_app(g0, g1, V.AaAcc.empty())), Equal.trans(V.AaAcc, V.AaAcc.from(g1, V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty()))), V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty())), V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), from_idem(g1, V.AaAcc.from(g0, V.AaAcc.empty())), Equal.sym(V.AaAcc, V.AaAcc.from(P.AaGrant.append(g0, g1), V.AaAcc.empty()), V.AaAcc.from(g1, V.AaAcc.from(g0, V.AaAcc.empty())), from_app(g0, g1, V.AaAcc.empty())))))