---

Step * 1 1 1 1 1 of Lemma pi-rep-trans_wf


1. l_loc : Id
2. P : pi_term()
3. g : {Q:pi_term()| pi-rank(Q) < pi-rank(pirep(P))}  ─→ Id ─→ Name ─→ (Name List) ─→ pi-process()
4. l : Id@i
5. serial : Name@i
6. avoid : Name List@i
7. T : Type
8. pi-process() ⊆r T
9. s : ℕ4@i
10. s = 1 ∈ ℤ
11. m : piM(T)@i
12. ¬((s = 0 ∈ ℤ) ∧ (↑pDVfire?(m)))
13. ff ∈ 𝔹
14. pDVloc_tag?(m) ∈ 𝔹
15. ↑pDVloc_tag?(m)
16. l1 : Id@i
17. n1 : Name@i
⊢ P ∈ {Q:pi_term()| pi-rank(Q) < pi-rank(pirep(P))} 
BY
{ (MemTypeCD THEN Auto THEN RWO "rank-rep" 0 THEN Auto')⋅ }

---

Latex:

---

Latex:

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


By

---

Latex:
(MemTypeCD  THEN  Auto  THEN  RWO  "rank-rep"  0  THEN  Auto')\mcdot{}

---

Home Index