mb automata 2 Sections GenAutomata Doc

Def l1 = l2 == Case(l1) Case ptn_atom(x) = > Case(l2) Case ptn_atom(y) = > x=yAtom Default = > false Case ptn_int(x) = > Case(l2) Case ptn_int(y) = > x=y Default = > false Case ptn_var(x) = > Case(l2) Case ptn_var(y) = > x=yAtom Default = > false Case ptn_pr( < x, y > ) = > Case(l2) Case ptn_pr( < u, v > ) = > x = uy = v Default = > false Default = > false (recursive)

is mentioned by

Def smts_eff(ss;x) == smt_terms( < s ss | s.lbl = x > )[smts_eff]
Def action_effect(a;es;fs) == < e.smt | e < e es | e.kind = a > > + < mk_smt(f.var, f.var, f.typ) | f < f fs | a f.acts > > [action_effect]
Def dec_lookup(ds;x) == < d.typ | d < d ds | d.lbl = x > > [dec_lookup]
Def eq_relname(a;b) == Case(a) Case eq(x) = > Case(b) Case eq(x') = > st_eq(x;x') Case x' = > false Default = > false Case x = > Case(b) Case eq(x') = > false Case x' = > x = x' Default = > false Default = > false[eq_relname]
Def term_mentions_guard(g;t) == term_iterate(x.false;x.false;x.false;x.false;x.x = g;x,y. x y;t)[term_mentions_guard]
Def action_pre(a;ps) == < p.rel | p < p ps | p.kind = a > > [action_pre]
Def covers_var(A;x) == fr:frame(). fr < fr A.frame | fr.var = x > & (a:Label. (a fr.acts) (ef:eff(). ef < ef A.eff | ef.kind = a & ef.smt.lbl = x > ))[covers_var]

In prior sections: mb basic mb label mb automata 1 mb declaration

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc