---

Step * 1 of Lemma rank-pi-choices


1. pre : pi_prefix()@i
2. body : pi_term()@i
3. ∀choice:{c:pi_prefix() × pi_term()| (c ∈ pi-choices(body))} . pi-rank(snd(choice)) < pi-rank(body)@i
4. choice : pi_prefix() × pi_term()@i
5. choice = <pre, body> ∈ (pi_prefix() × pi_term())
⊢ pi-rank(snd(choice)) < pi-rank(body) + 1
BY
{ ((HypSubst' (-1) 0 THENM Reduce 0) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  pre  :  pi\_prefix()@i
2.  body  :  pi\_term()@i
3.  \mforall{}choice:\{c:pi\_prefix()  \mtimes{}  pi\_term()|  (c  \mmember{}  pi-choices(body))\} 
          pi-rank(snd(choice))  <  pi-rank(body)@i
4.  choice  :  pi\_prefix()  \mtimes{}  pi\_term()@i
5.  choice  =  <pre,  body>
\mvdash{}  pi-rank(snd(choice))  <  pi-rank(body)  +  1


By

---

Latex:
((HypSubst'  (-1)  0  THENM  Reduce  0)  THEN  Auto)\mcdot{}

---

Home Index