---

Step * 1 1 of Lemma pi-trans_wf

.....assertion..... 
1. l_loc : Id
⊢ ∀n:ℕ. ∀P:pi_term().  (pi-rank(P) < n ⇒ (pi-trans(l_loc;P) ∈ Id ─→ Name ─→ (Name List) ─→ pi-process()))
BY
{ (InductionOnNat
   THEN Auto'
   THEN D -2
   THEN Unfold `pi-rank` -1
   THEN Reduce (-1)
   THEN Try (Fold `pi-rank` (-1))
   THEN RecUnfold `pi-trans` 0 THEN Reduce 0
   THEN RepUR ``let`` 0
   THEN Auto
   THEN RepUR ``pi-rank`` -1
   THEN Try (Fold `pi-rank` (-1))
   THEN BackThruSomeHyp
   THEN Auto) }

1
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. pre : pi_prefix()
6. P2 : pi_term()
7. pi-rank(P2) + 1 < n@i
8. ∀Q:pi_term(). ((∃C∈pi-choices(picomm(pre;P2)). pi-rank(Q) ≤ pi-rank(snd(C))) ∈ Type)
9. p : pi_term()@i
10. (∃C∈pi-choices(picomm(pre;P2)). pi-rank(p) ≤ pi-rank(snd(C)))@i
⊢ pi-rank(p) < n - 1

2
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

---

Latex:

---

Latex:
.....assertion..... 
1.  l$_{loc}$  :  Id
\mvdash{}  \mforall{}n:\mBbbN{}.  \mforall{}P:pi\_term().
        (pi-rank(P)  <  n  {}\mRightarrow{}  (pi-trans(l$_{loc}$;P)  \mmember{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-\000Cprocess()))


By

---

Latex:
(InductionOnNat
  THEN  Auto'
  THEN  D  -2
  THEN  Unfold  `pi-rank`  -1
  THEN  Reduce  (-1)
  THEN  Try  (Fold  `pi-rank`  (-1))
  THEN  RecUnfold  `pi-trans`  0  THEN  Reduce  0
  THEN  RepUR  ``let``  0
  THEN  Auto
  THEN  RepUR  ``pi-rank``  -1
  THEN  Try  (Fold  `pi-rank`  (-1))
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index