Nuprl Definition : glues

g glues Ia ──f─→ Ib == g glues Ia:λe,e'. e ≤loc e' ──f─→ Ib:λe,e'. e ≤loc e'

Definitions occuring in Statement : Q-R-glues: g glues Ia:Qa ──f─→ Ib:Rb, es-le: e ≤loc e' , lambda: λx.A[x]
FDL editor aliases : glues

Latex:
g glues Ia {}{}f{}\mrightarrow{} Ib == g glues Ia:\mlambda{}e,e'. e \mleq{}loc e' {}{}f{}\mrightarrow{} Ib:\mlambda{}e,e'. e \mleq{}loc e' Date html generated: 2015_07_21-PM-04_13_33 Last ObjectModification: 2012_02_25-PM-03_06_35 Home Index