Nuprl Definition : app_perm
app_perm(m;n;p;q) == mk_perm(app_permf(m;n;p.f;q.f);app_permf(m;n;p.b;q.b))
Definitions occuring in Statement :
app_permf: app_permf(m;n;p;q),
mk_perm: mk_perm(f;b),
perm_b: p.b,
perm_f: p.f
Definitions occuring in definition :
mk_perm: mk_perm(f;b),
perm_f: p.f,
app_permf: app_permf(m;n;p;q),
perm_b: p.b
Latex:
app\_perm(m;n;p;q) == mk\_perm(app\_permf(m;n;p.f;q.f);app\_permf(m;n;p.b;q.b))
Date html generated:
2016_05_16-AM-07_30_46
Last ObjectModification:
2015_09_23-AM-09_51_21
Theory : perms_1
Home
Index