is mentioned by

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)

[term_iterate]

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

[ts_eq]

Try larger context: GenAutomata