---

Step * 3 1 1 1 1 of Lemma pW-rec_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 : pW par
11. 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])
    ⟶ ℙ
12. ∀[pp:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))]. (Barred(pp) ∈ ℙ)
13. n : ℕ
14. s : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
15. ∀%6:ℕn. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) %6 s (s %6))
16. ∀t:{t:pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])| param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) n s t} 
      (let q,w',d = t in 
       case d
        of inl(b) =>
        let a,f = w' 
        in let ind(p,a,f,G) = ind[p;a;f;G] in 
           letrec F(p,w) = let a,f=w in 
                           ind(p,a,f,λb.F(C[p;a;b],f(b)) in 
           F(C[q;a;b];f b)
        | inr(z) =>
        Ax ∈ let q,w',d = t in 
       case d of inl(b) => let a,f = w' in Q[C[q;a;b];f b] | inr(z) => True)
17. 0 < n
18. p : P
19. a : A[p]
20. w2 : b:B[p;a] ⟶ (pco-W C[p;a;b])
21. x : B[p;fst(<a, w2>)]
22. (s (n - 1)) = <p, <a, w2>, inl x> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
23. pco-W ∈ P ⟶ Type
24. v : P
25. C[p;a;x] = v ∈ P
26. a1 : A[v]
27. z1 : b:B[v;a1] ⟶ (pco-W C[v;a1;b])
28. (w2 x) = <a1, z1> ∈ (pco-W v)
⊢ ind v a1 z1 
  (λb.let ind(p,a,f,G) = ind p a f G in 
      letrec F(p,w) = let a,f=w in 
                      ind(p,a,f,λb.F(C p a b,f(b)) in 
      F(C v a1 b;z1 b)) ∈ Q v pW-sup(a1;z1)
BY
{ TACTIC:Assert ⌜z1 ∈ b:B[v;a1] ⟶ (pW C[v;a1;b])⌝⋅ }

1
.....assertion..... 
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 : pW par
11. 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])
    ⟶ ℙ
12. ∀[pp:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))]. (Barred(pp) ∈ ℙ)
13. n : ℕ
14. s : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
15. ∀%6:ℕn. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) %6 s (s %6))
16. ∀t:{t:pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])| param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) n s t} 
      (let q,w',d = t in 
       case d
        of inl(b) =>
        let a,f = w' 
        in let ind(p,a,f,G) = ind[p;a;f;G] in 
           letrec F(p,w) = let a,f=w in 
                           ind(p,a,f,λb.F(C[p;a;b],f(b)) in 
           F(C[q;a;b];f b)
        | inr(z) =>
        Ax ∈ let q,w',d = t in 
       case d of inl(b) => let a,f = w' in Q[C[q;a;b];f b] | inr(z) => True)
17. 0 < n
18. p : P
19. a : A[p]
20. w2 : b:B[p;a] ⟶ (pco-W C[p;a;b])
21. x : B[p;fst(<a, w2>)]
22. (s (n - 1)) = <p, <a, w2>, inl x> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
23. pco-W ∈ P ⟶ Type
24. v : P
25. C[p;a;x] = v ∈ P
26. a1 : A[v]
27. z1 : b:B[v;a1] ⟶ (pco-W C[v;a1;b])
28. (w2 x) = <a1, z1> ∈ (pco-W v)
⊢ z1 ∈ b:B[v;a1] ⟶ (pW C[v;a1;b])

2
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 : pW par
11. 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])
    ⟶ ℙ
12. ∀[pp:n:ℕ × (ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]))]. (Barred(pp) ∈ ℙ)
13. n : ℕ
14. s : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
15. ∀%6:ℕn. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) %6 s (s %6))
16. ∀t:{t:pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])| param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) n s t} 
      (let q,w',d = t in 
       case d
        of inl(b) =>
        let a,f = w' 
        in let ind(p,a,f,G) = ind[p;a;f;G] in 
           letrec F(p,w) = let a,f=w in 
                           ind(p,a,f,λb.F(C[p;a;b],f(b)) in 
           F(C[q;a;b];f b)
        | inr(z) =>
        Ax ∈ let q,w',d = t in 
       case d of inl(b) => let a,f = w' in Q[C[q;a;b];f b] | inr(z) => True)
17. 0 < n
18. p : P
19. a : A[p]
20. w2 : b:B[p;a] ⟶ (pco-W C[p;a;b])
21. x : B[p;fst(<a, w2>)]
22. (s (n - 1)) = <p, <a, w2>, inl x> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
23. pco-W ∈ P ⟶ Type
24. v : P
25. C[p;a;x] = v ∈ P
26. a1 : A[v]
27. z1 : b:B[v;a1] ⟶ (pco-W C[v;a1;b])
28. (w2 x) = <a1, z1> ∈ (pco-W v)
29. z1 ∈ b:B[v;a1] ⟶ (pW C[v;a1;b])
⊢ ind v a1 z1 
  (λb.let ind(p,a,f,G) = ind p a f G in 
      letrec F(p,w) = let a,f=w in 
                      ind(p,a,f,λb.F(C p a b,f(b)) in 
      F(C v a1 b;z1 b)) ∈ Q v pW-sup(a1;z1)

---

Latex:

---

Latex:

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  :  pW  par
11.  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{}
12.  \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{})
13.  n  :  \mBbbN{}
14.  s  :  \mBbbN{}n  {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
15.  \mforall{}\%6:\mBbbN{}n.  (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w)  \%6  s  (s  \%6))
16.  \mforall{}t:\{t:pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])| 
                param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w)  n  s  t\} 
            (let  q,w',d  =  t  in 
              case  d
                of  inl(b)  =>
                let  a,f  =  w' 
                in  let  ind(p,a,f,G)  =  ind[p;a;f;G]  in 
                      letrec  F(p,w)  =  let  a,f=w  in 
                                                      ind(p,a,f,\mlambda{}b.F(C[p;a;b],f(b))  in 
                      F(C[q;a;b];f  b)
                |  inr(z)  =>
                Ax  \mmember{}  let  q,w',d  =  t  in 
              case  d  of  inl(b)  =>  let  a,f  =  w'  in  Q[C[q;a;b];f  b]  |  inr(z)  =>  True)
17.  0  <  n
18.  p  :  P
19.  a  :  A[p]
20.  w2  :  b:B[p;a]  {}\mrightarrow{}  (pco-W  C[p;a;b])
21.  x  :  B[p;fst(<a,  w2>)]
22.  (s  (n  -  1))  =  <p,  <a,  w2>,  inl  x>
23.  pco-W  \mmember{}  P  {}\mrightarrow{}  Type
24.  v  :  P
25.  C[p;a;x]  =  v
26.  a1  :  A[v]
27.  z1  :  b:B[v;a1]  {}\mrightarrow{}  (pco-W  C[v;a1;b])
28.  (w2  x)  =  <a1,  z1>
\mvdash{}  ind  v  a1  z1 
    (\mlambda{}b.let  ind(p,a,f,G)  =  ind  p  a  f  G  in 
            letrec  F(p,w)  =  let  a,f=w  in 
                                            ind(p,a,f,\mlambda{}b.F(C  p  a  b,f(b))  in 
            F(C  v  a1  b;z1  b))  \mmember{}  Q  v  pW-sup(a1;z1)


By

---

Latex:
TACTIC:Assert  \mkleeneopen{}z1  \mmember{}  b:B[v;a1]  {}\mrightarrow{}  (pW  C[v;a1;b])\mkleeneclose{}\mcdot{}

---

Home Index