Nuprl - mb automata 2 Citations of term iter

mb automata 2 Sections GenAutomata Doc

Def iterate(statevar x- > v(x) statevar x''- > v'(x') funsymbol op- > opr(op) freevar f- > fvar(f) trace(tr)- > trace(tr) a(b)- > comb(a;b) over t) == term_iterate(

x.v(x);

x'.v'(x');

op.opr(op);

f.fvar(f);

tr.trace(tr);

a,b. comb(a;b); t)

is mentioned by

Def term_primed_vars(t) == iterate(statevar v- > nil statevar v'- > [v] funsymbol f- > nil freevar f- > nil trace(P)- > nil x(y)- > x @ y over t) [term_primed_vars]

Def affects_trace(e;k;t) == iterate(statevar x- > false statevar x'- > false funsymbol x- > false freevar x- > false trace(P)- > e(P,k) x(y)- > x y over t) [affects_trace]

Def mentions_trace(t) == iterate(statevar x- > false statevar x'- > false funsymbol x- > false freevar x- > false trace(P)- > true x(y)- > x y over t) [mentions_trace]

Def term_subst2(as;t) == iterate(statevar v- > v statevar v'- > apply_alist(as;v;v') funsymbol f- > f freevar f- > f trace(P)- > trace(P) x(y)- > x y over t) [term_subst2]

Def term_subst(as;t) == iterate(statevar v- > apply_alist(as;v;v) statevar v'- > apply_alist(as;v;v') funsymbol f- > f freevar f- > f trace(P)- > trace(P) x(y)- > x y over t) [term_subst]

Def [[t]] e s s' a tr == iterate(statevar x- > s.x statevar x'- > s'.x funsymbol x- > e.x freevar x- > a trace(P)- > tr.P x(y)- > x(y) over t) [term_mng2]

Try larger context: GenAutomata

mb automata 2 Sections GenAutomata Doc

`Def term_primed_vars(t) == iterate(statevar v- > nil statevar v'- > [v] funsymbol f- > nil freevar f- > nil trace(P)- > nil x(y)- > x @ y over t)`	[term_primed_vars]
`Def affects_trace(e;k;t) == iterate(statevar x- > false statevar x'- > false funsymbol x- > false freevar x- > false trace(P)- > e(P,k) x(y)- > x y over t)`	[affects_trace]
`Def mentions_trace(t) == iterate(statevar x- > false statevar x'- > false funsymbol x- > false freevar x- > false trace(P)- > true x(y)- > x y over t)`	[mentions_trace]
`Def term_subst2(as;t) == iterate(statevar v- > v statevar v'- > apply_alist(as;v;v') funsymbol f- > f freevar f- > f trace(P)- > trace(P) x(y)- > x y over t)`	[term_subst2]
`Def term_subst(as;t) == iterate(statevar v- > apply_alist(as;v;v) statevar v'- > apply_alist(as;v;v') funsymbol f- > f freevar f- > f trace(P)- > trace(P) x(y)- > x y over t)`	[term_subst]
`Def [[t]] e s s' a tr == iterate(statevar x- > s.x statevar x'- > s'.x funsymbol x- > e.x freevar x- > a trace(P)- > tr.P x(y)- > x(y) over t)`	[term_mng2]