{ 
[P,Q:Pi_term]. (pi-rank((P + Q)) = ((pi-rank(P) + pi-rank(Q)) + 1)) }
{ Proof }
Definitions occuring in Statement :
pi-rank: pi-rank(p),
pioption: (left + right),
pi_term: Pi_term,
nat: 
,
uall: [x:A]. B[x],
add: n + m,
natural_number: $n,
equal: s = t
Definitions :
uall: [x:A]. B[x],
pi-rank: pi-rank(p),
member: t 
T,
nat:
Lemmas :
pi-rank_wf,
nat_wf,
pi_term_wf
\mforall{}[P,Q:Pi\_term]. (pi-rank((P + Q)) = ((pi-rank(P) + pi-rank(Q)) + 1))
Date html generated:
2011_08_17-PM-06_47_16
Last ObjectModification:
2011_06_18-PM-12_18_46
Home
Index