Nuprl Definition : pi-normal

pi-normal(t) ==
  pi_term_ind(t;tt;pr,A,nm.nm;A,B,na,nb.na
  ∧_b nb
  ∧_b (picomm?(A) ∨_bpioption?(A))
  ∧_b (picomm?(B) ∨_bpioption?(B));A,B,na,nb.na ∧_b nb;A,na.na;x,A,na.na)

Definitions occuring in Statement : pi_term_ind: pi_term_ind(v;zero;pre,body,rec1....;left,right,rec2,rec3....;left,right,rec4,rec5....;body,rec6....;name,body,rec7....), pioption?: pioption?(v), picomm?: picomm?(v), bor: p ∨_bq, band: p ∧_b q, btrue: tt
FDL editor aliases : pi-normal

Latex:
pi-normal(t) == pi\_term\_ind(t;tt;pr,A,nm.nm;A,B,na,nb.na \mwedge{}\msubb{} nb \mwedge{}\msubb{} (picomm?(A) \mvee{}\msubb{}pioption?(A)) \mwedge{}\msubb{} (picomm?(B) \mvee{}\msubb{}pioption?(B));A,B,na,nb.na \mwedge{}\msubb{} nb;A,na.na;x,A,na.na) Date html generated: 2015_07_23-AM-11_33_50 Last ObjectModification: 2012_08_30-PM-01_19_36 Home Index