---

Step * 1 1 of Lemma pi-new-trans_wf


1. x : Name
2. P : pi_term()
3. g : {Q:pi_term()| pi-rank(Q) < pi-rank(pinew(x;P))}  ─→ Id ─→ Name ─→ (Name List) ─→ pi-process()
4. l : Id
5. serial : Name
6. avoid : Name List
7. T : {T:Type| pi-process() ⊆r T} 
8. pi-new-trans : Id ─→ Name ─→ (Name List) ─→ T@i
9. l1 : Id@i
10. s1 : Name@i
11. a1 : Name List@i
12. m : piM(T)@i
13. pDVfire?(m) ∈ 𝔹
14. ↑pDVfire?(m)
⊢ pi-simple-subst(maybe-new-local(s1;x;a1);x;P) ∈ {Q:pi_term()| pi-rank(Q) < pi-rank(pinew(x;P))} 
BY
{ (MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. x : Name
2. P : pi_term()
3. g : {Q:pi_term()| pi-rank(Q) < pi-rank(pinew(x;P))}  ─→ Id ─→ Name ─→ (Name List) ─→ pi-process()
4. l : Id
5. serial : Name
6. avoid : Name List
7. T : {T:Type| pi-process() ⊆r T} 
8. pi-new-trans : Id ─→ Name ─→ (Name List) ─→ T@i
9. l1 : Id@i
10. s1 : Name@i
11. a1 : Name List@i
12. m : piM(T)@i
13. pDVfire?(m) ∈ 𝔹
14. ↑pDVfire?(m)
⊢ pi-rank(pi-simple-subst(maybe-new-local(s1;x;a1);x;P)) < pi-rank(pinew(x;P))

---

Latex:

---

Latex:

1.  x  :  Name
2.  P  :  pi\_term()
3.  g  :  \{Q:pi\_term()|  pi-rank(Q)  <  pi-rank(pinew(x;P))\}    {}\mrightarrow{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-process()
4.  l  :  Id
5.  serial  :  Name
6.  avoid  :  Name  List
7.  T  :  \{T:Type|  pi-process()  \msubseteq{}r  T\} 
8.  pi-new-trans  :  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  T@i
9.  l1  :  Id@i
10.  s1  :  Name@i
11.  a1  :  Name  List@i
12.  m  :  piM(T)@i
13.  pDVfire?(m)  \mmember{}  \mBbbB{}
14.  \muparrow{}pDVfire?(m)
\mvdash{}  pi-simple-subst(maybe-new-local(s1;x;a1);x;P)  \mmember{}  \{Q:pi\_term()|  pi-rank(Q)  <  pi-rank(pinew(x;P))\} 


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index