{ 
[P:Pi_term]. [pre:pi_prefix()]. (pi-rank(pre.P) = (pi-rank(P) + 1)) }
{ Proof }
Definitions occuring in Statement :
pi-rank: pi-rank(p),
picomm: pre.body,
pi_term: Pi_term,
pi_prefix: pi_prefix(),
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_prefix_wf,
pi_term_wf
\mforall{}[P:Pi\_term]. \mforall{}[pre:pi\_prefix()]. (pi-rank(pre.P) = (pi-rank(P) + 1))
Date html generated:
2011_08_17-PM-06_46_59
Last ObjectModification:
2011_06_18-PM-12_18_14
Home
Index