mb automata 3 Sections GenAutomata Doc

Def unprime(t) == term_iterate(x.x;x.x;op.op;f.f;P.trace(P);a,b. a b;t)

is mentioned by

Thm* r:rel(), as:(LabelTerm) List. (x:Label. unprime(apply_alist(as;x;x)) = x) rel_unprime(rel_subst(as;r)) = rel_unprime(r)[trivial_rel_subst]
Thm* t:Term, as:(LabelTerm) List. (x:Label. unprime(apply_alist(as;x;x)) = x) unprime(term_subst(as;t)) = unprime(t)[trivial_term_subst]
Thm* t:Term, ds,da,de:Top. term_types(ds;da;de;unprime(t)) ~ term_types(ds;da;de;t)[term_types_unprime]

In prior sections: mb automata 2

Try larger context: GenAutomata

mb automata 3 Sections GenAutomata Doc