WhoCites Definitions mb automata 4 Sections GenAutomata Doc

Who Cites ttrace?
ttraceDef trace(l) == tree_leaf(ts_trace(l))
Thm* l:Label. trace(l) Term
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)

Syntax:trace(l) has structure: ttrace(l)

About:
inlinruniversememberall!abstraction

WhoCites Definitions mb automata 4 Sections GenAutomata Doc