Nuprl Lemma : rank-par

[P,Q:pi_term()].  (pi-rank(pipar(P;Q)) ((pi-rank(P) pi-rank(Q)) 1) ∈ ℕ)


Proof




Definitions occuring in Statement :  pi-rank: pi-rank(p) pipar: pipar(left;right) pi_term: pi_term() nat: uall: [x:A]. B[x] add: m natural_number: $n equal: t ∈ T
Lemmas :  pi-rank_wf nat_wf pi_term_wf

Latex:
\mforall{}[P,Q:pi\_term()].    (pi-rank(pipar(P;Q))  =  ((pi-rank(P)  +  pi-rank(Q))  +  1))



Date html generated: 2015_07_23-AM-11_33_13
Last ObjectModification: 2015_01_29-AM-00_54_24

Home Index