---

Step * of Lemma pcw-pp-lemma

∀P:Type. ∀A:P ⟶ Type. ∀B:p:P ⟶ A[p] ⟶ Type. ∀C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P. ∀par:P. ∀w:pW par. ∀n:ℕ. ∀m:ℕn.
∀ss:ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]).
  ((∀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)))
  ⇒ (fst(snd((ss m))) ∈ pW (fst((ss m)))))
BY
{ (InductionOnNat
   THEN Auto
   THEN (InstHyp [⌜m⌝] (-1)⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜ss m⌝⋅ THENA Auto)
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN Auto
   THEN RepUR ``param-W-rel`` (-1)
   THEN (Decide ⌜0 < m⌝⋅ THENA Auto)
   THEN ((Reduce (-2) THENA Auto) THEN RepUR ``pcw-step-agree pcw-steprel`` (-2)⋅)⋅) }

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. (↑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
18. 0 < m
⊢ w1 ∈ pW p

2
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. (p = par ∈ P) ∧ (w1 = w ∈ (pco-W par))
18. ¬0 < m
⊢ w1 ∈ pW p

---

Latex:

---

Latex:
\mforall{}P:Type.  \mforall{}A:P  {}\mrightarrow{}  Type.  \mforall{}B:p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type.  \mforall{}C:p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P.  \mforall{}par:P.  \mforall{}w:pW  par.
\mforall{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}n.  \mforall{}ss:\mBbbN{}n  {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b]).
    ((\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)))
    {}\mRightarrow{}  (fst(snd((ss  m)))  \mmember{}  pW  (fst((ss  m)))))


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}ss  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  Reduce  0
  THEN  Auto
  THEN  RepUR  ``param-W-rel``  (-1)
  THEN  (Decide  \mkleeneopen{}0  <  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ((Reduce  (-2)  THENA  Auto)  THEN  RepUR  ``pcw-step-agree  pcw-steprel``  (-2)\mcdot{})\mcdot{})

---

Home Index