Nuprl - mb automata 2 Citations of addprime

mb automata 2 Sections GenAutomata Doc

Def (t)' == term_iterate(

x.x';

op.op;

f.f;

P.trace(P);

a,b. a b;t)

is mentioned by

Thm* t:Term. term_primed_vars((t)') ~ term_vars(t) [term_vars_addprime]

Thm* x:Term, as:(LabelTerm) List. (v:Label. (v term_vars(x)) (v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x) [term_subst2_addprime]

Thm* t:Term. term_free_vars((t)') ~ term_free_vars(t) [term_free_vars_addprime]

Thm* t:Term, e,s,s',a,tr:Top. [[(t)']] e s s' a tr ~ [[t]] e s' a tr [term_mng2_addprime]

Def (r)' == mk_rel(r.name, map(t.(t)';r.args)) [rel_addprime]

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc

`Thm* t:Term. term_primed_vars((t)') ~ term_vars(t)`	[term_vars_addprime]
`Thm* x:Term, as:(LabelTerm) List. (v:Label. (v term_vars(x)) (v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x)`	[term_subst2_addprime]
`Thm* t:Term. term_free_vars((t)') ~ term_free_vars(t)`	[term_free_vars_addprime]
`Thm* t:Term, e,s,s',a,tr:Top. [[(t)']] e s s' a tr ~ [[t]] e s' a tr`	[term_mng2_addprime]
`Def (r)' == mk_rel(r.name, map(t.(t)';r.args))`	[rel_addprime]