---

Step * of Lemma pi-guarded-aux_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-aux(compList;g) ∈ Id ⟶ Name ⟶ (Name List) ⟶ pi-process())
BY
{ Auto
THEN (ExtWith [`l'] [⌜Top ⟶ Top⌝]⋅ THENA Auto THEN RecUnfold `pi-guarded-aux` 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
⊢ pi-guarded-aux(compList;g) l ∈ Name ⟶ (Name List) ⟶ 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-aux(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-aux`  0  THEN  Auto)

---

Home Index