Nuprl Definition : oal_hgp

oal_hgp(s;g) ==  <|oal(s;g↓hgrp)|, =b, λx,y. x ≤≤b y, λx,y. (x ++ y), 00, λx.x>



Definitions occuring in Statement :  oal_ble: ps ≤≤b qs oal_merge: ps ++ qs oal_nil: 00 oalist: oal(a;b) lambda: λx.A[x] pair: <a, b> hgrp_of_ocgrp: g↓hgrp set_eq: =b set_car: |p|
Definitions occuring in definition :  set_car: |p| set_eq: =b oalist: oal(a;b) oal_ble: ps ≤≤b qs oal_merge: ps ++ qs pair: <a, b> oal_nil: 00 hgrp_of_ocgrp: g↓hgrp lambda: λx.A[x]

Latex:
oal\_hgp(s;g)  ==    <|oal(s;g\mdownarrow{}hgrp)|,  =\msubb{},  \mlambda{}x,y.  x  \mleq{}\mleq{}\msubb{}  y,  \mlambda{}x,y.  (x  ++  y),  00,  \mlambda{}x.x>



Date html generated: 2016_05_16-AM-08_22_19
Last ObjectModification: 2015_09_23-AM-09_53_08

Theory : polynom_2


Home Index