t:Term, ds,da,de:Top.
term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t)
x.x';x.x';op.op;f.f;P.trace(P);a,b. a b;t)
is mentioned by
|
Thm* t:Term, ds,da,de:Top.
term_types(ds;da;de;(t)') ~ term_types(ds;da;de;t) | [term_types_addprime] |
In prior sections: mb automata 2
Try larger context: GenAutomata