Def | | switch_inv(E; tr) | [switch_inv2001_03_15_DASH_PM_DASH_12_53_21] | mb hybrid |
Def | | x R_del(E) y | [R_del] | mb hybrid |
Def | | tTop | [st_top] | mb automata 1 |
Def | | relname_eq(x) | [relname_eq] | mb automata 1 |
Def | | relname_other(x) | [relname_other] | mb automata 1 |
Def | | outl(x) | [outl] | union |
Def | | outr(x) | [outr] | union |
Def | | fappend(f;n;x) | [fappend] | mb nat |
Def | | ... | [hide] | mb basic |
Def | | ptn_int(x) | [ptn_int] | mb basic |
Def | | ptn_var(x) | [ptn_var] | mb basic |
Def | | const_ptn(l) | [const_ptn] | mb basic |
Def | | int_ptn(l) | [int_ptn] | mb basic |
Def | | var_ptn(l) | [var_ptn] | mb basic |
Def | | left_ptn(l) | [left_ptn] | mb basic |
Def | | right_ptn(l) | [right_ptn] | mb basic |
Def | | StAntiSym(T;x,y.R(x;y)) | [st_anti_sym] | rel 1 |
Def | | Irrefl(T;x,y.E(x;y)) | [irrefl] | rel 1 |
Def | | left_child(t) | [left_child] | mb tree |
Def | | right_child(t) | [right_child] | mb tree |
Def | | leaf_value(t) | [leaf_value] | mb tree |
Def | | Default = > body
EndSwitch | [switch_default] | prog 1 |
Def | | < x,y > = >
body(x;y) | [case_pair] | prog 1 |
Def | | x::y = >
body(x;y)
cont | [case_cons] | prog 1 |
Def | | [] = >
body
cont | [case_nil] | prog 1 |
Def | | = >
body | [case_it] | prog 1 |
Def | | x:body | [case_bind] | prog 1 |
Def | | < < "a", b > , c, 1 > = >
body(b;c)
cont | [case_pattern1] | prog 1 |
Def | | < a, inl < < "a", b > , c, 1 > > = >
body(a;b;c)
cont | [case_pattern2] | prog 1 |
Def | | < a, inl < < "a", b > , c, 1 > > | [pattern2] | prog 1 |
Def | | union1() | [union1] | prog 1 |
Def | | union1_term1(x) = >
body(x)
cont | [case_union1_term1] | prog 1 |
Def | | union1_term1(x) | [union1_term1] | prog 1 |
Def | | union1_term2(x) = >
body(x)
cont | [case_union1_term2] | prog 1 |
Def | | union1_term2(x) | [union1_term2] | prog 1 |
Def | | union1_term3(x) = >
body(x)
cont | [case_union1_term3] | prog 1 |
Def | | union1_term3(x) | [union1_term3] | prog 1 |
Def | | enum1_switch(value;el1;el2;el3) | [enum1_switch] | prog 1 |
Def | | enum1_el1 = >
body
cont | [case_enum1_el1] | prog 1 |
Def | | enum1_el2 = >
body
cont | [case_enum1_el2] | prog 1 |
Def | | enum1_el3 = >
body
cont | [case_enum1_el3] | prog 1 |
Def | | module1_type(prop) | [module1_type] | prog 1 |
Def | | t.tag | [module1_tag] | prog 1 |
Def | | t.data | [module1_data] | prog 1 |
Def | | module1(tag, data) = >
body(tag;data) | [case_module1] | prog 1 |
Def | | module1(tag, data) | [module1] | prog 1 |
Def | | For{T,op,id} x as. f(x) | [for] | list 1 |
Def | | ForHdTl{A,f,k} h::t as. g(h;t) | [for_hdtl] | list 1 |
Def | | mapc(f) | [mapc] | list 1 |
Def | | p q | [bxor] | bool 1 |
Def | | p  q | [rev_bimplies] | bool 1 |
Def | | i j k | [lele] | int 1 |
Def | | S T | [suptype] | int 1 |
Def | | t ...$L | [label] | core |
Def | | ??? | [error] | core |
Def | | I | [icomb] | core |
Def | | K | [kcomb] | core |
Def | | S | [scomb] | core |
Def | | let x,y,z = a in t(x;y;z) | [spread3] | core |
Def | | let w,x,y,z = a in t(w;x;y;z) | [spread4] | core |
Def | | let a,b,c,d,e = u in v(a;b;c;d;e) | [spread5] | core |
Def | | let a,b,c,d,e,f = u in v(a;b;c;d;e;f) | [spread6] | core |
Def | | let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g) | [spread7] | core |
Def | | XM | [xmiddle] | core |
Def | | [x]{T} | [type_inj] | core |
Def | | rel_arg_typ(rn;i;de) | [rel_arg_typ] | mb automata 1 |
Def | | trace_env(d) | [trace_env] | mb automata 1 |
Def | | [[s]] rho | [sig_mng] | mb automata 3 |
Def | | sig() | [sig] | mb automata 2 |
Def | | subst_mentions_trace(as) | [subst_mentions_trace] | mb automata 3 |
Def | | {p} | [record_pair] | mb record |
Def | | r | [pred_rel] | mb automata 1 |
Def | | closed_pred(p) | [closed_pred] | mb automata 3 |
Def | | c1 = c2 | [col_equal] | mb collection |
Def | | (P)' | [pred_addprime] | mb automata 3 |
Def | | pred_unprime(P) | [pred_unprime] | mb automata 3 |
Def | | c1 c2 | [col_le] | mb collection |
Def | | [[A]] rho de e | [ioa_mng] | mb automata 4 |
Def | | ioa_all(I; i.A(i)) | [ioa_all] | mb automata 1 |
Def | | ioa{i:l}() | [ioa] | mb automata 3 |
Def | | ioa_mentions_trace(A) | [ioa_mentions_trace] | mb automata 3 |
Def | | wp_rel(A;a;r) | [wp_rel] | mb automata 4 |
Def | | wp2_rel(A;a;r) | [wp2_rel] | mb automata 3 |
Def | | pred_mng_2(p; rho; ds; da; de; e; s; s'; a; tr) | [pred_mng_2] | mb automata 3 |
Def | | wp2(A;a;Q) | [wp2] | mb automata 3 |
Def | | tc_ioa(A;de) | [tc_ioa] | mb automata 4 |
Def | | single_valued_decls(c) | [single_valued_decls] | mb automata 2 |
Def | | rel_eq(a;b) | [rel_eq] | mb automata 3 |
Def | | sm{i:l}() | [sm] | mb state machine |
Def | | covers_rel(A;r) | [covers_rel] | mb automata 2 |
Def | | wp(A;a;Q) | [wp] | mb automata 4 |
Def | | trace_consistent_vc(rho;da;R;v) | [trace_consistent_vc] | mb automata 4 |
Def | | covers_pred(A;p) | [covers_pred] | mb automata 3 |
Def | | tc_vcs{i}(vs;ds;da;de) | [tc_vcs] | mb automata 4 |
Def | | VCs | [vcs] | mb automata 2 |
Def | | [[vs]] rho ds da de e s tr | [vcs_mng] | mb automata 4 |
Def | | VCs(A;I) | [ioa_inv_vc] | mb automata 4 |
Def | | guarded_trace(da;e;I) | [guarded_trace] | mb automata 3 |
Def | | (M |= always s,t.P(s;t)) | [trace_inv] | mb state machine |
Def | | let x = a in b(x) | [let] | core |
Def | | closed_term(t) | [closed_term] | mb automata 2 |
Def | | unzip(as) | [unzip] | mb list 1 |
Def | | a b | [arrow] | mb automata 1 |
Def | | SQType(T) | [sq_type] | sqequal 1 |
Def | | tc1(r;de) | [tc1] | mb automata 1 |
Def | | No-dup-send(E) | [no_duplicate_send] | mb structures |
Def | | EventStruct | [event_str] | mb structures |
Def | | (L -msg(a;b) L1) | [remove_msgs] | mb hybrid |
Def | | ( x L.P(x)) | [l_exists] | mb list 2 |
Def | | Tag-by-msg(E) | [P_tag_by_msg] | mb hybrid |
Def | | TaggedEventStruct | [tagged_event_str] | mb structures |
Def | | PTrue | [PTrue] | mb hybrid |
Def | | I fuses P | [fusion_condition] | mb hybrid |
Def | | R_ad_normal(tr) | [R_ad_normal] | mb hybrid |
Def | | R_strong_safety(E) | [R_strong_safety] | mb hybrid |
Def | | P Q | [prop_and] | mb nat |
Def | | Structure | [struct] | mb structures |
Def | | TraceProperty(E) | [trace_property] | mb hybrid |
Def | | tag_splitable(E;R) | [tag_splitable] | mb structures |
Def | | totalorder(E) | [totalorder] | mb hybrid |
Def | | single-tag-decomposable(E) | [single_tag_decomposable] | mb hybrid |
Def | | switch-decomposable(E) | [switch_decomposable] | mb hybrid |
Def | | AD-normal(E) | [switch_normal] | mb hybrid |
Def | | MCS(E) | [memoryless_composable_safety] | mb hybrid |
Def | | R_permutation(E) | [R_permutation] | mb hybrid |
Def | | R^-1 | [rel_inverse] | mb nat |
Def | | switchR(tr) | [switch_inv_rel] | mb hybrid |
Def | | local_deliver_property(E;P) | [local_deliver_property] | mb hybrid |
Def | | switchable0(E) | [switchable0] | mb hybrid |
Def | | switchable(E) | [b_switchable] | mb hybrid |
Def | | adR(E) | [R_ad] | mb hybrid |
Def | | P o evt | [compose_map] | mb structures |
Def | | induced_event_str(E;A;f) | [induced_event_str] | mb structures |
Def | | full_switch_inv(E;A;evt;tg;tr_u;tr_l) | [full_switch_inv] | mb hybrid |
Def | | interleaving(T;L1;L2;L) | [interleaving] | mb list 2 |
Def | | null(as) | [null] | list 1 |
Def | | last(L) | [last_RENAMED] | mb list 1 |
Def | | compose_flips(L) | [compose_flips] | mb list 2 |
Def | | x before y l | [l_before] | mb list 1 |
Def | | guarded_permutation(T;P) | [guarded_permutation] | mb list 2 |
Def | | Bij(A; B; f) | [biject] | fun 1 |
Def | | count(x < y in L | P(x;y)) | [count_pairs] | mb list 1 |
Def | | i:I
M(i) | [sm_all] | mb state machine |
Def | | (f o M) | [sm_a_rename] | mb state machine |
Def | | (M |= initially x,tr.P(x;tr)) | [initially] | mb state machine |
Def | | (M |= x,tr.P(x;tr) while Q(x;tr)) | [while] | mb state machine |
Def | | {i...j} | [int_iseg] | int 1 |
Def | | i j | [ge] | core |
Def | | A List | [listp] | mb list 1 |
Def | | sublist_occurence(T;L1;L2;f) | [sublist_occurence] | mb list 1 |
Def | | interleaving_occurence(T;L1;L2;L;f1;f2) | [interleaving_occurence] | mb list 1 |
Def | |   | [nat_plus] | int 1 |
Def | | i = j | [pm_equal] | int 2 |
Def | | |i| | [absval] | int 2 |
Def | | Preorder(T;x,y.R(x;y)) | [preorder] | rel 1 |
Def | | gcd(a;b) | [gcd] | num thy 1 |
Def | |  x:A. B(x) | [sq_exists] | core |
Def | | CoPrime(a,b) | [coprime] | num thy 1 |
Def | | SqStable(P) | [sq_stable] | core |
Def | | atomic(a) | [atomic] | num thy 1 |
Def | | prime(a) | [prime] | num thy 1 |
Def | | a = b mod m | [eqmod] | num thy 1 |
Def | | fib(n) | [fib] | num thy 1 |
Def | | isl(x) | [isl] | union |
Def | | nondecreasing(f;k) | [nondecreasing] | mb nat |
Def | | fadd(f;g) | [fadd] | mb nat |
Def | | R1 = > R2 | [rel_implies] | mb nat |
Def | | f^n | [fun_exp] | mb nat |
Def | | search(k;P) | [search] | mb nat |
Def | | dec2bool(d) | [dec2bool] | mb basic |
Def | | Decision | [decision] | mb basic |
Def | | Symmetrize(x,y.R(x;y);a;b) | [symmetrize] | rel 1 |
Def | | IsEqFun(T;eq) | [eqfun_p] | rel 1 |
Def | | strict_part(x,y.R(x;y);a;b) | [strict_part] | rel 1 |
Def | | Linorder(T;x,y.R(x;y)) | [linorder] | rel 1 |
Def | | is_leaf(t) | [is_leaf] | mb tree |
Def | | enum1() | [enum1] | prog 1 |
Def | | rev(as) | [reverse] | list 1 |
Def | | as[m..n ] | [segment] | list 1 |
Def | | as\[i] | [reject] | list 1 |
Def | | f{m..n } | [listify] | list 1 |
Def | | A List(n) | [list_n] | list 1 |
Def | | i > j | [gt] | core |
Def | | {...i} | [int_lower] | int 1 |
Def | | imin(a;b) | [imin] | int 2 |
Def | | a -- b | [ndiff] | int 2 |
Def | | Rem(a;n;r) | [rem_nrel] | int 2 |
Def | | a mod n | [modulus] | int 2 |
Def | | a  n | [div_floor] | int 2 |
Def | | WellFnd{i}(A;x,y.R(x;y)) | [wellfounded] | well fnd |
Def | | {i...} | [int_upper] | int 1 |
Def | | b2i(b) | [b2i] | bool 1 |
Def | | p= q | [eq_bool] | bool 1 |
Def | | A ~~ B | [one_one_corr] | fun 1 |
Def | | Stable{P} | [stable] | core |
Def | | {a:T} | [singleton] | core |
Def | | {!x:T | P(x)} | [unique_set] | core |
Def | | a = !x:T. Q(x) | [uni_sat] | core |
Def | | tc_vc(v;ds;da;de) | [tc_vc] | mb automata 4 |
Def | | tc_pred(P;ds;da;de) | [tc_pred] | mb automata 4 |
Def | | tc(r;ds;da;de) | [tc] | mb automata 3 |
Def | | tc_eff(ef;ds;de) | [tc_eff] | mb automata 4 |
Def | | tc_smt(s;ds;da;de) | [tc_smt] | mb automata 3 |
Def | | vc_mng(v;rho;ds;da;de;e;s;tr) | [vc_mng] | mb automata 4 |
Def | | term_types(ds;da;de;t) | [term_types] | mb automata 3 |
Def | | dec_lookup(ds;x) | [dec_lookup] | mb automata 2 |
Def | | [[p]] rho ds da de e s a tr | [pred_mng] | mb automata 3 |
Def | | trace_consistent_pred(rho;da;R;p) | [trace_consistent_pred] | mb automata 4 |
Def | | trace_consistent_rel(rho;da;R;r) | [trace_consistent_rel] | mb automata 3 |
Def | | trace_consistent(rho;da;R;t) | [trace_consistent] | mb automata 3 |
Def | | [[ds]] rho | [decls_mng] | mb automata 3 |
Def | | ioa_trans_all{i}(A;I) | [ioa_trans_all] | mb automata 4 |
Def | | ioa_trans(A;a;I) | [ioa_trans] | mb automata 4 |
Def | | smts_eff_pred(ss;p) | [smts_eff_pred] | mb automata 4 |
Def | | smts_eff_rel(ss;r) | [smts_eff_rel] | mb automata 3 |
Def | | st_app(c1;c2) | [st_app] | mb automata 2 |
Def | | ( x c.f(x)) | [col_accum] | mb collection |
Def | | [[sts]] rho | [sts_mng] | mb automata 2 |
Def | | action_effect(a;es;fs) | [action_effect] | mb automata 2 |
Def | | ( x c.P(x)) | [col_all] | mb collection |
Def | | action_pre(a;ps) | [action_pre] | mb automata 2 |
Def | | P Q | [pred_and] | mb automata 1 |
Def | | col_subst(c;r) | [col_subst] | mb automata 3 |
Def | | col_subst2(c;r) | [col_subst2] | mb automata 3 |
Def | | col_map_subst(x.f(x);c) | [col_map_subst] | mb automata 2 |
Def | | smts_eff(ss;x) | [smts_eff] | mb automata 2 |
Def | | smt_terms(c) | [smt_terms] | mb automata 2 |
Def | | < f(x) | x c > | [col_map] | mb collection |
Def | | a +* b | [vcs_add] | mb automata 2 |
Def | | covers_var(A;x) | [covers_var] | mb automata 2 |
Def | | pred_mentions(p;x) | [pred_mentions] | mb automata 2 |
Def | | col_list_prod(l) | [col_list_prod] | mb collection |
Def | | < x c | P(x) > | [col_filter] | mb collection |
Def | | a + b | [col_add] | mb collection |
Def | | i:I. C(i) | [col_union] | mb collection |
Def | | x c | [col_member] | mb collection |
Def | | P  Q | [implies] | core |
Def | | pre() | [pre] | mb automata 3 |
Def | | < *v* > | [vcs_singleton] | mb automata 2 |
Def | | vc{i:l}() | [vc] | mb automata 2 |
Def | | qimp{i:l}() | [qimp] | mb automata 2 |
Def | | imp{i:l}() | [imp] | mb automata 2 |
Def | | Fmla | [pred] | mb automata 1 |
Def | | rel() | [rel] | mb automata 2 |
Def | | x:A. B(x) | [all] | core |
Def | | t.typ | [eff_typ] | mb automata 1 |
Def | | frame() | [frame] | mb automata 2 |
Def | | eff() | [eff] | mb automata 2 |
Def | | dec() | [dec] | mb automata 2 |
Def | | smt() | [smt] | mb automata 2 |
Def | | st_app1(s1;s2) | [st_app1] | mb automata 2 |
Def | | relname() | [relname] | mb automata 2 |
Def | | SimpleType | [st] | mb automata 1 |
Def | | < x > | [col_singleton] | mb collection |
Def | | t.smt | [eff_smt] | mb automata 1 |
Def | | t.var | [frame_var] | mb automata 1 |
Def | | t.typ | [frame_typ] | mb automata 1 |
Def | | t.acts | [frame_acts] | mb automata 1 |
Def | | rel_mentions(r;x) | [rel_mentions] | mb automata 2 |
Def | | composableR(E) | [R_composable] | mb hybrid |
Def | | ( x L.P(x)) | [l_all] | mb list 2 |
Def | | agree_on_common(T;as;bs) | [agree_on_common] | mb list 1 |
Def | | (x l) | [l_member] | mb list 1 |
Def | | layerR(E) | [layer_rel] | mb hybrid |
Def | | R(tg) | [tag_rel] | mb hybrid |
Def | | R^* | [rel_star] | mb nat |
Def | |  | [nat] | int 1 |
Def | | sublist(T;L1;L2) | [sublist] | mb list 1 |
Def | | delayableR(E) | [R_delayable] | mb hybrid |
Def | | asyncR(E) | [R_async] | mb hybrid |
Def | | swap adjacent[P(x;y)] | [swap_adjacent] | mb list 2 |
Def | | C(Q) | [message_closure] | mb hybrid |
Def | | x somewhere delivered before y | [delivered_before_somewhere] | mb hybrid |
Def | | No-dup-deliver(E) | [P_no_dup] | mb hybrid |
Def | | Causal(E) | [P_causal] | mb hybrid |
Def | | switch_inv(E) | [switch_inv] | mb hybrid |
Def | | disjoint_sublists(T;L1;L2;L) | [disjoint_sublists] | mb list 1 |
Def | | increasing(f;k) | [increasing] | mb basic |
Def | | {i..j } | [int_seg] | int 1 |
Def | | Div(a;n;q) | [div_nrel] | int 2 |
Def | | i j < k | [lelt] | int 1 |
Def | | A B | [le] | core |
Def | | is-deliver(E)(x) | [event_is_deliver] | mb structures |
Def | | x delivered at time k | [delivered_at] | mb hybrid |
Def | | Dec(P) | [decidable] | core |
Def | | reducible(a) | [reducible] | num thy 1 |
Def | |    | [int_nzero] | int 1 |
Def | | a b | [nequal] | core |
Def | | A | [not] | core |
Def | | t.frame | [ioa_frame] | mb automata 1 |
Def | | t.term | [smt_term] | mb automata 1 |
Def | | [[r]] rho ds da de e s a tr | [rel_mng] | mb automata 3 |
Def | | [[t]] e s a tr | [term_mng] | mb automata 1 |
Def | | t.lbl | [smt_lbl] | mb automata 1 |
Def | | t.kind | [eff_kind] | mb automata 1 |
Def | | t.eff | [ioa_eff] | mb automata 1 |
Def | | rel_mng_2(r; rho; ds; da; de; e; s; s'; a; tr) | [rel_mng_2] | mb automata 3 |
Def | | [[t]] e s s' a tr | [term_mng2] | mb automata 2 |
Def | | tre.P | [tproj] | mb automata 1 |
Def | | tr | P | [trace_projection] | mb events |
Def | | kind(a) | [kind] | mb record |
Def | | t.kind | [pre_kind] | mb automata 1 |
Def | | t.pre | [ioa_pre] | mb automata 1 |
Def | | t.init | [ioa_init] | mb automata 1 |
Def | | t.ds | [ioa_ds] | mb automata 1 |
Def | | t.da | [ioa_da] | mb automata 1 |
Def | | tappend(tr;a) | [tappend] | mb automata 1 |
Def | | vc_hyp(v) | [vc_hyp] | mb automata 2 |
Def | | t.hyp | [qimp_hyp] | mb automata 2 |
Def | | t.lbl | [qimp_lbl] | mb automata 2 |
Def | | t.hyp | [imp_hyp] | mb automata 2 |
Def | | t.lbl | [dec_lbl] | mb automata 1 |
Def | | rel_unprime(r) | [rel_unprime] | mb automata 2 |
Def | | rel_subst(as;r) | [rel_subst] | mb automata 2 |
Def | | (r)' | [rel_addprime] | mb automata 2 |
Def | | rel_subst2(as;r) | [rel_subst2] | mb automata 2 |
Def | | t.name | [rel_name] | mb automata 1 |
Def | | t.fun | [sig_fun] | mb automata 1 |
Def | | term_subst(as;t) | [term_subst] | mb automata 2 |
Def | | term_subst2(as;t) | [term_subst2] | mb automata 2 |
Def | | apply_alist(as;l;d) | [apply_alist] | mb automata 1 |
Def | | tr delivered at p | [deliveries_at] | mb hybrid |
Def | | < A,evt,tg > (E) | [induced_tagged_event_str] | mb structures |
Def | | loc(E) | [event_loc] | mb structures |
Def | | memorylessR(E) | [R_memoryless] | mb hybrid |
Def | | =msg=(E) | [event_msg_eq] | mb structures |
Def | | < tr > _tg | [tag_sublist] | mb structures |
Def | | tag(E) | [event_tag] | mb structures |
Def | | send-enabledR(E) | [R_send_enabled] | mb hybrid |
Def | | is-send(E) | [event_is_snd] | mb structures |
Def | | Trace(E) | [str_trace] | mb structures |
Def | | safetyR(E) | [R_safety] | mb hybrid |
Def | | P refines Q | [tr_refines] | mb hybrid |
Def | | MessageStruct | [message_str] | mb structures |
Def | | |S| | [carrier] | mb structures |
Def | | msg(E) | [event_msg] | mb structures |
Def | | MS(E) | [event_msg_str] | mb structures |
Def | | t.trace | [trace_env_trace] | mb automata 1 |
Def | | =(M) | [msg_eq] | mb structures |
Def | | uid(MS) | [msg_id] | mb structures |
Def | | sender(MS) | [msg_sender] | mb structures |
Def | | content(MS) | [msg_content] | mb structures |
Def | | cEQ(MS) | [msg_content_eq] | mb structures |
Def | | =(DE) | [eq_dequiv] | mb structures |
Def | | (M |= x,x',tr,tr'.R(x;x';tr;tr')) | [tla] | mb state machine |
Def | | (M -tr- > s) | [reachable_via] | mb state machine |
Def | | trace_reachable(M;s;l;s') | [trace_reachable] | mb state machine |
Def | | M.state | [sm_state] | mb state machine |
Def | | t.ds | [sm_ds] | mb state machine |
Def | | M.action | [sm_action] | mb state machine |
Def | | t.da | [sm_da] | mb state machine |
Def | | t.init | [sm_init] | mb state machine |
Def | | 1of(t) | [pi1] | core |
Def | | [[rn]] rho e | [relname_mng] | mb automata 2 |
Def | | r.l | [r_select] | mb record |
Def | | t.typ | [smt_typ] | mb automata 1 |
Def | | [[l]] rho | [st_list_mng] | mb automata 2 |
Def | | [[d]] rho | [dec_mng] | mb automata 2 |
Def | | [[s]] rho | [st_mng] | mb automata 2 |
Def | | value(a) | [value] | mb record |
Def | | t.rel | [pre_rel] | mb automata 1 |
Def | | Term | [term] | mb automata 1 |
Def | | ( d) | [sigma] | mb record |
Def | | closed_rel(r) | [closed_rel] | mb automata 3 |
Def | | ts() | [ts] | mb automata 1 |
Def | | {d} | [record] | mb record |
Def | | Decl | [decl] | mb declaration |
Def | | d o f | [rename_decl] | mb declaration |
Def | | Label | [lbl] | mb label |
Def | | P & Q | [and] | core |
Def | | niltrace() | [niltrace] | mb automata 1 |
Def | |  | [it] | core |
Def | | < > | [col_none] | mb collection |
Def | | mk_sm(da, ds, init, trans) | [mk_sm] | mb state machine |
Def | | False | [false] | core |
Def | | vc_concl(v) | [vc_concl] | mb automata 2 |
Def | | rel_mentions_trace(r) | [rel_mentions_trace] | mb automata 3 |
Def | | mentions_trace(t) | [mentions_trace] | mb automata 2 |
Def | | termlist_eq(a;b) | [termlist_eq] | mb automata 2 |
Def | | eq_relname(a;b) | [eq_relname] | mb automata 2 |
Def | | rel_primed_vars(r) | [rel_primed_vars] | mb automata 3 |
Def | | term_primed_vars(t) | [term_primed_vars] | mb automata 2 |
Def | | affects_trace_rel(e;k;r) | [affects_trace_rel] | mb automata 3 |
Def | | affects_trace(e;k;t) | [affects_trace] | mb automata 2 |
Def | | rel_vars(r) | [rel_vars] | mb automata 2 |
Def | | term_vars(t) | [term_vars] | mb automata 1 |
Def | | iterate(statevar x- > v(x)
statevar x''- > v'(x')
funsymbol op- > opr(op)
freevar f- > fvar(f)
trace(tr)- > trace(tr)
a(b)- > comb(a;b)
over t) | [term_iter] | mb automata 2 |
Def | | rel_free_vars(r) | [rel_free_vars] | mb automata 2 |
Def | | term_mentions_guard(g;t) | [term_mentions_guard] | mb automata 2 |
Def | | term_eq(a;b) | [term_eq] | mb automata 2 |
Def | | (a=b) | [ts_eq] | mb automata 1 |
Def | | st_eq(s1;s2) | [st_eq] | mb automata 1 |
Def | | x ls | [lbls_member] | mb label |
Def | | x:y | [dbase] | mb declaration |
Def | | l1 = l2 | [eq_lbl] | mb basic |
Def | | unprime(t) | [unprime] | mb automata 2 |
Def | | term_free_vars(t) | [term_free_vars] | mb automata 2 |
Def | | (t)' | [addprime] | mb automata 2 |
Def | | term_iterate(v;
p;
op;
f;
tr;
a;
t) | [term_iterate] | mb automata 1 |
Def | | t_iterate(l;n;t) | [t_iterate] | mb tree |
Def | | ts_case(x)
var(a)= > v(a)
var'(b)= > p(b)
opr(f)= > op(f)
fvar(x)= > f(x)
trace(P)= > t(P)
end_ts_case | [ts_case] | mb automata 1 |
Def | | ground_ptn(p) | [ground_ptn] | mb basic |
Def | | Default = > body | [case_default] | prog 1 |
Def | | t.concl | [qimp_concl] | mb automata 2 |
Def | | Case vc_qimp(x) = >
body(x)
cont | [case_vc_qimp] | mb automata 2 |
Def | | t.concl | [imp_concl] | mb automata 2 |
Def | | t.proj | [trace_env_proj] | mb automata 1 |
Def | | mk_trace_env(trace, proj) | [mk_trace_env] | mb automata 1 |
Def | | Case vc_imp(x) = >
body(x)
cont | [case_vc_imp] | mb automata 2 |
Def | | Case(value)
body | [case] | prog 1 |
Def | | mk_dec(lbl, typ) | [mk_dec] | mb automata 1 |
Def | | mk_qimp(lbl, hyp, concl) | [mk_qimp] | mb automata 2 |
Def | | vc_qimp(x) | [vc_qimp] | mb automata 2 |
Def | | mk_imp(hyp, concl) | [mk_imp] | mb automata 2 |
Def | | vc_imp(x) | [vc_imp] | mb automata 2 |
Def | | false | [bfalse] | bool 1 |
Def | | t.args | [rel_args] | mb automata 1 |
Def | | t.rel | [sig_rel] | mb automata 1 |
Def | | t.typ | [dec_typ] | mb automata 1 |
Def | | t.trans | [sm_trans] | mb state machine |
Def | | 2of(t) | [pi2] | core |
Def | | p  q | [bimplies] | bool 1 |
Def | | p  q | [bor] | bool 1 |
Def | | (first x as s.t. P(x) else d) | [find] | mb list 1 |
Def | | filter(P;l) | [filter] | mb list 1 |
Def | | compose_list(L) | [compose_list] | mb list 1 |
Def | | reduce(f;k;as) | [reduce] | list 1 |
Def | | p q | [band] | bool 1 |
Def | | Collection(T) | [col] | mb collection |
Def | | $x | [clbl] | mb basic |
Def | | lbl_pr( < x, y > ) | [lbl_pair] | mb basic |
Def | | t | [typ] | mb automata 1 |
Def | | D(i) for i I | [dall] | mb declaration |
Def | | list_accum(x,a.f(x;a);y;l) | [list_accum] | mb list 1 |
Def | | l1 l2 | [iseg] | mb list 1 |
Def | | swap(L;i;j) | [swap] | mb list 2 |
Def | | (L o f) | [permute_list] | mb list 2 |
Def | | mklist(n;f) | [mklist] | mb list 1 |
Def | | as @ bs | [append] | list 1 |
Def | | zip(as;bs) | [zip] | mb list 1 |
Def | | map(f;as) | [map] | list 1 |
Def | | DecidableEquiv | [dequiv] | mb structures |
Def | | b | [assert] | bool 1 |
Def | | Case x = >
body(x)
cont | [case_relname_other] | mb automata 1 |
Def | | l[i] | [select] | list 1 |
Def | | ||as|| | [length] | list 1 |
Def | | A & B | [cand] | core |
Def | | Case eq(x) = >
body(x)
cont | [case_relname_eq] | mb automata 1 |
Def | | x:A. B(x) | [exists] | core |
Def | | P Q | [or] | core |
Def | | Case ts_trace(x) = >
body(x)
cont | [case_ts_trace] | mb automata 1 |
Def | | Case ts_fvar(x) = >
body(x)
cont | [case_ts_fvar] | mb automata 1 |
Def | | Case ts_op(x) = >
body(x)
cont | [case_ts_op] | mb automata 1 |
Def | | Case ts_pvar(x) = >
body(x)
cont | [case_ts_pvar] | mb automata 1 |
Def | | Case ptn_int(x) = >
body(x)
cont | [case_ptn_int] | mb basic |
Def | | Case ptn_var(x) = >
body(x)
cont | [case_ptn_var] | mb basic |
Def | | nth_tl(n;as) | [nth_tl] | list 1 |
Def | | tl(l) | [tl] | list 1 |
Def | | hd(l) | [hd] | list 1 |
Def | | inr(x) = >
body(x)
cont | [case_inr] | prog 1 |
Def | | True | [true] | core |
Def | | Case tree_leaf(x) = >
body(x)
cont | [case_tree_leaf] | mb tree |
Def | | Case x;y = >
body(x;y)
cont | [case_node] | mb tree |
Def | | Y | [ycomb] | core |
Def | | if b t else f fi | [ifthenelse] | bool 1 |
Def | | st_lift(rho) | [st_lift] | mb automata 1 |
Def | | t1 t2 | [tapp] | mb automata 1 |
Def | | trace(l) | [ttrace] | mb automata 1 |
Def | | l | [tfvar] | mb automata 1 |
Def | | f | [topr] | mb automata 1 |
Def | | l | [tvar] | mb automata 1 |
Def | | l' | [tpvar] | mb automata 1 |
Def | | mk_smt(lbl, term, typ) | [mk_smt] | mb automata 1 |
Def | | imax(a;b) | [imax] | int 2 |
Def | | i j | [le_int] | bool 1 |
Def | |  b | [bnot] | bool 1 |
Def | | true | [btrue] | bool 1 |
Def | | Prop | [prop] | core |
Def | | Case lbl : typ = >
body(lbl;typ) | [case_mk_dec] | mb automata 1 |
Def | | mk_rel(name, args) | [mk_rel] | mb automata 1 |
Def | | x f y | [infix_ap] | core |
Def | | (ternary) R preserves P | [preserved_by2] | mb nat |
Def | | R preserves P | [preserved_by] | mb nat |
Def | | R1 R2 | [rel_or] | mb nat |
Def | | inl(x) = >
body(x)
cont | [case_inl] | prog 1 |
Def | | Case ts_var(x) = >
body(x)
cont | [case_ts_var] | mb automata 1 |
Def | | Tree(E) | [tree] | mb tree |
Def | | ts_var(x) | [ts_var] | mb automata 1 |
Def | | tree_leaf(x) | [tree_leaf] | mb tree |
Def | | ts_fvar(x) | [ts_fvar] | mb automata 1 |
Def | | ts_trace(x) | [ts_trace] | mb automata 1 |
Def | | ts_pvar(x) | [ts_pvar] | mb automata 1 |
Def | | ts_op(x) | [ts_op] | mb automata 1 |
Def | | tree_node( < x, y > ) | [node] | mb tree |
Def | | Unit | [unit] | core |
Def | | mk_ioa(ds, da, init, pre, eff, frame) | [mk_ioa] | mb automata 1 |
Def | |  | [bool] | bool 1 |
Def | | Top | [top] | core |
Def | | EquivRel x,y:T. E(x;y) | [equiv_rel] | rel 1 |
Def | | (i, j) | [flip] | mb nat |
Def | | sum(f(x;y) | x < n; y < m) | [double_sum] | mb nat |
Def | | sum(f(x) | x < k) | [sum] | mb nat |
Def | | primrec(n;b;c) | [primrec] | mb nat |
Def | | R^n | [rel_exp] | mb nat |
Def | | Case v = > case
cont | [switch_case] | prog 1 |
Def | | i= j | [eq_int] | bool 1 |
Def | | InvFuns(A; B; f; g) | [inv_funs] | fun 1 |
Def | | f o g | [compose] | fun 1 |
Def | | decl_type(d;x) | [decl_type] | mb declaration |
Def | | Pattern | [ptn] | mb basic |
Def | | firstn(n;as) | [firstn] | list 1 |
Def | | i < j | [lt_int] | bool 1 |
Def | | GCD(a;b;y) | [gcd_p] | num thy 1 |
Def | | a ~ b | [assoced] | num thy 1 |
Def | | b | a | [divides] | num thy 1 |
Def | | ptn_con(T) | [ptn_con] | mb basic |
Def | | Case ptn_atom(x) = >
body(x)
cont | [case_ptn_atom] | mb basic |
Def | | Case ptn_pr( < x, y > ) = >
body(x;y)
cont | [case_lbl_pair] | mb basic |
Def | | x= y Atom | [eq_atom] | bool 1 |
Def | | ptn_atom(x) | [ptn_atom] | mb basic |
Def | | ptn_pr(x) | [ptn_pr] | mb basic |
Def | | Order(T;x,y.R(x;y)) | [order] | rel 1 |
Def | | Trans x,y:T. E(x;y) | [trans] | rel 1 |
Def | | Sym x,y:T. E(x;y) | [sym] | rel 1 |
Def | | Refl(T;x,y.E(x;y)) | [refl] | rel 1 |
Def | | P  Q | [iff] | core |
Def | | AntiSym(T;x,y.R(x;y)) | [anti_sym] | rel 1 |
Def | | Connex(T;x,y.R(x;y)) | [connex] | rel 1 |
Def | | tree_con(E;T) | [tree_con] | mb tree |
Def | | tree_node(x) | [tree_node] | mb tree |
Def | | < < "a", b > , c, 1 > | [pattern1] | prog 1 |
Def | | EndSwitch | [switch_done] | prog 1 |
Def | | enum1_el3 | [enum1_el3] | prog 1 |
Def | | enum1_el2 | [enum1_el2] | prog 1 |
Def | | enum1_el1 | [enum1_el1] | prog 1 |
Def | | Switch(t)
b | [switch] | prog 1 |
Def | | {T} | [guard] | core |
Def | | x:T. b(x) | [tlambda] | fun 1 |
Def | | mapcons(f;as) | [mapcons] | list 1 |
Def | | S T | [subtype] | core |
Def | | Id | [tidentity] | fun 1 |
Def | | Id | [identity] | fun 1 |
Def | | Surj(A; B; f) | [surject] | fun 1 |
Def | | Inj(A; B; f) | [inject] | fun 1 |
Def | | P  Q | [rev_implies] | core |
Def | | T | [squash] | core |