---

Step * 1 1 1 2 of Lemma pi-bar-trans_wf


1. l_loc : Id
2. P : pi_term()
3. Q : pi_term()
4. g : {R:pi_term()| pi-rank(R) < pi-rank(pipar(P;Q))}  ─→ Id ─→ Name ─→ (Name List) ─→ pi-process()
5. l : Id@i
6. serial : Name@i
7. avoid : Name List@i
8. T : Type
9. pi-process() ⊆r T
10. s : ℕ4@i
11. m : piM(T)@i
12. ¬(s = 0 ∈ ℤ)
13. ¬(s = 1 ∈ ℤ)
14. s = 2 ∈ ℤ
15. ↑pDVloc_tag?(m)
⊢ Q ∈ {R:pi_term()| pi-rank(R) < pi-rank(pipar(P;Q))} 
BY
{ (MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. l_loc : Id
2. P : pi_term()
3. Q : pi_term()
4. g : {R:pi_term()| pi-rank(R) < pi-rank(pipar(P;Q))}  ─→ Id ─→ Name ─→ (Name List) ─→ pi-process()
5. l : Id@i
6. serial : Name@i
7. avoid : Name List@i
8. T : Type
9. pi-process() ⊆r T
10. s : ℕ4@i
11. m : piM(T)@i
12. ¬(s = 0 ∈ ℤ)
13. ¬(s = 1 ∈ ℤ)
14. s = 2 ∈ ℤ
15. ↑pDVloc_tag?(m)
⊢ pi-rank(Q) < pi-rank(pipar(P;Q))

---

Latex:

---

Latex:

1.  l$_{loc}$  :  Id
2.  P  :  pi\_term()
3.  Q  :  pi\_term()
4.  g  :  \{R:pi\_term()|  pi-rank(R)  <  pi-rank(pipar(P;Q))\}    {}\mrightarrow{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-process()
5.  l  :  Id@i
6.  serial  :  Name@i
7.  avoid  :  Name  List@i
8.  T  :  Type
9.  pi-process()  \msubseteq{}r  T
10.  s  :  \mBbbN{}4@i
11.  m  :  piM(T)@i
12.  \mneg{}(s  =  0)
13.  \mneg{}(s  =  1)
14.  s  =  2
15.  \muparrow{}pDVloc\_tag?(m)
\mvdash{}  Q  \mmember{}  \{R:pi\_term()|  pi-rank(R)  <  pi-rank(pipar(P;Q))\} 


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index