WhoCites Definitions mb automata 4 Sections GenAutomata Doc

Who Cites pred?
pred Def Fmla == Collection(rel())
Thm* Fmla{i} Type{i'}
col Def Collection(T) == TProp
Thm* T:Type{i'}. Collection{i}(T) Type{i'}
trace_consistent_pred Def trace_consistent_pred(rho;da;R;p) == (rp.trace_consistent_rel(rho;da;R;r))
Thm* p:Fmla, rho:Decl, da:Collection(dec()), R:(LabelLabel). trace_consistent_pred(rho;da;R;p) Prop
trace_consistent_rel Def trace_consistent_rel(rho;da;R;r) == i:||r.args||. trace_consistent(rho;da;R;r.args[i])
Thm* rho:Decl, r:rel(), da:Collection(dec()), R:(LabelLabel). trace_consistent_rel(rho;da;R;r) Prop
trace_consistent Def trace_consistent(rho;da;R;t) == g:Label. term_mentions_guard(g;t) subtype_rel(({a:([[da]] rho)| (R(g,kind(a))) } List); (rho(lbl_pr( < Trace, g > ))))
Thm* rho:Decl, t:Term, da:Collection(dec()), R:(LabelLabel). trace_consistent(rho;da;R;t) Prop
decls_mng Def [[ds]] rho == [[d]] rho for d {d:dec()| d ds }
Thm* ds:Collection(dec()), rho:Decl. [[ds]] rho Decl
dec Def dec() == LabelSimpleType
Thm* dec() Type
decl Def Decl == LabelType
Thm* Decl{i} Type{i'}
pred_addprime Def (P)' == (rP. < (r)' > )
Thm* P:Fmla. (P)' Fmla
rel Def rel() == relname()(Term List)
Thm* rel() Type
relname Def relname() == SimpleType+Label
Thm* relname() Type
st Def SimpleType == Tree(Label+Unit)
Thm* SimpleType Type
term Def Term == Tree(ts())
Thm* Term Type
ts Def ts() == Label+Label+Label+Label+Label
Thm* ts() Type
sigma Def (d) == l:Labeldecl_type(d;l)
Thm* d:Decl. (d) Type
lbl Def Label == {p:Pattern| ground_ptn(p) }
Thm* Label Type
rel_addprime Def (r)' == mk_rel(r.name, map(t.(t)';r.args))
Thm* r:rel(). (r)' rel()
ground_ptn Def ground_ptn(p) == Case(p) Case ptn_var(v) = > false Case ptn_pr( < x, y > ) = > ground_ptn(x)ground_ptn(y) Default = > true (recursive)
Thm* p:Pattern. ground_ptn(p)
assert Def b == if b True else False fi
Thm* b:. b Prop
ptn Def Pattern == rec(T.ptn_con(T))
Thm* Pattern Type
col_singleton Def < x > (y) == y = x T
Thm* T:Type, x:T. < x > Collection(T)
col_accum Def (xc.f(x))(y) == x:T. x c & y f(x)
Thm* T,T':Type, f:(TCollection(T')), c:Collection(T). (xc.f(x)) Collection(T')
rel_args Def t.args == 2of(t)
Thm* t:rel(). t.args Term List
addprime Def (t)' == term_iterate(x.x';x.x';op.op;f.f;P.trace(P);a,b. a b;t)
Thm* t:Term. (t)' Term
map Def map(f;as) == Case of as; nil nil ; a.as' [(f(a)) / map(f;as')] (recursive)
Thm* A,B:Type, f:(AB), l:A List. map(f;l) B List
Thm* A,B:Type, f:(AB), l:A List. map(f;l) B List
rel_name Def t.name == 1of(t)
Thm* t:rel(). t.name relname()
mk_rel Def mk_rel(name, args) == < name,args >
Thm* name:relname(), args:Term List. mk_rel(name, args) rel()
col_all Def (xc.P(x)) == x:T. x c P(x)
Thm* T:Type, c:Collection(T), P:(TProp). (xc.P(x)) Prop
select Def l[i] == hd(nth_tl(i;l))
Thm* A:Type, l:A List, n:. 0n n < ||l|| l[n] A
length Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)
Thm* A:Type, l:A List. ||l||
Thm* ||nil||
int_seg Def {i..j} == {k:| i k < j }
Thm* m,n:. {m..n} Type
tree Def Tree(E) == rec(T.tree_con(E;T))
Thm* E:Type. Tree(E) Type
term_mentions_guard Def term_mentions_guard(g;t) == term_iterate(x.false;x.false;x.false;x.false;x.x = g;x,y. x y;t)
Thm* t:Term, g:Label. term_mentions_guard(g;t)
term_iterate Def term_iterate(v;p;op;f;tr;a;t) == t_iterate(x.ts_case(x)var(a)= > v(a)var'(b)= > p(b)opr(c)= > op(c)fvar(d)= > f(d)trace(P)= > tr(P)end_ts_case ;a;t)
Thm* A:Type, v,op,f,p,tr:(LabelA), a:(AAA), t:Term. term_iterate(v;p;op;f;tr;a;t) A
ts_case 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 == Case(x) Case ts_var(a) = > v(a) Case ts_pvar(b) = > p(b) Case ts_op(f) = > op(f) Case ts_fvar(x) = > f(x) Case ts_trace(P) = > t(P) Default = >
Thm* A:Type, v,op,f,p,t:(LabelA), x:ts(). ts_case(x)var(a)= > v(a)var'(b)= > p(b)opr(f)= > op(f)fvar(y)= > f(y)trace(P)= > t(P)end_ts_case A
dec_mng Def [[d]] rho == Case(d) Case x : s = > x:[[s]] rho
Thm* rho:Decl, d:dec(). [[d]] rho Decl
st_mng Def [[s]] rho == t_iterate(st_lift(rho);x,y. xy;s)
Thm* rho:Decl, s:SimpleType. [[s]] rho Type
t_iterate Def t_iterate(l;n;t) == Case(t) Case x;y = > n(t_iterate(l;n;x),t_iterate(l;n;y)) Case tree_leaf(x) = > l(x) Default = > True (recursive)
Thm* E,A:Type, l:(EA), n:(AAA), t:Tree(E). t_iterate(l;n;t) A
dbase Def x:y(a) == if a = x y else Top fi
Thm* x:Label, y:Type. x:y Decl
eq_lbl 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)
Thm* l1,l2:Pattern. l1 = l2
case_default Def Default = > body(value,value) == body
band Def pq == if p q else false fi
Thm* p,q:. (pq)
case_lbl_pair Def Case ptn_pr( < x, y > ) = > body(x;y) cont(x1,z) == InjCase(x1; _. cont(z,z); x2. InjCase(x2; _. cont(z,z); x2@0. InjCase(x2@0; _. cont(z,z); x2@1. x2@1/x3,x2@2. body(x3;x2@2))))
case_ptn_var Def Case ptn_var(x) = > body(x) cont(x1,z) == (x1.inr(x2) = > (x1.inr(x2) = > (x1.inl(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x2 / tl(x1)]) cont(hd(x1),z))([x2 / tl(x1)]) cont(hd(x1),z))([x1])
case Def Case(value) body == body(value,value)
ptn_con Def ptn_con(T) == Atom++Atom+(TT)
Thm* T:Type. ptn_con(T) Type
col_member Def x c == c(x)
Thm* T:Type, x:T, c:Collection(T). x c Prop
pi2 Def 2of(t) == t.2
Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))
tapp Def t1 t2 == tree_node( < t1, t2 > )
Thm* t1,t2:Term. t1 t2 Term
ttrace Def trace(l) == tree_leaf(ts_trace(l))
Thm* l:Label. trace(l) Term
tfvar Def l == tree_leaf(ts_fvar(l))
Thm* l:Label. l Term
topr Def f == tree_leaf(ts_op(f))
Thm* f:Label. f Term
tpvar Def l' == tree_leaf(ts_pvar(l))
Thm* l:Label. l' Term
kind Def kind(a) == 1of(a)
Thm* d:Decl, a:(d). kind(a) Label
Thm* M:sm{i:l}(), a:M.action. kind(a) Label & kind(a) Pattern
pi1 Def 1of(t) == t.1
Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A
nth_tl Def nth_tl(n;as) == if n0 as else nth_tl(n-1;tl(as)) fi (recursive)
Thm* A:Type, as:A List, i:. nth_tl(i;as) A List
case_ts_trace Def Case ts_trace(x) = > body(x) cont(x1,z) == (x1.inr(x2) = > (x1.inr(x2) = > (x1.inr(x2) = > (x1.inr(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x2 / tl(x1)]) cont(hd(x1),z))([x2 / tl(x1)]) cont(hd(x1),z))([x2 / tl(x1)]) cont(hd(x1),z))([x1])
case_ts_fvar Def Case ts_fvar(x) = > body(x) cont(x1,z) == (x1.inr(x2) = > (x1.inr(x2) = > (x1.inr(x2) = > (x1.inl(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x2 / tl(x1)]) cont(hd(x1),z))([x2 / tl(x1)]) cont(hd(x1),z))([x2 / tl(x1)]) cont(hd(x1),z))([x1])
case_ts_op Def Case ts_op(x) = > body(x) cont(x1,z) == (x1.inr(x2) = > (x1.inr(x2) = > (x1.inl(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x2 / tl(x1)]) cont(hd(x1),z))([x2 / tl(x1)]) cont(hd(x1),z))([x1])
case_ts_pvar Def Case ts_pvar(x) = > body(x) cont(x1,z) == (x1.inr(x2) = > (x1.inl(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x2 / tl(x1)]) cont(hd(x1),z))([x1])
case_ptn_int Def Case ptn_int(x) = > body(x) cont(x1,z) == (x1.inr(x2) = > (x1.inl(x2) = > body(hd([x2 / tl(x1)])) cont(hd(x1),z))([x2 / tl(x1)]) cont(hd(x1),z))([x1])
hd Def hd(l) == Case of l; nil "?" ; h.t h
Thm* A:Type, l:A List. ||l||1 hd(l) A
Thm* A:Type, l:A List. hd(l) A
clbl Def $x == ptn_atom("$x")
lbl_pair Def lbl_pr( < x, y > ) == ptn_pr( < x,y > )
Thm* x,y:Pattern. lbl_pr( < x, y > ) Pattern
Thm* x,y:Label. lbl_pr( < x, y > ) Label
lelt Def i j < k == ij & j < k
tree_con Def tree_con(E;T) == E+(TT)
Thm* E,T:Type. tree_con(E;T) Type
tl Def tl(l) == Case of l; nil nil ; h.t t
Thm* A:Type, l:A List. tl(l) A List
case_inl Def inl(x) = > body(x) cont(value,contvalue) == InjCase(value; x. body(x); _. cont(contvalue,contvalue))
case_inr Def inr(x) = > body(x) cont(value,contvalue) == InjCase(value; _. cont(contvalue,contvalue); x. body(x))
node Def tree_node( < x, y > ) == tree_node( < x,y > )
Thm* E:Type, x,y:Tree(E). tree_node( < x, y > ) Tree(E)
ts_trace Def ts_trace(x) == inr(inr(inr(inr(x))))
Thm* x:Label. ts_trace(x) ts()
tree_leaf Def tree_leaf(x) == inl(x)
Thm* E,T:Type, x:E. tree_leaf(x) tree_con(E;T)
Thm* E:Type, x:E. tree_leaf(x) Tree(E)
ts_fvar Def ts_fvar(x) == inr(inr(inr(inl(x))))
Thm* x:Label. ts_fvar(x) ts()
ts_op Def ts_op(x) == inr(inr(inl(x)))
Thm* x:Label. ts_op(x) ts()
ts_pvar Def ts_pvar(x) == inr(inl(x))
Thm* x:Label. ts_pvar(x) ts()
le_int Def ij == j < i
Thm* i,j:. (ij)
ptn_atom Def ptn_atom(x) == inl(x)
Thm* T:Type, x:Atom. ptn_atom(x) ptn_con(T)
Thm* x:Atom. ptn_atom(x) Pattern
Thm* x:Atom. ptn_atom(x) Label
ptn_pr Def ptn_pr(x) == inr(inr(inr(x)))
Thm* T:Type, x:(TT). ptn_pr(x) ptn_con(T)
Thm* x,y:Pattern. ptn_pr( < x,y > ) Pattern
dall Def D(i) for i I(x) == i:I. D(i)(x)
Thm* I:Type, D:(IDecl). D(i) for i I Decl
decl_type Def decl_type(d;x) == d(x)
Thm* dec:Decl, x:Label. decl_type(dec;x) Type
bor Def p q == if p true else q fi
Thm* p,q:. (p q)
le Def AB == B < A
Thm* i,j:. (ij) Prop
tree_node Def tree_node(x) == inr(x)
Thm* E,T:Type, x:(TT). tree_node(x) tree_con(E;T)
Thm* E:Type, x,y:Tree(E). tree_node( < x,y > ) Tree(E)
case_ts_var Def Case ts_var(x) = > body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z))
case_tree_leaf Def Case tree_leaf(x) = > body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z))
case_node Def Case x;y = > body(x;y) cont(x1,z) == InjCase(x1; _. cont(z,z); x2. x2/x3,x2@0. body(x3;x2@0))
lt_int Def i < j == if i < j true ; false fi
Thm* i,j:. (i < j)
bnot Def b == if b false else true fi
Thm* b:. b
case_mk_dec Def Case lbl : typ = > body(lbl;typ)(x,z) == x/x2,x1. body(x2;x1)
eq_atom Def x=yAtom == if x=yAtomtrue; false fi
Thm* x,y:Atom. x=yAtom
eq_int Def i=j == if i=j true ; false fi
Thm* i,j:. (i=j)
case_ptn_atom Def Case ptn_atom(x) = > body(x) cont(x1,z) == InjCase(x1; x2. body(x2); _. cont(z,z))
not Def A == A False
Thm* A:Prop. (A) Prop
st_lift Def st_lift(rho)(x) == InjCase(x; x'. rho(x'); a. Top)
Thm* rho:(LabelType). st_lift(rho) (Label+Unit)Type
top Def Top == Void given Void
Thm* Top Type

About:
pairspreadspreadspreadproductproductlistconsconsnil
list_indboolbfalsebtrueifthenelse
assertunititvoidintnatural_numberaddsubtractint_eqless
less_thanatomtokenatom_equnioninlinr
decidesetisectisect
lambdaapplyfunctionrecursive_def_noticerecuniverseequal
membertoppropimpliesandfalsetrueallexists
!abstraction

WhoCites Definitions mb automata 4 Sections GenAutomata Doc