def from_idem

bend-osdev-apparmor@0.1.0.0 · PROOF.bend:3483

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

3483def from_idem(+ys: List<&2, P.AaGrant>, +acc: V.AaAcc) -> {V.AaAcc.from(ys, V.AaAcc.from(ys, acc)) == V.AaAcc.from(ys, acc) : V.AaAcc}:
3484  Equal.trans(V.AaAcc, V.AaAcc.from(ys, V.AaAcc.from(ys, acc)), V.AaAcc.join(V.AaAcc.from(ys, acc), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, acc), from_join(ys, V.AaAcc.from(ys, acc)), Equal.trans(V.AaAcc, V.AaAcc.join(V.AaAcc.from(ys, acc), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.join(V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, acc), Equal.cong(V.AaAcc, V.AaAcc, x => V.AaAcc.join(x, V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, acc), V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), from_join(ys, acc)), Equal.trans(V.AaAcc, V.AaAcc.join(V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.join(acc, V.AaAcc.join(V.AaAcc.from(ys, V.AaAcc.empty()), V.AaAcc.from(ys, V.AaAcc.empty()))), V.AaAcc.from(ys, acc), acc.join_assoc(acc, V.AaAcc.from(ys, V.AaAcc.empty()), V.AaAcc.from(ys, V.AaAcc.empty())), Equal.trans(V.AaAcc, V.AaAcc.join(acc, V.AaAcc.join(V.AaAcc.from(ys, V.AaAcc.empty()), V.AaAcc.from(ys, V.AaAcc.empty()))), V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, acc), Equal.cong(V.AaAcc, V.AaAcc, x => V.AaAcc.join(acc, x), V.AaAcc.join(V.AaAcc.from(ys, V.AaAcc.empty()), V.AaAcc.from(ys, V.AaAcc.empty())), V.AaAcc.from(ys, V.AaAcc.empty()), acc.join_idem(V.AaAcc.from(ys, V.AaAcc.empty()))), Equal.sym(V.AaAcc, V.AaAcc.from(ys, acc), V.AaAcc.join(acc, V.AaAcc.from(ys, V.AaAcc.empty())), from_join(ys, acc))))))