---

Step * of Lemma pi-guarded-trans_wf

∀[compList:(pi_prefix() × pi_term()) List]. ∀[g:{Q:pi_term()| (∃C∈compList. pi-rank(Q) ≤ pi-rank(snd(C)))} 
                                                ─→ Id
                                                ─→ Name
                                                ─→ (Name List)
                                                ─→ pi-process()].
  (pi-guarded-trans(compList;g) ∈ Id ─→ Name ─→ (Name List) ─→ pi-process())
BY
{ ((Auto THEN ExtWith [`l'] [⌈Top ─→ Top⌉]⋅ THENA Auto THEN RecUnfold `pi-guarded-trans` 0 THEN Auto)⋅
   THEN (ExtWith [`serial'] [⌈Top ─→ Top⌉]⋅ THENA Auto THEN RecUnfold `pi-guarded-trans` 0 THEN Reduce 0 THEN Auto⋅)
   THEN (ExtWith [`avoid'] [⌈Top ─→ Top⌉]⋅ THENA Auto THEN RecUnfold `pi-guarded-trans` 0 THEN Reduce 0 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
⊢ pi-guarded-trans(compList;g) l serial avoid ∈ pi-process()

---

Latex:

---

Latex:
\mforall{}[compList:(pi\_prefix()  \mtimes{}  pi\_term())  List].  \mforall{}[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()].
    (pi-guarded-trans(compList;g)  \mmember{}  Id  {}\mrightarrow{}  Name  {}\mrightarrow{}  (Name  List)  {}\mrightarrow{}  pi-process())


By

---

Latex:
((Auto  THEN  ExtWith  [`l']  [\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}  THENA  Auto  THEN  RecUnfold  `pi-guarded-trans`  0  THEN  Auto)\mcdot{}
  THEN  (ExtWith  [`serial']  [\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}
  THENA  Auto
              THEN  RecUnfold  `pi-guarded-trans`  0
              THEN  Reduce
              0  THEN
              Auto\mcdot{}
  )
  THEN  (ExtWith  [`avoid']  [\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}
  THENA  Auto
              THEN  RecUnfold  `pi-guarded-trans`  0
              THEN  Reduce  0
              THEN  Auto
  ))

---

Home Index