---

Step * 2 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 : pco-W par@i
7. ∀path:Path. (StepAgree(path 0;par;w) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
8. n : ℤ
9. 0 < n
10. ∀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))) ∈ {w:pco-W (fst((ss m)))| 
                              ∀path:Path. (StepAgree(path 0;fst((ss m));w) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))} ))
11. m : ℕn@i
12. ss : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])@i
13. ∀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))
14. p : P@i
15. w1 : pco-W p@i
16. v2 : B[p;fst(w1)]?@i
17. (ss m) = <p, w1, v2> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
18. p = par ∈ P
19. w1 = w ∈ (pco-W par)
20. ¬0 < m
21. path : Path@i
22. StepAgree(path 0;p;w1)
⊢ StepAgree(path 0;par;w)
BY
{ (NthHypEq (-1) THEN At ⌜𝕌'⌝EqCD⋅ THEN Auto THEN InstLemma `param-co-W_wf` [⌜P⌝;⌜A⌝;⌜B⌝;⌜C⌝]⋅ THEN Auto) }

---

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  :  pco-W  par@i
7.  \mforall{}path:Path.  (StepAgree(path  0;par;w)  {}\mRightarrow{}  (\mdownarrow{}\mexists{}n:\mBbbN{}.  Barred(pcw-partial(path;n))))
8.  n  :  \mBbbZ{}
9.  0  <  n
10.  \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{}  \{w:pco-W  (fst((ss  m)))| 
                                                            \mforall{}path:Path
                                                                (StepAgree(path  0;fst((ss  m));w)
                                                                {}\mRightarrow{}  (\mdownarrow{}\mexists{}n:\mBbbN{}.  Barred(pcw-partial(path;n))))\}  ))
11.  m  :  \mBbbN{}n@i
12.  ss  :  \mBbbN{}n  {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])@i
13.  \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))
14.  p  :  P@i
15.  w1  :  pco-W  p@i
16.  v2  :  B[p;fst(w1)]?@i
17.  (ss  m)  =  <p,  w1,  v2>
18.  p  =  par
19.  w1  =  w
20.  \mneg{}0  <  m
21.  path  :  Path@i
22.  StepAgree(path  0;p;w1)
\mvdash{}  StepAgree(path  0;par;w)


By

---

Latex:
(NthHypEq  (-1)
  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}EqCD\mcdot{}
  THEN  Auto
  THEN  InstLemma  `param-co-W\_wf`  [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index