Nuprl Definition : transition-at-e

transition-at-e(es;e;T;R;init;X) ==

t1,t2:T. (t2

X(e)

t1

Prior(X)?{init}(e)

(R t1 t2))

Proof not projected

Definitions occuring in Statement : primed-class-opt: Prior(X)?b, classrel: v

X(e), all:

x:A. B[x], implies: P

Q, apply: f a, single-bag: {x}
FDL editor aliases : transition-at-e

transition-at-e(es;e;T;R;init;X) == \mforall{}t1,t2:T. (t2 \mmember{} X(e) {}\mRightarrow{} t1 \mmember{} Prior(X)?\{init\}(e) {}\mRightarrow{} (R t1 t2)) Date html generated: 2011_10_20-PM-04_52_24 Last ObjectModification: 2011_06_23-PM-02_42_18 Home Index