t:Term, e,s,s',a,tr:Top. [[unprime(t)]] e s s' a tr ~ [[t]] e s a trt:Term, e,a,s,tr:Top. [[t]] e s a tr ~ [[unprime(t)]] e s a tr
t.unprime(t);r.args))x.x;x.x;op.op;f.f;P.trace(P);a,b. a b;t)
is mentioned by
| Thm* t:Term, e,s,s',a,tr:Top. [[unprime(t)]] e s s' a tr ~ [[t]] e s a tr | [term_mng2_unprime] |
| Thm* t:Term, e,a,s,tr:Top. [[t]] e s a tr ~ [[unprime(t)]] e s a tr | [term_mng_unprime] |
| Def rel_unprime(r) == mk_rel(r.name, map(t.unprime(t);r.args)) | [rel_unprime] |
Try larger context:
GenAutomata