---

Step * 1 1 1 of Lemma pcw-pp-lemma


1. P : Type@i'
2. A : P ⟶ Type@i'
3. B : p:P ⟶ A[p] ⟶ Type@i'
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P@i
5. par : P@i
6. w : pW par@i
7. n : ℤ
8. 0 < n
9. ∀m:ℕn - 1. ∀ss:ℕn - 1 ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]).
     ((∀x:ℕn - 1. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) x ss (ss x)))
     ⇒ (fst(snd((ss m))) ∈ pW (fst((ss m)))))
10. m : ℕn@i
11. ss : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])@i
12. ∀x:ℕn. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) x ss (ss x))
13. p : P@i
14. w1 : pco-W p@i
15. v2 : B[p;fst(w1)]?@i
16. (ss m) = <p, w1, v2> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
17. 0 < m
18. fst(snd((ss (m - 1)))) ∈ pW (fst((ss (m - 1))))
19. pW ≡ λp.(a:A[p] × (b:B[p;a] ⟶ (pW C[p;a;b])))
⊢ ((↑isl(snd(snd((ss (m - 1))))))
∧ let p@0,w,d = ss (m - 1) in 
  let a,f = w 
  in case d of inl(b) => (p = C[p@0;a;b] ∈ P) ∧ (w1 = (f b) ∈ (pco-W C[p@0;a;b])) | inr(x) => True)
⇒ (w1 ∈ pW p)
BY
{ ((GenConclTerm ⌜ss (m - 1)⌝⋅ THENA Auto)
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN pcoWD (-3)
   THEN D -3
   THEN Reduce 0
   THEN D -2
   THEN Reduce 0
   THEN (InstLemma `param-co-W_wf` [⌜P⌝;⌜A⌝;⌜B⌝;⌜C⌝]⋅ THEN Auto)⋅) }

1
1. P : Type@i'
2. A : P ⟶ Type@i'
3. B : p:P ⟶ A[p] ⟶ Type@i'
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P@i
5. par : P@i
6. w : pW par@i
7. n : ℤ
8. 0 < n
9. ∀m:ℕn - 1. ∀ss:ℕn - 1 ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]).
     ((∀x:ℕn - 1. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) x ss (ss x)))
     ⇒ (fst(snd((ss m))) ∈ pW (fst((ss m)))))
10. m : ℕn@i
11. ss : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])@i
12. ∀x:ℕn. (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w) x ss (ss x))
13. p : P@i
14. w1 : pco-W p@i
15. v2 : B[p;fst(w1)]?@i
16. (ss m) = <p, w1, v2> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
17. 0 < m
18. fst(snd((ss (m - 1)))) ∈ pW (fst((ss (m - 1))))
19. pW ≡ λp.(a:A[p] × (b:B[p;a] ⟶ (pW C[p;a;b])))
20. p1 : P@i
21. a : A[p1]
22. w3 : b:B[p1;a] ⟶ (pco-W C[p1;a;b])
23. x : B[p1;fst(<a, w3>)]@i
24. (ss (m - 1)) = <p1, <a, w3>, inl x> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
25. pco-W ∈ P ⟶ Type
26. True
27. p = C[p1;a;x] ∈ P
28. w1 = (w3 x) ∈ (pco-W C[p1;a;x])
⊢ w1 ∈ pW p

---

Latex:

---

Latex:

1.  P  :  Type@i'
2.  A  :  P  {}\mrightarrow{}  Type@i'
3.  B  :  p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type@i'
4.  C  :  p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P@i
5.  par  :  P@i
6.  w  :  pW  par@i
7.  n  :  \mBbbZ{}
8.  0  <  n
9.  \mforall{}m:\mBbbN{}n  -  1.  \mforall{}ss:\mBbbN{}n  -  1  {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]).
          ((\mforall{}x:\mBbbN{}n  -  1.  (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w)  x  ss  (ss  x)))
          {}\mRightarrow{}  (fst(snd((ss  m)))  \mmember{}  pW  (fst((ss  m)))))
10.  m  :  \mBbbN{}n@i
11.  ss  :  \mBbbN{}n  {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])@i
12.  \mforall{}x:\mBbbN{}n.  (param-W-rel(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b];par;w)  x  ss  (ss  x))
13.  p  :  P@i
14.  w1  :  pco-W  p@i
15.  v2  :  B[p;fst(w1)]?@i
16.  (ss  m)  =  <p,  w1,  v2>
17.  0  <  m
18.  fst(snd((ss  (m  -  1))))  \mmember{}  pW  (fst((ss  (m  -  1))))
19.  pW  \mequiv{}  \mlambda{}p.(a:A[p]  \mtimes{}  (b:B[p;a]  {}\mrightarrow{}  (pW  C[p;a;b])))
\mvdash{}  ((\muparrow{}isl(snd(snd((ss  (m  -  1))))))
\mwedge{}  let  p@0,w,d  =  ss  (m  -  1)  in 
    let  a,f  =  w 
    in  case  d  of  inl(b)  =>  (p  =  C[p@0;a;b])  \mwedge{}  (w1  =  (f  b))  |  inr(x)  =>  True)
{}\mRightarrow{}  (w1  \mmember{}  pW  p)


By

---

Latex:
((GenConclTerm  \mkleeneopen{}ss  (m  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0
  THEN  pcoWD  (-3)
  THEN  D  -3
  THEN  Reduce  0
  THEN  D  -2
  THEN  Reduce  0
  THEN  (InstLemma  `param-co-W\_wf`  [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{})

---

Home Index