Nuprl Definition : no-change-at-e

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

x,y.(x = y);init;X)

Proof not projected

Definitions occuring in Statement : transition-at-e: transition-at-e(es;e;T;R;init;X), lambda:

x.A[x], equal: s = t
FDL editor aliases : no-change-at-e

no-change-at-e(es;e;T;init;X) == transition-at-e(es;e;T;\mlambda{}x,y.(x = y);init;X) Date html generated: 2011_10_20-PM-04_52_46 Last ObjectModification: 2011_06_23-PM-03_53_57 Home Index