---

Step * 1 1 1 1 of Lemma param-W-ext


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. pco-W ∈ P ⟶ Type
6. p : P
7. a : A[p]
8. x1 : b:B[p;a] ⟶ (pco-W C[p;a;b])
9. ∀path:Path. (StepAgree(path 0;p;<a, x1>) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
10. <a, x1> ∈ pco-W p
11. b : B[p;a]
12. path : ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
13. ∀i:ℕ. StepRel(path i;path (i + 1))
14. p1 : P
15. w : pco-W p1
16. v2 : B[p1;fst(w)]?
17. (path 0) = <p1, w, v2> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
18. p1 = C[p;a;b] ∈ P
19. w = (x1 b) ∈ (pco-W C[p;a;b])
⊢ ↓∃n:ℕ. Barred(pcw-partial(path;n))
BY
{ (InstHyp [⌜λn.if (n =z 0) then <p, <a, x1>, inl b> else path (n - 1) fi ⌝] 9⋅
   THENA (RepUR ``pcw-step-agree`` 0
          THEN Auto
          THEN MemTypeCD
          THEN Reduce 0
          THEN Auto
          THEN Try ((pcoWD (-1) THEN Auto)⋅))
   )⋅ }

1
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. pco-W ∈ P ⟶ Type
6. p : P
7. a : A[p]
8. x1 : b:B[p;a] ⟶ (pco-W C[p;a;b])
9. ∀path:Path. (StepAgree(path 0;p;<a, x1>) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
10. <a, x1> ∈ pco-W p
11. b : B[p;a]
12. path : ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
13. ∀i:ℕ. StepRel(path i;path (i + 1))
14. p1 : P
15. w : pco-W p1
16. v2 : B[p1;fst(w)]?
17. (path 0) = <p1, w, v2> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
18. p1 = C[p;a;b] ∈ P
19. w = (x1 b) ∈ (pco-W C[p;a;b])
20. i : ℕ
⊢ StepRel(if (i =z 0) then <p, <a, x1>, inl b> else path (i - 1) fi ;if (i + 1 =z 0)
then <p, <a, x1>, inl b>
else path ((i + 1) - 1)
fi )

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. pco-W ∈ P ⟶ Type
6. p : P
7. a : A[p]
8. x1 : b:B[p;a] ⟶ (pco-W C[p;a;b])
9. ∀path:Path. (StepAgree(path 0;p;<a, x1>) ⇒ (↓∃n:ℕ. Barred(pcw-partial(path;n))))
10. <a, x1> ∈ pco-W p
11. b : B[p;a]
12. path : ℕ ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
13. ∀i:ℕ. StepRel(path i;path (i + 1))
14. p1 : P
15. w : pco-W p1
16. v2 : B[p1;fst(w)]?
17. (path 0) = <p1, w, v2> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
18. p1 = C[p;a;b] ∈ P
19. w = (x1 b) ∈ (pco-W C[p;a;b])
20. ↓∃n:ℕ. Barred(pcw-partial(λn.if (n =z 0) then <p, <a, x1>, inl b> else path (n - 1) fi ;n))
⊢ ↓∃n:ℕ. Barred(pcw-partial(path;n))

---

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.  pco-W  \mmember{}  P  {}\mrightarrow{}  Type
6.  p  :  P
7.  a  :  A[p]
8.  x1  :  b:B[p;a]  {}\mrightarrow{}  (pco-W  C[p;a;b])
9.  \mforall{}path:Path.  (StepAgree(path  0;p;<a,  x1>)  {}\mRightarrow{}  (\mdownarrow{}\mexists{}n:\mBbbN{}.  Barred(pcw-partial(path;n))))
10.  <a,  x1>  \mmember{}  pco-W  p
11.  b  :  B[p;a]
12.  path  :  \mBbbN{}  {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
13.  \mforall{}i:\mBbbN{}.  StepRel(path  i;path  (i  +  1))
14.  p1  :  P
15.  w  :  pco-W  p1
16.  v2  :  B[p1;fst(w)]?
17.  (path  0)  =  <p1,  w,  v2>
18.  p1  =  C[p;a;b]
19.  w  =  (x1  b)
\mvdash{}  \mdownarrow{}\mexists{}n:\mBbbN{}.  Barred(pcw-partial(path;n))


By

---

Latex:
(InstHyp  [\mkleeneopen{}\mlambda{}n.if  (n  =\msubz{}  0)  then  <p,  <a,  x1>,  inl  b>  else  path  (n  -  1)  fi  \mkleeneclose{}]  9\mcdot{}
  THENA  (RepUR  ``pcw-step-agree``  0
                THEN  Auto
                THEN  MemTypeCD
                THEN  Reduce  0
                THEN  Auto
                THEN  Try  ((pcoWD  (-1)  THEN  Auto)\mcdot{}))
  )\mcdot{}

---

Home Index