---

Step * 2 of Lemma rank-pi-choices


1. left : pi_term()@i
2. right : pi_term()@i
3. ∀choice:{c:pi_prefix() × pi_term()| (c ∈ pi-choices(left))} . pi-rank(snd(choice)) < pi-rank(left)@i
4. ∀choice:{c:pi_prefix() × pi_term()| (c ∈ pi-choices(right))} . pi-rank(snd(choice)) < pi-rank(right)@i
5. choice : pi_prefix() × pi_term()@i
6. (choice ∈ pi-choices(left)) ∨ (choice ∈ pi-choices(right))
⊢ pi-rank(snd(choice)) < pi-rank(left) + pi-rank(right) + 1
BY
{ (D -1 THEN AllHyps h.(InstHyp [⌈choice⌉] h⋅ THENA Complete (Auto))  THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  left  :  pi\_term()@i
2.  right  :  pi\_term()@i
3.  \mforall{}choice:\{c:pi\_prefix()  \mtimes{}  pi\_term()|  (c  \mmember{}  pi-choices(left))\} 
          pi-rank(snd(choice))  <  pi-rank(left)@i
4.  \mforall{}choice:\{c:pi\_prefix()  \mtimes{}  pi\_term()|  (c  \mmember{}  pi-choices(right))\} 
          pi-rank(snd(choice))  <  pi-rank(right)@i
5.  choice  :  pi\_prefix()  \mtimes{}  pi\_term()@i
6.  (choice  \mmember{}  pi-choices(left))  \mvee{}  (choice  \mmember{}  pi-choices(right))
\mvdash{}  pi-rank(snd(choice))  <  pi-rank(left)  +  pi-rank(right)  +  1


By

---

Latex:
(D  -1  THEN  AllHyps  h.(InstHyp  [\mkleeneopen{}choice\mkleeneclose{}]  h\mcdot{}  THENA  Complete  (Auto))    THEN  Auto')\mcdot{}

---

Home Index