---

Step * 1 1 2 of Lemma pi-trans_wf


1. l_loc : Id
2. n : ℤ
3. 0 < n
4. ∀P:pi_term(). (pi-rank(P) < n - 1 ⇒ (pi-trans(l_loc;P) ∈ Id ─→ Name ─→ (Name List) ─→ pi-process()))
5. left : pi_term()
6. P2 : pi_term()
7. pi-rank(left) + pi-rank(P2) + 1 < n@i
8. ∀Q:pi_term(). ((∃C∈pi-choices(pioption(left;P2)). pi-rank(Q) ≤ pi-rank(snd(C))) ∈ Type)
9. p : pi_term()@i
10. (∃C∈pi-choices(pioption(left;P2)). pi-rank(p) ≤ pi-rank(snd(C)))@i
⊢ pi-rank(p) < n - 1
BY
{ ((RWO "l_exists_iff" (-1) THENA Auto)
   THEN D -1
   THEN InstLemma `rank-pi-choices` [⌈pioption(left;P2)⌉;⌈C⌉]⋅
   THEN Auto
   THEN RepUR ``pi-rank`` -1
   THEN Try (Fold `pi-rank` (-1))
   THEN Auto) }

---

Latex:

---

Latex:

1.  l$_{loc}$  :  Id
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}P:pi\_term()
          (pi-rank(P)  <  n  -  1  {}\mRightarrow{}  (pi-trans(l$_{loc}$;P)  \mmember{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\000C\mrightarrow{}  pi-process()))
5.  left  :  pi\_term()
6.  P2  :  pi\_term()
7.  pi-rank(left)  +  pi-rank(P2)  +  1  <  n@i
8.  \mforall{}Q:pi\_term().  ((\mexists{}C\mmember{}pi-choices(pioption(left;P2)).  pi-rank(Q)  \mleq{}  pi-rank(snd(C)))  \mmember{}  Type)
9.  p  :  pi\_term()@i
10.  (\mexists{}C\mmember{}pi-choices(pioption(left;P2)).  pi-rank(p)  \mleq{}  pi-rank(snd(C)))@i
\mvdash{}  pi-rank(p)  <  n  -  1


By

---

Latex:
((RWO  "l\_exists\_iff"  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  InstLemma  `rank-pi-choices`  [\mkleeneopen{}pioption(left;P2)\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RepUR  ``pi-rank``  -1
  THEN  Try  (Fold  `pi-rank`  (-1))
  THEN  Auto)

---

Home Index