---

Step * 1 2 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()))
⊢ ∀[P:pi_term()]. (pi-trans(l_loc;P) ∈ Id ⟶ Name ⟶ (Name List) ⟶ pi-process())
BY
{ Auto }

1
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()

---

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()))
\mvdash{}  \mforall{}[P:pi\_term()].  (pi-trans(l$_{loc}$;P)  \mmember{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-proce\000Css())


By

---

Latex:
Auto

---

Home Index