{ 
[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),
pipar: (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_34
Last ObjectModification:
2011_06_18-PM-12_19_18
Home
Index