mb
automata
2
Sections
GenAutomata
Doc
Def
(a=b) == ts_case(a)var(v)= > ts_case(b)var(v')= > v =
v'var'(x)= > false
opr(x)= > false
fvar(x)= > false
trace(x)= > false
end_ts_case var'(p)= > ts_case(b)var(x)= > false
var'(p')= > p =
p'opr(x)= > false
fvar(x)= > false
trace(x)= > false
end_ts_case opr(op)= > ts_case(b)var(x)= > false
var'(x)= > false
opr(op')= > op =
op'fvar(x)= > false
trace(x)= > false
end_ts_case fvar(f)= > ts_case(b)var(x)= > false
var'(x)= > false
opr(x)= > false
fvar(f')= > f =
f'trace(x)= > false
end_ts_case trace(P)= > ts_case(b)var(x)= > false
var'(x)= > false
opr(x)= > false
fvar(x)= > false
trace(P')= > P =
P'end_ts_case end_ts_case
is mentioned by
Def
term_eq(a;b) == Case(a) Case x;y = > Case(b) Case x';y' = > term_eq(x;x')
term_eq(y;y') Case tree_leaf(x) = > false
Default = > True Case tree_leaf(x) = > Case(b) Case x';y' = > false
Case tree_leaf(x') = > (x=x') Default = > True Default = > True (recursive)
[term_eq]
In prior sections:
mb
automata
1
Try larger context:
GenAutomata
mb
automata
2
Sections
GenAutomata
Doc