Nuprl Lemma : rank-zero
pi-rank(pizero()) = 0 ∈ ℕ
Proof
Definitions occuring in Statement : 
pi-rank: pi-rank(p), 
pizero: pizero(), 
nat: ℕ, 
natural_number: $n, 
equal: s = t ∈ T
Lemmas : 
le_weakening, 
le_wf
Latex:
pi-rank(pizero())  =  0
 Date html generated: 
2015_07_23-AM-11_33_07
 Last ObjectModification: 
2015_01_29-AM-00_54_03
Home
Index