---

Step * 1 of Lemma pi-trans_wf


1. l_loc : Id
⊢ ∀[P:pi_term()]. (pi-trans(l_loc;P) ∈ Id ─→ Name ─→ (Name List) ─→ pi-process())
BY
{ Assert ⌈∀n:ℕ. ∀P:pi_term().  (pi-rank(P) < n ⇒ (pi-trans(l_loc;P) ∈ Id ─→ Name ─→ (Name List) ─→ pi-process()))⌉⋅ }

1
.....assertion..... 
1. l_loc : Id
⊢ ∀n:ℕ. ∀P:pi_term().  (pi-rank(P) < n ⇒ (pi-trans(l_loc;P) ∈ Id ─→ Name ─→ (Name List) ─→ pi-process()))

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

---

Latex:

---

Latex:

1.  l$_{loc}$  :  Id
\mvdash{}  \mforall{}[P:pi\_term()].  (pi-trans(l$_{loc}$;P)  \mmember{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-proce\000Css())


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}P:pi\_term().
                    (pi-rank(P)  <  n  {}\mRightarrow{}  (pi-trans(l$_{loc}$;P)  \mmember{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  \000C{}\mrightarrow{}  pi-process()))\mkleeneclose{}\mcdot{}

---

Home Index