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)
is mentioned by
| Def (t)' == term_iterate(x.x';x.x';op.op;f.f;P.trace(P);a,b. a b;t) | [addprime] |
| Def term_free_vars(t) == term_iterate(f.nil;f.nil;f.nil;v.[v];P.nil;x,y. x @ y;t) | [term_free_vars] |
| Def unprime(t) == term_iterate(x.x;x.x;op.op;f.f;P.trace(P);a,b. a b;t) | [unprime] |
| 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_iterate(x.v(x);
x'.v'(x');
op.opr(op);
f.fvar(f);
tr.trace(tr);
a,b. comb(a;b);
t) | [term_iter] |
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] |
Try larger context:
GenAutomata