---

Step * 1 1 1 of Lemma pi-guarded-aux_wf


1. compList : (pi_prefix() × pi_term()) List
2. g : {Q:pi_term()| (∃C∈compList. pi-rank(Q) ≤ pi-rank(snd(C)))}  ─→ Id ─→ Name ─→ (Name List) ─→ pi-process()
3. l : Id
4. serial : Name
5. avoid : Name List
6. T : Type
7. Process(T.piM(T)) ⊆r T
8. pi-guarded-aux : 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. ↑pDVmsg?(m)
14. val : Name@i
15. pDVmsg-val(m) = val ∈ Name@i
16. i : ℕ@i
17. pDVmsg-index(m) = i ∈ ℕ@i
18. i < ||compList||
19. v1 : pi_prefix()@i
20. v2 : pi_term()@i
21. compList[i] = <v1, v2> ∈ (pi_prefix() × pi_term())@i
22. ↑pircv?(v1)
23. P' : pi_term()@i
24. pi-simple-subst(val;pircv-var(v1);v2) = P' ∈ pi_term()@i
⊢ pi-rank(P') ≤ pi-rank(snd(compList[i]))
BY
{ (Assert pi-rank(pi-simple-subst(val;pircv-var(v1);v2)) = pi-rank(v2) ∈ ℤ BY
         BLemma `pi-rank-pi-simple-subst`⋅
         THEN Auto)⋅ }

1
1. compList : (pi_prefix() × pi_term()) List
2. g : {Q:pi_term()| (∃C∈compList. pi-rank(Q) ≤ pi-rank(snd(C)))}  ─→ Id ─→ Name ─→ (Name List) ─→ pi-process()
3. l : Id
4. serial : Name
5. avoid : Name List
6. T : Type
7. Process(T.piM(T)) ⊆r T
8. pi-guarded-aux : 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. ↑pDVmsg?(m)
14. val : Name@i
15. pDVmsg-val(m) = val ∈ Name@i
16. i : ℕ@i
17. pDVmsg-index(m) = i ∈ ℕ@i
18. i < ||compList||
19. v1 : pi_prefix()@i
20. v2 : pi_term()@i
21. compList[i] = <v1, v2> ∈ (pi_prefix() × pi_term())@i
22. ↑pircv?(v1)
23. P' : pi_term()@i
24. pi-simple-subst(val;pircv-var(v1);v2) = P' ∈ pi_term()@i
25. pi-rank(pi-simple-subst(val;pircv-var(v1);v2)) = pi-rank(v2) ∈ ℤ
⊢ pi-rank(P') ≤ pi-rank(snd(compList[i]))

---

Latex:

---

Latex:

1.  compList  :  (pi\_prefix()  \mtimes{}  pi\_term())  List
2.  g  :  \{Q:pi\_term()|  (\mexists{}C\mmember{}compList.  pi-rank(Q)  \mleq{}  pi-rank(snd(C)))\} 
{}\mrightarrow{}  Id
{}\mrightarrow{}  Name
{}\mrightarrow{}  (Name  List)
{}\mrightarrow{}  pi-process()
3.  l  :  Id
4.  serial  :  Name
5.  avoid  :  Name  List
6.  T  :  Type
7.  Process(T.piM(T))  \msubseteq{}r  T
8.  pi-guarded-aux  :  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.  \muparrow{}pDVmsg?(m)
14.  val  :  Name@i
15.  pDVmsg-val(m)  =  val@i
16.  i  :  \mBbbN{}@i
17.  pDVmsg-index(m)  =  i@i
18.  i  <  ||compList||
19.  v1  :  pi\_prefix()@i
20.  v2  :  pi\_term()@i
21.  compList[i]  =  <v1,  v2>@i
22.  \muparrow{}pircv?(v1)
23.  P'  :  pi\_term()@i
24.  pi-simple-subst(val;pircv-var(v1);v2)  =  P'@i
\mvdash{}  pi-rank(P')  \mleq{}  pi-rank(snd(compList[i]))


By

---

Latex:
(Assert  pi-rank(pi-simple-subst(val;pircv-var(v1);v2))  =  pi-rank(v2)  BY
              BLemma  `pi-rank-pi-simple-subst`\mcdot{}
              THEN  Auto)\mcdot{}

---

Home Index