---

Step * 1 2 1 of Lemma pi-trans_wf


1. l_loc : Id
2. ∀n:ℕ. ∀P:pi_term().  (pi-rank(P) < n ⇒ (pi-trans(l_loc;P) ∈ Id ⟶ Name ⟶ (Name List) ⟶ pi-process()))
3. P : pi_term()
⊢ pi-trans(l_loc;P) ∈ Id ⟶ Name ⟶ (Name List) ⟶ pi-process()
BY
{ InstHyp [⌜pi-rank(P) + 1⌝;⌜P⌝] 2⋅
THEN Auto' }

---

Latex:

---

Latex:

1.  l$_{loc}$  :  Id
2.  \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\000C-process()))
3.  P  :  pi\_term()
\mvdash{}  pi-trans(l$_{loc}$;P)  \mmember{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-process()


By

---

Latex:
InstHyp  [\mkleeneopen{}pi-rank(P)  +  1\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]  2\mcdot{}
THEN  Auto'

---

Home Index