bend-osdev-apparmor

Search uses release 0.1.0.0 · 1,104 definitions

Releases (1)

0.1.0.0 indexed

Definitions (1,104)

LAWS.bend

PROOF.bend

def b.or_assoc
def b.or_false_r
def b.and_false_r
def b.and_true_r
def b.factor(p and n and f) or (p and q) is p and ((n and f) or q)
def b.disc
def b.ft
def b.absurd
def b.absurd_tf
def fethe pieces d fit the tokens r after an empty first piece
def fe_any
def fa_app
def fe_app
def ef_charan empty first piece: no single-byte token fits it
def ef_any
def ef_class
def ef_star...
def ef_star2
def gr_chara first piece that starts with h: a single-byte token takes h and leaves an empty piece
def gr_any
def gr_class
def gr_star...
def gr_star2...
def fe_efcutting into one more piece and asking for an empty first piece is cutting into as many
def fe_gr
def fe_cuts
def glob.thmthe matcher agrees with the list model: induction on the sequence, and on the path under a star
def nfa.taut_nil
def nfa.taut_adv
def nfa.taut_star
def nfa.taut_star2
def nfa.stepone byte: the positions after it accept t exactly when, before it, the positions (with the carried ones) accept h then t
def nfa.deadno position active: nothing accepted
def nfa.runthe run: the positions accept the path (a: whether some position is active)
def nfa.falses_dead
def nfa.startonly the whole sequence active: what the backtracking matcher accepts
def nfa.start_alive
def nfa.thm
def glob.alts
def glob.alts_ref
def bits.minus_meetswhat minus leaves never meets what it took away
def bits.nany_meetsa request with no bit set meets nothing
def bits.covers_meetsa request that minus(a, d) covers does not meet d
def bits.or_assoc
def b.or_idem
def bits.or_idem
def bits.or_nil_r
def pm.covers_meets
def pm.minus_meets