---

Step * 1 1 of Lemma pW-rec_wf

.....wf..... 
1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]) ∈ Type
6. pW ∈ P ⟶ Type
7. Q : par:P ⟶ (pW par) ⟶ ℙ
8. ind : par:P
⟶ a:A[par]
⟶ f:(b:B[par;a] ⟶ (pW C[par;a;b]))
⟶ (b:B[par;a] ⟶ Q[C[par;a;b];f b])
⟶ Q[par;pW-sup(a;f)]
9. par : P
10. w : pco-W par
11. ∀path:Path. (StepAgree(path 0;par;w) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
12. param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) ∈ n:ℕ
    ⟶ (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))
    ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
    ⟶ ℙ
13. ∀[pp:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))]. (Barred(pp) ∈ ℙ)
14. alpha : ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
15. ∀n:ℕ. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) n alpha (alpha n))
⊢ alpha ∈ Path
BY
{ TACTIC:(MemTypeCD
          THEN Auto
          THEN (InstHyp [⌜i + 1⌝] (-2)⋅ THENA Auto)
          THEN MoveToConcl (-1)
          THEN RepUR ``param-W-rel`` 0
          THEN (Subst' (i + 1) - 1 ~ i 0 THENA Auto)
          THEN AutoSplit
          THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  P  :  Type
2.  A  :  P  {}\mrightarrow{}  Type
3.  B  :  p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type
4.  C  :  p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P
5.  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])  \mmember{}  Type
6.  pW  \mmember{}  P  {}\mrightarrow{}  Type
7.  Q  :  par:P  {}\mrightarrow{}  (pW  par)  {}\mrightarrow{}  \mBbbP{}
8.  ind  :  par:P
{}\mrightarrow{}  a:A[par]
{}\mrightarrow{}  f:(b:B[par;a]  {}\mrightarrow{}  (pW  C[par;a;b]))
{}\mrightarrow{}  (b:B[par;a]  {}\mrightarrow{}  Q[C[par;a;b];f  b])
{}\mrightarrow{}  Q[par;pW-sup(a;f)]
9.  par  :  P
10.  w  :  pco-W  par
11.  \mforall{}path:Path.  (StepAgree(path  0;par;w)  {}\mRightarrow{}  (\mdownarrow{}\mexists{}n:\mBbbN{}.  Barred(pcw-partial(path;n))))
12.  param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w)  \mmember{}  n:\mBbbN{}
        {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))
        {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
        {}\mrightarrow{}  \mBbbP{}
13.  \mforall{}[pp:n:\mBbbN{}  \mtimes{}  (\mBbbN{}n  {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))].  (Barred(pp)  \mmember{}  \mBbbP{})
14.  alpha  :  \mBbbN{}  {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
15.  \mforall{}n:\mBbbN{}.  (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w)  n  alpha  (alpha  n))
\mvdash{}  alpha  \mmember{}  Path


By

---

Latex:
TACTIC:(MemTypeCD
                THEN  Auto
                THEN  (InstHyp  [\mkleeneopen{}i  +  1\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
                THEN  MoveToConcl  (-1)
                THEN  RepUR  ``param-W-rel``  0
                THEN  (Subst'  (i  +  1)  -  1  \msim{}  i  0  THENA  Auto)
                THEN  AutoSplit
                THEN  Auto)

---

Home Index